[FOM] multi-sorted logic

[A.P. Hazen]

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 
into.)

    Feferman, in one of the first few volumes ofSpringer's  "Lecture 
Notes in  Mathematics" has lectures on the proof theory of 
multi-sorted logic.

    Sorry, that's at the level of random thoughts rather than  a real answer.
---
Allen Hazen
Philosophy Department
University of Melbourne