[FOM] Foundational Challenge

[Timothy Y. Chow]

On Sun, 12 Jan 2020, Harvey Friedman wrote:
> But handling this kind of thing efficiently and simply in the classical 
> set theoretic foundation is second nature to me. So what Chow is writing 
> there doesn't even come close to making me lose any faith in the set 
> theoretic approach.

I feel like I'm losing track of what is under debate here.

Joe Shipman's challenge was about length of proofs, which I have loosely 
interpreted as "amount of engineering effort" rather than strictly the 
number of symbols required to express the proof.  In Maddy's language, 
this is really about Proof Checking, not necessarily any of the other 
roles she articulated.  So I don't think that philosophical coherence has 
much to do with it.  If the goal is just to get the computers to help us 
formalize our proofs, then all we need is technical correctness and 
pragmatic efficiency, not philosophical coherence.  Using a 
non-set-theoretic framework for Proof Checking doesn't force us to 
jettison set theory for other purposes.

If we're talking about engineering, then let me draw an analogy with the 
choice of programming languages---say C versus C++, or C versus Python.

An advocate of C++ can list all kinds of supposed advantages of working in 
C++ as opposed to C.

A C programmer can listen patiently, and then say, "It's second nature to 
me to do all those things you're talking about in C.  So I see no reason 
to switch to C++."

The C programmer is absolutely correct.  There isn't anything that can be 
done in C++ that can't be done in C.

But it doesn't follow that for every large software engineering project, 
programming it in C is going to be just as efficient as programming it in 
C++.

In other words, whether UF provides a more efficient engineering framework 
can't be decided just by looking at one side of the equation (the 
set-theoretic side) and convincing ourselves that it could be done.  One 
has to examine what happens in both cases and see whether there is any 
gain to be had.

Tim