Proof Logic

Jacques Bailhache (jacques.bailhache@gmail.com) February 2021

Proof Logic is a formalism for representing proofs in formal systems. A proof is an expression that proves the truth of a sentence in a given formal system, which is a formalization of a theory. In Proof Logic, a sentence is an equality between two terms. Proof Logic expressions are both terms and proofs. This does not mean that some Proof Logic expression are terms and other are proofs, but that ANY Proof Logic expression is BOTH a term and a proof. A term x is identified with the proof of the sentence x = x. Proof Logic expressions are called "proofs".

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.

a = b & a = c => b = c
a = b & b = c => a = c
a = b & c = a => b = c
a = b & c = b => a = c

We must also be able to prove the equality between an expression and its reduced form, for example [* *] a = a a. We could introduce a special operator for this, but we will rather modify the transitivity, saying, for example, that if a = b, and c = d, and a reduces to e, and c reduces to e, then b = d. This operator will be called "generalized transitivity with reduction". It is written x ; y. For example, if x proves a = b, and y proves c = d, and a reduces to e, and c reduces to e, then x ; y proves b = 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 :

A symbol
* (the variable)
'x where x is a proof
[x] where x is a proof
@x where x is a proof
/x where x is a proof
\x where x is a proof
x y (application) where x and y are proofs
x ; y where x and y are proofs
x=y (axiom) where x and y are proofs
? x y where x and y are proofs

The left and right terms of the conclusion of a proof are defined as follows :

If x is a symbol or the variable "*", then left(x) = x and right(x) = x, which means that x proves x = x.
left('x) = 'left(x) ; right('x) = 'right(x)
left([x]) = [left(x)] ; right([x]) = [right(x)]
left(@x) = left(red(x)) ; right(@x) = right(red(x))
left(/x) = red1(left(x)) ; right(/x) = right(x)
left(\x) = left(x) ; right(\x) = red(right(x))
left(x y) = left(x) left(y) ; right(x y) = right(x) right(y), which means that if x proves a = b and y proves c = d then x y proves a c = b d.
if x proves a = b and y proves c = d and a or b is equivalent to c or d, then x ; y proves the equality of the two other terms, two terms being equivalent if they are equal, or they reduce to the same term, or one reduces to the other.
left(a=b) = a ; right(a=b) = b
left(? x y) = left(y) ; right(? x y) = right(y)

These operators (except the last one which expresses the axiom a=b) can be seen as logical rules, where x proves a = b and y proves c = d :

s : |- s = s ; * : |- * = *
' : a = b |- 'a = 'b
[] : a = b |- [a] = [b]
/ : a = b |- red1(a) = b
\ : a = b |- a = red1(b)
() : a = b, c = d |- a c = b d
; : a = b, c = d, red(a) = red(c) |- b = d
; : a = b, c = d, red(b) = red(c) |- a = d
; : a = b, c = d, red(a) = red(d) |- b = c
; : a = b, c = d, red(b) = red(d) |- a = c
? : a = b, c = d |- c = d

The operator "@" is more difficult to express in terms of logical rules because the definition of left(@x) and right(@x) does not involve left(x) and right(x). Perhaps we could write something like :

@ : x |- left(red(x)) = right(red(x))

De Bruijn index is efficient and theoretically satisfying, but resulting expressions are not always easily writeable and readable. So it could be useful to write expression with named variables like in Lambda Calculus, and convert them into De Bruijn index. The notation "^x y" represents a proof obtained by "abstracting" from y the symbol x (playing the role of a Lambda Calculus variable). For example, the identity function may be represented either by "^x x" or by "[*]".

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. 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) = [*]) 

! gpTheorem1
 ( grandparent allan charles ;
   gpAxiom2 (grandparent allan charles) ;
   gpAxiom1 (parent brenda charles (grandparent allan charles)) ;
   gpRule1 allan brenda charles )

gpTheorem1

Running the Proof Logic program with this proof gives the following result :

$ ./pl-new grandparent-new.prf 

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 "skk.prf" proving the Combinatory Logic equality "S K K = I" :

