What you need to know for test 1

• The definitions in class: theorem, sentence, sound, complete, metatheorem, in fact anything that I labelled "definition".
• Know how to write up a complete "full-dress" proof. It is likely that you will be asked to fill in the brackets a la Q2 Assignment 1.
• Know all the inference rules, and derived inference rules (Derived Leibniz, and simultaneous substitution), and of course how to use them.

A list of theorems and axioms will be given to you, and in any proof it will say what level of detail is expected, and which theorems you can use (at any time you can use any axiom). Therefore, read the instructions carefully, as failure to follow them will result in large loss of marks.

• Know how to prove a metatheorem (we did two in class). typically the proof style goes as follows:

we normally start being given a theorem or two (recall 3.7 "If |-P, |-Q..."). Your first step is to say "Assume P and Q are theorems ...".

The second step is to look for a theorem or axiom that looks similar to what we want and (Simultaneously) Substitute in (say) p:=P, q:=Q. This gives us a theorem in P and Q.

The third step is to insert true, or replace P or Q by true (which we can do by Metatheorems Redundant True, 3.7 respectively) if needs be.

To help you spot key theorems, note that in the proof of redundant true, and the proof of 3.7 the key theorem was 3.3 in both cases.

Remember: we can also use inference rules at any stage.

ANYONE caught cheating will automatically get 0 on the test.