* Brouwer: A Proof Finding Program for Intuitionistic, BCI, BCK, and Classical Logic

The Brouwer theorem-prover for Intuitionistic, BCI, BCK, and Classical logic (© Anthony Dekker 1992-1995) operates by enumerating lambda-calculus terms of a given type. The initial Brouwer 0.5.0 release [Macintosh SEA/HQX file: 283K] is available for download and testing on request.

Using Brouwer Version 0.5.0

This program was written by Anthony Dekker to construct terms in long form of a given type. It is based on work conducted by Martin Bunder, drawing on earlier work by Ben-Yelles. The program is written in the CLEAN Functional Programming Language.

The program uses about 3MB of RAM. For complex types, this may not be sufficient, since the algorithm uses exponential space and time. On memory overflow, the program may terminate with a 'Heap Full' message, or simply crash with an 'Error of Type 1'. The heap size cannot be increased without recompiling the program.

Select Apple-D (from the 'Brouwer' menu) to open the dialog box if necessary, enter a type, and click one of the proof buttons. The 'One Proof' button produces a single term of the given type, while the 'All Proofs' button generates all terms of the given type. The 'Return' key has the same effect as the 'One Proof' button.

While entering a type, Apple-C, Apple-X, Apple-V, etc. can be used. The data-entry field scrolls to allow large types to be entered. An alternative way to enter types is to open a file of strings using Apple-O (from the 'File' menu), and click 'Next' to read the next string from the file into the data-entry field. Types have the form:

        Variables:       A,B,..,AA,.. {upper case A..W, not X,Y,Z}
        True:            1
        False:           0
        Implication:     p->q
        Negation:        ~p     {shorthand for p->0}
        Universal Quant: @A.p   {p must be of the form q1->...->qn->A}
        Equality:        p=q    {shorthand for (p->q)/\(q->p)}
        Conjunction:     p/\q   {shorthand for @X.(p->q->X)->X}
        Disjunction:     p\/q   {either ~p->q or @X.(p->X)->(q->X)->X}
        Brackets:        (p)

Note that only a subset of the second order lambda calculus (System F) is represented: universal quantification is only allowed in types of the form @A.q1->...->qn->A. Universal quantification is represented internally using de Bruijn notation, so that e.g. @A.A->A and @B.B->B are the same type. However, bound variables are printed using the reserved names X,Y,Z,XX,XY,...

There are five proof modes, selected by radio buttons. The default mode 'Clas' proves p classically by using Peirce's Law (@A.@B.((A->B)->A)->A) and proof by contradiction (@A.0->A). In this mode the entered type may not contain @, i.e. only propositional calculus is allowed. This mode translates ~p\/q as p->q and p\/q as ~p->q otherwise. Conjunction is proved using pairing, but used as if p/\q was shorthand for @X.(p->q->X)->X, i.e. the combination of p/\q and p->q->r proves any atomic type r. Termination of this mode is guaranteed, although (since the algorithm is exponential in space) the program may crash on memory overflow.

The 'SubF' mode proves p in the subset of System F where universal quantification is only allowed in types of the form @A.q1->...->qn->A. This mode uses proof by contradiction as an axiom, but not Peirce's Law. Termination of this mode is NOT guaranteed if @ is used, although it usually occurs.

The 'SK' mode is like 'Clas' and 'SubF', but only permits implicational logic (i.e. types formed from ->, type variables, and brackets). Neither proof by contradiction or Peirce's Law are used.

The 'BCK' mode is like 'SK', but restricts proofs to terms where each variable occurs at most once. This mode does not use the same termination technique as the previous modes, but termination is guaranteed by a theorem of Bunder.

The 'BCI' mode is like 'BCK', but restricts proofs to terms where each variable occurs EXACTLY once.

The calculated proof(s) are counted and are displayed in a scrollable window. Use Apple-S (from the 'File' menu) to save the list of proofs to a file. Both the 'One Proof' and 'All Proofs' algorithms use depth-first search, but are guaranteed to terminate if @ is not used.

To quit the program use Apple-Q (from the 'File' menu), and hit any key to dismiss the 'Messages' window.

The 'Brouwer' menu contains two items ('Debug Mode' and 'Memo Table') which should be left turned off.

