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 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/z y (B=>A) assumption y/y x (A=>B) assumption x/x 1 B modus ponens z x (zx)/xz 2 A modus ponens y 1 (y(zx))/xyz 3 ((A=>B)=>A) discharge x 2 (\x.(y(zx)))/yz a (((A=>B)=>A)=>A) axiom a/a 4 A modus ponens a 3 (a(\x.(y(zx))))/ayz 5 ((B=>A)=>A) discharge y 4 (\y.(a(\x.(y(zx)))))/az 6 (((A=>B)=>B)=>((B=>A)=>A)) discharge z 5 (\z.(\y.(a(\x.(y(zx))))))/a Here the inference labels are the part of the line before the `/', and the letters following the slash name the axioms and undischarged assumptions used in proving the inference. These letters are also called the `free variables' in the inference label (for reasons described below). Note that inference names and inference labels are different things, though for assumptions and axioms they happen to be equal. Labels and free variables are computed as follows: Axiom. The label of an axiom inference is the name of the inference, a lower case letter. That is also the sole free variable of the label. Assumption. The label of an assumption inference is the name of the inference, a lower case letter. That is also the sole free variable of the label. 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. The free variable set of the label is the union of the free variable set of N1 and the free variable set of 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. The free variable set of the label is the free variable set of N2 with N1 removed (the N1 label is a variable that is `bound' by `\X': see notes below). 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 ----- For each test case, first a line containing just the test case name. Then 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 white- space may be used to separate the name, the logical formula, the reason, and the separate parts of the reason. At the end of the inferences there is a line containing just `.'. There may be many test cases in the input. An end of file terminates the input. No two inferences in a test case 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 test case, first print the test case name line exactly as input. Then for each inference print the exact input line containing the inference followed by one additional line containing the label of the infer- ence indented by 4 spaces, followed by a `/', followed by the free variables in alphabetical order. There must be no space in this line except for the beginning 4 space indent. At the end of the test case, print the line containing just `.' exactly as it was input. 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 and make the free variable set of the inference be empty. This label and its empty free variable set will then propa- gate to the labels and free variable sets 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 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). Sample Input ------ ----- -- SAMPLE 1 -- x A assumption 1 (A=>A) discharge x x . -- SAMPLE 2 -- x (A=>B) assumption y A assumption 1 B modus ponens x y . -- SAMPLE 3 -- x (A=>B) assumption y A assumption 1 B modus ponens x y 2 A modus ponens x 1 3 (A=>B) discharge y 1 4 (A=>A) discharge y 2 5 (B=>(A=>B)) discharge 1 3 6 B modus ponens 3 2 7 B modus ponens 3 y . -- SAMPLE 4 -- x (A=>(B=>C)) assumption y A assumption z B assumption 1 (B=>C) modus ponens x y 2 C modus ponens 1 z 3 (A=>C) discharge y 2 4 (B=>(A=>C)) discharge z 3 5 ((A=>(B=>C))=>(B=>(A=>C))) discharge x 4 . Sample Output ------ ------ -- SAMPLE 1 -- x A assumption x/x 1 (A=>A) discharge x x (\x.x)/ . -- SAMPLE 2 -- x (A=>B) assumption x/x y A assumption y/y 1 B modus ponens x y (xy)/xy . -- SAMPLE 3 -- x (A=>B) assumption x/x y A assumption y/y 1 B modus ponens x y (xy)/xy 2 A modus ponens x 1 $/ 3 (A=>B) discharge y 1 (\y.(xy))/x 4 (A=>A) discharge y 2 (\y.$)/ 5 (B=>(A=>B)) discharge 1 3 $/ 6 B modus ponens 3 2 ((\y.(xy))$)/x 7 B modus ponens 3 y ((\y.(xy))y)/xy . -- SAMPLE 4 -- x (A=>(B=>C)) assumption x/x y A assumption y/y z B assumption z/z 1 (B=>C) modus ponens x y (xy)/xy 2 C modus ponens 1 z ((xy)z)/xyz 3 (A=>C) discharge y 2 (\y.((xy)z))/xz 4 (B=>(A=>C)) discharge z 3 (\z.(\y.((xy)z)))/x 5 ((A=>(B=>C))=>(B=>(A=>C))) discharge x 4 (\x.(\z.(\y.((xy)z))))/ . Notes on Labels ----- -- ------ 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. This is the same as saying that the free variable set of the proof contains only axioms. 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'. Lastly, our notion of `free variables' in a label corresponds exactly to the notion of free variables in a formula of the lambda calculus. 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. Notes on Minimal Propositional Logic ----- -- ------- ------------- ----- The system of propositional logic with just the => logical connective and with Pierce's axiom is equivalent to the standard notion of propositional logic. The negation of A is represented by (A=>F) where F is not constrained by the assumptions and may take the value false. Logical OR of A and B is represented by (A=>F)=>B. Logical AND of A and B is represented by ((A=>(B=>F))=>F), i.e., the negation of the logical OR of the negation of A and the negation of B. If one likes one can introduce F as a constant with the axiom (F=>F1) for any formula F1 (if you can prove that `false is true' you can prove anything and your assump- tions are inconsistent). File: prooflabel.txt Author: Bob Walton Date: Tue Feb 24 04:13:50 EST 2015 The authors have placed this file in the public domain; they make no warranty and accept no liability for this file.