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