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. If it is not possible to give necessary and sufficient conditions for the primitive, write down in English as precise a definition as you can manage, and try at least to bound the concept by giving some necessary conditions and some sufficient conditions.
3. If you want to adopt any notational conventions beyond a simple sorted FOL with equality, write them down explicitly (in English). 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:
5. Cast a cold eye on every material implication. Keep in mind that "p implies 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) implies 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) implies q(X,Y)". Rewrite this for clarity as "forall (Y) p(Y) implies exists(X) q(X,Y)."
8. If you have the implication "p implies q", see if you can turn it into a biconditional "p iff q." You may have to strengthen the right hand side to "p iff [q and r]". This can be an easy way to get a more powerful theory.
This does, however, require some care in choosing a grouping. Forms
that are logically equivalent as implications may cease to be so
when the implication is turned into a biconditional, and you have
to choose the correct form. For instance, the two formulas
Another example: The assertion "If a triangle is equilateral then it is equiangular" can be represented
9. Equality and function symbols are powerful representational tools; by all means, use them. However, there are a number of common errors to be avoided.
For example, if you are translating the sentence, "Your father is older than you are," (in the sense of "you" meaning "everyone"), it is natural to gloss this as "If X is the father of Y then X is older than Y" and then to write it as "forall(X,Y) X=father(Y) implies older(X,Y)". This can be expressed more elegantly as "forall(Y) older(father(Y),Y)."
On the other hand, the original form with the explicit implication may
lend itself to conversion to a biconditional, as discussed in (8) above.
For instance, the fact, "2 is a even prime," if expressed in the form
"forall(X) X=2 implies even(X) and prime(X)", can be easily converted
to the biconditional "2 is the only even prime,"
"forall(X) X=2 iff even(X) and prime(X)."
10. 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
forall(X,Y) on(Z,Y) implies above(X,X)
forall(X,Y,Z) [on(X,Y) and above(Y,Z)] implies 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.
11. 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.
12. Check to see whether there exists a simpler or more general model for your axiomatization than the microworld you have in mind. For example, if you think a microworld involves gravity, then imagine a gravity-less version, and ask whether your axioms are still true in that. Another example: there are in the literature theories of spatial regions that in fact apply to arbitrary sets.
Finding such an alternative model can have its pros and cons. Clearly, it means that you have not captured all aspects of your microworld. On the other hand, in a given application, you may not need these aspects. Identifying the axiomatization as a description of a simpler model may lead you to effective algorithms, decidability results, and so on. But, one way or another, it is definitely a fact worth knowing about an axiomatic system.
13. "Seek simplicity and distrust it." --- Alfred North Whitehead
Acknowledgements: Thanks to Pat Hayes, Vladimir Lifschitz, Rob Miller, and Ray Reiter for helpful criticisms and suggestions. This research was supported in part by NSF grant #IRI-9625859.