Talk:Deduction theorem

difference?

I'm having trouble understanding how the deduction theorem differs from the conditional proof inference rule in the propositional calculus. We have:

"if φ |-- ψ, then |-- φ -> ψ" (Deduction_theorem)

vs

"If ψ can be derived while assuming the hypothesis φ, we may infer ( φ → ψ )." Propositional calculus

I can't help but think these are synonymous. Maybe the problem is that the former is given in much more formal notation than the latter. Would it help me, do people suppose, if someone would translate the latter into a more symbolic form? (Can that even be done?)

In any case, there must be something subtle (at least given my background) going on here. Help? --Ryguasu 19:31, 17 May 2005 (UTC)

The deduction theorem applies to axiomatic systems, and the rule of conditional proof to natural deduction systems. They're analogous, but different. The deduction theorem is not a rule of the formal system; it is a property of the system's deducibility relation abstractly construed. Nortexoid 05:33, 2 April 2007 (UTC)

Actually the deduction theorem is deeply relevant for axiomatic systems, as it justifies the modus ponens rule : the deduction theorem "says" that the arrow is deeply linked to the notion of derivation form assumptions (which is a notion missing from axiomatic systems). So, by saying that you have the deduction theorem in an axiomatic system you're justifying the modus ponens as a rule because you showed that the arrow keeps the track of a derivation. And then, by composition of derivations, you know that if you have a proof of, say, A you have a proof of B (assuming that you have a proof of A --> B). This is why it's relevant in axiomatic systems. But if you consider natural deduction systems for example, it's not relevant anymore as you already have the notion of a derivation from assumptions. Then, the deduction theorem is "internalized" within the rules for the arrow. Ianshil (talk) 14:49, 13 February 2017 (UTC)

What's the difference between "deeply relevant" and just plain "relevant"? — Preceding unsigned comment added by 184.179.86.135 (talk) 14:21, 3 July 2018 (UTC)

Proof

In the middle part of the proof:

• Q→((Q→R)→R) 8. deduction from 5 to 7 QED

Would it not be sufficient to use 5 and 7 instead 5, 6 and 7, because 6 does not show up in this line, to get to this last line? Further 6 is already used the line above. Is this not enough? Indeed very clear your article and I understand here more than in Deduktionstheorem Cheers.--de:Benutzer:Roomsixhu —The preceding unsigned comment was added by 87.187.55.111 (talk) 02:20, 2 April 2007 (UTC).

I just looked at it a second time: Line 6 results from a hypothesis, line 5, and an axiom 1, line 4, thus you only have to remember the hypothesis not the axiom, and can omit it. But line 7 is essential because this is combined and not axiomatic. Cheers de:Benutzer:Roomsixhu

I said "deduction from 5 to 7" rather than say "deduction 5 and 7" because all of the steps from 5 to 7, i.e. steps 5, 6, and 7 depend on the hypothesis 5. And they are used in deducing the conclusion 7. Step 7 depends on step 6 which depends on step 5. In any case, the form of this virtual rule of inference is fixed and cannot be varied depending on the peculiarities of a special case. JRSpriggs 09:43, 2 April 2007 (UTC)

Thank you again: I only noticed that, because 6 depends on 5 an the axiom 1 (line 4) and 8 depends on 5, 6 and 7, but 6 depends on 5 and 4, and 4 is the axiom. In my calculus you have basic formulas and basic rules, and can leave the basic formulas out, that seems to be different with your calculus which has axioms. But I did not find it in our german wikipadia described that clearly. I still will do some practice, to get more secure. Point 3.2 is a simple example how to get further "meta"-formulas from the basic lattice. --de:Benutzer:Roomsixhu —The preceding unsigned comment was added by 87.187.55.111 (talk) 13:24, 2 April 2007 (UTC).

References to Herbrand's and Tarski's proofs, etc.

I have heard this before but I am suspicious because no-one ever gives evidence. Where is Herbrand's proof and for what system? Where is Tarski's proof and for what system? And how is it known that neither got it from the other, directly or indirectly. And how is it known that no-one did it earlier?Tyro13 (talk) 18:46, 2 November 2014 (UTC)

