Rules of Inference « Paul Nicholls

17May/090

Rules of Inference

Proof Theory allows the representation of mathematical proofs facilitates the analysis of proofs by expressing them syntactically. For example, in the sequent below the formulas $\phi _1 \ldots \phi _n$ allow us to conclude $\psi$ . Such a sequent is valid if it can be proved.

$\phi_1 \ldots \phi_n \vdash \psi$

We can form a collection of proof rules which allow us to infer new forumlae from existing ones. These inference rules are a relation between premise formulae and conclusions. Such rules take the general form:

$\begin{array}{l}\underline {\begin{array}{*{20}c}{\phi_1 \mbox{ Premise 1 } } \\\ldots \\{\phi _n \mbox{Premise 2 }} \\\end{array}} \\\psi \mbox{ Conclusion }\\\end{array}$ name of rule

There are a number of natural deducation rules we can apply to this system.

And Introduction ( $\wedge i$ )

Quite simply, if two things are true then their conjunction is true.

$\dfrac{\phi_1 , \phi_2 }{\phi_1 \wedge \phi_2} \wedge i$

And Elimination ( $\wedge e$ )

Similarly, if a conjunction is true then so must be its indivudal atoms

$\dfrac{\phi_1 \wedge \phi_2 }{\phi_1 } \wedge e_1$ $\dfrac{\phi_1 \wedge \phi_2 }{\phi_2 } \wedge e_2$

Double Negation ( $\neg \neg e$ )

Two wrongs do make a right.

$\dfrac{\neg \neg \phi}{\phi} \neg \neg e$

And likewise, from a right you can make two wrongs.

$\dfrac{\phi}{\neg \neg \phi} \neg \neg i$

Implication Elimination ( $\rightarrow e$ )

If you know an implication, then if it's premise is true so must be its conclusion. Also known as Modus Ponendo Ponens.

$\dfrac{\phi_1 \rightarrow \phi_2 , \phi_1}{\phi_2} \rightarrow e$

Derived from this is Modus Tollendo Tollens. If you know the outcome of an implication is false, then the premise must also be false.

$\dfrac{\phi_1 \rightarrow \phi_2 , \neg \phi_2}{\neg\phi_1} \rightarrow e$

Implication Introduction ( $\rightarrow i$ )

If you assume the premise of an introduction, you can prove its outcome to be true in context.

$\dfrac{{\begin{array}{*{20}c}\phi_1 \\\vdots \\\phi_2 \\\end{array} }}{{\phi_1 \to \phi_2 }} \to i$

Or Introduction ( $\vee i$ )

If you know something to be true then its disjunction with anything else will also be true.

$\dfrac{\phi_1}{\phi_1 \vee \phi_2} \vee i_1$ $\dfrac{\phi_2}{\phi_1 \vee \phi_2} \vee i_2$

Or Elimination ( $\vee e$ )

If A entails C and B entails C, then when A or B is true, C is true. A bit of a mouthful.

$\dfrac{{\phi_1 \vee \phi_2 ,\begin{array}{*{20}c}\phi_1 \\\vdots \\\chi \\\end{array} ,\begin{array}{*{20}c}\phi_2 \\\vdots \\\chi \\\end{array} }}{\chi } \vee e$

Contradictions ( $\perp$ )

Any formula can be derived from a contradiction. For example:

$\dfrac{\perp}{\phi} \perp e$

$\dfrac{\phi , \neg \phi}{\perp} \perp i$

$\dfrac{{\begin{array}{*{20}c}\phi \\\vdots \\\perp \\\end{array} }}{{\neg \phi}} \neg i$

Tagged as: PR, PR-SV, Proof Theory Leave a comment

Comments (0) Trackbacks (0) ( subscribe to comments on this post )

No comments yet.

Tweets

The @hi_lights_tv boys are playing International Rescue again #fb http://t.co/fqgUmQFQ 2012/02/04
"wetter than an otters pocket" #fb 2012/02/04
went to Palace Green Library for the first time ever today. Don't think I really missed much. #ThingsIWontMissAboutDurham #fb 2012/02/03
Good day at the tank factory. Very upset we're not allowed to drive any of them though :-( #fb 2012/01/25

Lifestream

Checked in at The Mill House

— 44m ago via Foursquare
Checked in at Hi-Lights

— 8h ago via Foursquare
Checked in at Van Mildert College

— 1d ago via Foursquare
Listened to 4 songs.

— February 5th via Last.fm
Listened to 5 songs.

— February 3rd via Last.fm
Checked in at Tennyson House

— February 3rd via Foursquare
Checked in at Durham University Library | Palace Green

— February 3rd via Foursquare
Checked in at Hi-Lights

— February 3rd via Foursquare

Paul Nicholls Stuff