Theoretical Discussion

Terms have the form:

        Variables:        a,b,..,aa,.. {lower case}
        Unit:             []           {of type 1}
        Pairing:          [e,e']       {of type p/\q}
        Abstraction:      \x:p.e
        Null Abstraction: %p.e         {equiv to \x:p.e for x not in e}
        Application:      e e'
        Type Abstraction: ^A.e
        Type Application: e{p}
        Circular term:    $p:..(#p)..
        Contradiction:    !e           {of any type, if e has type 0}
        Peirce's Law:     *x:p->q.e    {of type q, if e has type q}

A circular term is valid provided the $p and #p are in the same environment, and there is some alternative proof e of type p for that environment. Then there is an infinite set of proofs of type p in that environment: e, $p:..(e).., $p:..($p:..(e)..).., etc. obtained by substituting for #p.

Special variables of the form +0, +A, +B,... are used for Peirce's Law.

Terms in long form are as follows (this definition is slightly different from that of Bunder). All uses of Peirce's Law must occur at the head, and Peirce's Law cannot be used in the presence of @.

        []                  of type 1
        a,b,...             of any type other than 1
        !e                  of any type other than 1 and 0
                                if e is in long form of type 0
        [e,e']              of type p/\q, for long e of type p
                                and long e' of type q
        \x:p.e              of type p->q, for long e of type q
                                if y:p is not in scope for any y {Note 1}
        %p.e                of type p->q, for long e of type q
                                if y:p is already in scope for some y
        ^B.e                of type @A.p, for long e of type p[B/A]
        xe1..en             of atomic type U = 0,A,B,C,...
                                for x of type p1->..pn->U
                                and long ei of type pi
        xe1..en{U}e1'..em'  of atomic type U = 0,A,B,C,...
                                for x of type p1->..pn->@B.q1->..qn->B
                                and long ei of type pi
                                and long ei' of type qi[U/B]
        xe1..en{U}e'        of atomic type U = 0,A,B,C,...
                                for x of type p1->..pn->q1/\q2
                                and long ei of type pi
                                and long e of type q1->q2->U
        *x:p->q.e           of any type p other than 1
                                if e is in long form of type p, using
                                the variable x of type p->q (q is atomic)

It can be shown that every term can be converted to a long form of the same type. The termination proof for the 'One Proof' and 'All Proofs' algorithms (in the absence of @) uses the fact that if any proof exists, then a non-circular proof exists, and if both circular and non-circular proof exist, then infinitely many proofs exist, of the form indicated. In every case, the set of free variables is bounded in size. This proof fails in the presence of @ because we can have may free variables of types differing only in type variable names. The proof by Bunder that all uses of Peirce's Law can be moved to the head extends easily to /\, but not to @.

Note 1

In the 'BCK' and 'BCI' modes the restriction to only one variable of each type is relaxed, and we use the following alternative definition of long form. Recall that 0 and 1 are not permitted in these modes:

        a,b,...             of any type
        \x:p.e              of type p->q, for long e of type q
        xe1..en             of atomic type U = A,B,C,...
                                for x of type p1->..pn->U
                                and long ei of type pi

The 'Some Proofs' Algorithm

This produces a subset of all proofs in long form, empty only if there are no proofs. The head of the list returned is used for 'One Proof'.

Some A 1 = {[]}

Some A p = {},  if Some A p is presently being 
                calculated (circularity)                    {Note 2}
                
Some A p = L,   if Some A p = L has already been calculated {Note 3}
         
Some A p = {x | x:p in A} 
           + (Some' A p) 
           + {!e | e in Some A 0}                           {Note 4}
           + {+p e | e in Some A q,  
                     where q is the proposition
                     in the first call to Some,
                     and p is a type variable or 0}         {Note 5}

Some' A @X.p = {^Y.e | e in Some A p[Y/X]}
               where Y is a new type variable
        
Some' A p->q = {%p.e | e in Some A q},  if x:p occurs in A for some x
                  
             = {\y:p.e | e in Some (A+{y:p}) q},  otherwise
               where y is a new variable

Some' A p/\q = {[e1,e2] | e1 in Some A p, e2 in Some A q}

And if p is a type variable or 0:

Some' A p = {xe1..en | x:p1->..->pn->p in A, n > 0, ei in Some A pi}
            +
            {xe1..en{p}e1'..em' | y:p1->..->pn->@X.q1->..qm->X in A,
                                  n>=0, m>=0, ei in Some A pi,
                                  ej' in Some A qi[p/X]}
            +
            {xe1..en{p}e' | y:p1->..->pn->q1/\q2 in A,
                            n>=0, ei in Some A pi,
                            e' in Some A q1->q2->p}

Note 2

We say that the pair (A,p) is BUSY if we are currently inside a call to Some A p. This is detected by adding (MARK p) to A when entering the call, and deleting the marks when adding new variables to A. Entering Some A p when (A,p) is busy indicates a circularity. Ignoring circularities guarantees termination (at least without @) without affecting provability. In the 'BCI' and 'BCK' modes this check is not performed, since it affects provability in those cases, and termination for those cases is already guaranteed.

Note 3

The program allows memoisation of the results. If Some A p is calculated to be L, it can save the triple (A,p,L) in a MEMO TABLE. Since the list L depends on busy pairs, A must include the busy markers here. However, since the memo table grows very large without significantly improving performance, this step turned OFF by default.

Note 4

Proof by contradiction is not used in the 'SK', 'BCK', or 'BCI' modes.

Note 5

Later *+p is added to the head of the term for each +p actually used. Peirce's Law is not used in the 'SubF', 'SK,' 'BCK', or 'BCI' modes.

The 'All Proofs' Algorithm

This produces all proofs in long form, together with a count of the number of proofs, used for 'All Proofs'. The list of proofs produced has an associated cardinality, which is either the actual length, or 0, or infinity.

All A 1 = {[]}

All A p = (0,{#p}),  if All A p is presently being 
                     calculated (circularity)               {Note 2}
                
All A p = L,   if All A p = L has already been calculated   {Note 3}
         
All A p = Resolve p ({x | x:p in A} 
                     + (All' A p) 
                     + {!e | e in All A 0}                  {Note 4}
                     + {+p e | e in All A q,  
                               where q is the
                               proposition in the
                               first call to All,
                               and p is a type
                               variable or 0})              {Note 5}

Resolve p L = {}, if every e in L contains #p unbound by $p
            = L, if no e in L contains #p unbound by $p
            = (INFINITY, {e | e in L does not contain free #p}
                         + {$p:e | e in L contains free #p}),  otherwise

All' A @X.p = {^Y.e | e in All A p[Y/X]}
              where Y is a new type variable
        
All' A p->q = {%p.e | e in All A q},  if x:p occurs in A for some x
                  
            = {\y:p.e | e in All (A+{y:p}) q},  otherwise
              where y is a new variable

All' A p/\q = {[e1,e2] | e1 in All A p, e2 in All A q}

And if p is a type variable or 0:

                      
All' A p = {xe1..en | x:p1->..->pn->p in A, n > 0, ei in All A pi}
           +
           {xe1..en{p}e1'..em' | y:p1->..->pn->@X.q1->..qm->X in A,
                                 n>=0, m>=0, ei in All A pi,
                                 ej' in All A qi[p/X]}
           +
           {xe1..en{p}e' | y:p1->..->pn->q1/\q2 in A,
                           n>=0, ei in All A pi,
                           e' in All A q1->q2->p}

The 'BCI' and 'BCK' Algorithms

These produce all proofs in long form, used for both 'All Proofs' and 'One Proof'. The list of proofs produced is simply counted.

BCI A p = L,   if BCI A p = L has already been calculated   {Note 3}
         
BCI A p = {x | x:p in A} + (BCI' A p)    

BCI' A p->q = {\y:p.e | e in BCI (A+{y:p}) q}, 
              where y is a new variable which occurs
              exactly once in e                             {Note 6}

And if p is a type variable:

                    
BCI' A p = {xe1..en | x:p1->..->pn->p in A,
                      n>0, ei in All (A-x) pi,
                      no variable occurs twice in xe1..en}  {Note 7}     

Note 6

It suffices to check that y occurs in e (see Note 7). For the 'BCK' algorithm, y occurs at most once, so this test is omitted.

Note 7

A set of free variables is maintained for every term, which is checked for duplicates on each application.