3. Proofs in Propositional Logic

We explain how to code natural deduction style proofs in Tutch, how to check validity of the coded proof and how to submit proofs as homework solutions.

3.1 Propositional Logic I		Proofs of Conjunctions and Implications
3.2 Propositional Logic II		Proofs of Equivalences, Incomplete Proofs
3.3 Propositional Logic III		Proofs of Disjunctions and Negations
3.4 Propositional Logic IV		Classical Proofs
3.5 Requirements and Submission		Submitting your Proofs

3.1 Propositional Logic I

The proof rules for conjunction & and implication => in natural deduction are:

AndI

If A true and B true then A & B true

AndEL

If A & B true then A true

AndER

If A & B true then B true

ImpI

If A true |- B true then A => B true

ImpE

If A => B true and A true then B true

The following Tutch file `prop0.tut' is a proof of the proposition A & (A=>B) => B:

proof mp: A & (A=>B) => B = begin [ A & (A=>B); A; A=>B; B ]; A & (A=>B) => B end;

A proof begins with the keyword `proof', followed by a identifier (here `mp'), a colon `:', then the goal proposition (here `A & (A=>B) => B'), an equal symbol `=' and then the proof, enclosed between `begin' and `end'. The last proposition of the proof must match the goal.

Each entry of the proof is either a single assertion (like the last line) or a frame, enclosed between brackets `[' and `]'. The first proposition of a frame (here `A & (A=>B)') is a hypothesis that can be used to prove the entries of the frame, but not outside the frame. The entries of a frame can be assertions, separated by semicolons `;', or frames again. All entries of a frame are usable only within that frame.

Each entry of a proof must be derivable from previous entries by a single inference step, i.e., by a single proof rule application. In our case `A' and `A=>B' are immediately derivable from the hypothesis `A & (A=>B)' by &-Elimination. `B' is the result of eliminating `A=>B' using `A'.

A frame `[A; ... C]' itself stands for the hypothetical judgment "A true |- C true". Frames can be used in proofs which discharge a hypothesis, like the ImpI-rule. In our example the frame is used to prove the final line `A & (A=>B) => B'.

Scoping: Entries within a frame can only be used within that frame. Once a frame is closed, it can be used as a whole as a hypothetical judgment, but its entries are no longer "visible".

