Predicate Calculus as S Expressions

While contemplating some simple proofs for group theory I wanted a scheme for showing Fitch format proofs in a web page. It soon occurred to me to adopt an S-expression form for such proofs and then write a Scheme program to generate svg expressions for the web page. 

(all x (all t (is z (= (* x z) y))))
seems like a simple thing to edit.

Here is predicate calculus as S expressions.
⟨id⟩≡ “Scheme symbol”
⟨phrase⟩≡ (and . ⟨plist⟩) | (or . ⟨plist⟩) | (not ⟨phrase⟩)
| (implies ⟨phrase⟩ ⟨phrase⟩) | (iff ⟨phrase⟩ ⟨phrase⟩)
| (all ⟨id⟩ ⟨phrase⟩) | (is ⟨id⟩ ⟨phrase⟩)
| (⟨pred⟩ ⟨nl⟩)
⟨plist⟩≡ () | (⟨phrase⟩ . ⟨plist⟩)
⟨nl⟩≡ () | (⟨id⟩ . ⟨nl⟩)
⟨pred⟩≡ ⟨id⟩ but none of (and or not implies iff all is)
The above is like BNF but for Scheme values instead of strings. An ⟨id⟩ is an individual variable or constant. The symbols that cannot serve as a predicate (⟨pred⟩) are the reserved syntax symbols. It is probably poor form to use those symbols as ⟨id⟩s but such use does not cause ambiguity. ‘(is x (red x))’ means (∃x Rx), or there is an x such that x is red.

As in conventional presentations of predicate logic some explicit list of predicates, along with the number of operands each take must be included. Some constant ⟨id⟩s may also be provided. An additional category of ⟨phrase⟩es called ‘sentences’ is usually needed which the BNF does not capture. Here is Scheme code to test for sentences. A sentence is a ⟨phrase⟩ in which every occurrence of ⟨id⟩ in an ⟨nl⟩, is also an occurrence of a larger ⟨phrase⟩ beginning with ‘all’ or ‘is’, or the ⟨id⟩ is one of the individual constants. I.e. no free variable in sentences. For some purposes some axioms are also provided.

Proof

Proof notions generally involve a sequence of proof steps. The simplest proof notions do not afford the shortest proofs. The more elaborate notions afford shorter proofs and can be mechanically transformed into proofs conforming to the simple notions. There is a complexity gamut of proof notions. Fitch’s notions are more elaborate.

The Scheme array captures the simple notion of a sequence of steps. The simplest notions involve one array where each element is a proven sentence which results either from applying modus ponens to two previous sentences in the array, or quoting an axiom. With this simple notion the axioms must be infinite but they are easily generated by systematic substitution of arbitrary well formed ⟨phrase⟩es or ⟨id⟩s into a finite set of axiom schemas.

A proof formatting program is scarcely more complex than a proof checking program. The input to the latter is shorter in that it indicates the earlier proof steps on which it relies, and the necessary inference rule. It is easier for the checker to generate the ⟨phrase⟩es than to verify that the indicated inference rule produces the claimed result.

Proof Notion F

A proof is an array of steps. A step is a list of:

Predicate calculus with functions

Sometimes predicate calculus is stretched to include functions. Here we extend the syntax to allow functional notation. We augment the above rules thus:
⟨nl⟩≡ () | (⟨id⟩ . ⟨nl⟩) | (⟨fc⟩ . ⟨nl⟩)
⟨fc⟩≡ (⟨fun⟩ . ⟨nl⟩)
⟨fun⟩≡ “Scheme Symbol”
The rule for ⟨nl⟩ is extended to include function invocations, ⟨fc⟩, which denote a thing. Now the solvability axiom for groups may be written:
(all a (all b (is x (= (* a x) b)))).

This program verifies sentences in this expanded syntax.

More work

We want to find and display proofs that convince: I aim to produce Fitch style graphics for people and some yet undefined internal form for programs. But first we must define the logical form for a proof. Also perhaps it is feasible to write a Javascript program to interact with the human proof finder via SVG.