2
$\begingroup$

When I look up the mechanics of a propositional logic system here we have a collection of both rules of inference ($a \vdash b$) and axioms ($\vdash b$), if I understand right.

One such rule of inference is modus ponens, $p, (p\to q) \vdash q$ which on a metalogical level is "from $p$ and $p\to q$, infer $q$".

However I have also seen people "prove" it using truth tables or treating it as a tautology by stating it as $(p \land (p\to q)) \to q$.

Why do I see it stated these two ways if the latter is not technically modus ponens? Is it totally and utterly wrong to even ask the question how to "prove modus ponens" because it's considered a rule of inference, i.e. it has no proof since it's a metalogical assumption? Why do I sometimes see it stated the second way, if so, and how do we know that's the correct interpretation as a tautological claim?

I know informally it makes sense as "if $a$ then $b$" or "whenever $a$ is true, $b$ is true" but the whole $\vdash$ concept seems to be a little different from $\to$ (especially since $\vdash$ is metalogical) and so I'm trying to understand what's going on here.

$\endgroup$
  • $\begingroup$ NB: $p \land (p\to q) \to q$ is missing parentheses. $\endgroup$ – Shaun Sep 2 '18 at 14:08
  • $\begingroup$ Very relevant here: What the tortoise said to Achilles $\endgroup$ – Henning Makholm Sep 2 '18 at 14:29
  • $\begingroup$ In particular Peter Smith's answer to the linked question is a good and complete answer to this one, too. $\endgroup$ – Henning Makholm Sep 2 '18 at 14:39
  • $\begingroup$ @HenningMakholm reading that question and answer I'm still not sure I understand the problem. Sounds like he's just saying "just because you say it implies Z, I'm not convinced" until you make a specific rule that overrides that need to be convinced. Which to me is not directly addressing the difference between usage of implies and infers with respect to modus ponens $\endgroup$ – user525966 Sep 2 '18 at 15:57
  • $\begingroup$ To prove $(p \land (p\to q)) \to q$. using truth tables, you have to use the truth table for material implication, which is usually presented simply as a definition. Each line of that truth table, however, can also be derived using well-known principles of logic including MP, direct proof (introducing $\to$), proof by contradiction and double negation. $\endgroup$ – Dan Christensen Sep 4 '18 at 10:44
1
$\begingroup$

As I stated in my previous answer, the rule modus ponens is part of the definition of many common proof systems. Let HPC stand for Hilbert's system for classical propositional logic whose only rule of inference is modus ponens and whose axioms are listed here after Frege's. This is a well-defined mathematical object. It is one proof system for classical propositional logic. Literally over a dozen others are mentioned on that page, and those are restricted to Hilbert-style proof systems. There are also many others in the style of natural deduction or the sequent calculus.

In HPC a (formal) proof is either an instance of one of the axioms, or it is a use of the rule modus ponens which combines two other proofs. This produces a binary-tree-like structure whose leaves are instances of axioms. This is the definition of a proof in HPC. A formula of classical propositional logic is proven by HPC if we can build a proof which has that formula as the conclusion (i.e. the root of the tree). This is an example of the syntactic approach to logic. We don't even need to formulate the idea of "truth tables" to completely specify this.

