Micromathematics

[JOSEPH SHIPMAN]

I’m curious about an even stricter form of “reverse mathematics” that deals with the totally finite objects V0, V1, …, V9.

V0 is empty. V5 has cardinality 65536, and the elements of V7 are objects which are each infeasibly large to specify. 

Therefore, if I had an oracle for Th(V7) I could settle practically all questions any mathematician would care about by asking, for the given proposition P, “is there an object which codes for a proof of P from ZFC “?

Difficulties coding this up might mean you need an oracle for V8 to ask the question feasibly, and an oracle for V9 to ask it easily and succinctly. But V9 should be plenty!

Can anything interesting be said about V5 or V6?

More generally, can anything be said about how much longer ZFC-proofs of statements about, say, V7 must be if the Axiom of Infinity is prohibited? We don’t know yet if PA proves Wiles’s Theorem, but we know it must prove (infeasibly) that there are no counterexamples to Wiles’s theorem coded straightforwardly by an element of V7. 

— JS

Sent from my iPhone