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.
The proof rules for conjunction & and implication => in natural deduction are:
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:
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;
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
Now we can continue and add the missing proof of `A => A & A'. We leave this as a simple exercise to the reader.
The remaining constructs of intuitionistic propositional logic are disjunction |, truth T and falsehood F. These are their proof rules:
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 classImpDef : ~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 prop2 (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 prop2.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.
How to complete your homework in five steps:
Let us assume you have to complete assignment `prop'.
The requirement files for the homework assignments are stored under /afs/andrew/course/80/317/req. First copy the requirements file to obtain a template proof file:
$ cp /afs/andrew/course/80/317/req/prop.req prop.tut
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.
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/course/80/317/req/prop.req] [Closing requirements file /afs/andrew/course/80/317/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
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
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 $
Go to the first, previous, next, last section, table of contents.