[Top] [All Lists]

Re: [oor-forum] Ontologies vs Theories / Axioms vs Rules

To: OpenOntologyRepository-discussion <oor-forum@xxxxxxxxxxxxxxxx>
From: Christopher Menzel <cmenzel@xxxxxxxx>
Date: Tue, 18 Oct 2011 21:38:26 +0200
Message-id: <601DF855-CDF5-48F8-919A-CA50B813E2E7@xxxxxxxx>
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:

A first-order theory (in some first-order language) is any set of non-logical axioms in the language of first-order logic.  Peano Arithmetic, Pat Hayes' ontology of liquids, etc are all first-order theories.

I have a feeling you already knew this stuff but maybe someone else will find it helpful.


Message Archives: http://ontolog.cim3.net/forum/oor-forum/  
Subscribe: mailto:oor-forum-join@xxxxxxxxxxxxxxxx 
Config/Unsubscribe: http://ontolog.cim3.net/mailman/listinfo/oor-forum/  
Shared Files: http://ontolog.cim3.net/file/work/OOR/ 
Wiki: http://ontolog.cim3.net/cgi-bin/wiki.pl?OpenOntologyRepository     (01)
<Prev in Thread] Current Thread [Next in Thread>