Proof of the Deduction Principle

  • Context: Graduate 
  • Thread starter Thread starter loseyourname
  • Start date Start date
  • Tags Tags
    Principle Proof
Click For Summary

Discussion Overview

The discussion revolves around the proof of the Deduction Principle in propositional logic, specifically the assertion that if a set of formulae combined with a formula implies another formula, then the original set of formulae implies the conditional of the first formula leading to the second. Participants explore the nature of this principle, its implications for Conditional Introduction, and the methods of proof, including semantic and syntactic approaches.

Discussion Character

  • Exploratory
  • Technical explanation
  • Debate/contested
  • Mathematical reasoning

Main Points Raised

  • Some participants express confusion about how to formally prove the Deduction Principle, seeking clarity on the necessary steps and methods.
  • One participant suggests that the proof follows from the definition of the semantic entailment, indicating that if the premises hold, the conclusion must also hold.
  • Another participant proposes a semantic proof involving a contradiction if the conclusion does not follow from the premises, suggesting that this approach simplifies the proof process.
  • Some participants note that the Deduction Theorem is an "if and only if" statement, which adds complexity to the discussion.
  • One participant introduces an alternative proof method that involves considering truth assignments and their implications for the premises and conclusion.
  • There is mention of the distinction between semantic notions (|=) and syntactic notions (|-) in the context of the Deduction Theorem, with some participants emphasizing the importance of the deductive rules of the system in question.
  • A later reply provides a more formalized approach to the proof, detailing the logical steps and truth valuations involved in reaching a contradiction.

Areas of Agreement / Disagreement

Participants do not reach a consensus on the proof method or the complexity of the proof. Multiple competing views on the nature of the proof and its implications remain present throughout the discussion.

Contextual Notes

Some participants highlight the need for clarity on whether a syntactic or semantic proof is required, as well as the implications of the Deduction Theorem being an "if and only if" statement. The discussion also reflects varying levels of familiarity with the concepts involved.

loseyourname
Staff Emeritus
Gold Member
Messages
1,840
Reaction score
5
Let [tex]\varphi[/tex] and [tex]\psi[/tex] both be formulae, and let [tex]\Gamma[/tex] be a set of formulae.

If [tex]\Gamma \cup \{\varphi\} \models \psi[/tex], then [tex]\Gamma \models (\varphi \rightarrow \psi)[/tex]

This is the principle by which the rule of inference known as Conditional Introduction is justified, but I cannot seem to find a proof for it, though the claim in the text is that it is an easy proof. Does anybody know what the proof is?
 
Physics news on Phys.org
loseyourname said:
Let [tex]\varphi[/tex] and [tex]\psi[/tex] both be formulae, and let [tex]\Gamma[/tex] be a set of formulae.

If [tex]\Gamma \cup \{\varphi\} \models \psi[/tex], then [tex]\Gamma \models (\varphi \rightarrow \psi)[/tex]

This is the principle by which the rule of inference known as Conditional Introduction is justified, but I cannot seem to find a proof for it, though the claim in the text is that it is an easy proof. Does anybody know what the proof is?

It pretty much follows from the definition of [tex]\models[/tex]. Suppose [tex]\Gamma \cup \{\varphi\} \models \psi[/tex]. Then every truth assignment that satisfies [tex]\Gamma \cup \{\varphi\}[/tex] must also satisfy [tex]\psi[/tex].
 
Last edited:
I can see intuitively why it's true, I'd just like to know how to write out the actual proof for purposes of demonstration. I guess the real question is just if there is some special method that has to be used to demonstrate that one argument implies another, or if we can just treat each as a conditional, in which case the proof seems to be a simple, one-step case of exportation:

1. [tex](\gamma \wedge \varphi) \rightarrow \psi[/tex]
2. [tex]\therefore \gamma \rightarrow (\varphi \rightarrow \psi)[/tex]
3. [tex]\gamma \rightarrow (\varphi \rightarrow \psi)[/tex] 1. Exp.

Can it really be that simple, or do I also have to demonstrate how [itex]\Gamma \cup \{\varphi\} \models \psi[/itex] is equivalent to [itex](\gamma \wedge \varphi) \rightarrow \psi[/itex] and so on?
 
Last edited:
loseyourname said:
I can see intuitively why it's true, I'd just like to know how to write out the actual proof for purposes of demonstration.

