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.

  • $\begingroup$ For the sake of the problem Im sure you can take modus ponens as a given. Its not an axiom; it can be proven from simpler statements. $\endgroup$ – CogitoErgoCogitoSum Mar 21 '17 at 1:45
  • 1
    $\begingroup$ And I want to know how can it be proven. $\endgroup$ – xamid Mar 21 '17 at 8:54
  • $\begingroup$ I think that first you need the notion of "derivation from assumption" : $\Gamma \vdash \varphi$. $\endgroup$ – Mauro ALLEGRANZA Mar 22 '17 at 13:25
  • $\begingroup$ But in this case you have to state the MP rule without the "restriction" : $\vdash$. With it standing, you can only prove tautologies, and the fact that you can add (by monotonicity) unused premises $\Gamma$ does not change the fact that in this way the $\varphi$ in $\Gamma \vdash \varphi$ is a tautology, simply because you must have first a derivation $\vdash \varphi$ and after you add the premises. $\endgroup$ – Mauro ALLEGRANZA Mar 22 '17 at 13:27
  • $\begingroup$ @MauroALLEGRANZA Yes, that's exactly what I have been trying to tell the OP as well. I believe the OP is confused about what $R1$ means. Could you please take a look at my Answer? Thanks! $\endgroup$ – Bram28 Mar 23 '17 at 13:27

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$).

  • 1
    $\begingroup$ But my $(R1)$ works only if $\vdash\varphi$ and $\vdash\varphi\rightarrow\psi$ hold (i.e. they are tautologies), which is not the case. You want to use $(R1')$ which I want to prove. $\endgroup$ – xamid Mar 21 '17 at 8:51
  • $\begingroup$ @xamid Oh, I see what you mean. Well, then you have a problem, since then A1, A2, A3, and R1 can only derive tautologies. $\endgroup$ – Bram28 Mar 21 '17 at 13:44
  • $\begingroup$ Can you prove that? In the above comments @CogitoErgoCogitoSum stated that it could be proven from simpler statements, but he did neither prove his claim, and your statements are contradicting each other. I would be surprised if there is no valid argumentation for $(R1')$ based on $(R1)$, since they are similar. $\endgroup$ – xamid Mar 22 '17 at 11:36
  • $\begingroup$ @xamid Yes. The statement you can get by the application of A1, A2, and A3 are tautologies. And the way you interpret R1, which is: if you can derive $\varphi$ from nothing, and if you can derive $\varphi \rightarrow \psi$ from nothing, then you can derive $\psi$. Now, since the only statements you can get from nothing are the ones you can get through A1, A2, and A3, which are all tautologies, that means that any statements of the form $\varphi$ and $\varphi \rightarrow \psi$ that you can get from nothing are tautologies as well ... and that means that $\psi$ has to be a tautology as well. $\endgroup$ – Bram28 Mar 22 '17 at 11:39
  • $\begingroup$ I dont understand what you mean. I want to show $(R1')$. You say you can show even based on the above explaination of syntactic consequence $(\vdash)$, you could prove this impossible. How? Also note that we are talking about metatheorems. (To your edit: This shows only that you cannot derive it only from $(A1),(A3),(R1)$, but it doesn't consider the definition of syntactic consequence $\Gamma\vdash\psi$ for $\Gamma\ne\emptyset$.) $\endgroup$ – xamid Mar 22 '17 at 11:44

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')$:

  1. (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')$.


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.