Which will be in the future the basis of modern mathematics, brainlet ZFC or anti-tranny HoTT?

[Anonymous No.15058136]

ZFC is old and archaic and has many flaws.

On the other hand, HOMOtopy type theory's basedness is off the charts: https://github.com/HoTT/book/pull/1101#issuecomment-1065813889

[Anonymous No.15058137]

>>15058136
for the zoomies: i'm talking about the foundations of mathematics

[Anonymous No.15058269]

Mathematics doesn't need a basis unless you're a robot. If you need to communicate mathematics to robots, then type theories such as HoTT are more suitable.

[Anonymous No.15058323]

>>15058136
The future will be press button and wait for AI to find solution

[Anonymous No.15058361]

>>15058269
What are numbers then? What's a function? You need some foundation upon which you can such questions.

[Anonymous No.15058379]

>>15058361
Foundations don't answer those questions.

[Anonymous No.15058416]

>>15058379
Yes it does, you can model arithmetic with sets and you can define functions as sets.

[Anonymous No.15058418]

>>15058416
That only changes the question to "What's a set?"

[Anonymous No.15058596]

>>15058136
Wait, is HoTT anti-tranny or pro-tranny? I haven't looked into it, but since it seems to be in the realm of things like category theory, I thought it would be something trannies would flock towards.

[Anonymous No.15058687]

>>15058418
The more general the axioms, the better contrarian bait retard

[Anonymous No.15058734]

>>15058687
So what's a set?

[Anonymous No.15058845]

>>15058269
Agreed on the highest level, but there is still value in formalizing mathematics -- the formal system won't derive every possible truth, but everything derived by the formal system is true

[Anonymous No.15058873]

>But like, what ARE NUMBERS, bro?
Why did the men of the 17th and 18th centuries who did calculus not bother with this shit? Why did they not need it if it is so "fundamental?"

[Anonymous No.15059178]

>>15058873
Because Eudoxus had already bothered figuring out how irrational numbers worked a long long time ago, and it was not yet fashionable to reinvent things that had already been invented with "more rigor."

[Anonymous No.15059462]

Is it possible to formulate the continuum hypothesis in HoTT? If so, it's the same infinitist garbage.

[Anonymous No.15059519]

>>15058596
It became pro-tranny after they adopted the new Coc (Code of Conduct). See OP's linked thread.

[Anonymous No.15059692]

>>15058687
You are not generalising anything if the axioms are equivalent. You could a build ZFC-equivalent system using numbers as the fundamental structure rather than sets. It doesn't make a difference, it's juts shifting the question.

[Anonymous No.15059694]

>>15058873
Because they just assumed a significant property of real numbers: completeness.
Real numbers don't exist in real and world and that's a perfectly valid question. Here's a question for you: what does it mean to raise a number to an irrational power?

[Anonymous No.15059697]

>>15059694
no numbers exist in real

[Anonymous No.15059760]

>>15059697

[Anonymous No.15059764]

>>15059760

[Anonymous No.15059936]

>>15058136
>anti-tranny HoTT
You're aware that HoTT internet is unironically dominated by trannies and there's another rage drama event involving trannies ever month!?
I mean Schulman was cenceled from conferences even

[Anonymous No.15059957]

>>15058734
"X is a set" is shorthand for that ∃X (Whatever characterises X) is a true sentence of ZFC-set theory.

[Anonymous No.15059959]

>>15059957
>true sentence of ZFC-set theory
What does it mean for a first order sentence to be "a true sentence of ZFC-set theory"? What characterizes true sentences of ZFC set theory?

[Anonymous No.15060026]

>>15059959
anon misspoke, he should have said "is a consequence of ZFC-set theory"
>what does it mean to be a consequence of ZFC-set theory?
Can be derived from the ZFC axioms in a formal proof system -- two of which are the Hilbert and Gentzen proof systems for predicate logic.
Alternatively, a sentence for which every model of the ZFC axioms satisfies that sentence
>What does it mean to satisfy a sentence?
https://en.wikipedia.org/wiki/Semantic_theory_of_truth#Tarski's_theory_of_truth

