Math went on because it doesn’t matter. Nobody cares about incompleteness. If you can prove ZFC is inconsistent, do it and we’ll all move to a new system and most of us wouldn’t even notice (since nobody references the axioms outside of set theorists and logicians anyway). If you can prove it’s incomplete, do it and nobody will care since the culprit will be an arcane theorem far outside the realm of non-logic fields of math.
You wouldn’t even notice if some proof is wrong because it relies on an inconsistency that’s the issue. And that’s before you didn’t notice because noone builds anything on axioms but instead uses fragile foundations made of intuition, hand-waving, and mass psychology.
Incomplete is fine that’s exactly what constructive maths is doing.
You wouldn’t even notice if some proof is wrong because it relies on an inconsistency that’s the issue.
You wouldn’t notice because there’s no realistic chance that any meaningful result in the vast majority of math depends strictly on the particular way in which ZFC is hypothetically inconsistent.
And that’s before you didn’t notice because noone builds anything on axioms but instead uses fragile foundations made of intuition, hand-waving, and mass psychology.
This is a ridiculous attitude. Nobody uses the axioms of ZFC directly because that would be stupid. It’s obviously sufficient to know how to do so. There is literally no difference to the vast majority of all math which particular axiomatic formalism you decide to use, because all of those results are trivially translatable between them.
Hence why what you’re saying is stupid. You might as well say “all computer science should be done in binary.” What you’re saying is completely unreasonable and has no bearing on actual mathematics.
Are you saying that the proofs of the four colour theorem aren’t proofs, aren’t mathematics, or something to that effect?
And no, working in Coq (as Gonthier did) is quite different from punching holes into cardstock. CS loves abstraction, all those Type Theory based systems basically look like functional programming languages and are just as ergonomic. Because they are functional programming languages (with fancy-pants type systems).
And by denying those systems you then are also denying the value of category theory because there’s some rather strong isomorphisms between those systems. Are you sure you want to throw all that maths out of the window just to be salty on the internet?
Are you saying that the proofs of the four colour theorem aren’t proofs, aren’t mathematics, or something to that effect?
No, and I can’t see how a reasonable person would think I’m saying anything like that.
And no, working in Coq (as Gonthier did) is quite different from punching holes into cardstock.
I didn’t say anything to that effect whatsoever.
CS loves abstraction, all those Type Theory based systems basically look like functional programming languages and are just as ergonomic. Because they are functional programming languages (with fancy-pants type systems). And by denying those systems you then are also denying the value of category theory because there’s some rather strong isomorphisms between those systems. Are you sure you want to throw all that maths out of the window just to be salty on the internet?
Who are you talking to? What is this fucking insanity?
No, and I can’t see how a reasonable person would think I’m saying anything like that.
So now you do consider working in CoC to be a reasonable way to do maths. Thus, we have a contradiction. Thus, you make no sense. QED.
I didn’t say anything to that effect whatsoever.
You said “in binary”. Peolpe haven’t done that since the days of hand-punching things into cardstock. Which is, precisely, working in binary. Don’t ask me whether a hole is a 0 or 1 I’m not from that era.
So now you do consider working in CoC to be a reasonable way to do maths. Thus, we have a contradiction. Thus, you make no sense. QED.
I never said otherwise you literal lunatic. I said it would be completely unreasonable to “just rewrite the whole thing in rust CoC.” The vast majority of all math has literally nothing to do with nitpicky foundations issues.
You said “in binary”. Peolpe haven’t done that since the days of hand-punching things into cardstock. Which is, precisely, working in binary. Don’t ask me whether a hole is a 0 or 1 I’m not from that era.
I can’t have this conversation with someone who can’t read.
Math went on because it doesn’t matter. Nobody cares about incompleteness. If you can prove ZFC is inconsistent, do it and we’ll all move to a new system and most of us wouldn’t even notice (since nobody references the axioms outside of set theorists and logicians anyway). If you can prove it’s incomplete, do it and nobody will care since the culprit will be an arcane theorem far outside the realm of non-logic fields of math.
You wouldn’t even notice if some proof is wrong because it relies on an inconsistency that’s the issue. And that’s before you didn’t notice because noone builds anything on axioms but instead uses fragile foundations made of intuition, hand-waving, and mass psychology.
Incomplete is fine that’s exactly what constructive maths is doing.
You wouldn’t notice because there’s no realistic chance that any meaningful result in the vast majority of math depends strictly on the particular way in which ZFC is hypothetically inconsistent.
This is a ridiculous attitude. Nobody uses the axioms of ZFC directly because that would be stupid. It’s obviously sufficient to know how to do so. There is literally no difference to the vast majority of all math which particular axiomatic formalism you decide to use, because all of those results are trivially translatable between them.
Then go ahead, reformulate everything in CoC or HoTT or similar. I’m waiting. Prove it trivial, prove that what you did is actually consistent.
Hence why what you’re saying is stupid. You might as well say “all computer science should be done in binary.” What you’re saying is completely unreasonable and has no bearing on actual mathematics.
Are you saying that the proofs of the four colour theorem aren’t proofs, aren’t mathematics, or something to that effect?
And no, working in Coq (as Gonthier did) is quite different from punching holes into cardstock. CS loves abstraction, all those Type Theory based systems basically look like functional programming languages and are just as ergonomic. Because they are functional programming languages (with fancy-pants type systems).
And by denying those systems you then are also denying the value of category theory because there’s some rather strong isomorphisms between those systems. Are you sure you want to throw all that maths out of the window just to be salty on the internet?
No, and I can’t see how a reasonable person would think I’m saying anything like that.
I didn’t say anything to that effect whatsoever.
Who are you talking to? What is this fucking insanity?
So now you do consider working in CoC to be a reasonable way to do maths. Thus, we have a contradiction. Thus, you make no sense. QED.
You said “in binary”. Peolpe haven’t done that since the days of hand-punching things into cardstock. Which is, precisely, working in binary. Don’t ask me whether a hole is a 0 or 1 I’m not from that era.
I never said otherwise you literal lunatic. I said it would be completely unreasonable to “just rewrite the whole thing in
rustCoC.” The vast majority of all math has literally nothing to do with nitpicky foundations issues.I can’t have this conversation with someone who can’t read.