FOM: Clarification

[JoeShipman@aol.com]

In order to forestall further confusion, I shall elaborate upon some 
statements from my previous posting:

<< Because of SOL's incompleteness, there is no obvious choice for a 
deductive 
 calculus (deductive calculus=algorithm for generating validities, or, 
 alternatively, satisfiabilities).  <<

Satisfiabilities are the complement of (negations of validities).  Obviously 
satisfiabilities and validities can't both be r.e. unless they are both 
recursive (and hence represent a very weak calculus).  So you could have a 
calculus for generating validities, and a calculus for generating 
satisfiabilities, but these will not be related to each other in the obvious 
way.  Traditionally, "deductive calculus" refers to an enumeration of 
validities rather than an enumeration of satisfiabilities.  


>>However, there are some standard deductive 
 calculi for SOL, for example the ones given in chapter II of Manzano's book, 
 which are sound for standard semantics.  Furthermore, these calculi allow 
for 
 the development of "ordinary mathematics" without the standard 
 set-theoretical apparatus, using an interpretation where the first-order 
 variables are integers, the unary relations are sets of integers, etc.  >>

This is stated very imprecisely.  In the usual development, the integers are 
simply (some of the) elements of the (otherwise unspecified) domain, and the 
sets of integers are (some of the) unary relations, etc.  It doesn't matter 
what else is there because you can, with a single second-order sentence S, 
take a particular unary relation [to represent integerness] and a particular 
binary relation [to represent successor] and state Peano's axioms for them; 
the categoricity of SOL here ensures that you can get real theorems of number 
theory from second-order validities of the form S -->T .

-- Joe Shipman