To check this small proof, run tutch prop0. The extension `.tut' is added automatically. The output should look like this:

$ tutch prop0 TUTCH Version ... [Opening file prop0.tut] Proving mp: A & (A => B) => B ... QED [Closing file prop0.tut] $

As in most programming languages, we can supply comments for better understandability or informal explanations. There are two kinds of comments:

1. Multi-line comments are enclosed between `%{' and `}%'.
2. Everything after `%' until the end of the line forms a single line comment.

The following file `prop1.tut' contains the above proof decorated with justifications and a file header, giving name and informal content.

%{ prop1.tut Modus ponens. }% proof mp: A & (A=>B) => B = begin [ A & (A=>B); % 1 Assumption A; % 2 by AndE1 1 A=>B; % 3 by AndE2 1 B ]; % 4 by ImpE 3 2 A & (A=>B) => B % 5 by ImpI 4 end;

3.2 Propositional Logic II

Logical equivalence A <=> B is just defined as implication in both directions, made into a conjunction: A => B & B => A. Thus, to prove an assertion `A <=> B' we have to prove `A => B' and `B => A' in any order. The goal `A <=> B' then follows by AndI. Example: Idempotency of the conjunction.

% prop2.tut % Idempotency of conjunction proof idemAnd : A & A <=> A = begin [ A & A; A ]; A & A => A; A => A & A; A & A <=> A end;

The file `prop2.tut' contains our incomplete proof. Before we finish it, we want to check correctness of this fragment. We run tutch -v prop2:

$ tutch -v prop2 TUTCH Version ... [Opening file prop2.tut] Proving idemAnd: A & A <=> A ... 1 [ A & A; 2 A ]; by AndE1 1 3 A & A => A; by ImpI 2 prop2.tut:9.1-9.11 Error: Unjustified line (A & A |- A); (A & A) => A |- A => (A & A) Assuming this line, checking remainder... 4 A => A & A; UNJUSTIFIED 5 A & A <=> A by AndI 3 4 Proof incomplete [Closing file prop2.tut]

Tutch verifies the first three lines and finds line 4 to be unjustified. It prints out all visible judgments, then a turnstile `|-' and then the unproven assertion `A => (A & A)'. In our case the available judgments are

A & A |- A

This hypothetical judgment is the result of the frame `[A & A; A]' (lines 1-2).

|- (A & A) => A

This non-hypothetical judgment, result of line 3, is printed with out the turnstile. All parenthesis are made explicit.

Now we can continue and add the missing proof of `A => A & A'. We leave this as a simple exercise to the reader.

3.3 Propositional Logic III

The remaining constructs of intuitionistic propositional logic are disjunction |, truth T and falsehood F. These are their proof rules:

OrI1

If A true then A | B true

OrI2

If B true then A | B true

OrE

If A | B true, A true |- C true and B true |- C true then C true

TrueI

T true

FalseE

If F true then C true for any proposition C

We treat negation as an abbreviation: `~A' stands for `A => F'.

In the following we present an example making use of `|'-elimination. We prove `~A|B => A=>B'.

(An aside on the meaning of this proposition: In classical logic the implication `A => B' can be defined as `~A | B'. In intuitionistic logic the disjunction `~A | B' is stronger than the implication `A => B'. This means `(A=>B) => ~A|B' is not provable, only the direction given here:)

% prop3.tut % Classical implication definition ~A|B => A=>B proof impDef : ~A|B => A=>B = begin [ ~A|B; [ A; [ ~A; F; B ]; [ B; B ]; B ]; A=>B ]; ~A|B => A=>B end;

We assume `~A|B' and `A' and have to show `B'. Using OrE on the first hypothesis leaves us to show the validity of the hypothetical judgements `~A |- B' and `B |- B' in our context. While the second is trivial, we proof the first by contradiction after assuming `~A' (recall that `~A' stands for `A=>F').

We obtain the justifications for each proof entry by running tutch -v prop3 (verbose output):

$ tutch -v prop3 TUTCH Version ... [Opening file prop3.tut] Proving impDef: ~A | B => A => B ... 1 [ ~A | B; 2 [ A; 3 [ ~A; 4 F; by ImpE 3 2 5 B ]; by FalseE 4 6 [ B; 7 B ]; by Hyp 6 8 B ]; by OrE 1 5 7 9 A => B ]; by ImpI 8 10 ~A | B => A => B by ImpI 9 QED [Closing file prop3.tut] $

Precedence and associativity of the connectives: `~' binds strongest, then come `&', `|' and `=>' (weakest). All of these three infix operators are right-associative. Thus `A => (B => C)' and `A => B => C' denote the same proposition, but `(A => B) => C' a different. In the same way from `A & B & C' we can infer `A' in one step, but neither `B' nor `C', since we have to prove `B & C' first.

3.4 Propositional Logic IV

In the last sections, we have presented every possibility of proving a proposition, have we? Then what about proof by contradiction, i.e., to prove a proposition `A' we may assume the opposite `~A' and show that there is a contradiction `F'? This principle is intuitionistically not valid, but part of classical logic. Classical reasoning available via the rule `Class'

Class

If ~A true |- F true then A true

To make use of proof by contradiction, we have to declare our proof as `classical'. Now we are able to define the other direction of the classical definition of implication from the last section.

% prop4.tut % Classical implication definition II (A=>B) => ~A|B classical proof classImpDef : (A=>B) => ~A|B = begin [ A => B; [ ~(~A | B); [ ~A; ~A | B; F ]; A; B; ~A | B; F ]; ~A|B ]; (A=>B) => ~A|B end;

To show `~A | B', we assume the opposite and derive a contradiction `F'. To this end, we first derive `A' (again classically), then `B' which lets us infer the contraction.

$ tutch -v prop4.tut TUTCH Version ... [Opening file prop4.tut] Proving classImpDef: (A => B) => ~A | B ... (classically) 1 [ A => B; 2 [ ~(~A | B); 3 [ ~A; 4 ~A | B; by OrIL 3 5 F ]; by ImpE 2 4 6 A; by Class 5 7 B; by ImpE 1 6 8 ~A | B; by OrIR 7 9 F ]; by ImpE 2 8 10 ~A | B ]; by Class 9 11 (A => B) => ~A | B by ImpI 10 QED [Closing file prop4.tut]

Using rule `Class' we can derive the law of excluded middle, which states that `A | ~A' hold for every `A'. The Tutch proof is left to the reader as an exercise. The law of the excluded middle does not hold intutionistically because it violates the disjunction property: Whenever we have a proof of `A | B', we either have a proof of `A' or a proof of `B'. Since, in classical logic, `A | ~A' holds for every formula `A', regardless its meaning, the disjunction property would imply that we either have a proof of `A' or a proof of `~A', without looking at `A'! Again, this would imply that either every formula is true or every formulat is false which is clearly not valid.

3.5 Requirements and Submission

How to complete your homework in five steps:

1. Getting the requirements
2. Completing the proofs
3. Checking against the requirements
4. Submitting
5. Checking status of submission

Let us assume you have to complete assignment `prop'.

3.5.1 Getting the requirements

The requirement files for the homework assignments are stored under /afs/andrew/scs/cs/15-399/req. First copy the requirements file to obtain a template proof file:

$ cp /afs/andrew/scs/cs/15-399/req/prop.req prop.tut

3.5.2 Completing the proofs

Edit file `prop.tut' in your favored editor (we recommend xemacs), fill in the proofs and run Tutch whenever you want to check your accomplishments. You can even check incomplete proofs, as long as the syntax is correct and there are no open frames.

3.5.3 Checking against the requirements

To check whether you fulfilled the requirements run Tutch with option `-r'. After this option you specify the requirements file. If your proof file has the same name as the requirements file (except extension), you can save some keystrokes. You will see an output like this:

$ tutch -r prop.req prop.tut TUTCH Version ... [Opening requirements file /afs/andrew/scs/cs/15-399/req/prop.req] [Closing requirements file /afs/andrew/scs/cs/15-399/req/prop.req] [Opening file prop.tut] Proving mp: A & (A => B) => B ... QED Proving impDef: ~A | B => A => B ... QED [Closing file prop.tut] Checking requirements... [X] proof mp: A & (A => B) => B [X] proof impDef: ~A | B => A => B Congratulations! All problems solved! $

A short version of that command is `tutch -r prop'. You can also distribute your proofs over several files. To check the two files `prop1.tut' and `prop2.tut' against `prop.req', type

$ tutch -r prop prop1 prop2

3.5.4 Submitting

You do not get credits for your homework unless you submit. You must be registered student of course and have access to the Andrew File System (afs). To submit you type:

$ submit -r prop SUBMIT Version ... ... [Submitting files: prop.tut ] [Submission OK] $

This submits file `prop.tut' for homework `prop.req'. To submit several files, e.g., type

$ submit -r prop prop1 prop2

3.5.5 Checking status of submission

With the `status' command you can check the status of your submission, e.g.,

$ status prop STATUS Version ... Getting status of submission prop... Submitted files: prop.tut Assignment: prop Student ID: foo Date: today [X] proof mp: A & (A => B) => B [X] proof impDef: ~A | B => A => B $