3 ms·
> It seems strange to me that there isn't one standard system. It would be much stranger to me if there was only one. These formal systems are much like progr
by tromp 3y ago
> It seems strange to me that there isn't one standard system.
It would be much stranger to me if there was only one.
These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites.
Where programming languages can be based on procedures, objects, or functions, proof systems can be based on set theory, on simple type theory, or on dependent type theory.
In his comparison of formal systems [1], Freek Wiedijk identifies no less than seven ways to represent mathematics.
[1] https://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf https://www.cs.ru.nl/F.Wiedijk/comparison/diffs.pdf
- riku_iki 3y ago> These formal systems are much like programming languages, and just like those, come in many flavors, appealing to different appetites. and they all compile into the same fol/hol assembly (e.g. Isabelle translates its languages to fol and uses E for actual theorem proving, and E knows nothing about Isabelle language coolness), so in theory they should be able to integrate nicely. My understanding is that the problem is they formalize in different mathematical foundations/axiomatic theories, but I am not an expert in this.