0
$\begingroup$

The Deduction Theorem states: $\Sigma \cup \theta \vdash \phi <=> \Sigma \vdash \theta \to \phi$ and I will claim to prove it as follows:

<-: Assume $\Sigma \vdash \theta \to \phi$. Because of monotony it follows that $\Sigma \cup \theta \vdash \theta \to \phi $ and because of triviality we also have $\Sigma \cup \theta \vdash \theta$ which by mp leads us to $\Sigma \cup \theta \vdash \phi$.

->: Assume $\Sigma \cup \theta \vdash \phi$ and assume soundness, so we know that $\Sigma \cup \theta \vdash \phi$ is a tautology of the form $ (\Sigma \lor \theta) \to \phi$ and $\Sigma \vdash \theta \to \phi$ is a tautology of the form $\Sigma \to (\theta \to \phi)$. Now we assume the implication to be false, i.e. $ ((\Sigma \lor \theta) \to \phi) \land \lnot(\Sigma \to (\theta \to \phi))$ to be true. A truth table shows us that this conjunction is always false which means that the assumption of the implication to be false was false itself which makes the implication true. $ \square$

Is this a legit proof or where does it fail? I am especially curious if I can go from $\Sigma \cup \theta$ to $\Sigma \lor \theta$ and if not why not. If my proof fails can you rescue it somehow because I like my proof since it's simple while most proofs of the deduction theorem look rather complicated, mostly they prove it by induction, probably because they don't assume soundness like I do?

$\endgroup$
6
  • $\begingroup$ $\Sigma \cup \{ \theta \}$ means $\Sigma \land \theta$. $\endgroup$ Jan 8, 2020 at 19:29
  • $\begingroup$ The usual proof of DT is "complicated" exactly because it does not assume soundness: it is a purely syntactical proof. $\endgroup$ Jan 8, 2020 at 19:39
  • 2
    $\begingroup$ In addition, the DT holds also when $\Sigma$ is infinite, while the "tautology" $\Sigma \to (\theta \to \phi)$ is a wff only if it is a finite expression. $\endgroup$ Jan 8, 2020 at 19:40
  • $\begingroup$ Is the first comment really true? I thought $\Sigma \cup \theta$ means just the union/disjunction of both, not the intersection/conjunction. $\endgroup$
    – user714882
    Jan 13, 2020 at 20:29
  • $\begingroup$ Also: Can someone give me a complete proof or link of a proof that is relatively easy/structured to understand? $\endgroup$
    – user714882
    Jan 13, 2020 at 20:32

1 Answer 1

1
$\begingroup$

Long comment

The usual proof of the Deduction Theorem is "boring" exactly because it does not assume soundness: it is a purely syntactical proof.

A semantic one amounts to showing: if $A \vDash B$, then $\vDash A \to B$, which is straightforward (for propositional logic it is a simple check with truth table).

The proof of DT is by induction and this is the reason why it is boring. We can find it in every textbook that uses a so-called Hilbert-style proof system (like e.g. Mendelson, page 30), i.e. a proof system with axioms and Modus Ponens rule of inference: the lesser is the number of axioms, the shortest the proof.

It is worth noting that there are proof systems, like e.g. Natural Deduction where the DT is built-in into the rules.

Two points must be stressed:

(i) the DT holds also when $Σ$ is infinite, while the tautology $Σ → (θ → \phi)$ is a well-formed formula only when it is a finite expression.

(ii) the inductive proof of the DT gives a recipe (a "mechanical" procedure) to produce, form the derivation $Σ,θ \vdash \phi$ the new derivation $Σ ⊢ θ → \phi$.

$\endgroup$
2
  • $\begingroup$ So if I understand you then the syntactical proof of DT is always connected to a certain formal system like natural deduction, Hilbert-calculus etc.? $\endgroup$
    – user714882
    Jan 16, 2020 at 16:49
  • 1
    $\begingroup$ Your semantic version of DT is wrong: it should be "if $A\models B$, then $\models A\rightarrow B$" or "if $A,C\models C$, then $A\models B\rightarrow C$." (@Pippen, yes, DT is a priori a result about a specific formal system, and any proof of DT has to address that - either by using the completeness theorem for that formal system or by working entirely within that formal system. The former approach is the "semantic" one and the latter is the "syntactic" one.) $\endgroup$ Feb 19, 2020 at 17:29

You must log in to answer this question.