An alternate approach is semantics. Here there are no axioms or rules. Instead, we need to provide a way of interpreting formulas as some mathematical object (in a compositional way, but I won't elaborate on that). There are many possible semantics you could use. One possibility is to use a Boolean algebra, and, in particular, the simplest possible non-trivial Boolean algebra built on a two element set. Any two element set will do. Let's use $\{\mathsf{cat},\mathsf{dog}\}$ for concreteness. With this choice of semantics, formulas with $n$ (distinct) propositional variables become $n$-ary operations on that two element set. Now we define a formula to be "true" if its interpretation is function that constantly has the value $\mathsf{dog}$. Dually from before, we can completely specify this semantics without ever mentioning any notion of formal proof.

Now we can ask the question: are the formulas that HPC proves the same as the formulas that the Boolean algebra semantics calls "true"? The soundness theorem for HPC with respect to this Boolean algebra semantics states that the formulas that HPC proves are "true" in the semantics. The completeness theorem for HPC with respect to this Boolean algebra semantics states that every formula that is "true" in the semantics has a proof in HPC. These (meta-)theorems can be proven either with informal mathematical reasoning or formally within some richer logical framework.

At no point in this do you need to accept the rules or axioms of HPC or agree that the Boolean algebra semantics I gave correctly reflects some philosophical notion of truth. This is no different from studying any other mathematical object. If I'm studying the ring of square matrices, I don't have to reject my prior notions of addition and multiplication and accept matrix addition/multiplication as the One True Meaning of addition and multiplication. I don't need to have a first principles account of how there is no other way of adding and multiplying matrices. (There are other ways of adding and multiplying matrices!) The formulas proven by HPC are the same regardless of one's philosophical stance. The formulas that are "true" with respect to the Boolean algebra semantics are the same regardless of one's philosophical stance. One's philosophical stance simply doesn't come into it.1

The only time I would need to convince you of the axioms/rules of HPC is if I'm making a philosophical claim that they correspond to some philosophical notion of "truth". There are plenty of reasons to study classical propositional logic quite apart from philosophical notions of "truth" such as applications to digital circuits. Similarly, there are plenty of reasons to study intuitionistic logics unrelated to philosophical notions of truth such as extracting computational content from constructive proofs or proving theorems that hold for a much broader and mathematically important class of semantics than classical logics. There are good reasons to study both simultaneously, and there is no cognitive dissonance in doing so.

As to some people calling $(p\land(p\to q))\to q$ "modus ponens", it wouldn't be the first time in mathematics that two distinct but related concepts were given the same name. That said, I think many of the times you see that it is being said by someone who doesn't have (or at least hasn't demonstrated that they have) a clear understanding of the separation between logic and meta-logic. Like your earlier question, if you try to naively formalize the usual informal description of the rule modus ponens but don't take care to separate syntax from semantics and logic from meta-logic, then you readily get the above formula. If you do take care to keep these separate, it is readily apparent that treating the above formula as the formalization of the rule modus ponens is a mish-mash of logic and meta-logic.

Write $\vdash p$ for the meta-logical claim that HPC proves $p$. The typical informal description of the rule modus ponens is: "if $p$ is provable and $p\to q$ is provable, then $q$ is provable". Let me write that a bit more formally. To make the distinction between logic and meta-logic a bit clearer, I'll write $\curlywedge$ and $\leadsto$ for the meta-logical conjunction and implication. The informal "modus ponens" is then more formally: $((\vdash p)\curlywedge(\vdash(p\to q)))\leadsto(\vdash q)$. This has the form $(\varphi\curlywedge\psi)\leadsto \chi$ where $\varphi$, $\psi$, and $\chi$ are atomic propositions in the meta-logic. Saying $(p\land(p\to q))\to q$ is a tautology is via the soundness and completeness theorems equivalent to saying $\vdash ((p\land(p\to q))\to q)$. This is an atomic proposition of the meta-logic. It should be clear now why I speak of a mish-mash. Viewing these two meta-logical propositions as being the same leads to $\to$ being used for both the $\to$ connective of the logic and the meta-logical $\leadsto$.

Still, if someone wants to call $(p\land(p\to q))\to q$ "modus ponens", that's their prerogative. It's no different than saying you are going to call it $A$. If, however, they are claiming it is the formalization of the rule modus ponens, then they are simply wrong.

1 This isn't completely true as one's philosophical stance on truth impacts their informal reasoning. For example, an ultrafinitist might reject the claim that sufficiently large formulas of classical propositional logic can have proofs in HPC or can be shown to be "true" in the Boolean algebra semantics. However, a classical mathematician, an ultrafinitist, and an intuitionist will all agree that $p\lor\neg p$ is provable in HPC and is "true" with respect to the Boolean algebra semantics. They just may not agree that HPC is a good reflection of their (philosophical) notion of "truth".

$\endgroup$
  • $\begingroup$ "This is a well-defined mathematical object." No, it's not well-defined. For it to qualify as well-defined, it has to actually use well-formed formulas, not abbreviations for well-formed formulas. Also, note that Frege's actual notation (the one in the Begriffsschrift), doesn't have any way to write anything like a->b->c. That's one of the virtues of Frege's "Concept Notation". " The typical informal description of the rule modus ponens is..." There's not necessarily any conjunction in the meta-logic. We might have a set of two distinct propositions instead of a conjunction. $\endgroup$ – Doug Spoonwood Sep 2 '18 at 21:36
  • $\begingroup$ The only reason "Frege" occurs in this answer is that the Wikipedia page lists Hilbert's choice of axioms after Frege's. I'm making no particular reference to Frege. I do agree that I certainly haven't provided a complete definition of HPC nor does the Wikipedia page on its own. Still, the remaining parts of the definition are standard. Nevertheless, if you still find that unacceptable here is a formalization of a similar system in Coq. To be clear, I'm referring to the ancillary Coq files not the paper. That should be sufficiently well-defined. $\endgroup$ – Derek Elkins Sep 2 '18 at 21:58
  • $\begingroup$ As for my slightly more formal rendition of a common informal statement related to modus ponens, I agree that it is hardly fully fleshed out nor the only possible way of formalizing the informal statement. I didn't mention it here (but I did in the referenced answer), I would describe modus ponens as an operation on proofs like addition is an operation on numbers. It's no more a declarative statement than $2+3$ is. A more accurate rendition of the informal statement in my view would be: "Given a proof of $P$ and a proof of $P\to Q$, we can use modus ponens to build a proof of $Q$." $\endgroup$ – Derek Elkins Sep 2 '18 at 21:59
  • $\begingroup$ @DerekElkins When you say "We can use modus ponens to build a proof of $Q$"... is the proof of $Q$ not "built" for us once we have proven $P$ as well as $P \to Q$? Is showing that both $P$ true and $P \to Q$ true the very definition of what it means to build the proof of $Q$ under modus ponens? $\endgroup$ – user525966 Sep 3 '18 at 3:48
  • $\begingroup$ @user525966 No. If you have a proof of P, and one of (P->Q), you have to write another line where Q is. The proof analysis will refer to P, and (P->Q) provided that such exists. $\endgroup$ – Doug Spoonwood Sep 3 '18 at 4:15
1
$\begingroup$

"Why do I see it stated these two ways if the latter is not technically modus ponens?"

Because people don't think about this much or are confused.

" Is it totally and utterly wrong to even ask the question how to "prove modus ponens" because it's considered a rule of inference, i.e. it has no proof since it's a metalogical assumption?"

Given that "proof" means "formal proof" where a formal proof has every step being a well-formed formula, then yes. Why? Because {(p->q), p} $\vdash$ q (I note in passing that {p, q} and {q, p} are the same set, so I referred to the same rule of inference as you did) is not a well-formed formula in the same context where "formal proof" applies to for propositional calculus.

"Why do I sometimes see it stated the second way, if so, and how do we know that's the correct interpretation as a tautological claim?"

At the very least, the well-formed formula (one you would parenthesize it) is just one well-formed formula. The antecedent is a single well-formed conjunction also, and sometimes conjunction is not a primitive, and sometimes not even a defined connective, for a propositional calculus. On the other hand, {(p->q), p} consists of a set of two well-formed formulas.

$\vdash$ is not a connective between propositions. If we where to write:

"If p, if (p->q) also, then q" we would have stepped outside of propositional calculus, since "if", "then", "also, and "," are not part of the language for well-formed formulas in propositional calculus. In other words, they are not part of the "formula language".

However, "$\vdash$" doesn't happen inside of the formula language. If we wrote:

"If p, if (p>q) also, $\vdash$ q"

we haven't stepped outside of the meta-language where $\vdash$ comes as permissible, since there doesn't exist any formation rules prescribing the correct or incorrect use of $\vdash$ other than it gets used intelligibly. So, as long as the above comes as comprehensible to the reader, it qualifies as correct. That differs from the use of (well-formed) formulas, where every string used needs to follow the formation rules to stay in the language.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.