In Case You Were Still Awake

Here is a step by step walk through of a linear formal proof that I wrote out for my class. Enjoy.

the first column is the label of the sequent (set of premises)
the second column is the line number
the third column is the formula
the forth column is the action we applied to the formula

Just for fun(not really) I will step through each line of of the linear proof
We are proving "(P OR Q) AND R is syntactically equivalent to (P AND R) OR (Q AND R) "

We first have to prove the following sequent: "(P OR Q) AND R --> (P AND R) OR (Q AND R) "

We start with three labeled assumptions:
1-(P OR Q) AND R,
4-P
7-Q

The first line is 1 (1) (P OR Q) AND R ass, assuming that the formula is true

The second line is 1 (2) R 1 AND-elim2, this takes the 1st line and performs the AND-elim2 rule on it to get R (see the bottom of page 128). AND-elim2 returns the right side of a conjunction. (the first column is always listing the labels that we are working with)

The third line is 1 (3) P OR Q AND-elim1, this takes the 1st line and performs the AND-elim1 rule on it to get P OR Q (see the bottom of page 128). AND-elim1 returns the left side of a conjunction.

The fourth line is 4 (4) P ass, assuming that P is true

The fifth line is 1,4 (5) P AND R 4,2 AND-int, this takes lines 2 and 4, and performs the AND-int rule on it to get P and R (see the top of 129). AND-int returns the conjunction of what follows from the union of two premises.

the sixth line is 1,4 (6) (P AND R) OR (Q AND R) 5 OR-int1, this takes line 5 and performs the OR-int1 rule on it to get (P AND R) OR (Q AND R) (see the middle of page 129). OR-int1 returns the disjunction of A and B, given A.

the seventh line is 7 (7) Q ass, assuming that Q is true

the eighth line is 1,7 (8) Q AND R 7,2 AND-int (same as line 5), this takes line seven and two and performs the AND-int rule on it to get Q AND R.

the ninth line is 1,7 (9) (P AND R) OR (Q AND R) 8 OR-int2, this takes line 8 and performs the OR-int2 rule on it to get (P AND R) OR (Q AND R) (refer to line 6). OR-int2 returns the disjunction of A and B, given B

the tenth line is 1 (10) (P AND R) OR (Q AND R) 3,6,9 OR-elim, this takes lines 3, 6, and 9, and performs the OR-elim rule on it to get (P AND R) OR (Q AND R) (refer to the top pg 129 and the bottom of page 137-138). OR-elim returns what follows from the premises LAMBDA, DELTA, and EPSILON when the disjunction of A and B is the result from the premises of LAMBDA, C follows from the premises DELTA and A, and C follows from EPSILON and B, are all given as input.

The purpose of line 10 is to show that (P AND R) OR (Q AND R) is a valid formula for the right hand side of the sequent. It has to build off the three assumptions we started with, but we have to get the three assumptions to a usable form first (lines 3,6, and 9).