mathematical objects dont exist until you construct themplatonists btfonominalists btfop.s. proof by contradiction is mostly overpowered bullshit
>>16847997Construct a point then. I'm waiting.
>>16847999The compass did punch a pretty big hole in the paper. You could fit a lot of points in there.Can I use the Axiom of Choice?
>>16847999Make a dot or point and label it with a letter.
>>16848005A hole is a point? Where do I see this stated in Euclid's Elements?>>16848007What does "make a dot" mean? And how would me labeling something equate to constructing it?[math]\mathbb{R}[/math]There, I just constructed the real numbers.
>>16848014"Construct" and "define" are essentially synonyms in this context.I define a point at location (0,0) and I have therefore constructed it.
>>16848014>A hole is a point? Where do I see this stated in Euclid's Elements? No, you doubleplusnotfun moron. The physical compass left a hole in the paper that is larger than a point. I have too many options, so I asked to use AoC.JHFC, you are stupid.
>>16848015What's a "location"? Where does Euclid define a location? Your definition of a point means it's crucial for me to know how a location is defined.>>16848016You still haven't told me what a point is so the phrase "larger than a point" is meaningless.
>>16848017>You still haven't told me what a point isGoddamn you are stupid. I am constructing it, not defining it.Your fucking thread and you have a goldfish brain. Memory like a sieve.You suck at this.
>>16848019You are constructing a point by punching a hole into a paper? Alright. So if I choose to do Euclidean geometry on sand like the actual Greeks did it, then I suddenly have no points. Wat nou?
>>16848017Define an arbitrary location. For any location X I can define a point (0,0).
>>16848020The little divot in the sand, but it's too big too. Too many points fit in there.
>>16848021>define a location>NO U>>16848022So both a hole in the paper and a divot in the sand are points? Are you going to come up with a new definition every time someone tries to do geometry in a new setting? What's next, a point is a struct in C?
>>16848032No, the hole in tje paper and the divot in the sand are too big and have lots of points. Too many, like way too many.Is the axiom of choice ok to use?
>>16847997>mathematical objects dont exist until you construct themPartly true, but they are also known eternally by God's intellect.Also how does this btfo the nominalist?
It's funny because it's just OP and Tony in his head.
>>16848035>How many angels can dance on the head of a pin?
>>16848041Since both are point masses, we really need to know the relative spread rates of their respective wave functions.We can wait for you to get those if you like.
>>16848014You absolutely can construct the real numbers using Dedekind cuts.
>>16848044>a point is a point massMy man is huffing that circular reasoning hard.>>16848045I know. Or as a Cauchy completion of the rationals treated as a metric space. There are many equivalent constructions.
>>16847997>dont exist>existCare to define "exist"?
>>16848038Because mathematical objects do exist but they simply must be constructed to exist.
>>16848048That which is concretely instantiated.
>>16848047Angels, euclidean points, and photons are all point masses. If you choose to conflate euclidean points with point masses en masse then you are being foolish at best. Trollific at worst.
>>16847997We invent axiomsWe discover everything else deductive reasoning.
>>16848040
>>16848051>a point is a point
>>16848053else with*
>>16847997just put a global choice function T on the universe of discourse and define "There exists x such that P(x)" as a shorthand for P(T(P)), problem solved (this was shown by Paul Bernays to be conservative over predicate calculus and, when set theoretical axioms are added, it was shown to be conservative over ZFC, for exemple by V.N. Grishin).
>>16847999You have never once read the introduction to any maths textbook, have you?
>>16848055Your choice.
>>16848058I have certainly read Euclid's Elements. It says>a point is that which has no partWhich begs the ultimate question of what the fuck is a part? Case in point, Euclid would fail his dissertation if he had to write up to today's standards.
>>16848062>a point is that which has no partSounds like you bought a cheap translation.
>>16848063σημεῖόν ἐστιν, οὗ μέρος οὐθέν
>>16848063There are two ways to read old texts. You can let someone else think for you and just read the contemporary translation that's most widely accepted, or you can get to know the psyche of the author by considering the context of the literature and trying to reverse engineer how they came up with the original idea in the way you imagine they probably really meant, which may or may not line up with whatever is widely accepted in contemporary society, and you may or may not be branded a schizo for having a divergent thought in your mind when you encounter people that just want to fit into society more than they want to be accurate in their knowledge of reality.
>>16848049oh, based, fuck nominalists
>>16848120OP did neither one of those. A coin lands on edge. Checkmate.
>>16848055I dont get it why is Mr. Incredulous so mad?
>materialists once again fail to consider the monadI love God
>>16848049What do you mean by "exist?" One COULD argue existence as "the manifest", or one could argue existence as being per se (i.e. "the manifest AND the unmanfiest"). Your premise is vague and misleading; indicating nothing certain while maintaining a clear bias.
>>16847997Abstractions don't exist, unless you abuse the word "exist" to mean "conceived", which isn't what 'exists' means.
>>16848336See: >>16848316
>>16848338Only a concrete state of affairs that is objectively true exists.
>>16847997how do I construct addition
>>16848375Endow a set with abelian group structure.
>>16848336Abstractions are mental constructs we derive from sense data. These abstractions do not exist by themselves but can be instantiated once we construct them.
>>16848546>These abstractions do not exist by themselves but can be instantiated once we construct them.You can shape something that exists into a form where your abstraction becomes applicable, but that doesn't make the abstraction real. But you can't construct mathematical objects in that way. The construction of mathematical objects is itself abstract.
>>16848569The constructions are always concrete. Whenever you show how to construct an equilateral triangle, you get a real instance of an equilateral triangle, but one derived from your abstraction of other instances of equilateral triangles you encountered in the world.
>>16848761>he doesn't understand the difference between a triangle-shaped physical object, a triangle and the idea of constructivism
>>16848379I can tell your group isn't well endowed
>>16848375the successor function
>>16847997math is a language used to describe the physical world AND the hypothetical world. Are you saying circles didnt exist before math was invented? you are an idiot and this thread is toilet water. kys
>>16849039A circle is an abstraction derived when we encounter circle-like objects in the world.
dude, are you nuts? logically, when we speak of circles we already use the existential quantifier "there exists", so to have a subject in order to form the sentence around it. if we speak of any other type of existence the terms must be defined well, meaning what circle is, and circle is a shape, so the question boils down to whether or not shapes exist, and the elephant in the room (i.e. the tautology) here is again the existential quantifier that we used to ask the question "do shapes exist". this game of whether or not math objects are created or discovered, i.e. constructed or already existing, is a religious myth type bullshit people created to wonder about the existence of something perfect where existing is ill defined phenomenon. they just felt 'spiritual'
>>16849664But in order to show that circles exist you must prove they exist, and to do that you show that it is possible to construct one.
>>16848049You failed peekaboo
words don't exist until you construct them
I love Euclid
Irregardless of whether meth is invented or discovered, contructed or conceived, it helps me solve the problems I want, and that's all that matters.
>>16847997If I drop this drawing everyone's car explodes
>>16847997ZFC will never recover after this one lads
>>16847997Am i really supposed to take a man norwoodin' this hard seriously?I think not.
whatever iq you have it is directly analogous to the iq at which entertaining hypotheticals or the perfect tense becomes impossible, but for instance of
>>16847997everything already exists in the space of possibilities, it just remains to be discovered
>>16848316nothing we'll ever come up with can ever be demonstrated it didn't exist before. we have no clue what else is out there who already did all this shit. everything is discovered, not "created"
>>16851491ZFC holds in the constructible universe though
>>16852570>ZFC>C>constructible universelove choice, but it ain't constructive my dude
>>16852921constructible universe doesn't merely satisfy C, it has a global choice function -- you can well-order your constructions
Fuck set theory anyway.Can we PLEASE move on to HoTT with univalent foundations? ZFC+AC is so fucking outdated and always has been. Even from fucking day one there was pushback, but here we are because of fucking politics, not because of logic or science.
>>16847997Are the mathematical objects in the room with us now?
>>16853399>the manifold is right there in the corner. can't you see it??
>>16853399I'm replying to one right now. It seems to be converging into some kind of "asshole" function.
>>16853416Im going to throw a kinematics equation at you so hardHereImagine it
>>16853477alright that one got me lmao
>>16848045I am from Missouri, so you are going to have to show me and do dedekind cuts until you have posted all the real numbers ITT.
>>16853273Axiom of Constructibility isn't strictly constructive, see Ferrier, "Against the iterative conception of set".
>>16853297Not only HoTT is extremely crippled in terms of what can you achieve in it but worse, the entire idea that things like that would be less prone of contradiction because they have less (dangerous, or speulative) assumptions than set theory is an outright LIE.For instance there is an axiom-free proof of the consistency of the whole Zermelo set theory in Coq/Roq (and if you add some official variant of axiom of choice you get the same result this time for ZF, hence ZFC). And using Friedman A-translation you can even establish that whenever these classical frame for maths prove/disprove termination of Turing machines, Coq does exactly the same for the same machine.Sentence that aren't of this kind talks about the metahysical infinite and thus aren't constructive in any meaningful way (numbers above 2^(2^(2^(2^(2^(2^2)))))) are already 100% metaphysical, imagine anything beyond lol).
Euclid bros have been crashing out since Frege LMAO
>>16849664Hilbert solved this conundrum 100 years ago by introducting his formal choice function "epsilon term". Assuming the universe of discourse is not empty, for every formula P and every letter x, e(x,P) is a new term where x is bound. It is just a new name for some object in the universe. Then you can use in reasonings freely as axioms any sentence of the type P[x:= t] => P[x:= e(x, P)], as long with any tautology and the following inference rule: whenever A and ((~ A) \/ B) ar proven, B also is. With that you cannot prove anything than tautologies (Hilbert's first epsilon theorem). "there is a x such P" is merely an abbreviation for P[x:= e(x,P)]. No more panic about "muh huh I don't have the right to talk about that thing I haven't proven the existence yet".
>>16854598Then why do most proof assistants work on type theory based languages and not set theory? Hey, guess what, because set theory is fucking old and stupid and type theory is not. It is an analytical, constructive language by design. Set theory is not.
>>16849166A circle is what they saw when they looked up[ art the sun and moon. What is the difference between a circle and circle like object retarded psued and if you say perfection, while having ?plato btfo" in your op it wont surprise me in the least because this board is nothing but retards
>>16847997>mathematical objects dont exist until you construct them
>>16855726Does he concur?
>>16855229>Then why do most proof assistants work on type theory based languages and not set theory?This is mainly for historical reasons. Proof assistants development has been following closely the development of the Curry-Howard corrspondence which has been found first for typed lambda calculus, relating it to intuitionnism circa 1970 where the computing world became overly obsessed with types (up to the point they forgot a type is nothing more than a mere comment over a code, to be washed out by the compiler at the end).In 1990 Timothy Griffin discovered that scheme's call_cc was typable by ((A -> B) -> A) -> A, unlocking the possibility of classical logic calculi performing baktracking (like in real programming where there is no duty to stick all the time to pure typed functionnal programs, and side effects count) one year after COQ was made public and had the latter been issued one year later things would have been very very different.
>>16856007>In 1990 Timothy Griffin discovered that scheme's call_cc was typable by ((A -> B) -> A) -> A, unlocking the possibility of classical logic calculi performing backtrackinghuh, neat
