[FOM] Definability and provability

[hendrik@topoi.pooq.com]

On Tue, Sep 07, 2010 at 08:38:46AM -0700, Paul Budnik wrote:
> 
> Tools may become available that will allow us to directly define as 
> iterative processes, recursive ordinals large enough to prove the 
> consistency of ZF plus various large cardinal axioms. Using axioms that 
> define recursive ordinals and facilities for automating and verifying 
> complex proofs we should be able to solve some problems that currently 
> require large cardinal axioms (or at least the assertion that these 
> axiom systems are consistent). Will such results strengthen interest in 
> large cardinal axioms or suggest that they are a bridge or more too far 
> when it comes to mathematical definability? Will it perhaps do both?

When definitions of ordinals become sufficiently complicated, it 
becomes undeterminable which is greater.  Could it be that for two such 
incomparable ordinal definitions, the existence of the ordinal one 
defines would prove a conjecture, and existence of the other would prove  
its negation?

-- hendrik