Talk:Deduction theorem

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search
WikiProject Mathematics (Rated Start-class, Mid-importance)
WikiProject Mathematics
This article is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
Start Class
Mid Importance
 Field:  Foundations, logic, and set theory
WikiProject Philosophy (Rated Start-class, Mid-importance)
WikiProject icon This article is within the scope of WikiProject Philosophy, a collaborative effort to improve the coverage of content related to philosophy on Wikipedia. If you would like to support the project, please visit the project page, where you can get more details on how you can help, and where you can join the general discussion about philosophy content on Wikipedia.
Start-Class article Start  This article has been rated as Start-Class on the project's quality scale.
 Mid  This article has been rated as Mid-importance on the project's importance scale.


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)


"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 (talk) 14:21, 3 July 2018 (UTC)


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 (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 (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)


In much of this article, the ordinary turnstile (symbol) 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 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... (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. (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. (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. (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)

Retrieved from ""
This content was retrieved from Wikipedia :
This page is based on the copyrighted Wikipedia article "Talk:Deduction theorem"; it is used under the Creative Commons Attribution-ShareAlike 3.0 Unported License (CC-BY-SA). You may redistribute it, verbatim or modified, providing that you comply with the terms of the CC-BY-SA