Micromathematics

[JOSEPH SHIPMAN]

By the way, I asked roughly the same question in May 2013 but did not get any answers that addressed the point I was trying to make.

What I am really asking is “how useful would an oracle for Th(V_i) be?” for i=0,1,…9.

My impression is: of no use for i<=4, slightly useful for i=5, extremely useful for i>=8, and I’m not sure about i=6 and 7.

— JS

Sent from my iPhone

> On Nov 20, 2021, at 7:30 PM, JOSEPH SHIPMAN <joeshipman at aol.com> wrote:
> 
> 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