What you say is exactly what I mean regarding partial functions. General
logics which admit partial functions are very unsatisfactory and messy in my
opinion. But with the decidability conditions for partial functions then one can
can construct or recognize a model when the interpretation of the definedness
precondition is met. So the model theory works well for this limited kind of
Patrick Suppes has made a strong argument that standard FOL theories will
always be inadequate for axiomatizing applications; he suggests using set theory
as the alternative.
Many years ago I worked for Pat to engineer his version of set theory to be
used in a first order theorem prover/proof checker. The reduction of everything
to epsilon was just not really practical. This made me look for other
alternatives with the same expressive power. Topos theory was a natural
candidate as it simply gives algebraic axioms for the constructions of cartesian
product, disjoint union, etc. This approach turned out to work quite well for
implementation. I implemented a system based on the topos approach in the 1980s.
Topos theory also needs some engineering to get rid of existential statements in
My experience confirms that Pat is correct that
standard FOL will not work for application axiom system development, one needs
multiple sorts, and decidable preconditions for operations. However, there are
these alternatives to set theory such as topos theory. Type theory is another
alternative, but I prefer topos theory for physical applications. Type theory
works well software for software applications.
One way to look at using set theory or topos
theory represented within some slightly extended version of set theory, is that
one is separating the inference mechanism (logic) from the expressiveness (the
ontology). While they overlap, one can use relatively simple logics with very
expressive ontological languages. That is higher order logic is not needed for
applications as these systems can represent higher order logic in their term
calculus. One also sees this kind of thing in systems like Hilog.
Sent: Monday, July 07, 2014 4:22 AM
Subject: Re: [ontolog-forum] Types of Formal (logical) Definitions
I just have 2-sorted Goldblatt's description in TOPOI.
The categorial analysis of logic. 1979.
I like idea that set theory is may be over reduced to
one prime predicate symbol ∈. Maybe it's like a Scheffer stroke for
In this case category should replace algebraic system
as a model for theory?
When we work with a partial function it is necessary to
supply a predicate for an area where it's defined. For ex. for x/y it's
y<>0. This is just a pre-condition to calculate term "x/y" value without
abort. And if we have an arbitrary term with partial functions we should derive
pre-condition for it.
Is this what you keep as "decidable
well-formedness conditions for operations"?
Community Wiki: http://ontolog.cim3.net/wiki/