4 ms·
Mathematicians consider that there are "true" propositions of the form procedure P on input x does not halt but the propositions are not provable in ZFC.
by ProfHewitt 7y ago
Mathematicians consider that there are "true" propositions of the form procedure P on input x does not halt but the propositions are not provable in ZFC.
- bjornsing 7y agoSure, such statements exist. But would a mathematician consider one of them true without a proof of some sort? (Nope.)
- ProfHewitt 7y agoMathematicians consider them to be true because they are provably true, i.e., they hold in the unique up to isomorphism model of the theory Ordinals, which subsumes ZFC.
- bjornsing 7y agoOk, so Ordinals is the new foundation of mathematics so to speak? Doesn’t that mean that all of mathematics can be formalized within this Ordinals theory?
- ProfHewitt 7y agoAll of classical mathematics before 1930 can be formalized in the the theory Ordinals. However, formalizing digital computation requires the theory Actors, which is axiomatized here: https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3459566 https://papers.ssrn.com/sol3/papers.cfm?abstract_id=3459566
- bjornsing 7y agoWow. Thanks.