FOM: formalization

[holmes@catseye.idbsu.edu]

As a footnote to Simpson's remarks about formalization, it might be
worth noting that not all formalizations are based on the predicate
calculus per se.  For example, my automated theorem proving work is
not.  The basic logic of my prover is algebraic (equational
reasoning); the primitive mathematical constructions in the system are
definition of expressions by cases and definition of functions by
abstraction.  Propositional connectives and quantifiers are defined
notions in this system and their properties are presented as theorems
and derived rules of inference rather than axioms and basic rules of
inference.  Of course I use predicate logic, but its notions and
axioms are derived rather than basic in this particular formal context
(in fact, it took a fair amount of work to get the system to support
"user-friendly" simulations of certain aspects of predicate logic
reasoning, though it was clear from the outset that it supported
predicate logic in principle; I got a deeper appreciation of predicate
logic in the course of redeveloping it :-)

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes