2

I am using the deduction theorem from this site https://en.wikipedia.org/wiki/Deduction_theorem

Can you write the word implies as such for the deduction theorem (Δ∪{A}⊢B)⊢(Δ⊢A→B)? Also, I am confused because isn't {A} a set? I thought this {A} should be a sequence.

W. G.
  • 1,766
  • 1
    NO; the Deduction Th is a meta-theorem, i.e. a result about properties of the calculus and not a formula proved in the calculus. – Mauro ALLEGRANZA Apr 20 '17 at 19:33
  • 1
    The correct formulation of the DT is: if we have a derivation $\Delta \cup { A } \vdash B$, then we can build a new derivation: $\Delta \vdash A \to B$. – Mauro ALLEGRANZA Apr 20 '17 at 19:34
  • So it is okay that {A} is a set and that the formula is written the way I have it except the middle syntactic consequence should be ->? – W. G. Apr 20 '17 at 19:35
  • Okay thank you for your help. Just one more question. Should the middle syntactic consequence should be ->? – W. G. Apr 20 '17 at 19:40
  • @W.G. I would stay away from $\rightarrow$ as well, since that is a formal logic symbol. Just stick to an 'if ... then ...' expression! Indeed, what you call the 'midlle syntactic consequence' is NOT AT ALL a syntactic consequence: it is a statement about the derivability of logic statements from other logic statements (where those logic statements may involve $\rightarrow$'s). So $\rightarrow$, $\vdash$, and a plain ;if ... then ..' are all different! – Bram28 Apr 20 '17 at 19:42
  • Can I ask why you wouldn't use that symbol just out of curiosity? I thought that if... then is the same thing as that symbol. Also, if you put your answer down in the bottom I am sure I would give it to you. You have been very helpful! – W. G. Apr 20 '17 at 19:45

2 Answers2

5

The symbol $\vdash$ express derivability in the calculus.

The syntax is:

$Δ ⊢ φ$, where $Δ$ is a set of formulas: the set of assumptions (or premises) used in the derivation of the conclusion $\varphi$.

Thus it is correct to write $Δ \cup \{ A \}$.

The *Deduction Theorem is a meta-theorem, i.e. a result about properties of the calculus and not a formula proved in the calculus.

The correct formulation of the Deduction Theorem is:

if we have a derivation $Δ ∪ \{ A \} ⊢ B$, then we can build a new derivation: $Δ ⊢ A→B$.


We have here two "levels": the level of the calculus, working with formulas written with the connectives. One of them is the conditional: $\to$.

Thus, $\to$ is a symbol of the language used in the calculus.

The second "level" is the meta-theory, where we have the relation of derivability between a set of formulas and a formula.

Thus, $\vdash$ is a symbol of the meta-language used to express the properties of the calculus.

The calculus is purely symbolical: it is made of "objects" called formulas, rules and sequences of formulas: derivations.

In the meta-theory we prove mathematical theorems about the calculus and its properties.

One of these theorems is the DT, expressing the fact that from an existing derivation (in the calculus) we can manufacture a new derivation.

The language of meta.theory is the usual math-English made of a mixture of symbols, like $\vdash$ and natural language; thus, there is no real advantage to use $\to$ in palce of "if..., then...".

But we can find mathematical logic textbooks where $\to$ is used as connective and $\Rightarrow$ is used in the meta-language to abbreviate "implies".

1

No, you really shouldn't write $(\Delta \cap \{ A \} \vdash B) \vdash (\Delta \vdash A \rightarrow B)$, because the $\vdash$ in $\Delta \cap \{ A \} \vdash B$ as well as in $\Delta \vdash A \rightarrow B$ is about the derivability of statements from other statements relative to some proof system (and so it would be best to use something like $\vdash_P$ where $P$ is the proof system you are considering), while the $\vdash$ you use in the middle is not at all that. So you really should just say that:

"If $\Delta \cap \{ A \} \vdash B$ then $\Delta \vdash A \rightarrow B$"

Likewise, I would not use $(\Delta \cap \{ A \} \vdash B) \rightarrow (\Delta \vdash A \rightarrow B)$ since $\rightarrow$ is a symbol used in a particular logic system that the derivability statements are about. Indeed, the $\rightarrow$ in $\Delta \vdash A \rightarrow B$ is part of the logical expression $A \rightarrow B$ that is claimed to be derivable from the set of formulas $\Delta$. But the $\rightarrow$ you would put between $(\Delta \cap \{ A \} \vdash B)$ and $\Delta \vdash A \rightarrow B$ is not at all combining two logic formulas, but rather two meta-logical statements about derivability. So you really don't want to mix those up!

And yes, in logic we use $\rightarrow$ to try and capture 'if .. then ...' expressions, but the match is not perfect. The $\rightarrow$ is really just a mathematically defined truth-function, but the English conditional isn't always used in that way. Look up "Paradox of Material Implication", e.g: https://en.wikipedia.org/wiki/Paradoxes_of_material_implication!

Finally, the $A$ is a statement/formula, not a sequent.

Bram28
  • 100,612
  • 6
  • 70
  • 118