[FOM] multi-sorted logic
a.hazen at philosophy.unimelb.edu.au
Sun Mar 12 01:23:17 EST 2006
Alan Baker asks for a "user's guide" to multi-sorted and higher-order logic.
Probably not an answer on both scores: Maria Manzano's "Extensions
of First Order Logic" (Cambridge Tracts in Theoretical Computer
Science #19, 1996) is a textbook presenting Hogher-Order logic as a
special case of multi-sorted. Down-side: it's a fairly careful and
slow exposition of basic mathematical logic (completeness,
incompleteness, etc),and might be a frustratingly slow read for
someone interested in a user's guide.
Re: multi-sorted. I don't know of a good general work. Maybe
because the problem is seen as too simple? There are options: (i)
should singular terms (constants, things made from function-symbols)
be specified in advance for type, or can they be "ambiguous"? If the
latter, the formalism should follow that of FREE LOGIC, with
predicates specifying which "sort" of object something is playing
the role of the "existence" predicate.
(ii) Should argument places
of predicates and function symbols berestrictedto variables (and
other terms) of a single type, or not?
(iii) In the model theory, one CAN, but NEED
NOT, stipulate that the domains the various sorts of variables range
over are disjoint. (One motive for not having them disjoint: to
interpret talko "abstract" objects: one might, for example, have one
sort of variables for sets and another for cardinal numbers,with the
identity sign interpreted as identity when standing between
set-variables and as equipollence when standing between
number-variables. Thomas Forster's book "Reasoning with Abstract
Objects" has helpful discussions on the complexities this can get
Feferman, in one of the first few volumes ofSpringer's "Lecture
Notes in Mathematics" has lectures on the proof theory of
Sorry, that's at the level of random thoughts rather than a real answer.
University of Melbourne
More information about the FOM