[FOM] Question on Second Order Foundations

[Dmytro Taranovsky]

In my previous posting, I noted that almost all of current mathematics can be
formalized in second order logic with the universe having sufficiently many
objects relative to smaller numbers.  My best axiomatization is
1.  The usual logical rules.
2.  The comprehension schema.
3.  Uncountability of the universe.
4.  Existence of a binary relation enumerating all sets lacking a bijection with
the universe, with every set coded by a single object disjoint from the set.

The fourth axiom includes choice and inaccessibility of the universe.  Its
semi-formalization is that there is R such that: for every x, not xRx; not x=y
--> there is u such that not (xRu<-->yRu); every set (represented by a unary
predicate) lacking a bijection with the universe is {y: xRy} for some x.

The axiomatization is at the level of Kelley-Morse set theory.  To resolve basic
questions about the number of elements, one may want to add weak compactness
for the universe, which is easily formulated in second order logic through the
partition relation for graphs.

Dmytro Taranovsky
http://web.mit.edu/dmytro/www/main.htm