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.