As Alex notes the axioms for a category can be expressed in FOL. This was
first done by W. Lawvere and about 1965. He represented comp as a relation. This
is very messy. The most direct way to represent composition is, as Alex notes,
is to represent composition as a partial operation in FOL. This operation is not
an arbitrary partial operation. The well-formedness condition is decidable.
Lawvere calls this Tarski’s hygiene condition for formal systems. If anybody
knows a reference for this please let me know. In a FOL system which admits
decidable conditions for well-formedness natural deduction conditions work
perfectly well.
John S. may recall I have suggested that (a replacement for) CL should be a
multi-sorted and allow decidable well-formedness conditions for operations. I
encounter this situation frequently in both mathematics and applications to
engineering and molecular science.
Lawvere in the late 60s gave FOL axioms for a topos, which can be viewed as
an algebraic form of set theory, but provides a very useful generalization that
enables dynamic systems to be represented in the extended FOL, which I will call
for the moment conditional FOL. Also by using conditional FOL the concept of
functorial semantics in category theory can be made copasetic with FOL model
theory.
Lawvere’s Topos axioms, with one exception, can be expressed in a
restriction of the conditional FOL to rules. One can find this in Lambek
and Scott’s book. With great care the exception can be eliminated giving a very
constructive version of the topos axioms, which yields an implementable, very
tractable reasoning system.
These topos axioms serve as a formal ontology for a lot of classical
mathematical applications. When one goes to non-classical applications such as
quantum theory, one needs generalizations to monoidal categories to provide a
suitable ontology, see Abransky.
Category theory is definable in FOL and is, in my opinion, a better
universal foundation than set theory, as the interpretation of category
primitives in terms of recognition procedures works better in many applications
than set theory primitives in terms of collectives. It is much easier to talk
about a recognition procedure for an iPad than the collection of iPads.
The conditional FOL provides the logic, the category axioms provide a
formal ontology within the logic.
There is more to the story, as Andrei is aware. One generally needs to talk
about not just one theory, but multiple theories and their relationships. The
enclosed paper was given at PhML-2014.
Henson Graves
Sent: Sunday, July 06, 2014 9:16 AM
Subject: Re: [ontolog-forum] Types of Formal (logical) Definitions
inontology
Pat,
category
theory is just 2-sorts theory like this
Sorts:
ob {- objects-}, ar {- arrows-}.
Functions:
dom ar:ob, cod ar:ob, one ob:ar, comp ar ar:ar infix "∘".
And
axioms:
dom(g∘f)=dom(f).
cod(g∘f)=cod(g).
h∘(g∘f)=(h∘g)∘f.
dom(one(b))=b.
cod(one(b))=b.
one(b)∘f=f.
g∘one(b)=g.
And
we should keep in mind that comp
is partial with predicate of definability - Defined(x∘y)
=def
dom(x)=cod(y).
Alex
_________________________________________________________________
Message
Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Config Subscr:
http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe:
mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files:
http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To join:
http://ontolog.cim3.net/cgi-bin/wiki.pl?WikiHomePage#nid1J
