FOM: Clarification
JoeShipman@aol.com
JoeShipman at aol.com
Fri Sep 8 23:18:32 EDT 2000
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
More information about the FOM
mailing list