natural deduction

Printable View

April 22nd 2010, 09:52 PM
Kiwili49

natural deduction

Hey,

I am having trouble proving...

$\sigma \rightarrow Y \vdash (\phi \lor \sigma ) \to (\phi \lor Y)$

I know that the beginning hypotheses are $\sigma \rightarrow Y$ and $(\phi \lor \sigma )$ , but I am not sure how to break down the "or" statement.

Thanks!
April 23rd 2010, 12:07 AM
emakarov

Quote:

http://www.mathhelpforum.com/math-he...bf64801f-1.gif

You need the disjunction elimination rule (reasoning by cases). You have the assumption $\phi\lor\sigma$ . If $\phi$ is true, then $\phi\lor Y$ is. If $\sigma$ is true, then, using MP, again $\phi\lor Y$ is true. In both cases the needed conclusion is true.
April 23rd 2010, 06:12 AM
Kiwili49

I understand that I need to use disjunctive elimination, but I need to solve using natural deduction. Don't I need to break down the first "or" statement? If so, how do I do that only using the hypotheses I have?
April 23rd 2010, 07:17 AM
emakarov

Disjunction elimination is one of the inference rules of Natural Deduction. See lecture notes by Frank Pfenning (CMU), p. 8 and the famous book "Proofs and Types" by Girard, Lafont and Taylor, ch. 10, p. 72; these are available online. For an authoritative reference concerning the set of rules see the monograph by H. Schwichtenberg and A. Troelstra, "Basic Proof Theory".
April 23rd 2010, 08:05 AM
Kiwili49

thank you so much for your help! do you know of any more good resources that explain $\forall$ and $\exists$ introduction and elimination for natural deduction? All of the books and web sources I have looked at are difficult for me to understand. I don't know when I can introduce or eliminate those symbols because I don't understand the restrictions on free variables or the substitutions needed.
April 24th 2010, 11:47 AM
emakarov

I don't know what concrete source to recommend. Natural deduction is a very standard topic that is described in multiple textbooks. The original (and readable) book about ND is by the guy who popularized it: "Natural Deduction. A Proof-Theoretic Study" by Dag Prawitz (actually, this was his PhD dissertation). The book by Girard, Lafont & Taylor is highly praised but is written for smart readers. Frank Pfenning has taught many deep courses on constructive mathematics (which usually starts with ND), and he has good lecture notes.

I would choose some source by a solid practicing mathematical logician, such as Frank Pfenning. I personally don't like texts by philosophers, and I don't like texts that start proof theory using either Hilbert-style axiomatic system or in general anything other than ND or Sequent Calculus.

The brief idea concerning variables is to distinguish whether you are proving something or using an assumption, and between "for all" and "exists". To prove "for all", you fix some fresh x; you don't have control in choosing it. Similarly, when you use an existential fact, you say, "let's call the object that exists x". Again, there is no control over choosing it.

On the other hand, when you need to prove existence, any existing object works: you can choose 0, 5, or anything that makes the statement true. Similarly, if you have a universal assumption that starts with "for all x", you can take its special case for any x you like.

I could also add that natural deduction is close to such topics as lambda-calculus, type theory and constructive mathematics (though these are usually not considered elementary topics). Studying them, you can also understand natural deduction better.

After re-reading this, I think these recommendations are too comprehensive, but feel free to ask concrete questions here.