[FOM] First Order Logic

[Carl Hewitt]

Dear Harvey,

Computer science is interested having as strong axiomatizations as possible including, where possible, characterizing models up to isomorphism.

Can you give examples of where second order proofs might be problematical?  Computer science is not so much interested in higher (dubious?) cardinals.  In fact, for the foundations of Computer Science, the following inductively defined domain generally suffices:

Domain[0] ≡<https://en.wikipedia.org/wiki/Triple_bar> ℕ  (the natural numbers)
Domain[n] ≡<https://en.wikipedia.org/wiki/Triple_bar> Domain[n-1] UNION  POWERSET Domain[n-1]

Furthermore every set is a subset of Domain[i] for some i

With the above restriction, it is not hard to prove strong Categoricity:  Every model of the axioms is isomorphic via an unique isomorphism.

Of course, it is still possible for a computer to reason about mathematical theories of the higher cardinals :-)

________________________________
From: Harvey Friedman [hmflogic at gmail.com]
Sent: Sunday, August 25,

Imagine the situation if one proposed a second order version of ZFC, in the serious sense of second order here (not the fake notion used in so called second order arithmetic, where it is simply a two sorted first order theory). There would be widespread disagreement about whether a purported proof within second order ZFC is correct or not.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20130831/89a728b1/attachment-0001.html>