2 ms·

All formal systems have their limitations as far as what is provable. Example:, for any statement A unprovable in a particular formal system F , there are,

All formal systems have their limitations as far as what is provable. Example:, for any statement A unprovable in a particular formal system F , there are, trivially, other formal systems in which A is provable (take A as an axiom). On the other hand, there is the extremely powerful standard axiom system of Zermelo-Fraenkel set theory (denoted as ZF, or, with the axiom of choice, ZFC), which is more than sufficient for the derivation of all ordinary mathematics. Now there are, by Gödel’s first theorem, arithmetical truths that are not provable even in ZFC. Proving them would thus require a formal system that incorporates methods going beyond ZFC. There is thus a sense in which such truths are not provable using today’s “ordinary” mathematical methods and axioms, nor can they be proved in a way that mathematicians would today regard as unproblematic and conclusive.

guerrilla 6y ago
This is well known. Type theories also do not assume the law of excluded middle. What's your point and it's relevance to the comment?
jkhdigital 6y ago
The issue is not one of “power”—one can make almost any formal system sufficiently “powerful” by adding a few axioms that get you over the rough spots in your proofs. The problem is that the modern world increasingly relies on mathematics, in nearly all aspects of life, to make consequential decisions about how to interpret data and act on it. The challenge is not one of power, but of fidelity—using a mathematical structure that is a suitable abstraction for the real world situation. Use the wrong abstraction, and you end up with paradoxes like the incompleteness theorems. I believe a goal of univalent foundations is to make the abstract structure that one is working with absolutely explicit, evidenced by the (almost) total absence of axioms from the system. If you want to work in ZFC, you can add those axioms yourself.

guerrilla 6y ago

This is well known. Type theories also do not assume the law of excluded middle. What's your point and it's relevance to the comment?

jkhdigital 6y ago

The issue is not one of “power”—one can make almost any formal system sufficiently “powerful” by adding a few axioms that get you over the rough spots in your proofs. The problem is that the modern world increasingly relies on mathematics, in nearly all aspects of life, to make consequential decisions about how to interpret data and act on it. The challenge is not one of power, but of fidelity—using a mathematical structure that is a suitable abstraction for the real world situation. Use the wrong abstraction, and you end up with paradoxes like the incompleteness theorems. I believe a goal of univalent foundations is to make the abstract structure that one is working with absolutely explicit, evidenced by the (almost) total absence of axioms from the system. If you want to work in ZFC, you can add those axioms yourself.