🚀 go-pugleaf

In article <373@mtnmath.UUCP> paul@mtnmath.UUCP (Paul Budnik) writes:

       [...] The way mathematicians extend logic
   today is by postulating the existence of large cardinals.
   These abstractions are so far removed from the computational roots of
   mathematics that there is no intuitive basis for deciding between them.
   However these large cardinal axioms have combinatorial implications.
   For example they allow us to decide the halting problems for a wider
   class of Turing Machines. 


I assume that last sentence refers to this sort of situation: in ZFI, one
can prove Con(ZF), which in turn says that a Turing machine that spent its
time searching for a contradiction in ZF would never halt.

                            It is my contention that if one focused
   on understanding these combinatorial implications and forgot about the
   Platonic heaven of completed infinite totalities, real progress could
   be made in extending logic.

Suppose we have some large cardinal axiom, say R (for Really Big Cardinal).
In ZFR one can prove (say) that Turing machine T never halts.  Are you
saying that one should add that combinatorial statement (call it TR) as a
new axiom, but not R?

I can see a certain philosophical appeal, in that the combinatorial
statement TR is in principle falsifiable.  One might regard TR as having a
truth value in some absolute philosophical sense, but not R.  On the other
hand, what reason do I have for believing that TR is true, if I reject R as
meaningless?

Of course, I could always adopt a formalist attitude-- "let's play around
with this new axiom TR, and see what happens."  But I could do that with ZFR.