I am following the book Propositional and Predicate Calculus: A Model of Argument by Derek Goldrei, which includes a proof of the deduction theorem, first for propositional logic and then outlines a proof for predicate logic based on the proof for propositional logic. I do not see how (parts of) the proof for prop. logic works also for predicate logic.

The proof (for prop. logic) inductively shows that if $\Gamma, \phi \vdash \psi$ has a derivation $\psi_1,\dots,\psi_n = \psi$ under $\Gamma, \phi$, then we also have $\Gamma \vdash (\phi \rightarrow \psi_i)$ for $i = 1,\dots,n$. The inductive step involves "gluing" together different derivations to obtain the required derivation to complete the proof (see picture below for details).

The book later states that proving the deduction theorem for predicate calculus doesn't require much more and the prop. logic proof is most of the work required with an extended argument needed to cover Generalization as an inference rule.

Question: In predicate calculus, because of the Thinning Rule, $\Gamma \vdash \phi$ is defined by the book as there existing some $\Gamma_0 \subseteq \Gamma $ such that there exists a derivation (using certain Axioms, Modus Ponens and Generalization for variables not occurring free in any formula in the set of hypotheses) of $\phi$ under the hypotheses $\Gamma_0$. Because of this definition, how can we glue together two different derivations under $\Gamma$? What if one of the derivations involves Generalization which isn't valid unless one makes the set of hypotheses "smaller", i.e. work under $\Gamma_0$ rather than $\Gamma$.

I may be misunderstanding some definition here. If that is the case, please let me know. Thank you.

Inductive step in proof of deduction theorem for prop. logic:

enter image description here


See Goldrei's comment on the role of the thinning rule at page 223.

I think that there is no issue with it in the proof of the DT for predicate logic.

We have a derivation $Γ, \phi \vdash \psi$; due to the def of page 221, in it we have no use of Gen that quantifies a variable $x$ that is free in $\Gamma$ or $\phi$.

Thus, mimicking the propositional proof, in order to manage the step regarding the Gen rule we have to suppose that there is some $j < i$ such that $\psi_i$ is $∀x\psi_j$.

By the inductive hypotheses: $\Gamma \vdash \phi \to \psi_j$ and we know that $x$ is not a free variable of $\phi$, then, by axiom (A5), $(∀x(\phi → ψ_j) → (\phi → ∀xψ_j))$.

Since $Γ ⊢ \phi \to \psi_j$, we have, by Gen, $Γ ⊢ ∀x(\phi \to \psi_j)$, and so, by MP, $Γ ⊢ \phi \to ∀x\psi_j$; that is, $Γ ⊢ \phi \to \psi_i$.

  • $\begingroup$ Thanks for your answer. What I don't understand is that if it is the case that $\Gamma \vdash \phi$, then there is not necessarily a derivation (following the conditions given in the def on pg 221) of $\Gamma \vdash \phi$, it may be the case that there is a derivation of $\Gamma_0 \vdash \phi$ and the Thinning Rule has been applied to declare $\Gamma \vdash \phi$. So how do you know we have a derivation of $\Gamma, \phi \vdash \psi$? Again, by derivation I mean a sequence of formulas satisfying the conditions. In particular, Gen being used only for variables not free in $\Gamma, \phi$. $\endgroup$ – user334263 Dec 22 '17 at 11:50
  • $\begingroup$ @user334263 - it is the assumption of the DT: if there is a derivation $\Gamma, \phi \vdash \psi$, then ....". $\endgroup$ – Mauro ALLEGRANZA Dec 22 '17 at 12:21
  • $\begingroup$ That, I think, explains my confusion. However in Ex 5.5 on pg. 226, the deduction theorem for predicate calculus is stated as "for all formulas $\phi, \psi$ and sets of formulas $\Gamma$, if $\Gamma, \phi \vdash \psi$ then $\Gamma \vdash (\phi \rightarrow \psi)$." This is confusing because if $\Gamma, \phi \vdash \psi$, by the definition on pg 221, there isn't necessarily a derivation of it, which is a condition you added in your comment for DT. $\endgroup$ – user334263 Dec 22 '17 at 12:34
  • $\begingroup$ @user334263 - as explained in the answer above, if we have $\Gamma, \phi \vdash \psi$, this means that we have a "formally correct" derivation according to def of derivation (page 221). This means that we have used the axioms and rules according to the "specifications" of the def: "(iv) $\phi_i$ is of the form $∀x \phi_j$, where $\phi_j$ is a previous formula in the sequence and the quantified variable $x$ does not appear free in any formula in the set $Γ$ [nor in $\phi$]." $\endgroup$ – Mauro ALLEGRANZA Dec 22 '17 at 12:48
  • $\begingroup$ Following the discussion on pg. 223, we have $\phi(y), \forall x \phi(x) \vdash \forall y \phi(y)$, yet there is no "formally correct" derivation of this using the conditions outlined in the def of derivation. Does this not contradict what you said? (As shown, what we do have is that there is a derivation of $\forall x \phi(x) \vdash \forall y \phi(y)$ and by the thinning rule we declare $\phi(y), \forall x \phi(x) \vdash \forall y \phi(y)$, despite not having a derivation of it. Am I misunderstanding something?) $\endgroup$ – user334263 Dec 22 '17 at 13:02

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.