new foundations?

Stream: new members

[Daniel Ever]

I've seen some discussions related to type theory eventually becoming the new foundations of mathematic, replacing set theory and all that. Could anyone more competent in that field actually tell me how reasonable is that assumption? Is it possible that math needs no new foundations and type theory could be used just for proof checking and automatization alone, without the need for any change of paradigme? Thanks!

[Kevin Buzzard]

Mathematics doesn't need foundations at all -- just ask Gauss, Euler or Riemann. In fact just ask most of the people working in my department, many of whom will have no idea what the axioms of ZFC are and just use the kind of arguments which feel natural. It's not until you start asking "weird" questions like "what is a function" that you have to worry about foundations. I dispute your implicit assertion that the current foundations of mathematics are set theory. I don't think practical mathematics has foundations, 99% of people still work like Gauss

[Daniel Ever]

Kevin Buzzard said:

Mathematics doesn't need foundations at all -- just ask Gauss, Euler or Riemann. In fact just ask most of the people working in my department, many of whom will have no idea what the axioms of ZFC are and just use the kind of arguments which feel natural. It's not until you start asking "weird" questions like "what is a function" that you have to worry about foundations. I dispute your implicit assertion that the current foundations of mathematics are set theory. I don't think practical mathematics has foundations, 99% of people still work like Gauss

If I got your idea right, it's somewhat close to Feyerabend's methodological anarchism, basically 'we use whatever produces the results', regardless of any other attached considerations?

[Reid Barton]

I don't think it's quite the same thing. In math it's important to know that we could reduce our methods to (say) ZFC--that's how we know our theorems are correct. But once we know it's possible, we don't really care to know any more about how it's done. And choosing a different foundational system than ZFC makes no difference as long as it proves more or less the same theorems.

[Reid Barton]

Here is one viewpoint on how mathematicians work in practice and how that relates to a specific foundational system such as ZFC:
https://mathoverflow.net/questions/90820/set-theories-without-junk-theorems/90945#90945

[Reid Barton]

I guess it's also important to note that a lot has changed since the time of (particularly) Euler, who really did "use whatever produced the results". Notably, set theory was introduced and then found to contain paradoxes if one wasn't careful to avoid them.

[Reid Barton]

But most mathematicians will learn early on (maybe implicitly) that there are no foundational issues in their area or that someone else has already dealt with them, and never think about foundations.

[Kevin Buzzard]

Yes Reid makes the point clearly. The practicing mathematician doesn't think about foundations and argues the way they've learnt to argue from reading published and refereed books or papers. The set theorists know that it can all be translated into set theory, the type theorists know that it can all be translated into type theory. The only indication that set theory is somehow the established language is that we say "a group is a set equipped with..." rather than "a group is a type equipped with...".

[Daniel Ever]

So, the main motivation to somewhat embrace type theory lies in the fact it allows us to do the math just as before, but now we can formalize it way better to see our gaps in knowledge, gain certainty in our proofs, use the wider scope of instruments (like library_search etc.), and generally be able to investigate every step of deduction with the clarity not easily achieved in 'usual math' which heavily relies on natural languages?

[Riccardo Brasca]

If you mean why type theory is more common for proof assistants, this is a different story, and it's mainly for practical reasons. You can have a look a this mathoverflow question.

[Reid Barton]

Speaking for myself personally, the reason to formalize mathematics is all of those goals you listed, and the reason to do so using type theory specifically is that empirically it seems to work better (or at least not worse) than set theory. If it was way more effective to formalize math in set theory then I would use set theory instead.

[Riccardo Brasca]

But note that you can use a proof assistant without knowing its foundations, similarly as one do mathematics without never asking "what is a set/type?".

[Mario Carneiro]

also note that it's possible to swap out the "backend" of a proof assistant so that it's sitting on a different foundation without affecting the user experience at all. It is well known that all the major foundational systems are (in principle, approximately) equivalent, and with a translation layer you can make it so that "you were doing set theory all along"

[Daniel Ever]

Reading your link now, thanks! But using proof assistant without understanding why it works for me feels like defining some function, like determinant, by saying 'it's a black box that tells you something about linear dependence'. Guess at some point you may find yourself a person in Searl's Chinese room, typing symbols and checking the output without actually understanding what's going on.

[Mario Carneiro]

Using a proof assistant without understanding why it works is a different matter. There are things other than foundations that come to bear when understanding how the proof assistant ticks

[Mario Carneiro]

as a user, it's probably more important to understand elaboration order than induction principles in dependent type theory to use lean

[Reid Barton]

Maybe a more useful analogy is that it's like writing a program in Python without knowing the details of the instruction set that the hardware actually executes.

[Reid Barton]

And your Python program doesn't care about the underlying instruction set architecture at all (and you could run your Python program inside an emulator for one architecture that is actually running on a different architecture, etc)

[Daniel Ever]

but isn't really vague an unintuitive, trying to understand what certain tactics does, when it can or can't be applied? both the descriptions of tactics as well as error messages seem to require some familiriaty with type theory at a basic level (or so the impression I got)

[Reid Barton]

Lean's "frontend" is based on type theory and so you definitely have to understand Lean's flavor of type theory to some extent to use it effectively.

[Reid Barton]

But Lean's backend/kernel could be based on ZFC and then you wouldn't also need to understand ZFC to use Lean.

[Reid Barton]

In fact it isn't based on ZFC, because that would be extra work and in the context of Lean there is no real need to do it.

[Daniel Ever]

ok, that makes things easier, thanks!

[Damiano Testa]

My understanding is that you use a language, like Lean, to give instructions to a computer to perform some sequence of operations. While I may have an interpretation of what Lean is checking, ultimately the computer converts everything to machine language. At that level, I certainly do not know the foundations/meaning of the instructions,, but that does not prevent me from thinking that I know what is going on at the very abstract mathematical level.

Where you draw the line between what you think you understand and what you assume as obvious is a very personal and subjective choice.

[Kyle Miller]

Reid Barton said:

In fact it isn't based on ZFC, because that would be extra work and in the context of Lean there is no real need to do it.

This raises the question, though, of whether we'd be able to trust that the translation to ZFC preserved the meanings of our definitions and theorems. What if the elaborator is generally good at catching errors, so the translation is rarely checked, and no one notices that the kernel is basically getting statements in the Falso axiomatic system for complicated enough statements? That's one reason, beyond extra work, to have the frontend and backend use similar formal systems.

Granted, I've never checked what the Lean kernel sees even once!

[Mario Carneiro]

The easiest way to fix this issue is to actually look at the results (and set up the translation so that the results are lookable)

[Mario Carneiro]

you only need to verify that the axioms are good, no extra axioms have snuck in, and the statements of theorems are good. This last bit is the hardest, especially because lean has lots of fancy implicit stuff, but presumably a proof of false would stick out. Well, if you are trying to defend against Falso then looking at the axioms is enough, but the dual of that (Trutho?) would be if every statement translates to True, so even though the axioms are fine you aren't proving anything of interest