Proof of the Deduction Principle

[loseyourname]

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?

 

[wave]

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?

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.

 

[loseyourname]

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?

 

[wave]

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? \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).

 

[loseyourname]

Well gee, that's even simpler. Thanks.

 

[MathematicalPhysicist]

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?

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

 

[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

 

[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.

 

[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).

There's your plain-as-day contradiction.