# UNISA Chatter – Formal Logic: Formal proofs

See UNISA – Summary of 2010 Posts for a list of related UNISA posts. This post is in addition to three summary posts I am building over the next couple of months … in this case we are focusing on formal proofs and re-enforcing some of the concepts we have covered in the summary posts.

The content I am covering and trying to wrap my brain around at the moment is the deductive system F   also known as the system of natural deduction or principles of reasoning. Our companion will be the tool “Fitch”, which allows us to construct and evaluate formal proofs.

## Conjunction Elimination

 We need to prove the three goals, which fail as we are missing a few steps in the proof. Missing –> Elim By adding the rule of conjunction we can prove the three goals successfully as shown. In essence we are inferring Tet(a) from the sentence: Tet(a) Ù Tet(b) Ù Tet(c)  Ù (Small(a) Ú Small(b)). … same with the sentences three and four, both of which are Ù Elim’s.

## Conjunction Introduction

 The example below shows an example of a corresponding introduction rule based proof, which is missing a number of Elim’s and an Intro. Missing –> Elim, Intro … let’s fix the proof 🙂 Step 1 … breaking up the first sentence using conjunction elimination, we build sentence eight (8), which proves the first of two goals. Step 2 … repeat the same process for the second goal and prove both goals 🙂 We also enable the step numbering to make it more obvious in terms of what we are proving and referring to.

## Disjunction Elimination

 Step 2-4 and 5-6 are two sub proofs, one for each of the two disjuncts. 2-4 is a disjunction elimination example. 5-6 is a disjunction introduction example. Lines 4 & 6 bring us to the goal, hence completing the proof.

## Negation Elimination

 The example shows that by proving a contradiction ^ on the basis if an additional assumption (line 2), we can infer Ø from the original premise.

Next journey will be to the planet of “Conditionals” …

Tags