6 ms·

Let me try to reconstruct what has been said. You seem to be reacting to points different from the one I tried to make. bjornsing: All of mathematics can in pr

Let me try to reconstruct what has been said. You seem to be reacting to points different from the one I tried to make. bjornsing: All of mathematics can in principle be derived from ZFC. morelisp: not all, there are independent statements. Mathematics is beyond formalization. bjornsing: like what? are you saying that formalization is futile? or not? me: CH is an example. formalizing is not futile, but affected by incompleteness theorems in the sense that all those proof assistants, when used for developing some theory, will require something else to prove the consistency of that theory. dwohnitmok: the point of incompleteness is not that it requires a stronger system, but that a weaker system cannot prove a stronger system, killing the idea of trusted computing base. See, I was not trying to expound the significance of the Second Incompleteness Theorem; I do not really care what mathematicians consider as in or out of "all mathematics," but I noticed that "being able to formalize all mathematics" has become a somewhat technical expression in logic. I like very much what you're writing in that comment. I have also seen Gentzen's consistency argument for PA and think the qualification that you include at the end about weaker systems sometimes being able to show the consistency of stronger ones is needed. I did not imply that proving consistency of X within X is desirable. However, I am intrigued by Artemov using a provability operator to prove consistency of PA in PA: https://arxiv.org/abs/1902.07404 https://arxiv.org/abs/1902.07404 Provability logic is interesting, a modal logic that adds Loeb's theorem as axiom (maybe Carl Hewitt would consider it a foundation of computer science? but I digress.) Now, the reason I feel compelled to comment back: I do not understand why you bring up completeness. What are you reacting to? Are you trying to imply that using incomplete foundations is the key to ignore the challenge of proving consistency? Saying "ZFC is enough for all mathematics" is a commitment to ZFC axioms and to first-order logic. First order logic is compact and complete. As such, it is very much affected by the First Incompleteness Theorem and also the Second, and there will also be non-standard models and the Skolem paradox. I don't have a horse in the foundation and formalization race, just curious what you mean. As far as I can tell (and I may well be off, not a mathematician), it seems quite desirable that foundations worthy of the name would let us prove all theorems of arithmetic and natural numbers.

