Proof Logic extensions

Terms of Proof Logic are proofs. A proof x proves an equality a = b, where a = left(x) and b = right(x), and a and b are also proofs. The basic operators of the initial version of Proof Logic are defined by the left and right sides of the equality proved by a proof built with these operators :

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 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

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, c = d |- a c = b d
; : a = b, c = d, a is equivalent to c |- b = d
; : a = b, c = d, b is equivalent to c |- a = d
; : a = b, c = d, a is equivalent to d |- b = c
; : a = b, c = d, b is equivalent to d |- a = c

The order of the rules for the operator ";" is important, for example if x proves a=b then x;x proves b=b with this order, if we put the fourth rule was before the first one then it proves a=a.

The operator "@" can also be introduced to implement definitions of the form "let name = definition in proof". It is not necessary but useful to write proofs more easily. It is defined by :

left(@x) = left(red(x)) ; right(@x) = right(red(x))

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))

These basic operators can be composed to define new operators. For example, we can define operators LFT and RGT by :

left(LFT x) = left x ; right(LFT x) = left x
left(RGT x) = right(x) ; right(RGT x) = right x

corresponding to the logical rules :

LFT : a = b |- a = a
RGT : a = b |- b = b

These operators can obviously be defined by :

LFT x = x ; x
RGT x = x ; (x ; x ; x)

We can define an operator associated to the symmetry rule :

SYM : a = b |- b = a

This operator is defined by :

left(SYM x) = right(x)
right(SYM x) = left(x)

It can be defined by a combination of {,} and LFT, or of <|> and RGT :

SYM x = x ; x ; x

We can say that if a = b, then red(a) = b. This is formalized by the RDL rule :

RDL : a = b |- red(a) = b

The corresponding operator is defined by :

left(RDL x) = red(left(x))
right(RDL x) = right(x)

It can also be defined by a combination of ;, @ and LFT :

RDL x = @(LFT x);x

The symmetric rule is :

RDR : a = b |- a = red(b)

The corresponding operator is defined by :

left(RDR x) = left(x)
right(RDR x) = red(right(x))

It can also be defined by a combination of ;, @ and RGT :

RDR x = x;@(RGT x)

RDL can also be defined from RDR and reciprocally :

RDL x = SYM (RDR (SYM x))
RDR x = SYM (RDL (SYM x))

We can also reduce both left and right sides :

RDB : a = b |- red(a) = red(b)

The corresponding operator is defined by :

left(RDB x) = red(left(x))
right(RDB x) = red(right(x))

It can be defined by a combination of RDL or RDR, and SYM :

RDB x = SYM (RDL (SYM (RDL x)))
RDB x = RDL (SYM (RDL (SYM x)))
RDB x = SYM (RDR (SYM (RDR x)))
RDB x = RDR (SYM (RDR (SYM x)))

A rule can also be introduced to do the substitution in application of a function to an argument :

SUB : a = b, c = d |- [a] c = subst(*,b,d)

The corresponding operator is defined by :

left(SUB x y) = [left(x)] left(y)
right(SUB x y) = subst(*,right(x),right(y))

Definitions of extensions with C program

The definitions of new operators as combinations of basic operators look like the definition of new combinators as combination of basic combinators (K, S) in combinatory logic. But here we are at some kind of "meta" level. However, it seems that such definitions at "normal" level works if we use the @ operator. For example, we have seen that LFT x = x;(x;x;x). With lambda calculus-like notation it gives "LFT = ^x (x;(x;x;x))". If we apply it to a proof, for example the axiom a = b, we get :

? ^x (x;(x;x;x)) (a=b).

The proof  : [* ; ( ( * ; * ) ; * )] (a = b)
reduces to : a = b ; ( ( a = b ; a = b ) ; a = b )
and proves : [*] a
equals     : [*] b

We would like to obtain that it proves a = a. But with the @ operator, we get :

? @(^x (x;(x;x;x)) (a=b)).

The proof  : @([* ; ( ( * ; * ) ; * )] (a = b))
reduces to : @a = b ; ( ( a = b ; a = b ) ; a = b )
and proves : a
equals     : a

Remember that the @ operator is defined by :

left(@x) = left(red(x)) ; right(@x) = right(red(x))

The reduction of its operand gives :

? ^x (x;(x;x;x)) (a=b).

The proof  : [* ; ( ( * ; * ) ; * )] (a = b)
reduces to : a = b ; ( ( a = b ; a = b ) ; a = b )
and proves : [*] a
equals     : [*] b

which proves a = a :

? a = b ; ( ( a = b ; a = b ) ; a = b ).

The proof  : a = b ; ( ( a = b ; a = b ) ; a = b )
reduces to : a = b ; ( ( a = b ; a = b ) ; a = b )
and proves : a
equals     : a

We can also use the notation "! x y z" (equivalent of "let x = y in z" in Haskell) since the definition of ! embeds the @ operator. Here is the result with LFT defined by ! :

? ! LFT ^x (x;(x;x;x)) (LFT (a=b)).

The proof  : @([* (a = b)] [* ; ( ( * ; * ) ; * )])
reduces to : @a = b ; ( ( a = b ; a = b ) ; a = b )
and proves : a
equals     : a

This definition does not give exactly the same result than the operator we want to define, because the operator we obtain by this method also reduces the terms of the conclusion, for example :

? ! LFT ^x (x;(x;x;x)) (LFT ([*]a=b)).

The proof  : @([* ([*] a = b)] [* ; ( ( * ; * ) ; * )])
reduces to : @a = b ; ( ( a = b ; a = b ) ; a = b )
and proves : a
equals     : a

We obtain a = a instead of [*]a = [*]a.

Here are some other examples of such definitions :

? ! RGT ^x (x;x) (RGT (a=b)).

The proof  : @([* (a = b)] [* ; *])
reduces to : @a = b ; a = b
and proves : b
equals     : b

? ! SYM ^x (x;x;x) (SYM (a=b)).

The proof  : @([* (a = b)] [( * ; * ) ; *])
reduces to : @( a = b ; a = b ) ; a = b
and proves : b
equals     : a