[Anonymous No.15060033]

>>15059764
What is that supposed to represent in real life? What is the root 2th post in this board?

[Anonymous No.15060066]

>>15060033
>What is that supposed to represent in real life?
finitists BTFO

[Anonymous No.15060114]

>>15060066
What is that? I don't understand what little square pixels in a screen would have anything to do with irrational numbers.

[Anonymous No.15060182]

>>15060114
It's the ratio itself retard.

[Anonymous No.15060185]

>>15060182
Ratio of what? What exists in real life that has irrational ratio anon? Please do give an example.

[Anonymous No.15060478]

>>15060185
Take any length that you wish from real life, I transform it into a unit that will make it irrational, so there's an irrational number as measured by my unit in real life. QED. Where's my Nobel's Prize in philosophy?

[Anonymous No.15060493]

The real question is humanity supposed to keep up with all the "required" knowledge needed as technology advances, which is increasing at an alarming rate.

[Anonymous No.15061168]

>>15058136
I go to Western University, many of the topology professors specialize in homotopy type theory.

[Anonymous No.15061187]

>>15058596
Used to be heavily anti-tranny, but then Voevodsky died and the tranners flock to feast on his corpse.

[Anonymous No.15061247]

>>15060478
Excellent anon. Just one question, what exactly are you defining this irrational unit as? What length of what object? Surely you have thought that out.

[Anonymous No.15061252]

>>15058416
>you can model arithmetic with sets
It works perfectly fine for finite sets or if you're trying to defining natural numbers in terms of "m-sets." But it's unclear what's even going on with alleged infinite case. Moreso, no one can talk about arithmetic in the alleged arithmetic case. The only thing you get is some construction which is incredibly unclear as to how it relates to the idea of a number and often fails completely as a means to calculate new examples of numbers, or they depend on circular reasoning (no one has ever seen a real number so lets define the infinite sequence which we'd like to be able to find a "real" number at the end to be the "real" number). Meanwhile all the logical problems are handwaved away as these things are merely just given lip service while everyone just treats the arithmetic and existence of such numbers as an "axiom."
>you can define functions as sets.
Ordered pairs in the finite case as a definition is quite intuitive as a special finite list of pairs. However, the "definition" of a "function" as a "set" in any alleged non-finite case are quite problematic as there is no reason to imagine such a thing as a pair. The only things anyone can actually correctly talk about are finitely written expressions like [math] f(x) = x^2 +1 [/math]. However, in this case, one need not even appeal to sets it is solely: given two objects of a specified type, the expression must evaluate uniquely. The only truly tangible and hence meaningful parts of this definition are in the formal arithmetic. The "set" portion of the definition is at best lip service and not necessary. It's meaningless and does not accurately describe the reality of what is usually meant by a "function" like a polynomial or a power series. Everything about a "function" for non-finite cases is entirely in the formal arithmetic and a finitely represented expression given in terms of that arithmetic.

[Anonymous No.15061255]

Mathematical foundations are literally useless for anything other than automated theory proving and philosophy.
There is nothing to discover by going to a lower level.

[Anonymous No.15061291]

>>15061255
same is true of software coding, anon
many many programmers in my generation were filtered by low-level courses in C++, then got to the job where they did client/server and database lookups, which had next to nothing in common with Binary Trees or Linked Lists or ant of that bullshit

[Anonymous No.15061303]

>>15058136
Homotopy doesn't belong in foundations, Observational Type Theory is best.

[Anonymous No.15061314]

>>15058734
that which fulfills the ZFC axioms.

[Anonymous No.15061317]

>>15061252
You're genuinely retarded and a disgrace to finitism. Stop muddying the waters with your braindead babble, Hilbert is rolling in his grave right now.

[Anonymous No.15061334]

>>15061255
Automated theory proving i.e. making sure your program runs without bugs, is what you do as a programmer.