! 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-new skk-new.prf

The proof : @([@([@([* '* '* ; ''*] (S = [[[''* * ('* *)]]]))] (K = [['*]]))] (I = [*]))
proves    : S K K
equals    : I

Here 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)) = [*])
! EFQ ^p (imp false p = [*])
! RAA ^p (imp (imp (imp p false) false) p = [*])
! GEN ^p (p (all ^x p) = [*])
! PART ^p ^t (imp (all p) (p t) = [*])
! PERMUT ^p ^q (imp (all ^x  : imp p (q x)) (imp p (all q)) = [*])
! SOME ^p (imp (imp (all p) false) 
                   (imp (p (some ^x (imp (p x) false))) false)
               = [*])

# 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-new prop-new.prf 

The proof : @([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([*] ( ( imp p p ; * ) ; '* ))] ('''* (imp p p)))] ( * ; '* ))] (''* (imp p (imp p p) (imp p p))))] (''''''''''''''''* (imp p (imp p p)) (imp p 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)))))] (''''''''''* (imp p (imp (imp p p) p)) (imp (imp p (imp p p)) (imp p p))))] (''''''''* p (imp p p)))] (''''''* p (imp p p) p))] [imp (imp (all *) false) (imp (* (some [imp ('* *) false])) false) = [*]])] [[imp (all [:] imp '* (* x)) (imp '* (all *)) = [*]]])] [[imp (all '*) ('* *) = [*]]])] [* (all ['*]) = [*]])] [imp (imp (imp * false) false) * = [*]])] [imp false * = [*]])] [[[imp (imp ''* (imp '* *)) (imp (imp ''* '*) (imp ''* *)) = [*]]]])] [[imp '* (imp * '*) = [*]]])] [[imp '* * ('* *) = [*]]])
proves    : imp p p
equals    : [*]

We can replace "!" by "%" to display the intermediate results :

# 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)) = [*])
! EFQ ^p (imp false p = [*])
! RAA ^p (imp (imp (imp p false) false) p = [*])
! GEN ^p (p (all ^x p) = [*])
! PART ^p ^t (imp (all p) (p t) = [*])
! PERMUT ^p ^q (imp (all ^x  : imp p (q x)) (imp p (all q)) = [*])
! SOME ^p (imp (imp (all p) false) 
                   (imp (p (some ^x (imp (p x) false))) false)
               = [*])

# 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

It gives the same result after the intermediate results :

$ ./pl-new propv-new.prf 

Left  of lemma9 is : imp (imp p (imp p p)) (imp p p) (imp p (imp p p) (imp p p))
Right of lemma9 is : [*]

Left  of lemma3 is : 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)))
Right of lemma3 is : [*]

Left  of lemma1 is : imp (imp p (imp (imp p p) p)) (imp (imp p (imp p p)) (imp p p))
Right of lemma1 is : [*]

Left  of lemma4 is : 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)))
Right of lemma4 is : [*] (imp p (imp (imp p p) p) (imp (imp p (imp p p)) (imp p p)))

Left  of lemma5 is : [*] (imp p (imp (imp p p) p) (imp (imp p (imp p p)) (imp p p)))
Right of lemma5 is : [*]

Left  of lemma2 is : imp p (imp (imp p p) p)
Right of lemma2 is : [*]

Left  of lemma6 is : imp p (imp (imp p p) p) (imp (imp p (imp p p)) (imp p p))
Right of lemma6 is : [*] (imp (imp p (imp p p)) (imp p p))

Left  of lemma7 is : [*] (imp (imp p (imp p p)) (imp p p))
Right of lemma7 is : [*]

Left  of lemma10 is : [*] (imp (imp p (imp p p)) (imp p p)) (imp p (imp p p) (imp p p))
Right of lemma10 is : [*] (imp p (imp p p) (imp p p))

Left  of lemma11 is : [*] (imp p (imp p p) (imp p p))
Right of lemma11 is : [*]

Left  of lemma8 is : imp p (imp p p)
Right of lemma8 is : [*]

Left  of lemma12 is : imp p (imp p p) (imp p p)
Right of lemma12 is : [*] (imp p p)

The proof : @([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([*] ( ( imp p p ; * ) ; '* ))] ?lemma12 ('''* (imp p p)))] ?lemma11 * ; '*)] ?lemma10 (''* (imp p (imp p p) (imp p p))))] ?lemma9 (''''''''''''''''* (imp p (imp p p)) (imp p p)))] ?lemma8 (''''''''''''''* p p))] ?lemma7 * ; '*)] ?lemma6 ('''* (imp (imp p (imp p p)) (imp p p))))] ?lemma5 * ; '*)] ?lemma4 (''* (imp p (imp (imp p p) p) (imp (imp p (imp p p)) (imp p p)))))] ?lemma3 (''''''''''* (imp p (imp (imp p p) p)) (imp (imp p (imp p p)) (imp p p))))] ?lemma2 (''''''''* p (imp p p)))] ?lemma1 (''''''* p (imp p p) p))] [imp (imp (all *) false) (imp (* (some [imp ('* *) false])) false) = [*]])] [[imp (all [:] imp '* (* x)) (imp '* (all *)) = [*]]])] [[imp (all '*) ('* *) = [*]]])] [* (all ['*]) = [*]])] [imp (imp (imp * false) false) * = [*]])] [imp false * = [*]])] [[[imp (imp ''* (imp '* *)) (imp (imp ''* '*) (imp ''* *)) = [*]]]])] [[imp '* (imp * '*) = [*]]])] [[imp '* * ('* *) = [*]]])
proves    : imp p p
equals    : [*]

Amazingly, it also works with infix notation :

! MP ^p ^q ((p imp q) (p q) = [*])
! AK ^p ^q (p imp (q imp p) = [*])
! AS ^p ^q ^r ((p imp (q imp r)) imp ((p imp q) imp (p imp r)) = [*])
! EFQ ^p (false imp p = [*])
! RAA ^p (((p imp false) imp false) imp p = [*])
! GEN ^p (p (all ^x p) = [*])
! PART ^p ^t ((all p) imp (p t) = [*])
! PERMUT ^p ^q ((all ^x  :  p imp (q x)) imp (p imp (all q)) = [*])
! SOME ^p (((all p) imp false) imp 
                   ((p (some ^x ((p x) imp false))) imp false) 
               = [*])

! lemma1 (AS p (p imp p) p)

! lemma2 (AK p (p imp p))

! lemma3 (MP (p imp ((p imp p) imp p))
               ((p imp (p imp p)) imp (p imp p)))

! lemma4 (lemma1 ( (p imp ((p imp p) imp p))
                      ((p imp (p imp p)) imp (p imp p)) ) )

! lemma5 ( lemma4 ; lemma3 )

! lemma6 (lemma2 
              ((p imp (p imp p)) imp
               (p imp p)))

! lemma7 ( lemma6 ; lemma5 )

! lemma8 (AK p p)

! lemma9 
 (MP 
    (p imp (p imp p))
    (p imp p))

! lemma10 (lemma7 ((p imp (p imp p)) (p imp p)))

! lemma11 ( lemma10 ; lemma9 )

! lemma12 (lemma8 (p imp p))

! theorem1 ( p imp p ; lemma12 ; lemma11 )

theorem1

It proves the same sentence with the infix notation "p imp p" :

$ ./pl-new propi-new.prf 

The proof : @([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([*] ( ( p imp p ; * ) ; '* ))] ('''* (p imp p)))] ( * ; '* ))] (''* (p imp (p imp p) (p imp p))))] (''''''''''''''''* (p imp (p imp p)) (p imp p)))] (''''''''''''''* p p))] ( * ; '* ))] ('''* (p imp (p imp p) imp (p imp p))))] ( * ; '* ))] (''* (p imp (p imp p imp p) (p imp (p imp p) imp (p imp p)))))] (''''''''''* (p imp (p imp p imp p)) (p imp (p imp p) imp (p imp p))))] (''''''''* p (p imp p)))] (''''''* p (p imp p) p))] [all * imp false imp (* (some ['* * imp false]) imp false) = [*]])] [[all [:] '* imp (* x) imp ('* imp (all *)) = [*]]])] [[all '* imp ('* *) = [*]]])] [* (all ['*]) = [*]])] [* imp false imp false imp * = [*]])] [false imp * = [*]])] [[[''* imp ('* imp *) imp (''* imp '* imp (''* imp *)) = [*]]]])] [['* imp (* imp '*) = [*]]])] [['* imp * ('* *) = [*]]])
proves    : p imp 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 )
T  # false = [*]

If we run the Proof Logic programw with this proof, we see that it proves that false = [*], or that false is true !

$ ./pl-new contradv-new.prf

Left  of L17 is : imp c false (c false)
Right of L17 is : [*]

Left  of L10 is : imp (imp c c) (imp c false) (imp c c (imp c false))
Right of L10 is : [*]

Left  of L5 is : 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)))
Right of L5 is : [*]

Left  of L4 is : imp (imp c (imp c false)) (imp (imp c c) (imp c false))
Right of L4 is : [*]

Left  of L6 is : 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)))
Right of L6 is : [*] (imp c (imp c false) (imp (imp c c) (imp c false)))

Left  of L7 is : [*] (imp c (imp c false) (imp (imp c c) (imp c false)))
Right of L7 is : [*]

Left  of L1 is : imp c c
Right of L1 is : [*]

Left  of Ac is : c
Right of Ac is : imp c false

Left  of L2 is : imp c c
Right of L2 is : imp c (imp c false)

Left  of L3 is : imp c (imp c false)
Right of L3 is : [*]

Left  of L8 is : imp c (imp c false) (imp (imp c c) (imp c false))
Right of L8 is : [*] (imp (imp c c) (imp c false))

Left  of L9 is : [*] (imp (imp c c) (imp c false))
Right of L9 is : [*]

Left  of L11 is : [*] (imp (imp c c) (imp c false)) (imp c c (imp c false))
Right of L11 is : [*] (imp c c (imp c false))

Left  of L12 is : [*] (imp c c (imp c false))
Right of L12 is : [*]

Left  of L13 is : imp c c (imp c false)
Right of L13 is : [*] (imp c false)

Left  of L14 is : [*] (imp c false)
Right of L14 is : [*]

Left  of L18 is : [*] (imp c false) (c false)
Right of L18 is : [*] (c false)

Left  of L19 is : [*] (c false)
Right of L19 is : [*]

Left  of L15 is : imp c false
Right of L15 is : c

Left  of L16 is : c
Right of L16 is : [*]

Left  of L20 is : c false
Right of L20 is : [*] false

Left  of L21 is : [*] false
Right of L21 is : [*]

The proof : @([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([@([*] ( false ; * ))] ?L21 * ; '*)] ?L20 ('''* false))] ?L19 * ; '*)] ?L18 ('''* (c false)))] ?L17 (''''''''''''''''''''''* c false))] ?L16 * ; '*)] ?L15 ''''''''''''''* ; c)] ?L14 * ; '*)] ?L13 ('''''''''''* (imp c false)))] ?L12 * ; '*)] ?L11 ('* (imp c c (imp c false))))] ?L10 ('''''''''''''''* (imp c c) (imp c false)))] ?L9 * ; '*)] ?L8 (''''* (imp (imp c c) (imp c false))))] ?L7 * ; '*)] ?L6 ('* (imp c (imp c false) (imp (imp c c) (imp c false)))))] ?L5 (''''''''''* (imp c (imp c false)) (imp (imp c c) (imp c false))))] ?L4 (''''''* c c false))] ?L3 * ; '*)] ?L2 (imp c '*))] ?L1 ('''''* c))] ?Ac < \\\* , imp \* false >)] (c = * [imp * false]))] [[* *] ['* (* *)]])] [[[imp (imp ''* (imp '* *)) (imp (imp ''* '*) (imp ''* *)) = [*]]]])] [[imp '* (imp * '*) = [*]]])] [imp * * = [*]])] [[imp '* * ('* *) = [*]]])
proves    : false
equals    : [*]

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.