For reference, the referenced passage in the article introduction is

Though it has seemed "obvious" to mathematicians literally for centuries that proving B from A conjoined with a set of theorems is tantamount to proving the implication A → B based on those theorems alone, it was left to Herbrand and Tarski to show (independently) this was logically correct in the general case.

Indeed, I would regard this claim as not only unsourced but outright dubious, as the first axioms (P1–P3) of a Hilbert-style deduction system are precisely what one needs for the deduction theorem — why would one pick these particular axioms if one doesn't mean to establish hypothetical reasoning by means of the deduction theorem? Tarski and Herbrand were both born during the first decade of the 1900's, so it is highly unlikely that any work of theirs would have had much time to influence Hilbert on something as fundamental as the axioms of propositional logic.

On the other hand, the story told in Hilbert-style deduction system doesn't seem to check out when I look in van Heijenoort's From Frege to Gödel. The Hilbert axioms for implication are stated several times in that book (one text by Kolmogorov, one text by Hilbert himself), but the central P3 axiom $(C\to (B\to A))\to ((C\to B)\to (C\to A))$ is not in any of the presentations. Instead Hilbert's list of axioms of implication goes

1. $A\to (B\to A)$
2. $(A\to (A\to B))\to (A\to B)$
3. $(A\to (B\to C))\to (B\to (A\to C))$
4. $(B\to C)\to ((A\to B)\to (A\to C))$

The place where $(C\to (B\to A))\to ((C\to B)\to (C\to A))$ does appear is in Frege's Begriffsschrift, and Frege lists it (van Heijenoort, p. 29) together with $A\to (B\to A)$ and $(D\to (B\to A))\to (B\to (D\to A))$ as being those three propositions, out of the nine "forming the core of the presentation", that can be written using implication alone; it's easy to interpret this description as awarding these formulae a status as axioms. (Hilbert, D.; Ackermann, W. (1950). Mathematical Logic (Second ed.). New York: Chelsea. p. 29.), essentially from 1928, indeed gives a system of six axioms for propositional logic and ascribes it to Frege. But $A\to A$ is not an axiom in either, and Frege in fact gives a proof of it in the Begriffsschrift!

So yes, the history of this seems quite unintuitive. Proper sourcing is needed! 130.243.68.163 (talk) 17:07, 18 December 2019 (UTC)

More data points on this matter:

1. Mendelson (ISBN 0-534-06624-0) provides a reference for Herbrand, to (Herbrand, J. (1930). "Recherches sur la theorie de la demonstration". Travaux de la Soc. des Sci. et des Lettres Varsovie, III. 33: 33–160.), apparently translated as (Herbrand, J. (1971). Logical Writings. Harvard & Reidel.). Mendelson only makes this attribution in the context of the propositional calculus deduction theorem; for the predicate calculus deduction theorem he gives no attribution at all.
2. The Frege tradition could in fact be used to put lower bounds on the discovery of the deduction theorem. Since Frege did have all the axioms needed for the (propositional calculus) deduction theorem, but also included $(D\to (B\to A))\to (B\to (D\to A))$ as an "axiom" even though proving this would be a straightforward application of the deduction theorem, we can infer that he in fact did not have the deduction theorem. Hilbert&Ackermann (1928 edition or only 1938 edition?) attribute a simplified Frege-style axiom system to Lukasiewicz (not Lukasiewicz&Tarski jointly), so sometime during that half century a proof of $(D\to (B\to A))\to (B\to (D\to A))$ had been discovered (though that need not have been by way of a deduction theorem).

The Herbrand reference would probably need a page number before put back in the article. And even then it probably shouldn't be in the article top, but in a section on the history of the theorem. 130.243.68.37 (talk) 14:15, 19 December 2019 (UTC)

References

Turnstiles?

In much of this article, the ordinary turnstile (symbol) $\vdash$ is used. But then, in the section (rather confusingly) titled The deduction theorem in predicate logic, we read that

The deduction theorem is also valid in first-order logic ... the symbol ├ means "is a syntactical consequence of."

