Guide to Axiomatizing Domains in First-Order Logic
 
                  Ernest Davis, New York University
 
1. Define a model or microworld, as specifically and precisely as the
   nature of the domain allows. (Obviously, a much more concrete model
   can be given in the domain of spatial relations than in the domain
   of human emotions.)  You can then check for the soundness and consistency
   of your axioms by establishing that they are all true in the model.
 
   Do not cheat on your model. That is, if you find that you want to include in
   your axioms some new feature that is not in your model, do not just write
   down a new axiom.  Rather, you should rethink the model to include the
   new feature, and check that all of your axioms still make sense relative to
   the revised model.
 
 
2. Make two tables enumerating all the sorts and all the non-logical
   primitives you use in your logic, with their definitions in terms of the
   model.
 
3. If you want to adopt any notational conventions beyond vanilla
   sorted FOL, write them down. E.g. if you want to posit the unique names
   property for constant symbols, write it down.  If you have some standard
   convention for distinguishing fluents from related actions, write it down.
 
4. Some of the tenets of good programming style hold for axiomatizations
   as well:
   A. Non-logical primitives, like programming language identifiers, should
      be long enough that the reader can immediately know what they mean,
      but not so long that your axioms must be split up over many lines.
   B. Modularize. If you find the same subformula coming up again and again,
      define a new primitive to capture it.
   C. Use indentation and brackets to make the structure of the axiom
      apparent.
 
5. Cast a cold eye on every material implication.  Keep in mind that
   "p => q" means exactly "not p or q", and nothing more.
 
6. If you have written "forall(X) p(X) and q(X)" it is likely that you
   have made a mistake.  Rewrite it as the two axioms
   "forall(X) p(X)" and "forall(X) q(X)" and see if it still makes sense.
 
7. If you have written "exists(X) [p(X) => q(X)]" then it is
   100 to 1 that you have made a mistake.  Rewrite it in the logically
   equivalent form "[exists(X) not p(X)] or [exists(X) q(X)]" and you will
   probably realize where you have gone wrong.
 
   The only exception to this I have ever seen is where the variable X
   does not actually appear in the left hand side of the implication;
   for instance, in a form like "forall (Y) exists(X) p(Y) => q(X,Y)".
   Rewrite this for clarity as "forall (Y) p(Y) => exists(X) q(X,Y)."
 
8. If you have the implication "p => q", see if you can turn it
   into a biconditional "p <=> q."  You may have to strengthen the
   left hand side to "p <=> q and r".  This can be an easy way to get
   a more powerful theory.
 
9. Keep in mind that FOL does not have negation as failure.  This is
   not Prolog.  This is particularly important in recursive definitions.
   If you try to define "above" as the transitive closure of "on" in the
   Prolog style
        forall(X,Y) on(Z,Y) => above(X,X)
        forall(X,Y,Z) on(X,Y) and above(Y,Z) => above(X,Z)
   you will be able to prove that some things are above others, but
   you will never be able to prove that something is not above something else,
   because this definition is consistent with everything in the world
   being above everything.
 
10. Don't do programming.  FOL theories describe what's true, not how
    to compute things.  If you find yourself yearning  for loops,
    reassignable variables, data structures, or gotos, then either you're
    on the wrong track or you should stop working in FOL and switch to a
    programming language.
 
11. If you need a feature that's not within the scope of FOL, use a different
    logic; don't try to squeeze it into FOL.  For instance, if you want
    to reason with varying degrees of certainty, use a theory of
    plausible reasoning. Don't stick an extra argument "degree
    of certainty" onto each of your predicates; neither the semantics
    nor the proof theory will do what you want.
 
12. "Seek simplicity and distrust it." -- Alfred North Whitehead