Prove modus ponens for set of formulas from tautological formulation.

Question

I have given a correct and complete calculus for propositional logic:

$$(A1)~\psi\rightarrow(\varphi\rightarrow\psi)\\ (A2)~(\psi\rightarrow(\varphi\rightarrow\chi))\rightarrow((\psi\rightarrow\varphi)\rightarrow(\psi\rightarrow\chi))\\ (A3)~(\lnot\varphi\rightarrow\lnot\psi)\rightarrow(\psi\rightarrow\varphi)\\ (R1)~\text{If }\vdash\psi\text{ and }\vdash\psi\rightarrow\varphi\text{, then }\vdash\varphi.$$

In order to prove something (the deduction theorem), I need the general formulation of the modus ponens, i.e.

$(R1')~\text{If }\Gamma\vdash\psi\text{ and }\Gamma\vdash\psi\rightarrow\varphi\text{, then }\Gamma\vdash\varphi.$

Can I somehow prove $(R1')$ or do I have to take it as another axiom?

So far, I have mentioned that $\Gamma\vdash\psi$ means that $\psi$ holds if all $\varphi\in\Gamma$ hold. If all formulas of a superset of $\Gamma$ hold then especially all $\varphi\in\Gamma$ hold, therefore $\Gamma\vdash\psi$ implies $\Gamma\cup X\vdash\psi$ for all $X\subseteq\textit{PL}$. (monotonicity of $\vdash$)

Even though $(R1')$ basically states $\left(\big(\bigwedge\Gamma\Rightarrow\psi\big)\land\big(\bigwedge\Gamma\Rightarrow\psi\rightarrow\varphi\big)\right)\Rightarrow\big(\bigwedge\Gamma\Rightarrow\varphi\big)$, which is equivalent to $\bigwedge\Gamma\Rightarrow\left(\big(\psi\land(\psi\rightarrow\varphi)\big)\Rightarrow\varphi\right)$, and I can show $\Gamma\vdash(\psi\land(\psi\rightarrow\varphi))\rightarrow\varphi$ by using monoticity of $\vdash$, since $\vdash(\psi\land(\psi\rightarrow\varphi))\rightarrow\varphi$ holds, I would need the deduction theorem to be proven already in order for this to be helpful. Is there another way? I am free to use the semantics of propositional logic as an argument, as the calculus is correct and complete.

Answer 1

It turned out that in order to talk about conditional syntactic consequence $\Gamma\vdash\psi$, we need to define $\vdash$ based on sequences of formulas that are proofs, and use a derivation rule of modus ponens $\{\psi,\psi\rightarrow\varphi\}\vdash\varphi$ which is based on the semantic consequence, especially on $\{\psi,\psi\rightarrow\varphi\}\vDash\varphi$.

1. Define the semantics:

   The semantics of PL is given by a function $⟦\cdot⟧^\mathfrak{I}:\textit{PL}\rightarrow\{0,1\}$, such that ${\forall \psi,\varphi:}$

   • $⟦\lnot\psi⟧^\mathfrak{I}:=1-⟦\psi⟧^\mathfrak{I}$
   • $⟦\psi\lor\varphi⟧^\mathfrak{I}:=\textit{max}\left\{⟦\psi⟧^\mathfrak{I},⟦\varphi⟧^\mathfrak{I}\right\}$
   • $⟦\psi⟧^\mathfrak{I}:=\mathfrak{I}(\psi)$, for variable $\psi\in\tau$ and an interpretation $\mathfrak{I}:\tau\rightarrow\{0,1\}$

   A formula $\psi\in\textit{PL}$ is valid, if $⟦\psi⟧^\mathfrak{I}\,{=}\,1$ holds for all interpretations $\mathfrak{I}$ of variables.

   Semantic consequence of PL is a relation $\vDash\,\subseteq2^\textit{PL}\times\textit{PL}$ with $\Gamma\vDash\psi$ iff for every interpretation $\mathfrak{I}$ with $\forall\varphi\in\Gamma:⟦\varphi⟧^\mathfrak{I}=1$ follows $⟦\psi⟧^\mathfrak{I}=1$.

2. Show the foundation of modus ponens, i.e. $\{\psi,\psi\rightarrow\varphi\}\vDash\varphi$:

   Due to ${⟦\psi\rightarrow\varphi⟧^\mathfrak{I}}=⟦\lnot\psi\lor\varphi⟧^\mathfrak{I}=max\left\{⟦\lnot\psi⟧^\mathfrak{I},⟦\varphi⟧^\mathfrak{I}\right\}=max\left\{1-⟦\psi⟧^\mathfrak{I},⟦\varphi⟧^\mathfrak{I}\right\}\text{, therefore}$ $\begin{array}{@{}r@{}l@{}} {⟦\psi⟧^\mathfrak{I}=1\land⟦\psi\rightarrow\varphi⟧^\mathfrak{I}=1}~\Rightarrow&{⟦\psi⟧^\mathfrak{I}=1\land max\left\{1-⟦\psi⟧^\mathfrak{I},⟦\varphi⟧^\mathfrak{I}\right\}=1}\\ ~\Rightarrow&{⟦\psi⟧^\mathfrak{I}=1\land(1-⟦\psi⟧^\mathfrak{I}=1\lor⟦\varphi⟧^\mathfrak{I}=1)}\\ ~\Rightarrow&{⟦\psi⟧^\mathfrak{I}=1\land(⟦\psi⟧^\mathfrak{I}=0}\lor⟦\varphi⟧^\mathfrak{I}=1)\\ ~\Rightarrow&{({⟦\psi⟧^\mathfrak{I}=1\land⟦\psi⟧^\mathfrak{I}=0})\lor(⟦\psi⟧^\mathfrak{I}=1\land⟦\varphi⟧^\mathfrak{I}=1)}\\ ~\Rightarrow&⟦\varphi⟧^\mathfrak{I}=1, \end{array}$

   we have ${\{\psi,\psi\rightarrow\varphi\}\vDash\varphi}$, for all $\psi,\varphi\in\textit{PL}$.

3. Define syntactic consequence:

   For ${\psi,\varphi\in\textit{PL}}$, we define the derivation of modus ponens as $\{\psi,\psi\rightarrow\varphi\}\vdash\varphi$. $(\textit{MP})$

   A proof under conditions $\Gamma\subseteq\textit{PL}$, denoted $\Gamma$-proof, for a formula $\varphi_n\in\textit{PL}$ is a finite sequence of formulas $\sigma=\varphi_1,\dots,\varphi_n$ such that for all ${i\in\{1,\dots,n\}}$ holds: $\begin{array}{@{}l@{}}\begin{array}{@{}r@{\,}c@{\,}l@{}}\varphi_i\in\Gamma & \cup & \left\{\psi\rightarrow(\varphi\rightarrow\psi)~\middle|~\psi,\varphi\in\textit{PL}\right\}\\ & \cup & \left\{(\psi\rightarrow(\varphi\rightarrow\chi))\rightarrow((\psi\rightarrow\varphi)\rightarrow(\psi\rightarrow\chi))~\middle|~\psi,\varphi,\chi\in\textit{PL}\right\}\\ & \cup & \left\{(\lnot\varphi\rightarrow\lnot\psi)\rightarrow(\psi\rightarrow\varphi)~\middle|~\psi,\varphi\in\textit{PL}\right\}\text{, or}\end{array}\\ \exists j,m:(j<m<i)\land\left(\{\varphi_j,\varphi_m\}\overset{(\textit{MP})}{\vdash}\varphi_i\right)\end{array}$

   We say $\psi$ is a syntactic consequence of $\Gamma$, denoted $\Gamma\vdash\psi$, if there is a $\Gamma$-proof for $\psi$. Typical connotations are $\vdash\psi$ for $\emptyset\vdash\psi$, $\varphi\vdash\psi$ for $\{\varphi\}\vdash\psi$, and $\Gamma,\varphi\vdash\psi$ for $\Gamma\cup\{\varphi\}\vdash\psi$.

Now that we have defined syntactic consequence, we can prove $(R1')$:

4. (Theorem) It holds $\left\{\Gamma\vdash\psi,\Gamma\vdash\psi\rightarrow\varphi\right\}\Rightarrow\Gamma\vdash\varphi$, for ${\Gamma\subseteq\textit{PL}}$ and ${\psi,\varphi\in\textit{PL}}$. $(R1')$

   (Proof) By $\Gamma\vdash\psi$, there is a $\Gamma$-proof $\sigma_\psi=\psi_1,\dots,\psi_m$ with $\psi_m=\psi$, and by $\Gamma\vdash\psi\rightarrow\varphi$, there is a $\Gamma$-proof $\sigma_{\psi\rightarrow\varphi}=\psi_1',\dots,\psi_n'$ with $\psi_n'=\psi\rightarrow\varphi$. We can now construct a $\Gamma$-proof $\sigma_\varphi=\sigma_\psi,\sigma_{\psi\rightarrow\varphi},\varphi$, since $\{\psi_m,\psi_n'\}=\{\psi,\psi\rightarrow\varphi\}\overset{(\textit{MP})}{\vdash}\varphi$. $\square$

The calculus

$(A1)~\psi\rightarrow(\varphi\rightarrow\psi)\\ (A2)~(\psi\rightarrow(\varphi\rightarrow\chi))\rightarrow((\psi\rightarrow\varphi)\rightarrow(\psi\rightarrow\chi))\\ (A3)~(\lnot\varphi\rightarrow\lnot\psi)\rightarrow(\psi\rightarrow\varphi)\\ (R1)\left\{\vdash\psi,\vdash\psi\rightarrow\varphi\right\}\Rightarrow~\vdash\varphi$

now follows directly from the definition of syntactic consequence and $(R1')$:

$(R1)$ is the special case for $(R1')$ with $\Gamma=\emptyset$. It is important to note that the calculus $(A1),(A2),(A3),(R1)$ does not define syntactic consequence, but it is a system to infer statements about unconditional syntactic consequence (for which soundness and completeness can be shown).

It is now possible to prove the deduction theorem as desired, using $(MP)$ and/or $(R1')$.

Answer 2

I believe you are (understandably!) not interpreting the $R1$ rule correctly:

$(R1)~\text{If }\vdash\psi\text{ and }\vdash\psi\rightarrow\varphi\text{, then }\vdash\varphi.$

Since the $\vdash$ is typically used as a meta-logical theorem to express the derivability of some statement from other statements through the use of inference rules of some proof system (or calculus, as you call it), you understandably interpret this rule indeed as a kind of meta-theorem regarding the derivability of statements: "If $\psi$ is derivable (without any assumptions), and $\psi \rightarrow \varphi$ is derivable (without any assumptions), then $\varphi$ is derivable (without any assumptions)"

However, I am fairly sure the intended interpretation of $R1$ in the book (I don't have access to the book, so I can't tell for sure) is not as a meta-logical theorem, but as an inference rule. In fact, it would be your very Modus Ponens:

"If you are doing a derivation, and at some point you have $\psi$ as well as $\psi \rightarrow \varphi$ as lines in your derivation, then you can write down $\varphi$ as a line in your derivation"

In our discussions, you seem to indicate that $A1,A2, and A3$ are to be treated as statements about derivability such as well, i.e. that they can be written as:

$(A1)\vdash ~\psi\rightarrow(\varphi\rightarrow\psi)\\ (A2)\vdash ~(\psi\rightarrow(\varphi\rightarrow\chi))\rightarrow((\psi\rightarrow\varphi)\rightarrow(\psi\rightarrow\chi))\\ (A3)\vdash ~(\lnot\varphi\rightarrow\lnot\psi)\rightarrow(\psi\rightarrow\varphi)$

and where, as such, they are again to be seen as meta-logical theorems: "any statement of the form $\psi\rightarrow(\varphi\rightarrow\psi)$ is derivable"

Interestingly, this is exactly how Metamath (http://us.metamath.org/mpegif/mmset.html#axioms) describes its axioms.

But again, I believe $A1$, $A2$, and $A3$ should be seen as inference rules, which simply say (in the case of A1): "At any point during a derivation you can write down a line of the form $\psi\rightarrow(\varphi\rightarrow\psi)$"

Indeed, I think a purist would frown upon Metamath's use of $\vdash$ to define its inference rules, since inference rules are just that: inference rules. While meta-logical statements (for which we would use $\vdash$) are statements about the power of some set of inference rules.

I have several reasons for believing that, while R1 used the meta-logical symbol $\vdash$, it is really just used to define the Modus Ponens inference rule:

• Any axiomatic system that I have seen has Modus Ponens as a given inference rule, and $R1$ seems to fit that bill reading it the way I do. Indeed, while Metamath describes $A1,A2,A3,R1$ using the $\vdash$, it does not treat $A1,A2,A3,R1$ as meta-logical theorems, but as inference rules.
• If $R1$ is not an inference rule (and possibly $A1,A2,A3$ aren't either), then how are you supposed to perform any actual inferences?
• Indeed, if $R1$ (and possibly $A1,A2,A3$) are meta-logical theorems about the derivability of statements, then what proof system is it a meta-logical theorem of? What is it talking about?!

In the discussion you say that $\Gamma \vdash \varphi$ iff $\Gamma \vDash \varphi$, but we have to make that statement $\Gamma \vdash \varphi$ relative to specific proof systems. Indeed, it is easy to come up with proof systems where this does not hold. That is, you can have proof systems that are not sound and complete. For example, take a proof system (call it $N$, for 'Null') that has no inference rules at all. That system is (trivially) sound, but hopelessly incomplete. So, we don't have $\Gamma \vdash_N \varphi$ iff $\Gamma \vDash \varphi$. Or take a proof system (call it $Q$) that has the 'Hokus Ponens' rule that says that at any point during a derivation you can put down any statement you want. $Q$ is (trivially) complete, but hopelessly unsound. So, again, we don't have $\Gamma \vdash_Q \varphi$ iff $\Gamma \vDash \varphi$.

So, when you seem to indicate that you want to prove some kind of derivability ($\vdash$) claim on the basis of a logical consequence claim $\vDash$), you are putting the cart before the horse! First you need to define what $\vdash$ means for a particular system $S$, and then you can try to prove $\Gamma \vdash_S \varphi$ iff $\Gamma \vDash \varphi$

Indeed, the very use of $\vdash$ without indexing it to specify what proof system we are talking about is circumspect. Even worse, when you make claims like "it does not matter how we define it, because we have $\Gamma \vdash \varphi$ iff $\Gamma \vDash \varphi$", I am getting really concerned. Yes, we sometimes say that for propositional logic (and first-order logic) $\Gamma \vdash \varphi$ iff $\Gamma \vDash \varphi$, and as such we say that 'propositional logic is complete' and 'first-order logic is complete', but we do that because there exist proof systems for which this is true, and typically we use exactly such systems. But given any particular system $S$, we cannot simply assume that $\Gamma \vdash_S \varphi$ iff $\Gamma \vDash \varphi$: we would actually need to prove that (and, given the earlier examples of systems $N$ and $Q$, this may simply not be the case).

In other words, if $R1$ is supposed to be a derivability statement, as you take it to be, then you have to specify what proof system we are talking about, i.e. $R1$ would need to be formulated as:

$(R1)~\text{If }\vdash_S \psi\text{ and }\vdash_S\psi\rightarrow\varphi\text{, then }\vdash_S\varphi.$

where $S$ is a specific proof system. But this is not how $R1$ is described. Why not? You know my answer: Because I think it is really just an inference rule, not a meta-logical theorem.

Now, your $R1'$ is a meta-logical theorem though. And to be sure, let's specify that the proof system consisting of $A1,A2,A3,R1$ is system $HS$ (for Hilbert system), so we can properly write down $R1'$:

$(R1')~\text{If }\Gamma \vdash_{HS} \psi\text{ and }\Gamma \vdash_{HS}\psi\rightarrow\varphi\text{, then }\Gamma \vdash_{HS}\varphi.$

But $R1'$ follows immediately from the fact that $HS$ contains $R1$:

Suppose $\Gamma \vdash_{HS} \varphi$ and $\Gamma \vdash_{HS} \varphi \rightarrow \psi$

To show that $\Gamma \vdash_{HS} \psi$ do the following:

Start with $\Gamma$ as your premises.

Since $\Gamma \vdash_{HS} \varphi$, we now we can derive $\varphi$

Similarly, since $\Gamma \vdash_{HS} \varphi \rightarrow \psi$, we can also derive $\varphi \rightarrow \psi$

And now apply R1 on $\varphi$ and $\varphi \rightarrow \psi$ to get $\psi$

So, starting with $\Gamma$, we can derive $\psi$. And so $\Gamma \vdash_{HS} \psi$

Finally, please note that as a meta-logical theorem, R1' is not an inference rule, and it is not your typical Modus Ponens, which is an inference rule. An inference rule is part of a proof system (or calculus as you call it) that lets us derive statements from other statements. A meta-logical theorem is a claim about what such proof systems can or cannot derive. Indeed, if R1 itself is taken as a meta-logical theorem (as you seem to take it), then for this system it would not even be true that $\vdash P \rightarrow P$, even if $A1$, $A2$, and $A3$ are to be taken as axioms or inference rules that lets you derive statements of the respective forms, because you have no further inference rule to actually combine those statements to derive other statements (like $P \rightarrow P$).