dwohnitmok 6y ago
I hope that this comments this finds you even if it is some days after your original reply; I didn't have time the last few days to write a thoughtful reply that I think your comment deserves. I think the crucial part of bjornsing's original question is "Can you give an example of a statement that is independent of ZFC yet useful/often-used?" As such CH is not, in and of itself, an obvious answer to bjornsing's original question since there hasn't been a case to be made that CH is useful/often-used. Now there can be a case to be made that CH (or its consequences) are indeed useful/often-used, but that is not obvious and probably would need further exploration to convince bjornsing (certainly I personally find it arguable, potentially convincingly so, but nonetheless far from settled). That is, the way I interpret bjornsing's original intent is, "okay so [syntactic] incompleteness is theoretically a thing, practically what impact does it have on current attempts at formalizing mathematics?" And that impetus to explore the practical impact of the incompleteness theorems is what I'm jumping off of. My central thesis is this: The actual practical process of the formalization of mathematics in the last few decades, as exemplified by proof assistants, is minimally affected by syntactic incompleteness (i.e. Godel's incompleteness theorems). Your comment > Today, when people say "you can formalize all mathematics" post Gödel, it means you pick your area and formalize away, knowing that effectively proving consistency of your formal system (within the same system) is out of reach. So nobody tries to claim "all in one system" but many logics and sets of axioms coexist without there being any distinguished one that is better (in the sense of effectively proved consistent and strong enough to be "useful"). makes me think that you think the diversity of proof assistants and different logics underlying them is due to syntactic incompleteness, when this is not the case. These logics are for the most part bi-interpretable, they are not distinguished by what fragment of mathematics they are capable of formalizing, but rather the different ergonomics of different approaches. In expressiveness they are all basically ZFC (potentially plus some "smallish" large cardinal axiom). And perhaps the big thing is that mathematicians, maybe surprisingly, don't really care about consistency proofs. This is both because mathematicians don't really care about foundations as a whole, but also (and potentially a direct result of) because the vast majority of mathematics proofs are, logically speaking, extraordinarily simple. Even something like Peano Arithmetic is way overkill for most proofs out there, so Godel's incompleteness results, even in theory, have much less impact than might be assumed. > I do not understand why you bring up completeness. What are you reacting to? Are you trying to imply that using incomplete foundations is the key to ignore the challenge of proving consistency? I didn't really mean to bring up completeness when I linked to my previous comment, I meant more to talk about the "reverse" direction of consistency that is important for the second incompleteness theorem (rather than proving the consistency of the theory in question itself). However, now that the cat is out of the bag, I will secondarily state that I think semantic completeness (Godel's completeness theorem) is in fact a more influential factor behind different philosophies of formalization than syntactic incompleteness (I will go as far as to say that any human system for the foundations of mathematics implicitly assumes semantic completeness to hold, which I won't elaborate in this already long comment, but can in a reply if you would like). > First order logic is compact and complete. As such, it is very much affected by the First Incompleteness Theorem and also the Second, and there will also be non-standard models and the Skolem paradox. Semantic compactness and completeness are entirely independent of Godel's incompleteness theorems. There are theories which are semantically complete and syntactically incomplete and vice versa (as well as theories that are both semantically and syntactically incomplete or both semantically and syntactically complete). As an aside it is also weird to talk about first order logic being affected by the incompleteness theorems because the incompleteness theorems refer to specific theories within a logic rather than the logic itself. Godel's incompleteness theorems are instead closely tied to arithmetic, in particular arithmetic's peculiar property that any natural number in the metatheory can be translated to a natural number in the object theory, while preserving the usual arithmetic operators, by finite application of the successor function. Moreover non-standard models and the Lowenheim-Skolem theorem both affect first-order theories "from the outside" so to speak, but don't really affect them "from the inside." That is if you're using a proof assistant, you can never observe consequences of those non-standard models while you're formalizing things. > Saying "ZFC is enough for all mathematics" is a commitment to ZFC axioms and to first-order logic. Perhaps I should qualify my previous statement. When I said "ZFC would be enough to do the overwhelming majority of modern mathematics" I really do mean "modern" here. It's possible that future mathematics will require a different axiom system. My point was simply that basically none of the problems people in the field of formal proof assistants have right now can be chalked up to anything outside of ZFC or syntactic completeness. If those researchers could magically wave a wand and say "here's a perfectly ergonomic formal proof assistant understandable and usable by any mathematician but oh it's limited to things provable in ZFC" I think they would absolutely elated. Personally, far from being committed to ZFC, I don't actually like ZFC as a foundation of mathematics. However, I dislike ZFC for reasons completely unrelated to syntactic completeness. It's a clunky encoding of mathematics that doesn't reflect mathematicians' intuitions about various different structures. Now I do separately think that first-order logic (or something that obeys Godel's completeness theorem) is essentially a requirement for any system purporting to be a foundation of mathematics, but as I mentioned in an earlier parenthetical, I don't want to delve into that in this particular reply. > As far as I can tell (and I may well be off, not a mathematician), it seems quite desirable that foundations worthy of the name would let us prove all theorems of arithmetic and natural numbers. I agree. I think any mathematician pre-Godel would've wanted this. That being said, my point is that even though this state of affairs is undesirable, it has little practical effect on anything related to ongoing efforts to formalize mathematics.

dwohnitmok 6y ago

I hope that this comments this finds you even if it is some days after your original reply; I didn't have time the last few days to write a thoughtful reply that I think your comment deserves. I think the crucial part of bjornsing's original question is "Can you give an example of a statement that is independent of ZFC yet useful/often-used?" As such CH is not, in and of itself, an obvious answer to bjornsing's original question since there hasn't been a case to be made that CH is useful/often-used. Now there can be a case to be made that CH (or its consequences) are indeed useful/often-used, but that is not obvious and probably would need further exploration to convince bjornsing (certainly I personally find it arguable, potentially convincingly so, but nonetheless far from settled). That is, the way I interpret bjornsing's original intent is, "okay so [syntactic] incompleteness is theoretically a thing, practically what impact does it have on current attempts at formalizing mathematics?" And that impetus to explore the practical impact of the incompleteness theorems is what I'm jumping off of. My central thesis is this: The actual practical process of the formalization of mathematics in the last few decades, as exemplified by proof assistants, is minimally affected by syntactic incompleteness (i.e. Godel's incompleteness theorems). Your comment > Today, when people say "you can formalize all mathematics" post Gödel, it means you pick your area and formalize away, knowing that effectively proving consistency of your formal system (within the same system) is out of reach. So nobody tries to claim "all in one system" but many logics and sets of axioms coexist without there being any distinguished one that is better (in the sense of effectively proved consistent and strong enough to be "useful"). makes me think that you think the diversity of proof assistants and different logics underlying them is due to syntactic incompleteness, when this is not the case. These logics are for the most part bi-interpretable, they are not distinguished by what fragment of mathematics they are capable of formalizing, but rather the different ergonomics of different approaches. In expressiveness they are all basically ZFC (potentially plus some "smallish" large cardinal axiom). And perhaps the big thing is that mathematicians, maybe surprisingly, don't really care about consistency proofs. This is both because mathematicians don't really care about foundations as a whole, but also (and potentially a direct result of) because the vast majority of mathematics proofs are, logically speaking, extraordinarily simple. Even something like Peano Arithmetic is way overkill for most proofs out there, so Godel's incompleteness results, even in theory, have much less impact than might be assumed. > I do not understand why you bring up completeness. What are you reacting to? Are you trying to imply that using incomplete foundations is the key to ignore the challenge of proving consistency? I didn't really mean to bring up completeness when I linked to my previous comment, I meant more to talk about the "reverse" direction of consistency that is important for the second incompleteness theorem (rather than proving the consistency of the theory in question itself). However, now that the cat is out of the bag, I will secondarily state that I think semantic completeness (Godel's completeness theorem) is in fact a more influential factor behind different philosophies of formalization than syntactic incompleteness (I will go as far as to say that any human system for the foundations of mathematics implicitly assumes semantic completeness to hold, which I won't elaborate in this already long comment, but can in a reply if you would like). > First order logic is compact and complete. As such, it is very much affected by the First Incompleteness Theorem and also the Second, and there will also be non-standard models and the Skolem paradox. Semantic compactness and completeness are entirely independent of Godel's incompleteness theorems. There are theories which are semantically complete and syntactically incomplete and vice versa (as well as theories that are both semantically and syntactically incomplete or both semantically and syntactically complete). As an aside it is also weird to talk about first order logic being affected by the incompleteness theorems because the incompleteness theorems refer to specific theories within a logic rather than the logic itself. Godel's incompleteness theorems are instead closely tied to arithmetic, in particular arithmetic's peculiar property that any natural number in the metatheory can be translated to a natural number in the object theory, while preserving the usual arithmetic operators, by finite application of the successor function. Moreover non-standard models and the Lowenheim-Skolem theorem both affect first-order theories "from the outside" so to speak, but don't really affect them "from the inside." That is if you're using a proof assistant, you can never observe consequences of those non-standard models while you're formalizing things. > Saying "ZFC is enough for all mathematics" is a commitment to ZFC axioms and to first-order logic. Perhaps I should qualify my previous statement. When I said "ZFC would be enough to do the overwhelming majority of modern mathematics" I really do mean "modern" here. It's possible that future mathematics will require a different axiom system. My point was simply that basically none of the problems people in the field of formal proof assistants have right now can be chalked up to anything outside of ZFC or syntactic completeness. If those researchers could magically wave a wand and say "here's a perfectly ergonomic formal proof assistant understandable and usable by any mathematician but oh it's limited to things provable in ZFC" I think they would absolutely elated. Personally, far from being committed to ZFC, I don't actually like ZFC as a foundation of mathematics. However, I dislike ZFC for reasons completely unrelated to syntactic completeness. It's a clunky encoding of mathematics that doesn't reflect mathematicians' intuitions about various different structures. Now I do separately think that first-order logic (or something that obeys Godel's completeness theorem) is essentially a requirement for any system purporting to be a foundation of mathematics, but as I mentioned in an earlier parenthetical, I don't want to delve into that in this particular reply. > As far as I can tell (and I may well be off, not a mathematician), it seems quite desirable that foundations worthy of the name would let us prove all theorems of arithmetic and natural numbers. I agree. I think any mathematician pre-Godel would've wanted this. That being said, my point is that even though this state of affairs is undesirable, it has little practical effect on anything related to ongoing efforts to formalize mathematics.