Proof Labeling -------------- The following is an example of a proof in a limited logic language with just the implication operator => and propositional variables denoted by single upper case letters. z ((A=>B)=>B) assumption y (B=>A) assumption x (A=>B) assumption 1 B modus ponens z x 2 A modus ponens y 1 3 ((A=>B)=>A) discharge x 2 a (((A=>B)=>A)=>A) axiom 4 A modus ponens a 3 5 ((B=>A)=>A) discharge y 4 6 (((A=>B)=>B)=>((B=>A)=>A)) discharge z 5 Here each line is an inference. Inferences are named by lower case letters or integers. After the name comes the logical formula. After that, the reason the formula is a valid inference (e.g., `axiom' or `discharge z 5'). Assumptions and axioms are named by lower case letters, while other inferences are named by integers. Different inferences have distinct names. A logical formula is either an atom, denoted by a single upper case letter, or an implication, which has the form (F1=>F2), where F1 and F2 are any logical formulae. There are four kinds of inferences. Axioms. These are just named with a lower case letter. The only axiom needed by our limited logic language is Pierce's axiom, which is any formula of the form (((F1=>F2)=>F1)=>F1). (F1=>F2) is used as a stand-in for `not F1', since negation is not in our limited language, so Pierce's axiom just says that if you can prove F1 from `not F1', then F1 is true. Assumptions. These are named by a lower case letter. They must be discharged. Avoiding the use of undischarged assumptions in a proof is a subtle point that will be elaborated on in the notes below. Modus Ponens. This is the rule of logic that says given (F1=>F2) and F1 you can infer F2. A modus ponens infer- ence is named by an integer. Let F2 be the logical formula of the inference. Then the reason of the infer- ence must have the form `modus ponens N1 N2' where N1 names a previous inference whose logical formula has the form (F1=>F2) for some logical formula F1, and N2 names a previous inference whose logical formula is F1. Discharge. This is how you discharge assumptions. A discharge inference has an integer name and a logical formula of the form (F1=>F2). Its reason has the form `discharge N1 N2' where N1 names a previous inference that is an assumption with logical formula F1, and N2 names a previous inference with logical formula F2. Inferences in a proof can be given labels that completely describe how the inference was arrived at. When labels are added on a line after each inference in the above example, the example looks like this: z ((A=>B)=>B) assumption z y (B=>A) assumption y x (A=>B) assumption x 1 B modus ponens z x (zx) 2 A modus ponens y 1 (y(zx)) 3 ((A=>B)=>A) discharge x 2 (\x.(y(zx))) a (((A=>B)=>A)=>A) axiom a 4 A modus ponens a 3 (a(\x.(y(zx)))) 5 ((B=>A)=>A) discharge y 4 (\y.(a(\x.(y(zx))))) 6 (((A=>B)=>B)=>((B=>A)=>A)) discharge z 5 (\z.(\y.(a(\x.(y(zx)))))) Note that inference names and inference labels are different things, though for assumptions and axioms they happen to be equal. Labels are computed as follows: Axiom. The label of an axiom inference is the name of the inference, a lower case letter. Assumption. The label of an assumption inference is the name of the inference, a lower case letter. Modus Ponens. The label of a `modus ponens N1 N2' inference is (XY) where X is the label of inference N1 and Y is the label of inference N2. Discharge. The label of a `discharge N1 N2' inference is (\X.Y) where X is the label of the inference N1, and is always a lower case letter, as N1 is an assumption, while Y is the label of the inference N2. We have told you everything you need to know to do this problem, but there is more interesting stuff in the notes at the end. Input ----- A sequence of inferences, one per line, without any labels. Each inference consists of a name, a logical formula, and a reason. There are no spaces inside the logical formula. Any amount of whitespace may be used to separate the name, the logical formula, the reason, and the separate parts of the reason. An end of file terminates the input. No two inferences have the same name. Names are all lower case letters or integers in the range from 1 through 1000. No inference line is longer than 80 characters. Output ------ For each inference print the exact input line containing the inference followed by one additional line containing the label of the inference indented by 4 spaces. The label must not contain spaces. However, you must perform checks on modus ponens and discharge inferences. If the checks do not pass, you must output `$' as the label of the inference. This label may then propagate into the labels of other inferences that use the inference which did not check. The check for a `modus ponens N1 N2' inference with logical formula F2 is that inference N1 has a logical formula of the form (F1=>F2) and inference N2 has the logical formula F1. The check for a `discharge N1 N2' inference is that it has a logical formula of the form (F1=>F2), inference N1 is an assumption (check this) with logical formula F1, and inference N2 has logical formula F2. The input data will be such that no label will be longer than 76 characters (so no output line will be longer than 80 characters). The N1 and N2 above will always name previous inferences (though not necessarily those that will pass the checks for formula or reason). Example Input ------- ----- z ((A=>B)=>C) assumption y ((B=>A)=>C) assumption x (C=>B) assumption w (B=>A) assumption 1 C modus ponens y w 2 B modus ponens x 1 3 ((B=>A)=>B) discharge w 2 a (((B=>A)=>B)=>B) axiom 4 B modus ponens a 3 v A assumption 5 (A=>B) discharge v 4 6 C modus ponens z 5 7 ((C=>B)=>C) discharge x 6 b (((C=>B)=>C)=>C) axiom 8 C modus ponens b 7 9 (((B=>A)=>C)=>C) discharge y 8 10 (((A=>B)=>C)=>(((B=>A)=>C)=>C)) discharge z 9 11 (A=>A) discharge v v 12 C modus ponens v 11 13 B modus ponens x 12 14 (A=>B) discharge v 13 15 ((((B=>A)=>B)=>B)=>B) discharge a 13 Example Output ------- ------ z ((A=>B)=>C) assumption z y ((B=>A)=>C) assumption y x (C=>B) assumption x w (B=>A) assumption w 1 C modus ponens y w (yw) 2 B modus ponens x 1 (x(yw)) 3 ((B=>A)=>B) discharge w 2 (\w.(x(yw))) a (((B=>A)=>B)=>B) axiom a 4 B modus ponens a 3 (a(\w.(x(yw)))) v A assumption v 5 (A=>B) discharge v 4 (\v.(a(\w.(x(yw))))) 6 C modus ponens z 5 (z(\v.(a(\w.(x(yw)))))) 7 ((C=>B)=>C) discharge x 6 (\x.(z(\v.(a(\w.(x(yw))))))) b (((C=>B)=>C)=>C) axiom b 8 C modus ponens b 7 (b(\x.(z(\v.(a(\w.(x(yw)))))))) 9 (((B=>A)=>C)=>C) discharge y 8 (\y.(b(\x.(z(\v.(a(\w.(x(yw))))))))) 10 (((A=>B)=>C)=>(((B=>A)=>C)=>C)) discharge z 9 (\z.(\y.(b(\x.(z(\v.(a(\w.(x(yw)))))))))) 11 (A=>A) discharge v v (\v.v) 12 C modus ponens v 11 $ 13 B modus ponens x 12 (x$) 14 (A=>B) discharge v 13 (\v.(x$)) 15 ((((B=>A)=>B)=>B)=>B) discharge a 13 $ Notes ----- An assumption name X is discharged in a label if it only occurs inside subexpressions of the label that have the form (\X...). That is, the \X discharges all X's in the subexpression it begins. Thus z is discharged in (a(\z.(xz))) but is not discharged in (z(\z.(xz))) as in the latter the first z is outside any (\z...) In a valid proof of a theorem, all assumptions must be discharged. Notice we did NOT ask you to check this. It is possible to prove the following: If a formula F has a proof with label ((\X.Y)Z) then it has a proof with label Y[X=Z], which denotes the label Y with all undischarged X's in it replaced by Z, provided that Z has no undischarged assumption names that become discharged when Z is inserted into Y. Thus the label of a proof can be `reduced' by the `reduction rule' ((\X.Y)Z) --> Y[X=Z]. Inference labels as we have introduced them have exactly the same syntax as formula's in lambda calculus, where we have used the backslash \ in place of the Greek letter `lambda'. Furthermore, the reduction rule we have just introduced for inference labels is exactly the main reduction rule for the lambda calculus, beta reduc- tion, and our word `discharged' corresponds exactly to the lambda calculus word `bound'. It can also be shown that the other reduction rules for the lambda calculus, alpha reduction and eta reduction, are valid for inference labels. Thus there is an exact 1-1 correspondence between inference labels and lambda calculus. This is called the Curry-Howard Isomorphism. It further turns out that the relation between the logical formula of an inference and the label of the inference is exactly the same as the relation between the type of a lambda calculus formula and the formula. Thus logical formula can be read as the types of the labels of their proofs. File: prooflabel.txt Author: Bob Walton Date: Tue Oct 18 11:33:00 EDT 2005 The authors have placed this file in the public domain; they make no warranty and accept no liability for this file. RCS Info (may not be true date or author): $Author: walton $ $Date: 2005/10/18 15:38:43 $ $RCSfile: prooflabel.txt,v $ $Revision: 1.7 $