Introduction to Formal Proofs - A Toy Proof System
by Ken Monks
The following is an exercise designed to introduce you to some of the main
concepts used in doing formal mathematical proofs. Read the following and try
the exercises. We will discuss how this applies to actual mathematical
proofs in class.
We begin by defining our language.
Def: A TOY FORMULA is either
a. .
b. o
c. w|v where w and v are toy formulas
d. all the formulas are obtained by a-c.
In other words, toy formulas are just strings of o's and .'s separated by |'s. For
example o, ., o|., o|o|o|o, and o|.|o|o|.|. are all examples of toy formulas.
These toy formulas correspond to the mathematical statements we can make. Unlike
normal mathematical statements, these formulas don't MEAN anything.
We now define some axioms, which are toy formulas that are, by definition,
automatically provable.
Axiom 1: o|.
Axiom 2: .|o
We next specify some rules of inference which allow us to deduce new provable
toy formulas, or theorems, from the ones we already have proven.
The notation we will use to describe these rules of inference is as follows:
INPUTLINE1
INPUTLINE2
:
INPUTLINEn
---------------
OUTPUTLINE1
OUTPUTLINE2
:
OUTPUTLINEm
This describes a rule of inference in the following manner... if all of the
INPUTLINEs are proven, then we can conclude that all of the OUTPUTLINEs are
proven as well. Usually we will specify whole families of such rules of
inference by using meta-variables which stand for an arbitrary toy formula (such
as w and v in the Rules below).
In other words, if we interpret this notation as a "recipe" for deducing lines
in our proofs, then we can interpret the above notation as:
In order to show OUTPUTLINE1,...,OUTPUTLINEm
1. First show INPUTLINE1,
2. Then show INPUTLINE2,
:
n. Then show INPUTLINEn.
Here are the Rules of Inference for our toy system.
Rule of inference 1: For any formulas w and v,
w|v
v|w
---
w
Rule of inference 2: For any formulas w and v,
w
v
-----
w|.|v
Rule of inference 3: For any formulas w and v,
w|v|.
-----
w|o
That's it! You might want to stop reading here and try some proofs on your own
before reading the discussion below.
Comment: the |'s are not really needed at all but they might help you see that
a string can be broken into substrings in many ways, so I decided to keep
them for that reason.
Here is an example:
Thm A: .
Pf:
1. o|. Axiom 1
2. .|o Axiom 2
3. . Rule 1; 2,1
QED
Comments: note that when giving a rule as a reason I give the line numbers
used as inputs in the rule in the order that they correspond to the lines in
the rule. Thus in line 3 above I could not say it is because of Rule 1; 1,2.
If I had used Rule 1 with lines 1 and 2 then w would be o and v would be . and
so we would have concluded o instead of .
Let's try something with rule 2...
Thm B: .|.|.
Pf:
1. . Thm A
2. .|.|. Rule 2; 1,1
QED
Fun fun fun!
How about something with Rule 3?
Thm C: .|.|o
Pf:
1. .|.|. Thm B
2. .|.|.|.|.|.|. Rule 2; 1,1
3. .|.|o Rule 3; 2
QED
----------------------------------------------------------------------------
EXERCISES:
1. Prove the following:
Thm D: o
Thm E: .|o|o
Thm F: o|.|.|o
Thm G: o|o|o|o
Thm H: .|o|.
Thm I: .|o|o|o
2. Now the question that immediately comes to mind is:
Is EVERY formula provable in this toy proof system?
If so, then this would be analogous to having an inconsistent system in
normal logic. I know the answer to this, but I will let you think about it.
See if you can figure out whether or not every formula is provable in this
system. If not every formula is provable, can you determine exactly which
formulas are provable and which are not?
----------------------------------------------------------------------------
Notice that you can extend this system to illustrate other concepts easily.
For example, we can illustrate the use of a hypothesis:
Thm: Given o|o|. ,
.|o|o|.
Pf:
1. o|o|. Given
2. . Thm A
3. .|.|o|o|. Rule 2; 2,1
4. .|o Axiom 2
5. .|o|.|. Rule 2; 4,2
6. .|o|o Rule 3; 5
7. .|o|o|.|. Rule 2; 6,2
8. .|o|o|. Rule 1; 7,3
QED
We can also illustrate definitions (which we must state as rules since we
don't have equality or iff).
First we must expand our definition of toy formula to allow another symbol.
Def: A toy formula is either
a. .
b. o
c. ^
d. w|v where w and v are formulas
e. all the formulas are obtained by a-d.
Def: Let w be any formula,
w
----------------------------------------------------
w with any of it's occurrences of .|.|. replaced by ^
and
w
--------------------------------------------------------
w with any of it's occurrences of ^ replaced by .|.|.
These two new rules of inference define ^ as an abbreviation for .|.|. .
Thm: ^|o
Pf:
1. .|.|. Thm B
2. .|.|.|.|.|.|. Rule 2; 1,1
3. .|.|.|o Rule 3; 2
4. ^|o Def of ^; 3
QED
or we can use it in reverse
Thm: .|.|.|o|.|.|o
Pf:
1. ^|o Thm H
2. .|o Axiom 2
3. .|.|.|o Def of ^; 1
4. .|.|.|o|.|.|o Rule 2; 3,2
QED
So we can illustrate hypotheses and definitions. So it really is a toy
logic system.
|
