2

In the book "A tour through mathematical logic" - by Robert S. Wolf, the deduction theorem is specified as follows:

If T $\cup$ {P} $\vdash$ Q, then T $\vdash$ (P $\to$ Q)

Where T is a first-order theory and P & Q are some formulae, in the language of this first-order theory. Then, is the following interpretation, of the deduction-theorem, correct?

If Q is derivable/provable from T $\cup$ {P}, then one can say that - if P is derivable from T (i.e. P is a theorem of T) then Q is also derivable from T.

Also, does this interpretation capture the essence of the deduction theorem?

PS: another question titled Deduction Theorem - Intuition, seems to focus primarily on the syntactic aspects of the theorem and predicate calculus in general - rather than on its semantics.

x.projekt
  • 292
  • 1
  • 10
  • 1
    Your statement is true, but it doesn't at all capture the deduction theorem. Note that "If $T\vdash P$ then $T\vdash Q$" is a very weak claim: it's vacuously true if $T\not\vdash P$. The deduction theorem by contrast is not trivialized if $T\not\vdash P$. – Noah Schweber Sep 20 '20 at 07:11
  • 1
    @NoahSchweber - why does (P $\to$ Q) (in general, where P & Q are some formulae in a first-order language) become trivial, when P is not provable, since in an axiomatic-system the definition of $\to$ (implication connective) is not based on a truth table? Shouldn't it be that P not being provable doesn't say anything about provability of Q (from the same set of axioms) and should be independently verified by actually trying to prove Q? And why are we even considering the concepts of "truth" (and "falsity") in an axiomatic [formal] system, which should solely be based on provability? – x.projekt Sep 20 '20 at 07:49

1 Answers1

2

is the following interpretation, of the deduction-theorem, correct?

No. What you write is

If $T \cup \{P\} \vdash Q$, then if $T \vdash P$, then $T \vdash Q$.

This is the same as saying

(1) If $T \cup \{P\} \vdash Q$, then $T \nvdash P$ or $T \vdash Q$.

But this is not equivalent to

(2) If $T \cup \{P\} \vdash Q$, then $T \vdash P \to Q$.

It may be the case that $P$ is not provable, but $P \to Q$ isn't either. Then "$T \nvdash P$ or $T \vdash Q$" holds, but "$T \vdash P \to Q$" does not. So (1) $\not \Rightarrow$ (2).

This is what is meant in the comments by "trivialization": "if $T \vdash P$ then $T \vdash Q$" (= what you wrote) becomes trivially true if $T \nvdash P$, i.e. if $P$ is unprovable. But "$T \vdash P \to Q$" (= what the deduction theorem states) does not: Just because we can't prove $P$ doesn't mean we can prove $P\to Q$ -- as you observed. Hence why "$T \vdash P \to Q$" is a stronger claim that "If $T \vdash P$ then $T \vdash Q$".

The essence of the deduction theorem is that you can "flip-flop" between having a theorem dependent on an open assumption and proving a conditional statement:
If there is a proof of $Q$ which is still dependent on the assumption $P$, then there will be a proof in the theory of the statement $P \to Q$. This is the immediate effect of the conditional proof technique (see p. 14).
And for the converse direction of the deduction theorem, if you can prove $P \to Q$, then you will be able to prove $Q$ under the assumption that $P$. This is a consequence of the modus ponens rule of inference (see p. 13).
The two directions combined, the deduction theorem simply justifies what we mean by having a proof of "$\to$".

You are completely right in pointing out that the central notion of a formal system is that of proof rather than truth. But do keep in mind that we're normally interested in designing a "useful" proof system that is "in line" with the notion of truth: A statement should be provable in a theory exactly when it is true in all models of the theory. After all, the point of a proof system is to have a mechanical device to rigorously prove statements we consider true. So while the notion of a proof of $\to$ is formulated in terms of rules of inference, the way these rules are used does reflect the truth table for $\to$: A proof system should be (and as for the proof system presented in Wolf's book, is) sound w.r.t. the semantics: What can be proved is true (according to the truth table definitions) in all structures; the system (hopefully) doesn't prove random nonesense.

Natalie Clarius
  • 10,530
  • How is "If $T \cup {P} \vdash Q$, then if $T \vdash P$, then $T \vdash Q$" same as saying "If $T \cup {P} \vdash Q$, then $T \nvdash P$ or $T \vdash Q$"? And since we are on this topic - how should one interpret P $\to$ Q (where P & Q are some formulae in a first-order language), in an axiomatic system. – x.projekt Sep 20 '20 at 14:38
  • 1
    That's just the meaning of a mathematical "if ... then": "If $A$ then $B$" = "(not $A$) or ($B$)". So "If $T \vdash P$ then $T \vdash Q$" = "not $T \vdash P$ or $T \vdash Q$" = "$T \nvdash P$ or $T \vdash Q$". – Natalie Clarius Sep 20 '20 at 14:42
  • Doesn't this result come from the "truth-table" based definition of the $\to$ (implication connective). And would it be right to even consider this result in a purely a axiomatic-system? – x.projekt Sep 20 '20 at 14:43
  • Rather the other way round: The truth table of $\to$ in logic is derived from the mathematical understanding of "if ... then". And how "if ... then" is understood is just a matter of conventional language use. – Natalie Clarius Sep 20 '20 at 14:45
  • I'm not sure what you mean by "interpreting $P \to Q$ in an axiomatic system". "$T \vdash P \to Q$" means that the formula $P \to Q$ is derivable without further assumptions from the axioms of $T$ in the given system. – Natalie Clarius Sep 20 '20 at 14:50
  • In classical logic (the one based on truth or falsity of propositions) P $\to$ Q is propositionally-equivalent to $\neg$P $\lor$ Q (it's straight forward if one draws the truth tables, for the two propositions). But then how do you interpret $\neg$P in an axiomatic-system? Isn't it an operator that transforms P into an another formula whose proofs are the refutations of P? – x.projekt Sep 20 '20 at 14:54
  • The "interpretation" of a formula in a proof system is always that it is derivable using the rules of the system -- it is a purely syntactic notion, "syntactic" in the sense that it is defined purely in terms of fiddling around with symbols, without making explicit reference to "semantic" notions such as valuations or truth tables. – Natalie Clarius Sep 20 '20 at 14:58
  • What a proof of a formula looks like depends on the particular proof system, the formula in question, and what proof is being used (there may be several proofs for the same formula in the same system). A proof of $\neg P$ typically amounts to showing that a contradiction can be derived from assuming $P$ using the axioms of the theory. – Natalie Clarius Sep 20 '20 at 14:59
  • I don't understand, why is it valid to interchangeably use the concepts of classical-logic (truth-table based) and predicate-logic (formal-system based)? Because classical-logic and predicate-logic are only analogous (to some extent) and not the same. (See Pg. 30) – x.projekt Sep 20 '20 at 15:23
  • 1
    (I don't know why the links to the auto-created chat keep disappearing; here it is: https://chat.stackexchange.com/rooms/113227/discussion-between-harshatech2012-and-lemontree). – Natalie Clarius Sep 20 '20 at 16:55