Proof of the Deduction Principle

1. Jul 12, 2006

loseyourname

Staff Emeritus
Let $$\varphi$$ and $$\psi$$ both be formulae, and let $$\Gamma$$ be a set of formulae.

If $$\Gamma \cup \{\varphi\} \models \psi$$, then $$\Gamma \models (\varphi \rightarrow \psi)$$

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?

2. Jul 12, 2006

wave

It pretty much follows from the definition of $$\models$$. Suppose $$\Gamma \cup \{\varphi\} \models \psi$$. Then every truth assignment that satisfies $$\Gamma \cup \{\varphi\}$$ must also satisfy $$\psi$$.

Last edited: Jul 12, 2006
3. Jul 12, 2006

loseyourname

Staff Emeritus
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. $$(\gamma \wedge \varphi) \rightarrow \psi$$
2. $$\therefore \gamma \rightarrow (\varphi \rightarrow \psi)$$
3. $$\gamma \rightarrow (\varphi \rightarrow \psi)$$ 1. Exp.

Can it really be that simple, or do I also have to demonstrate how $\Gamma \cup \{\varphi\} \models \psi$ is equivalent to $(\gamma \wedge \varphi) \rightarrow \psi$ and so on?

Last edited: Jul 12, 2006
4. Jul 12, 2006

wave

You mean a syntactic proof? $\models$ is a semantic notion, so the following semantic proof will suffice:

Suppose $\Gamma \cup \{\varphi\} \models \psi$ but not $\Gamma \models (\varphi \rightarrow \psi)$. Then there is some truth assignment $\tau$ that satisfies $\Gamma$ and $\varphi$ but not $\psi$. But $\Gamma \cup \{\varphi\} \models \psi$, so $\tau$ satisfies $\Gamma$, $\varphi$ and $\psi$. That is a contradiction, hence $\Gamma \models (\varphi \rightarrow \psi)$.

Last edited: Jul 12, 2006
5. Jul 12, 2006

loseyourname

Staff Emeritus
Well gee, that's even simpler. Thanks.

6. Jul 14, 2006

MathematicalPhysicist

i should point out that the deduction thoerem is an iff statement.

7. Jul 14, 2006

MathematicalPhysicist

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

8. Jul 31, 2006

yossell

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.

9. Aug 1, 2006

honestrosewater

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 $\rightarrow$ be the one from the original object language.

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