You mean a syntactic proof? [itex]\models[/itex] is a semantic notion, so the following semantic proof will suffice:

Suppose [itex]\Gamma \cup \{\varphi\} \models \psi[/itex] but not [itex]\Gamma \models (\varphi \rightarrow \psi)[/itex]. Then there is some truth assignment [itex]\tau[/itex] that satisfies [itex]\Gamma[/itex] and [itex]\varphi[/itex] but not [itex]\psi[/itex]. But [itex]\Gamma \cup \{\varphi\} \models \psi[/itex], so [itex]\tau[/itex] satisfies [itex]\Gamma[/itex], [itex]\varphi[/itex] and [itex]\psi[/itex]. That is a contradiction, hence [itex]\Gamma \models (\varphi \rightarrow \psi)[/itex].
 
Last edited:
Well gee, that's even simpler. Thanks.
 
loseyourname said:
Let [tex]\varphi[/tex] and [tex]\psi[/tex] both be formulae, and let [tex]\Gamma[/tex] be a set of formulae.

If [tex]\Gamma \cup \{\varphi\} \models \psi[/tex], then [tex]\Gamma \models (\varphi \rightarrow \psi)[/tex]

This is the principle by which the rule of inference known as Conditional Introduction is justified, but I cannot seem to find a proof for it, though the claim in the text is that it is an easy proof. Does anybody know what the proof is?
i should point out that the deduction thoerem is an iff statement.
 
another way of proving this thoerem is as follows:
suppose a1,...,an|=b
then we either have the premise as true and the conclusion b as true, or the conclusion false.
the first case is trivial.
for the second part, suppose an is true then a1,...an-1 is false and an->b is either true or false depending on b, either way we get a1,...,an-1|=an->b
now if an is false then a1,...,an-1 is either false or true but the cocnlusion is always true, cause an->b is always true.
so either way we get a1,...,an-1|=an->b
 
As wave said, |= is a semantic notion. However, whenever I've heard of the deduction theorem, it's been about the deductive strength of a system. I.e. what you said but with |- instead of |=.

How hard this is to prove will depend upon the deductive rules and/or axioms of the system in question.
 
You can formalize the metaproof if that's what you want. Here are the parts that I felt like writing out, which seem to be the parts wave skipped. Since you need two implication symbols, I let [itex]\rightarrow[/itex] be the one from the original object language.

1. [tex]\forall \tau, \phi, \psi \ [(\tau(\phi \rightarrow \psi) = F) \ \Leftrightarrow \ (\tau(\phi) = T \ \wedge \ \tau(\psi) = F)][/tex] -- from definition of truth-valuation.
2. [tex]| \exists \tau, \Phi, \phi, \psi \ [((\tau(\Phi) = T \ \wedge \ \tau(\phi) = T) \ \Rightarrow \ \tau(\psi) = T) \ \wedge \ (\tau(\Phi) = T \ \wedge \ \tau(\phi \rightarrow \psi) = F)][/tex] -- theorem to prove written out in terms of truth-valuations, negated for Reductio, and simplified.
3. [tex]| \exists \tau, \Phi, \phi, \psi \ [(\neg(\tau(\Phi) = T \ \wedge \ \tau(\phi) = T \ \wedge \ \tau(\psi) = F) \ \wedge \ (\tau(\Phi) = T \ \wedge \ (\tau(\phi) = T \ \wedge \ \tau(\psi) = F)][/tex] -- to first conjunct: double negation, distribute inner negation, swap 'not equal to true' for 'equal to false'; to second conjunct: substitute formula from (1).

There's your plain-as-day contradiction.
 
Last edited:

Similar threads

  • · Replies 4 ·
Replies
4
Views
1K
  • · Replies 10 ·
Replies
10
Views
2K
  • · Replies 4 ·
Replies
4
Views
4K
  • · Replies 5 ·
Replies
5
Views
3K
  • · Replies 9 ·
Replies
9
Views
5K
  • · Replies 3 ·
Replies
3
Views
3K
  • · Replies 3 ·
Replies
3
Views
4K
  • · Replies 19 ·
Replies
19
Views
4K
  • · Replies 5 ·
Replies
5
Views
3K
  • · Replies 2 ·
Replies
2
Views
3K