well, duhh. But I'm now confused on multiple levels: are we talking about first-order logic, or about predicate logic? We can't have it both ways, can we?

Now I always thought that the turnstyle $\vdash$ always means "is a syntactic consequence of.", so why is there a different kind of turnstyle ├ being used in this section? Does this mean that the earlier turnstyles were not syntactic consequences? Some other kind of entailment? Or is this all just bad formatting and bad editing in this article? Or are these actually different turnstyles with different, ermmm... meanings?

I mean, if I do look at Logical consequence#Modal accounts, one gets a description of kripke frames. Is the sense of entailment being talked about in this article -- can it be one of those kinds of entailments, too? I'm pretty sure that once we dive into the deep end of modal logic, one will find some intermediate logics which don't have weakening as an axiom, as so are unable to prove the deduction theorem. So even the very concept of entailment for these logics leads to a morass -- some clarity in this article would really really help.

At any rate, it would be nice if the lead to the article wikilinked to both turnstile (symbol) and explained that it really means entailment and specifically, syntactic entailment, and not something else (?) (and maybe explain that "syntactic entailment" means "you can get a proof for it") as otherwise, one is left in the ozone... 67.198.37.16 (talk) 05:50, 31 August 2016 (UTC)

The two turnstile symbols are supposed to be the same. Unfortunately, they are rendered differently by TeX and HTML.

Propositional logic is a subset of Predicate logic. So most things said about Propositional logic also hold for Predicate logic (also called first order logic). JRSpriggs (talk) 19:46, 31 August 2016 (UTC)

You're ducking the core issues. The article is an ugly mess, a mish-mash that is incomprehensible, even if you already know a fair amount of logic. It's in dire need of repair and attention from someone who actually knows the topic. 67.198.37.16 (talk) 04:28, 1 September 2016 (UTC)

Axiom 1 ???

The section titled Examples of deduction -- the very first section after the lead, could use a bunch of words to explain what is going on. So, I recognize the so-called "axiom 1" because it is the first axiom in the Hilbert system -- well, except that its actually an axiom schema, not an axiom, and its actually axiom schema 2 not 1 ... it seems like "axiom 1" is just some random phrase concocted for just this article, and not a real thing. Confusing axioms with axiom schema also does not instill confidence.

I'm also confused about the indentation. The style clearly is NOT the sequent calculus so I assume that its supposed to be the Hilbert style. If so, can we say so, and wikilink to Hilbert system? However, the Hilbert system article does not talk about indentation.... and then the very next section contradicts everything:

The next section is called Virtual rules of inference, which does explain indentation, and also invokes the need for three rules of inference. Now, the Hilbert system has only one rule of inference, so this new system of inference is clearly some other system. If I go to rule of inference, I don't really see those three rules called out there. Nor do they make an appearance in List of rules of inference, so they seem to be some sort of exceptional or extraordinary rules, living in their own little special cloud. Is this why they are they called "virtual"? Is "virtual" an actual term used in the literature? If I google the phrase "virtual rule of inference", I don't get anything promising, so is this term some kind of original neologism invented just for this article??? This is kind of confusing.

Then the first rule of inference is called "hypothesis", but from my understanding, this rule would not be allowed in (for example) linear logic. It seems to be some kind of form of "weakening" aka Monotonicity of entailment, which is not allowed in a variety of different logics. Soo .. Is "hypothesis" actually the same thing as weakening, or is it something that is somehow different??? At any rate, it would appear that the deduction theorem can only hold in some logics, and not all ...

All these questions leave me largely confused. I mean, if I blur my eyes, I feel like I vaguely sort of get it, but the details are completely confusing; I cannot tell what is valid, when its valid, and under what circumstances what can be invoked where or when. 67.198.37.16 (talk) 06:18, 31 August 2016 (UTC)

Hilbert's axiom schema P1 is derivable from his axiom schemas P2 and P3. So many systems omit it.

I see no reason to treat Hilbert's system as the be-all and end-all as you seem to be doing.

The way HTML and Tex are handled on Wikipedia make it difficult to do certain kinds of indentation. JRSpriggs (talk) 19:57, 31 August 2016 (UTC)

