SUO: IFF-FOL -- the term namespace
SUO and SCL folk,
I am slowly working through an rigorous axiomatization for unsorted first
order logic (FOL). This axiomatization will be housed in the IFF First Order
Logic (meta) Ontology (IFF-FOL), and should provide a well-known traditional
bridge to the current rather novel and sorted logic as axiomatized in the
IFF Ontology (meta) Ontology (IFF-OO).
The SUO WG has on numerous occasions asserted the need for a FOL expression
of object-level ontologies. A rigorous axiomatization of FOL is important to
the IFF project, since all the IFF axiomatization has a first order
expression, with the "higher order" expressiveness of the IFF axiomatization
emerging from a first order expression at the various metalevels of the IFF.
The design strategy is to break up the IFF-FOL axiomatization into three
smaller modules: there will be basic modules (namespaces) for (1) terms and
(2) expressions (formulas), and an extension module (namespace) for (3)
equations. The straight equational extension to terms gives equational logic
or universal algebra (the axiomatization here is oriented toward the
functorial semantics of F.W. Lawvere). The combination of terms and
expression gives first order logic without equations, and the combination of
terms, expressions and equations gives first order logic with equations.
Most of the IFF Term Language namespace (IFF-TRM) is finished and posted at
the present time, the equational language namespace is finished in
rudimentary form but not yet posted, and I will work on the expression
language namespace in January. I will attempt to rigorously follow the
Categorical Design Principle [http://suo.ieee.org/IFF/version/20021205.htm]
in all FOL axiomatization. The IFF-TRM can be accessed by following the
sequence:
1. SUO IFF main page
[http://suo.ieee.org/IFF/]
2. Work In Progress page
[http://suo.ieee.org/IFF/work-in-progress/]
3. IFF-FOL main page
[http://suo.ieee.org/IFF/metalevel/lower/ontology/fol/version20040101.html]
4. IFF-TRM main page
(note: IE will not render all the math symbols here; but Mozilla works OK)
[http://suo.ieee.org/IFF/metalevel/lower/namespace/term-language/version2004
0101.html]
5. IFF-TRM abstract axiomatization PDF file
[http://suo.ieee.org/IFF/metalevel/lower/namespace/term-language/version2004
0101.pdf]
As always, all constructive comments are requested.
Robert E. Kent
rekent@ontologos.org