Proof Logic |
Jacques Bailhache (jacques.bailhache@gmail.com) February 2021 |
Proof Logic is a functional formalism, like Combinatory Logic and lambda Calculus. As in Combinatory Logic and Lambda Calculus, the application of a function f to an argument a is denoted f a, and (f a) b may be written more simply f a b which means : first apply f to a, and then apply the resulting function to b. But if we want to apply a function f to an argument a, and then apply another function g to the result, we must write it g (f a). It may also be written g : f a. The ":" is like a "(" with an implicit corresponding ")".
It uses De Bruijn index to represent variables. A function with one variable is represented by an expression of the form [ ... * ... * ... ] where * represents the variable (which may appear with 0, 1, or several occurences). For example, a function applying its argument to itself is written [ * * ] and when we apply it to an argument a we have the equality [ * * ] a = a a. A function with two variables is represented by a function with one variable giving, when applyed to a first argument, another function with one variable giving, when applied to the second argument, the final result. Such a function is written [[ ... '* ... * ... ]] where '* will be replaced by the first argument and * will be replaced by the second argument. So * corresponds to 1 in De Bruijn's index, '* to 2 , ''* to 3, and so on.
At this point, the formalism is equivalent to Lambda Calculus or Combinatory Logic. We will now extend it.
First, we will add symbols. A symbol, which is a member of a set of symbols, which can be chosen either as finite, but as big as needed, or infinite but countable. A symbol is represented by a sequence of letter, digits, and eventually some special characters like "_" which are not used for anything else.
We have seen that Proof Logic expressions represent proofs. The simplest proofs of a formal system are the axioms of the system. Since sentences of Proof Logic are equalities, an axiom has the form a = b. So the Proof Logic expression (or the proof) a = b represents the axioms asserting the equality between a and b. Of course, the operator "=" may be used only in axioms, otherwise we could prove anything !
Any Proof Logic expression may be seen as a proof which proves the truth of a sentence (the conclusion of the proof) which is an equality between two terms, which are also Proof Logic expressions. Given any Proof Logic expression x, we can determine which equality it proves. More precisely, there are two computable functions called "left" and "right", computing the terms of the equality proved by the given proof : x proves left(x) = right(x). For example, we have left(a = b) = a and right(a = b) = b, so a = b proves left(a = b) = right(a = b) or a = b proves a = b.
In theories based on equality, there are often 3 axioms representing the properties of equality : reflexivity (a = a), symmetry (a = b => b = a) and transitivity (a = b & b = c => a = c). In Proof Logic, a reflexivity axiom is useless because, as we have seen, any term a is also the proof of the sentence "a = a". Transitivity is generalized : if there is one common term in two equalities, the two other terms are equal.
If x proves a = b, we might want the conclusion in reduced form c = d where a reduces to c and b reduces to d. We can do this with the proof "c ; a = b ; d" but we must explicitely indicate c and d. To simplify the writing of proof, the operator "$" is introduced : if x proves a = b, then $x proves c = d, where a reduces to c and b reduces to d.
We also may want to display some intermediate result. To do this, we introduce the operator ? x y whose value is y but when we calculate the left part of its conclusion, it displays "Left of x is : " followed by this left part, and the same for the right part. This operator will be used to implement the notation % name definition proof that we will see later.
It is also useful to have an operator doing one step of reduction, to be able to prove that red1(a) = a, where red1 does one step of reduction, or more generally, if a = b then red1(a) = b. This operator is written "/". If x proves a = b, then /x proves red1(a) = b. We can also introduce the symmetrical operator "\" : if x proves a = b, then \x proves a = red1(b).
A last useful operator is the reduction operator written "@" which reduces its argument. We will see later that it is useful principally to implement a notation for definitions.
In summary, a proof may be :
We also need a notation to write a definition, to give a name to a proof and then use this name in other proofs instead of writing its full definition each time we need to use it. We can give globally a name to a proof with the notation "& name proof".
Another possibility is to give temporarily a name to a proof inside another proof. This is written ! name definition proof which means "replace name by definition in proof". It is similar to "let name = definition in proof" in Haskell. This notation is translated into @(^name proof definition).
Without definitions, the reduction operator "@" would not be necessary.
It may also be useful to display intermediate results. The notation "% name definition proof" is the same as "! name definition proof" but it also displays the left and right sides of the conclusion of the definition. It is translated into @(^name proof ? name definition).
We saw that in Proof Logic, all sentences are equality. But how can we represent a sentence that is not an equality ? A possible convention is to represent the truth of a sentence by the equality with a given term, for example the identity [*]. With this convention, the implication can be represented by application, and we get automatically the Modus Ponens rule : if p q = [*] and p = [*] then q = [*].
Here is an example of a formal system with one rule saying that if x is parent of y and y is parent of z, then x is grand parent of z, and two axioms saying that Allan is parent of Brenda and Brenda is parent of Charles :
& gpRule1 ^x ^y ^z ((parent x y : parent y z : grandparent x z) = [*]). & gpAxiom1 ((parent allan brenda) = [*]). & gpAxiom2 ((parent brenda charles) = [*]). $(gpAxiom1 (gpAxiom2 (grandparent allan charles)) ; gpRule1 allan brenda charles).Running the Proof Logic program with this proof gives the following result :
$ ./pl-v9 grandparent-np.prf & gpRule1 ^x ^y ^z ((parent x y : parent y z : grandparent x z) = [*]). The proof : gpRule1 proves : [[[parent ''* '* (parent '* * (grandparent ''* *))]]] equals : [[[[*]]]] & gpAxiom1 ((parent allan brenda) = [*]). The proof : gpAxiom1 proves : parent allan brenda equals : [*] & gpAxiom2 ((parent brenda charles) = [*]). The proof : gpAxiom2 proves : parent brenda charles equals : [*] & gpTheorem1 $( grandparent allan charles ; gpAxiom2 (grandparent allan charles) ; gpAxiom1 (parent brenda charles (grandparent allan charles)) ; gpRule1 allan brenda charles ). The proof : gpTheorem1 proves : grandparent allan charles equals : [*]Here is another version using local definitions with "!" :
! gpRule1 ^x ^y ^z ((parent x y : parent y z : grandparent x z) = [*]) ! gpAxiom1 ((parent allan brenda) = [*]) ! gpAxiom2 ((parent brenda charles) = [*]) ! gpTheorem1 ( grandparent allan charles ; gpAxiom2 (grandparent allan charles) ; gpAxiom1 (parent brenda charles (grandparent allan charles)) ; gpRule1 allan brenda charles ) gpTheorem1Running the Proof Logic program with this proof gives the following result :
$ ./pl-v9 grandparent-new.prf ! gpRule1 ^x ^y ^z ((parent x y : parent y z : grandparent x z) = [*]) ! gpAxiom1 ((parent allan brenda) = [*]) ! gpAxiom2 ((parent brenda charles) = [*]) ! gpTheorem1 ( grandparent allan charles ; gpAxiom2 (grandparent allan charles) ; gpAxiom1 (parent brenda charles (grandparent allan charles)) ; gpRule1 allan brenda charles ) gpTheorem1 The proof : @([@([@([@([*] ( ( ( grandparent allan charles ; * (grandparent allan charles) ) ; '* (parent brenda charles (grandparent allan charles)) ) ; ''* allan brenda charles ))] (parent brenda charles = [*]))] (parent allan brenda = [*]))] [[[parent ''* '* (parent '* * (grandparent ''* *)) = [*]]]]) proves : grandparent allan charles equals : [*]Here is a proof file proving the Combinatory Logic equality "S K K = I" :
& I ^a a. & K ^a ^b a. & S ^a ^b ^c (a c (b c)). S K K ; I.The conclusion of this proof is "S K K = I" :
$ ./pl-v9 skk-v9.prf & I ^a a. The proof : I proves : I equals : I & K ^a ^b a. The proof : K proves : K equals : K & S ^a ^b ^c (a c (b c)). The proof : S proves : S equals : S S K K ; I. The proof : S K K ; I proves : S K K equals : IHere is another version with local names :
! DI (I = ^a a) ! DK (K = ^a ^b a) ! DS (S = ^a ^b ^c (a c (b c))) ( DS DK DK ; DI )The conclusion of this proof is "S K K = I" :
$ ./pl-v9 skk-new.prf ! DI (I = ^a a) ! DK (K = ^a ^b a) ! DS (S = ^a ^b ^c (a c (b c))) ( DS DK DK ; DI ) The proof : @([@([@([* '* '* ; ''*] (S = [[[''* * ('* *)]]]))] (K = [['*]]))] (I = [*])) proves : S K K equals : IHere is a proof of p => p in propositional logic :
# Proof of p => p # Axioms & MP ^p ^q ((imp p q) (p q) = [*]). & AK ^p ^q (imp p (imp q p) = [*]. & AS ^p ^q ^r (imp (imp p (imp q r)) (imp (imp p q) (imp p r)) = [*]). # Proof & lemma1 $ (AS p (imp p p) p). & lemma2 $ (AK p (imp p p)). & lemma3 $ (MP (imp p (imp (imp p p) p)) (imp (imp p (imp p p)) (imp p p))). & lemma4 $ ( lemma1 ( (imp p (imp (imp p p) p)) (imp (imp p (imp p p)) (imp p p)) ) ). & lemma5 $ ( lemma4 ; lemma3 ). & lemma6 $ ( lemma2 (imp (imp p (imp p p)) (imp p p) ) ). & lemma7 $ ( lemma6 ; lemma5 ). & lemma8 $ (AK p p). & lemma9 $ (MP (imp p (imp p p)) (imp p p) ). & lemma10 $ (lemma7 ((imp p (imp p p)) (imp p p))). & lemma11 $ ( lemma10 ; lemma9 ). & lemma12 $ (lemma8 (imp p p)). & theorem1 $ ( imp p p ; lemma12 ; lemma11 ). theorem1.We can see that it effectively proves "p => p" (which is written "imp p p") :
$ ./pl-v9 prop-v9.prf # Proof of p => p # Axioms & MP ^p ^q ((imp p q) (p q) = [*]). The proof : MP proves : [[imp '* * ('* *)]] equals : [[[*]]] & AK ^p ^q (imp p (imp q p) = [*]. The proof : AK proves : [[imp '* (imp * '*)]] equals : [[[*]]] & AS ^p ^q ^r (imp (imp p (imp q r)) (imp (imp p q) (imp p r)) = [*]). The proof : AS proves : [[[imp (imp ''* (imp '* *)) (imp (imp ''* '*) (imp ''* *))]]] equals : [[[[*]]]] # Proof & lemma1 $ (AS p (imp p p) p). The proof : lemma1 proves : imp (imp p (imp (imp p p) p)) (imp (imp p (imp p p)) (imp p p)) equals : [*] & lemma2 $ (AK p (imp p p)). The proof : lemma2 proves : imp p (imp (imp p p) p) equals : [*] & lemma3 $ (MP (imp p (imp (imp p p) p)) (imp (imp p (imp p p)) (imp p p))). The proof : lemma3 proves : imp (imp p (imp (imp p p) p)) (imp (imp p (imp p p)) (imp p p)) (imp p (imp (imp p p) p) (imp (imp p (imp p p)) (imp p p))) equals : [*] & lemma4 $ ( lemma1 ( (imp p (imp (imp p p) p)) (imp (imp p (imp p p)) (imp p p)) ) ). The proof : lemma4 proves : imp (imp p (imp (imp p p) p)) (imp (imp p (imp p p)) (imp p p)) (imp p (imp (imp p p) p) (imp (imp p (imp p p)) (imp p p))) equals : imp p (imp (imp p p) p) (imp (imp p (imp p p)) (imp p p)) & lemma5 $ ( lemma4 ; lemma3 ). The proof : lemma5 proves : imp p (imp (imp p p) p) (imp (imp p (imp p p)) (imp p p)) equals : [*] & lemma6 $ ( lemma2 (imp (imp p (imp p p)) (imp p p) ) ). The proof : lemma6 proves : imp p (imp (imp p p) p) (imp (imp p (imp p p)) (imp p p)) equals : imp (imp p (imp p p)) (imp p p) & lemma7 $ ( lemma6 ; lemma5 ). The proof : lemma7 proves : imp (imp p (imp p p)) (imp p p) equals : [*] & lemma8 $ (AK p p). The proof : lemma8 proves : imp p (imp p p) equals : [*] & lemma9 $ (MP (imp p (imp p p)) (imp p p) ). The proof : lemma9 proves : imp (imp p (imp p p)) (imp p p) (imp p (imp p p) (imp p p)) equals : [*] & lemma10 $ (lemma7 ((imp p (imp p p)) (imp p p))). The proof : lemma10 proves : imp (imp p (imp p p)) (imp p p) (imp p (imp p p) (imp p p)) equals : imp p (imp p p) (imp p p) & lemma11 $ ( lemma10 ; lemma9 ). The proof : lemma11 proves : imp p (imp p p) (imp p p) equals : [*] & lemma12 $ (lemma8 (imp p p)). The proof : lemma12 proves : imp p (imp p p) (imp p p) equals : imp p p & theorem1 $ ( imp p p ; lemma12 ; lemma11 ). The proof : theorem1 proves : imp p p equals : [*] theorem1. The proof : theorem1 proves : imp p p equals : [*]Proof Logic is a powerful logical framework derived from Combinatory Logic and Lambda Calculus, which inherits from these theories some powerful features like fixed point. This means that we must be careful to avoid defining inconsistent axioms. For example, the fixed point combinator allows to define a term c such that c = (imp c false). If we do not take precautions to avoid that such a term may be considered as a proposition, it produces a contradiction, as shown by the following proof :
# Logical axioms & MP ^p ^q (imp p q (p q) = [*]). # Modus ponens & AI ^p (imp p p = [*]). & AK ^p ^q (imp p (imp q p) = [*]). & AS ^p ^q ^r (imp (imp p (imp q r)) (imp (imp p q) (imp p r)) = [*]). & Y [[* *] ['* (* *)]]. # Fixed point & defc (c = Y [imp * false]). & Ac @ ( \\\defc ; imp \defc false ). # c = (c => false). # Proof of false # This is a Proof Logic version of the following natural deduction proof : # 1 | c (hypothesis). # |--------------- # 2 | c => false (from 1 because c = (c => false)). # 3 | false (MP 2 1). # 4 c => false (hypothesis 1 3). # 5 c (from 4 because c = (c => false)). # 6 false (MP 4 5). & L1 $ (AI c). & L2 $ (imp c Ac). & L3 $ ( L2 ; L1 ). & L4 $ (AS c c false). & L5 $ (MP (imp c (imp c false)) (imp (imp c c) (imp c false))). & L6 $ (L4 ((imp c (imp c false)) (imp (imp c c) (imp c false)))). & L7 $ ( L6 ; L5 ). & L8 $ (L3 (imp (imp c c) (imp c false))). & L9 $ ( L8 ; L7 ). & L10 $ (MP (imp c c) (imp c false)). & L11 $ (L9 ((imp c c) (imp c false))). & L12 $ ( L11 ; L10 ). & L13 $ (L1 (imp c false)). & L14 $ ( L13 ; L12 ). & L15 $ ( Ac ; c ). & L16 $ ( L15 ; L14 ). & L17 $ (MP c false). & L18 $ (L14 (c false)). & L19 $ ( L18 ; L17 ). & L20 $ (L16 false). & L21 $ ( L20 ; L19 ). & T $ ( false ; L21 ). # false = [*]If we run the Proof Logic programw with this proof, we see that it proves that false = [*], or that false is true !
$ ./pl-v9 contrad-v9.prf # Logical axioms & MP ^p ^q (imp p q (p q) = [*]). The proof : MP proves : [[imp '* * ('* *)]] equals : [[[*]]] # Modus ponens & AI ^p (imp p p = [*]). The proof : AI proves : [imp * *] equals : [[*]] & AK ^p ^q (imp p (imp q p) = [*]). The proof : AK proves : [[imp '* (imp * '*)]] equals : [[[*]]] & AS ^p ^q ^r (imp (imp p (imp q r)) (imp (imp p q) (imp p r)) = [*]). The proof : AS proves : [[[imp (imp ''* (imp '* *)) (imp (imp ''* '*) (imp ''* *))]]] equals : [[[[*]]]] & Y [[* *] ['* (* *)]]. The proof : Y proves : Y equals : Y # Fixed point & defc (c = Y [imp * false]). The proof : defc proves : c equals : Y [imp * false] & Ac @ ( \\\defc ; imp \defc false ). The proof : Ac proves : c equals : imp c false # c = (c => false). # Proof of false # This is a Proof Logic version of the following natural deduction proof : # 1 | c (hypothesis). # |--------------- # 2 | c => false (from 1 because c = (c => false)). # 3 | false (MP 2 1). # 4 c => false (hypothesis 1 3). # 5 c (from 4 because c = (c => false)). # 6 false (MP 4 5). & L1 $ (AI c). The proof : L1 proves : imp c c equals : [*] & L2 $ (imp c Ac). The proof : L2 proves : imp c c equals : imp c (imp c false) & L3 $ ( L2 ; L1 ). The proof : L3 proves : imp c (imp c false) equals : [*] & L4 $ (AS c c false). The proof : L4 proves : imp (imp c (imp c false)) (imp (imp c c) (imp c false)) equals : [*] & L5 $ (MP (imp c (imp c false)) (imp (imp c c) (imp c false))). The proof : L5 proves : imp (imp c (imp c false)) (imp (imp c c) (imp c false)) (imp c (imp c false) (imp (imp c c) (imp c false))) equals : [*] & L6 $ (L4 ((imp c (imp c false)) (imp (imp c c) (imp c false)))). The proof : L6 proves : imp (imp c (imp c false)) (imp (imp c c) (imp c false)) (imp c (imp c false) (imp (imp c c) (imp c false))) equals : imp c (imp c false) (imp (imp c c) (imp c false)) & L7 $ ( L6 ; L5 ). The proof : L7 proves : imp c (imp c false) (imp (imp c c) (imp c false)) equals : [*] & L8 $ (L3 (imp (imp c c) (imp c false))). The proof : L8 proves : imp c (imp c false) (imp (imp c c) (imp c false)) equals : imp (imp c c) (imp c false) & L9 $ ( L8 ; L7 ). The proof : L9 proves : imp (imp c c) (imp c false) equals : [*] & L10 $ (MP (imp c c) (imp c false)). The proof : L10 proves : imp (imp c c) (imp c false) (imp c c (imp c false)) equals : [*] & L11 $ (L9 ((imp c c) (imp c false))). The proof : L11 proves : imp (imp c c) (imp c false) (imp c c (imp c false)) equals : imp c c (imp c false) & L12 $ ( L11 ; L10 ). The proof : L12 proves : imp c c (imp c false) equals : [*] & L13 $ (L1 (imp c false)). The proof : L13 proves : imp c c (imp c false) equals : imp c false & L14 $ ( L13 ; L12 ). The proof : L14 proves : imp c false equals : [*] & L15 $ ( Ac ; c ). The proof : L15 proves : imp c false equals : c & L16 $ ( L15 ; L14 ). The proof : L16 proves : c equals : [*] & L17 $ (MP c false). The proof : L17 proves : imp c false (c false) equals : [*] & L18 $ (L14 (c false)). The proof : L18 proves : imp c false (c false) equals : c false & L19 $ ( L18 ; L17 ). The proof : L19 proves : c false equals : [*] & L20 $ (L16 false). The proof : L20 proves : c false equals : false & L21 $ ( L20 ; L19 ). The proof : L21 proves : false equals : [*] & T $ ( false ; L21 ). The proof : T proves : false equals : [*] # false = [*]To avoid this, it is necessary either to define a condition for a term to be a proposition to avoid considering c = (imp c false) as a proposition, or to use a weakened logic permetting to have propositions verifying c = (imp c false) without producing a contradiction.
Historically, Proof Logic comes from SSLC (Simplified Symbolic Lambda Calculus), with a new notation introduced, the "AXM" proof replaced by "a = b", and DB0, DBS and DBL respectively replaced by VAR, NXV and FNC in Haskell representation. SSLC itself comes from Schönfinkel and Curry's Combinatory Logic and Church's Lambda Calculus throught this history.
Here is a C implementation of Proof Logic and here is an older Haskell implementation.