Well, I don't think it has anything to do with Hilbert systems either. So we are in complete agreement, there. But I think you're ducking the core issues. The article is an ugly mess, a mish-mash that is incomprehensible, even if you already know a fair amount of logic. It's in dire need of repair and attention from someone who actually knows the topic. It reads like an amateur attempt to explain the concept -- full of mis-directions and mis-statements and vague, undefined terms, invented terminology. Its horrid. 67.198.37.16 (talk) 04:31, 1 September 2016 (UTC)

I would delete most of the examples, which seem very idiosyncratic to me, and tighten up the prose some. — Carl (CBM · talk) 11:02, 1 September 2016 (UTC)

Derivation of the helpful theorems

See Deduction theorem#Helpful theorems. As an example of how much the deduction theorem simplifies proofs, I will derive the helpful theorems both with and without the deduction theorem. To show:

A→A

(B→C)→((A→B)→(A→C))

(A→(B→C))→(B→(A→C))

(A→B)→((B→C)→(A→C))

(A→(A→C))→(A→C)

With the deduction theorem:

1. ___A hypothesis

2. A→A deduction

3. ___B→C hypothesis

4. ______A→B hypothesis

5. _________A hypothesis

6. _________B modus ponens 5,4

7. _________C modus ponens 6,3

8. ______A→C deduction

9. ___(A→B)→(A→C) deduction

10. (B→C)→((A→B)→(A→C)) deduction

11. ___A→(B→C) hypothesis

12. ______B hypothesis

13. _________A hypothesis

14. _________B→C modus ponens 13,11

15. _________C modus ponens 12,14

16. ______A→C deduction

17. ___B→(A→C) deduction

18. (A→(B→C))→(B→(A→C)) deduction

19. ___A→B hypothesis

20. ______B→C hypothesis

21. _________A hypothesis

22. _________B modus ponens 21,19

23. _________C modus ponens 22,20

24. ______A→C deduction

25. ___(B→C)→(A→C) deduction

26. (A→B)→((B→C)→(A→C)) deduction

27. ___A→(A→C) hypothesis

28. ______A hypothesis

29. ______A→C modus ponens 28,27

30. ______C modus ponens 28,29

31. ___A→C deduction

32. (A→(A→C))→(A→C) deduction

Without the deduction theorem:

1. B→(A→B) given

2. (A→(B→C))→((A→B)→(A→C)) given

3. (A→((B→A)→A))→((A→(B→A))→(A→A)) 2

4. A→((B→A)→A) 1

5. (A→(B→A))→(A→A) modus ponens 4,3

6. A→(B→A) 1

7. A→A modus ponens 6,5 FIRST

8. [(A→(B→C))→((A→B)→(A→C))]→((B→C)→[(A→(B→C))→((A→B)→(A→C))]) 1

9. (B→C)→[(A→(B→C))→((A→B)→(A→C))] modus ponens 2,8

10. ((B→C)→[(A→(B→C))→((A→B)→(A→C))])→([(B→C)→(A→(B→C))]→[(B→C)→((A→B)→(A→C))]) 2

11. [(B→C)→(A→(B→C))]→[(B→C)→((A→B)→(A→C))] modus ponens 9,10

12. (B→C)→(A→(B→C)) 1

13. (B→C)→((A→B)→(A→C)) modus ponens 12,11 SECOND

14. ((A→B)→(A→C))→((B→(A→B))→(B→(A→C))) 13

15. [((A→B)→(A→C))→((B→(A→B))→(B→(A→C)))]→([(A→(B→C))→((A→B)→(A→C))]→[(A→(B→C))→((B→(A→B))→(B→(A→C)))]) 13

16. [(A→(B→C))→((A→B)→(A→C))]→[(A→(B→C))→((B→(A→B))→(B→(A→C)))] modus ponens 14,15

17. (A→(B→C))→((B→(A→B))→(B→(A→C))) modus ponens 2,16

18. [(A→(B→C))→((B→(A→B))→(B→(A→C)))]→([(A→(B→C))→(B→(A→B))]→[(A→(B→C))→(B→(A→C))]) 2

