[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: formalization*From*: holmes@catseye.idbsu.edu*Date*: Thu, 3 Jun 1999 10:34:19 -0600*Sender*: owner-fom@math.psu.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@math.idbsu.edu not glimpse the wonders therein. | http://math.idbsu.edu/~holmes

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]