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” …