19. [(A→(B→C))→(B→(A→B))]→[(A→(B→C))→(B→(A→C))] modus ponens 17,18

20. (B→(A→B))→[(A→(B→C))→(B→(A→B))] 1

21. (A→(B→C))→(B→(A→B)) modus ponens 1,20

22. (A→(B→C))→(B→(A→C)) modus ponens 21,19 THIRD

23. [(B→C)→((A→B)→(A→C))]→[(A→B)→((B→C)→(A→C))] 22

24. (A→B)→((B→C)→(A→C)) modus ponens 13,23 FOURTH

25. (A→(A→C))→((A→A)→(A→C)) 2

26. [(A→(A→C))→((A→A)→(A→C))]→[(A→A)→((A→(A→C))→(A→C))] 22

27. (A→A)→((A→(A→C))→(A→C)) modus ponens 25,26

28. (A→(A→C))→(A→C) modus ponens 7,27 FIFTH

Although the proof without the deduction theorem turned out to have fewer steps, those steps were much more complicated (and less obvious) in many cases. JRSpriggs (talk) 21:48, 23 October 2018 (UTC)

To show that two other theorems can be used in place of axiom 2.

1. B→(A→B) given

2. (A→B)→((B→C)→(A→C)) given

3. (A→(A→C))→(A→C) given

4. (A→(B→C))→(((B→C)→(A→C))→(A→(A→C))) 2

5. [(A→B)→((B→C)→(A→C))]→([((B→C)→(A→C))→(A→(A→C))]→[(A→B)→(A→(A→C))]) 2

6. [((B→C)→(A→C))→(A→(A→C))]→[(A→B)→(A→(A→C))] modus ponens 2,5

7. [(A→(B→C))→(((B→C)→(A→C))→(A→(A→C)))]→(([((B→C)→(A→C))→(A→(A→C))]→[(A→B)→(A→(A→C))])→[(A→(B→C))→((A→B)→(A→(A→C)))]) 2

8. ([((B→C)→(A→C))→(A→(A→C))]→[(A→B)→(A→(A→C))])→[(A→(B→C))→((A→B)→(A→(A→C)))] modus ponens 4,7

9. (A→(B→C))→((A→B)→(A→(A→C))) modus ponens 6,8

10. ((A→B)→(A→(A→C)))→[((A→(A→C))→(A→C))→((A→B)→(A→C))] 2

11. [(A→(B→C))→((A→B)→(A→(A→C)))]→([((A→B)→(A→(A→C)))→[((A→(A→C))→(A→C))→((A→B)→(A→C))]]→[(A→(B→C))→[((A→(A→C))→(A→C))→((A→B)→(A→C))]]) 2

12. [((A→B)→(A→(A→C)))→[((A→(A→C))→(A→C))→((A→B)→(A→C))]]→[(A→(B→C))→[((A→(A→C))→(A→C))→((A→B)→(A→C))]] modus ponens 9,11

13. (A→(B→C))→[((A→(A→C))→(A→C))→((A→B)→(A→C))] modus ponens 10,12

14. ((A→(A→C))→(A→C))→((A→(B→C))→((A→(A→C))→(A→C))) 1

15. (A→(B→C))→((A→(A→C))→(A→C)) modus ponens 3,14

16. [(A→(B→C))→[((A→(A→C))→(A→C))→((A→B)→(A→C))]]→([(A→(B→C))→((A→(A→C))→(A→C))]→[(A→(B→C))→[(A→(B→C))→((A→B)→(A→C))]]) 9

17. [(A→(B→C))→((A→(A→C))→(A→C))]→[(A→(B→C))→[(A→(B→C))→((A→B)→(A→C))]] modus ponens 13,16

18. (A→(B→C))→[(A→(B→C))→((A→B)→(A→C))] modus ponens 15,17

19. ((A→(B→C))→[(A→(B→C))→((A→B)→(A→C))])→[(A→(B→C))→((A→B)→(A→C))] 3

20. (A→(B→C))→((A→B)→(A→C)) modus ponens 18,19 QED

-- JRSpriggs (talk) 17:53, 29 October 2018 (UTC)