On Oct 18, 2011, at 8:50 PM, Ali SH wrote:
Hello Michael and all,
I noticed some confusion today during the telecon when Michael and Todd were talking about differences between Ontologies & Theories, and Rules & Axioms. I've actually encountered a number of people who make this distinction -- that an ontology doesn't really express "rules", and that these rules are somehow different from "axioms". The line is still blurry to me, but it seems to be that in this terminology, a "rule" refers to anything that OWL doesn't support, whereas in the CL (and FOL world) there is no distinction between these "rules" and "axioms".
In logic, "rule" typically means "rule of inference". Together with some set of logical axioms, rules are an essential part of a logical system like propositional or first order logic. Thus, a standard set of logical axiom (schemas) for propositional logic are:
(φ → (ψ → φ)
((φ → (ψ → θ)) → ((φ → ψ) → (φ → θ))
(¬φ → ψ) → ((¬φ → ¬ψ) → φ)
Note, however, that with axioms alone you are powerless to do anything more than write down axioms. Rules of inference define a notion of one sentence following from other and, hence, enables the derivation of theorems that are not axioms. The usual rule of inference for propositional logic, of course, is modus ponens:
MP: ψ follows from φ and φ → ψ.
A proof of propositional logic, then, is any sequence of sentences such that each sentence is either an axiom or follows from sentences occurring earlier in the sequence.
Predicate logic simply adds axioms for quantification, e.g.,
∀αφ → φ(τ), where τ is an "acceptable" instance of φ
∀α(φ → ψ) → (φ → ∀αφ), where α does not occur free in φ
and, optionally, identity, and (typically) adds a rule of inference for universal generalization:
UG: ∀αφ follows from φ. (Note this is usually qualified in certain ways but never mind.)
CL, for better or worse, does not specify a proof theory but, if it did, this is surely (?) what "rule" would mean. The senses of "rule" you describe for the most part seem rather different. In my experience, these "non-logical" uses of "rule" are usually synonymous with "non-logical axiom". Speaking of which: