The Main Points

Strictly equational:

All reasoning under Mark2 is manipulation of equations using equations, though this may be automated in ways which can produce surprising effects. In particular, there is nothing precisely corresponding to the usual style of reasoning in propositional or predicate logic. Recently, we have been encouraged in this approach by the work of Gries, Schneider and Cohen on teaching an equational style of logic.

Avoidance of bound variables:

Originally, Mark2 did not use bound variables at all. It is still the case that Mark2's variable binding facility is a sort of window dressing on top of the synthetic abstraction facility supported, for example, by the built-in theorem RAISE. The motivation for this comes out of the program of Curry, as well as work of Quine, Tarski and Givant, and others, on ways to formalize first-order logic while avoiding the use of variables. We were interested at the outset in the question of how much these theoretically effective but practically awkward approaches could be made more usable. A great deal of development was successfully carried out with no use of bound variables at all, and we feel that the early development of the prover benefited from the simplicity afforded by their absence, but our conclusion has been that bound variables have their place, both as having actual practical advantages and as making the prover's notation more familiar to hoped-for users. The current variable-binding system uses de Bruijn levels; users seem to be able to handle this.

Avoidance of types:

This is a feature both of the systems of Curry and of Quine's set theory. In fact, the original logic of the prover (in an earlier version) was a synthetic combinatory logic equivalent to first-order logic on an infinite universe, which did have distinctions of sort. Moreover, the use of ``New Foundations'' was at first avoided, although the prover project grew out of an investigation of systems of combinatory logic equivalent to NF. Considerations of polymorphism between the two sorts of functions present in the original logic led us to abandon that logic (basically a first-order logic) and adopt a higher order logic equivalent to a consistent subset of NF (the consistency of full NF remains an open question). A special state of the prover implements a predicative version of NF which, while technically a higher-order logic, is actually weaker than first-order arithmetic; one regains full higher order logic upon issuing the impredicative command. The appearance of NF was not obvious; the only role it played in the earliest version of the prover using higher-order logic was to provide the stratification criterion for parameterized function definitions. The use of stratification had the desired immediate effect of providing complete polymorphism with respect to commonly used operations on functions.

We now have the additional feature of built-in type retractions onto ``strongly Cantorian sets'', which allow subversion of the stratification restrictions when one is working in ``small'' domains.

The original logic had a base sort containing all objects of the theory under consideration and a second and third sort consisting of functions on the objects of the base type and operations on these functions. All of these sorts were identified when the stratified higher-order logic was adopted. It cannot be said that the resulting identification of the domain of objects of a theory with domain of operators on those objects (only the type level ones, though) has been entirely convenient, but it has not proved wholly inconvenient, either. The lack of obligatory type notation is quite liberating (though it necessitates care). Type labelling can be introduced (use retractions as type labels) and it appears that typing schemes of this sort are natural objects for manipulation by the tactic language.

It should be noted that it is still not the case that all operators are first-class citizens of the theory in which they are used; only operators with trivial left and right type can be expected to correspond to functions of the theory.