[HN Gopher] 'Equals' has more than one meaning in math
___________________________________________________________________
'Equals' has more than one meaning in math
Author : laktak
Score : 77 points
Date : 2024-06-17 06:42 UTC (2 days ago)
(HTM) web link (www.sciencealert.com)
(TXT) w3m dump (www.sciencealert.com)
| gus_massa wrote:
| In the first year of the University you write cpngruence with
| three horizontal lines. In the second, you just use two lines,
| aka an equal sign. Everyone knows = is overloaded.
|
| The same happens with other signs, like the arrow of limit. In
| many cases it's confusing so you add a small note to the arrow,
| unless it's obvious (whatever that means).
| SassyBird wrote:
| _> In the first year of the University you write cpngruence
| with three horizontal lines. In the second, you just use two
| lines, aka an equal sign._
|
| Obviously in the next step you achieve enlightenment when you
| then write them as just one horizontal line, but most don't
| reach that stage.
| programjames wrote:
| Ah yes, the ~.
| lupire wrote:
| ~ is a -- (em dash) that lacks the courage of its
| convictions.
| dang wrote:
| Related. Others?
|
| _Grothendieck's use of equality_ -
| https://news.ycombinator.com/item?id=40414404 - May 2024 (129
| comments)
|
| _Grothendieck 's Approach to Equality [pdf]_ -
| https://news.ycombinator.com/item?id=31557361 - May 2022 (37
| comments)
| Animats wrote:
| MathCAD once had about four equality symbols. Comparison,
| assignment, identity, and congruence, I think.
|
| Mathematica uses <=> for Boolean comparisons.
| gizmo686 wrote:
| Even general purpose programming languages have this. Java has
| at least 4 as well:
|
| * Assignment (=)
|
| * Referential equality (==)
|
| * Structural equality (.equals())
|
| * Comparison equality (.compareTo(_) == 0 )
| auggierose wrote:
| .equals() and .compareTo(_) == 0 are required to be the same.
| If you program it differently, it is a bug.
| gizmo686 wrote:
| From the javadoc:
|
| > It is strongly recommended, but not strictly required
| that (x.compareTo(y)==0) == (x.equals(y)). Generally
| speaking, any class that implements the Comparable
| interface and violates this condition should clearly
| indicate this fact. The recommended language is "Note: this
| class has a natural ordering that is inconsistent with
| equals."
| auggierose wrote:
| Nice catch. Now you also found buggy documentation /
| specification!
| xboxnolifes wrote:
| Why is it buggy?
| auggierose wrote:
| Why would you allow .equals and .compareTo to have
| inconsistent meanings? That is a guaranteed source of
| bugs. I cannot think of a single good reason to allow
| this. If you need a different order for some reason, that
| is what the Comparator interface is for.
| maxbond wrote:
| If it's a bad idea but considered legal according to the
| documentation, then that would make it a footgun rather
| than a bug, no?
| auggierose wrote:
| Yes, that makes this a footgun, and the specification
| containing this footgun buggy. It is a bug in the spec
| because there is no good reason for the footgun being
| there.
| maxbond wrote:
| You have not yet imagined a reason, and neither have I.
| That doesn't mean one doesn't exist. Likely it would be
| something idiosyncratic involving legacy code that would
| only make sense in a real world context - "we have to
| change the way it sorts to fix ticket ABC123, but we
| can't change the equality, or we'll have a regression of
| ABC456."
| auggierose wrote:
| Then provide a comparator to sort differently, no
| problem.
|
| There will never be a good reason for the spec to be like
| that. Just look how people here justify the mess of
| BigDecimal.
| myrryr wrote:
| Things where equality is on more than one axis, _but
| there is a primary one where people use._
|
| Think things like vectors or complex numbers, or people.
|
| The absolutely classic example however is types which
| have a signed zero...
| auggierose wrote:
| That is not a problem, just pick the same equality that
| your .compareTo method uses.
|
| You could pick -0 < 0, and -0 [?] 0, or -0 = 0. You
| should never pick -0 < 0 (via compareTo), but -0 = 0 (via
| equals).
| tsimionescu wrote:
| It is perfectly reasonable to want all sorted collections
| of X to have a canonical order, but to still allow people
| to consider equivalent items to be equal.
|
| The example someone else gives with +0 and -0 is very
| good: in most contexts, those two should probably be
| equal (+0.equals(-0)), but when sorting a list, you might
| want all -0s to come before all +0s (-0.compareTo(+0) ==
| -1).
|
| Given that Comparable is almost exclusively used for
| sorting, this is actually quite unlikely to cause
| problems in practice.
|
| Of course, it's a much bigger problem if you use entirely
| different concepts of equality. For example, a Name class
| where a.equals(b) only if they have the exact same
| Unicode code points, but where a.compareTo(b) == 0 if
| they have the same Unicode codepoints after normalization
| would be crazy.
|
| Edit: and of course BigDecimal from the example below
| does exactly this crazy thing...
| auggierose wrote:
| Yep, BigDecimal does this crazy thing, and it shouldn't.
| It does it, because the buggy spec allows it.
|
| If the canonical equality you want to provide is not
| compatible with the canonical order you want to provide,
| then don't provide the canonical order. Or provide an
| order that is compatible, which makes it pretty much
| canonical. It is really simple, and going against simple
| things like that is why software is such a mess. Because
| software really allows you to do anything you want. And
| now it is down to you to want the right thing.
| maple3142 wrote:
| Hmm, there was an article about Java's BigDecimal behaves
| differently for equals and compareTo:
| https://igorstechnoclub.com/java-bigdecimal/
| auggierose wrote:
| That is a great example why I consider the spec buggy.
| With a proper spec, stuff like that would not fly from
| the start.
| anon291 wrote:
| Trouble arises in any logical system when we start to make
| statements on the system itself. As long as there's a strict
| separation between the target of your logic and the logic itself,
| you can make it all work out, but recursion is what kills you. To
| avoid this, many thinkers have come up with a sort of infinite
| tower of sorts. For example, in ZFC set theory, sets are ordered
| in cumulative ranks. In theorem proving languages like Coq, Agda,
| etc, there are a hierarchy of universes. Even Aristotle's four
| causes can be seen to be a small subset of the infinite hierarchy
| of cause. It's just the nature of logic.
|
| Similarly, there is a hierarchy of equality at increasing
| abstraction levels. There's naive equality which is that two
| things are literally the same. Then there's equality as to the
| 'class' of objects, and we can even go beyond that talking about
| equality of equalities (another word for analogies). Most stop
| there, but you can go on and on and on.
|
| I'm currently interested in homotopy type theory systematizes
| this notion of varying 'levels' of equality, but it too has
| issues. It's an open question.
|
| The article does sensationalize a bit because math is just a
| method of discourse. Equality means different things to different
| fields, and nothing about this kind of equality means that
| previous results are wrong.
| VirusNewbie wrote:
| Unbounded recursion. Not recursion itself.
| anon291 wrote:
| Good point.
| zmgsabst wrote:
| Homotopy type theory isn't magic, but it nicely explores the
| difference between (strict) equality and context dependent
| equivalence. (Okay, technically that's univalence.)
|
| I think HoTT nicely capstones the idea algebra and geometry are
| equivalent by pointing out that semantics itself is defined by
| the topology of categorical diagrams -- and anywhere we find
| compatible topology is equivalent. Neat.
| woopwoop wrote:
| When I took Dan Freed's algebraic topology course, one time he
| asked us if two spaces were the same. Then he looked at us for a
| moment and said that actually that was a "Bill Clinton question:
| the answer depends on what the meaning of the word is is".
| 082349872349872 wrote:
| There's a (n improper) coarsest universe where anything is the
| same as everything else.
|
| (which reminds me of the buddhist monk at the hot dog stand:
|
| -- Make me one with everything
|
| -- Here ya go bud
|
| -- Uhhh ... I gave you a twenty?
|
| -- Change is an illusion )
|
| EDIT: and Ireneo Funes (the Memorious) inhabits that other
| improper, finest, universe where nothing is the same as
| anything else. (OnlyNaNs?)
| vinnyvichy wrote:
| Btw, the following might come across as a little Borgean..
|
| (Author of your Wikisourced cetacean)
|
| https://baike.baidu.com/item/%E4%BD%9A%E5%90%8D/37139#:~:tex.
| ..
|
| (Not a Name)
|
| Yu Gui Shen Tong
|
| "Converse with gods and spectres"
|
| https://www.feirao.com/chengyu/32963S.html
| vinnyvichy wrote:
| My guess is that your cetacean originates from the Sui-Tang
| under a nihilizing influence of Buddhist rationalizations.
|
| "No creation without injury, no injury without creation."
|
| (My interpretation, cf the Japanese distillation)
|
| https://en.m.wiktionary.org/wiki/%E5%89%B5#Japanese
|
| Compare with (note element of chance)
|
| https://en.m.wiktionary.org/wiki/incido
|
| More relevant to thread
| https://en.m.wiktionary.org/wiki/pare
|
| (Vs https://en.m.wiktionary.org/wiki/par#Latin)
| vinnyvichy wrote:
| https://en.m.wiktionary.org/wiki/%D1%83%D0%B4%D0%B3%D0%B0
| %D0...
|
| Note the gender, as well as the Korean
|
| Mudang,https://en.wikipedia.org/wiki/Korean_shamanism
|
| Chinese tongji (manifestly not gendered)
|
| https://en.wikipedia.org/wiki/Tongji_(spirit_medium)
|
| (& Old nordic seidkona apophenically
|
| Proto-tungusic
| https://en.wikipedia.org/wiki/Shamanism#Terminology
| vinnyvichy wrote:
| https://languagehat.com/kolmogorov/
|
| For the folklorists, the comments-readers, the
| invertebrate meme-chasers
|
| >If we're not in pain, we're not alive
|
| https://www.rifters.com/real/Blindsight.htm
| BalinKing wrote:
| Maybe I'm totally lost, but this thread of self-replies
| makes me suspect a Markov chain generated them or
| something like that. The same is true for some--but not
| all--of your other comments, which feels really weird to
| me. Of course, maybe I'm way off base, and what you're
| saying makes total sense and is just going over my head.
|
| I wonder if dang (or another mod) has already seen
| this....
| 082349872349872 wrote:
| I suspect vinnyvichy may have been "conversing with gods
| and ghosts" ... but until I manage to translate that page
| I shan't be sure :-)
| vinnyvichy wrote:
| Indeed I would have most preferred "spirits & spectres"
| because that one has a neutral connotation in Chinese.
|
| The referent of your San Sha Fa , "kill the buddha-
| spirit, kill your demised-forebears"<<Lin Ji Lu >>
| (written back when Taoism had not been fully
| differentiated from Buddhism) was way more suicidal in
| ideation..
|
| The heart of kenshin (or
| https://en.wikipedia.org/wiki/Saiyuki_(manga)):
|
| https://zhuanlan.zhihu.com/p/32380940?utm_id=0
|
| https://academic.oup.com/book/38937/chapter-
| abstract/3381231...
| vinnyvichy wrote:
| Let me prove that I am your curtness-challenged Dwalin :)
| 082349872349872 wrote:
| dwarves delve into discourses by the length of
| their beards not the height of their heads
| bradrn wrote:
| I've also noticed this with vinnyvichy and
| 082349872349872 (who mostly seem to respond to each
| other). Probably it should be reported to dang if it
| hasn't been already.
|
| (The first time I saw it, I wondered if I was going
| insane, because the conversations seemed unrelated to the
| topic and nonsensical in themselves... good to know
| there's nothing I'm missing!)
| 082349872349872 wrote:
| It's a bit like an abacus: the motion of beads on each
| individual rod may not seem to make much sense, but there
| is a meaning to the calculation taken as a whole.
|
| (Hmm: presentation does a great deal for providing
| meaning; imagine a "write-only" tetris game where instead
| of presenting the current state of the playfield,
| completed rows stayed on the display and dropped pieces
| stretched through them to incomplete rows. I think that'd
| be much more difficult than the traditional view)
|
| Lagniappe: https://news.ycombinator.com/item?id=40714981
|
| (Sorry for interrupting your regular HN? Maybe we ought
| to bump up the https://en.wikipedia.org/wiki/Chip_(CDMA)#
| :~:text=The%20chip.... rate and attempt to dive beneath
| the noise floor again?)
| vinnyvichy wrote:
| So your bufferbloat curve comment refers to how
| congestion doesn't depend linearly on symbol rate, e.g
| https://superuser.com/questions/1324956/is-bufferbloat-
| trigg...? Or is there more to it (like hidden Shannon
| assumptions not priced in with the chiprate e.g
| https://news.ycombinator.com/item?id=30130091
| https://phys.org/news/2024-06-cooperation-evolve-limited-
| pay... )
|
| Chemical clocks can get a bit crazier-- there can be much
| randomness, but the number of equivalent ahem pathways
| can be few.
|
| https://pubs.rsc.org/en/content/articlelanding/2015/cp/c5
| cp0...
| mistermann wrote:
| > good to know there's nothing I'm missing
|
| Hmmmm.
| 082349872349872 wrote:
| On a _Blindsight_ tangent, that 's exactly what
| "techniques will occur when a void is found" was about:
| the passive is on purpose, encoding the philosophical
| zombieism of martial zen.
|
| The conscious mind is useful (like s/w for resolving a
| TLB miss) for calculating useful things to have in the
| cache, but in an antagonistic situation, one needs to
| have a high percentage of h/w-served hits.
|
| If one consciously decides to employ a technique, one
| will certainly not surprise oneself, and one will
| probably not (unless one's heart is very spherical
| indeed?) surprise an opponent who is practicing the 3rd
| of the "3 pwns"*.
|
| (indeed, I find the evolutionary just-so for
| consciousness to arise from the 3rd pwn: once one has the
| grey matter in place to model others, modelling oneself
| would be a natural side effect)
|
| * https://news.ycombinator.com/item?id=39898001
| vinnyvichy wrote:
| You shoved everything into the utility functional (god of
| the spectral gap)).
|
| How should one incorporate theories of mind (to all
| orders) into the yu[ ]? (Or You [ ]*) With the
| aforementioned quiver varieties?
|
| *https://en.wikipedia.org/wiki/Y%C5%ABrei Let the holey
| spirit be formless for the now. (Genesis 1:2[?]3)
|
| Looking forward to from https://en.wikipedia.org/wiki/Ze
| n_in_the_Art_of_Archery#Infl...
| 082349872349872 wrote:
| Would that be a physicists/chemists', mathematicians', or
| psychologists' spectral gap? (or is it a mixed state, not
| a pure?)
|
| Glad to see you've found the unicode necessary for the
| naughty part of the AMEN combinators:
| https://www.dcs.ed.ac.uk/home/pgh/arithmetic.lhs
|
| EDIT: > _If we 're not in pain, we're not alive_
|
| I actually saw this non-ironically somewhere ( _The View
| From 80_ perhaps?) in which it was suggested that, after
| a certain age, waking up with pain is a positive sign,
| with the rationale that if some part of your body doesn
| 't hurt, maybe you didn't really wake up after all...
| vinnyvichy wrote:
| Mathematicians', although there IS an equivalent
|
| Physicist-chemist formulation:
| https://www.ncbi.nlm.nih.gov/pmc/articles/PMC9586289/
| https://arxiv.org/abs/1809.10171
|
| 'https://m.youtube.com/watch?v=R3NbM_wzSJ8
|
| And then there is the mixed one which could be
| undecidable. https://en.wikipedia.org/wiki/Yang%E2%80%93M
| ills_existence_a...
|
| RE: "naughty" = labelled "abstossende" by Cantor?
| mistermann wrote:
| > but in an antagonistic situation, one needs to have a
| high percentage of h/w-served hits.
|
| Can you explain "h/w-served hits"? (I am guessing _other
| than_ conscious?)
| vinnyvichy wrote:
| I'm guessing it's about the general rule of thumb that hw
| is faster than sw, and so can react to urgent situations
| in a timely fashion. As for why sw might be shorthand for
| consciousness: sw can modify itself (and thus react to
| strategic issues)
|
| ... so yeah, hw is more or less defined as something that
| cannot modify itself.
| mistermann wrote:
| Firmware is exceptional though.
| 082349872349872 wrote:
| Fair enough, and we could get into microcoded
| architectures too.
|
| But basically the analogy (originally built around TLB
| handling) is supposed to be: software
| slow & flexible conscious response hardware
| fast & inflexible reflex response
|
| We're altricial, not precocial, so over our lifetimes we
| can (and hopefully do) alter many of our own "reflex"
| behaviours. In particular, details of the 4 F's are
| firmware configurable.
|
| Does that make sense?
|
| Lagniappe: https://www.youtube.com/watch?v=__KfrDZoBgQ
| (for mistermann)
| mistermann wrote:
| Yes but "4 F's"?
|
| Also, there's lots of potential for failure (and I'd say
| it is overwhelmingly observable that we have and do) in
| "can (and hopefully do)". Who knows what our absolute
| capabilities are, especially if we hardly _or maybe even
| never_ try (at least certain things)?
|
| Writing the capabilities to firmware is a step after
| this, but only after the first step is accomplished.
| ysofunny wrote:
| whenever peoples ponder what the meaning of "is" is, the
| discussion eventually turns into questioning the meaning of
| "what"
|
| what is "is"?
|
| -- to know what is "what"?
| gizmo686 wrote:
| Terence Tao wrote a blog post years ago dividing math education
| into 3 stages: pre-rigourus, rigourus, and post-rigorous. That
| distinction seems relevent here.
|
| Every mathamatician knows that the integer 1 and the real number
| 1 different objects [0]. We could make every invocation of a
| canonical isomorphism explicit, but that would make all of math
| far too unwieldy to do.
|
| This is the core problem with formal proof verification. Current
| provers need you to prove things at such a low level that they
| are simply unwieldy to use. That does not mean we need to
| reinvent all of math. It means we need to improve formal
| verification tooling. Maybe we also need to train mathamaticians
| in formal verification systems. In much the same way that they
| had to be trained to use computer algebra systems. We didn't
| reconstruct all of math. We just learned how to work within the
| limitations of tools when we use those tools.
|
| [0] Unless you go out of your way to construct them to be the
| same thing. There is not actually any official definition of, for
| example, what the integer 1 is. Since so many definitions of it
| are equivalent, that is a fundamentally pointless conversation to
| have. A few textbook authors need to make a decision for
| pedalogical purposes. No one else cares.
| auggierose wrote:
| I think pretty much every mathematician agrees that you can
| assume N [?] Z [?] Q [?] R [?] C, and that 1 the integer is the
| same as 1 the real number.
| klodolph wrote:
| You have to use a very _funny_ notion of [?] for that to make
| sense. Mathematicians recognize that there is a lot of funny
| business going on behind the scenes... if you use the typical
| construction of these sets, then Z [?] Q is for sure false
| under the set-theoretic definition of what subsets are.
|
| So you are going to get a lot of funny explanations of why
| you can still say "Z [?] Q" and what that means. And what is
| "the same as" anyway?
| interroboink wrote:
| Could you provide an example? I'm not seeing it.
|
| Is there some integer that is not also a rational number?
| klodolph wrote:
| How about this example: the natural number 0 is not a
| member of the integers, from a set theoretic perspective.
|
| In the natural numbers, 0 = {}
|
| However, {} is not an element of the integers.
|
| This is not something I expect to be easy to understand.
| This is the standard set theoretic definition of integers
| that mainstream mathematicians use. This is not some
| esoteric, fringe theory.
| Affric wrote:
| Isn't the empty set a subset of all sets?
|
| A quick look at Wikipedia indicates that there exist
| other constructions.
| klodolph wrote:
| Yes, the empty set is a subset of all sets. I think some
| wires got crossed somewhere because whether zero is a
| subset of some other set doesn't fit into the questions
| we are trying to answer.
|
| You could pick a construction where the natural numbers
| are a subset of the integers. This is trivial, but this
| is a poor strategy overall, because you can always find a
| bigger set of numbers to work with. You can't take the
| "biggest" set of numbers and then define all other sets
| of numbers as subsets of that. It would be kind of like
| trying to count down from infinity.
| Affric wrote:
| I see where I have gone wrong. Element vs subset. Classic
| error when thinking fast. Thank you for the thought
| provoking comments.
| SAI_Peregrinus wrote:
| The Surreal Numbers manage to be a sort of "biggest"
| ordered field, in NBG, though they're a proper class not
| a set. All other ordered fields are subfields of the
| Surreals. Of course "ordered" is doing a lot, since it
| excludes the complex numbers, vectors, bivectors, etc.
| Whether elements of some object that isn't an ordered
| field should be considered "nubmers" is related but
| different question.
| enugu wrote:
| Yes, {} is a subset([?]) of all sets, but it is not a
| member([?]) of all sets. For instance, {} is not a member
| of {{{}}}. In the Von-Neumann definition, 1:={0}={{}}.
| So, 0[?]1, but 0 is not a member of {1} which is the
| above set. https://en.wikipedia.org/wiki/Set-
| theoretic_definition_of_na...
| interroboink wrote:
| Ah, thank you. It does actually make some sense, having
| looked into it some more now (:
|
| It looks like the approach of defining Z in terms of N is
| much more tedious to deal with overall, so can see the
| advantages.
| Cu3PO42 wrote:
| Conceptually, yes, every integer is also a rational
| number. But they are represented as different objects.
|
| It's a bit like saying every int32 is also a double. Yes,
| every value of int32 fits into a double, but the bit
| pattern is different.
|
| The canonical construction for rational numbers is pairs
| (a, b) which we interpret as a/b. An integer k "is the
| same as" (k, 1).
|
| So it might be more correct to say every integer has the
| same value as some rational number. Of course this
| distinction is pointless most of the time, so we don't
| worry about it.
|
| This is not unique to integers and rationals. It also
| applies to naturals and integers, rationals and reals,
| etc.
| pyrolistical wrote:
| But an int32 1 isn't the same as a mathematic object 1.
| So of course your analogy doesn't work
| klodolph wrote:
| By definition, analogies are between things that aren't
| the "same thing".
| Cu3PO42 wrote:
| And a double 1.0 isn't the same as a rational 1/1. But I
| also didn't claim either of these things.
| _nalply wrote:
| I understand that this might be a problem in a
| programming language, even if you decide to ignore that
| mathematical sets have infinitively many elements. When I
| programmed an RPN calculator supporting quotients and
| complex numbers, I had to grapple with the fact that 1
| (one) is a quotient (with denominator 1) and a complex
| number (with imaginary part 0). I solved it by defining
| the functions and operators taking a certain type and
| coercing the arguments to that type. One example, the
| logarithm can take complex numbers. If I had a quotient
| argument, I coerce it to a complex number before passing
| it to the logarithm.
|
| However I assumed that this is only a problem in
| programming languages. I am a bit surprised that
| mathematics also seems to be affected. I am going to
| study it a bit.
| ndriscoll wrote:
| Practical mathematics mostly isn't affected. That's what
| the earlier commenter was referring to with Tao's stages
| of maturity.
|
| In the pre-rigorous stage, you don't know it's an issue.
| In the rigorous stage, you know it's an issue. In the
| post-rigorous stage, you know it's not an issue (i.e. you
| know you know how to write down all the details if you
| needed to, and you know it will all work how you might
| hope it would, and so you don't need to).
| _nalply wrote:
| I think the magic word is: isomorphism!
|
| An isomorphism is a way to relate two different sets such
| that each element is paired with exactly one in the other
| set such that it does not matter if you do operations
| before or after.
|
| In my calculator the set of reals is isomorph to the set
| of complex numbers with imaginary part zero:
| R { c | c [?] C and im(c) = 0 }
|
| So I can coerce to complex numbers without impunity
| because of that isomporphism! And I know it is an
| isomorphism because if adding two reals then coercing to
| complex is the same as coercing first then adding.
|
| TIL: In a way mathematics has types like programming
| languages.
|
| I hope I am not too far off here. I didn't look up
| anything, this all went into my head this morning.
| ndriscoll wrote:
| This is sort of true, but there are isomorphisms which
| aren't "good enough" in some sense. E.g. if you're
| familiar with linear algebra, there's a thing called a
| dual space, which (for finite dimensions) is isomorphic
| to your space, but when you change coordinates, dual
| spaces change their coordinates backwards. Or for complex
| numbers, when you extend R by adding `i` (sometimes
| written C=R[i]), if you look carefully, you'll see that
| you could have instead added an element a = -i, and
| you'll notice that R[a] is isomorphic to R[i] in a way
| where the isomorphism maps R to itself; in a sense you
| can't tell whether you added i or -i, and this degree of
| freedom is important when studying field extensions.
|
| The closest thing I'm aware of to "pretty much equal" is
| "unique up to unique isomorphism", so they may not be
| equal, but they're isomorphic, and there's no flexibility
| to make any choices of which isomorphism to use. But
| "isomorphism" also implies you have a particular
| context/structure in mind that you want to preserve, e.g.
| a set isomorphism (a bijection) may not be a linear
| isomorphism (~an invertible matrix). In practice, you may
| be working in multiple contexts at once, so you invent
| Functors which map one type of morphism to another, and
| now you care about Categories.
| SAI_Peregrinus wrote:
| To expand: they're "equivalence classes". The digit 1
| represents a value, in the same equivalence class as 1/1,
| 2/2, 1.0, 1+0i, {0|}, 1.0+0i+0j+0k, etc. ad infinitum.
| sebtron wrote:
| I don't think it is a "funny" notion of inclusion, but
| rather that once Q is defined, Z is silently redefined to
| be that one subset of Q that was used in the construction.
| klodolph wrote:
| There's a very deep problem with that--every time you
| invent a "superset", do you then have to redefine the
| subset to be a subset of that "superset"?
|
| There is an infinite chain of supersets of the rational
| numbers, real numbers, etc.
|
| Think of it like this... we can define 0, and then define
| 1 as the successor. Repeating this, we can have a
| definition for every finite number. But we cannot do this
| the other way around. We cannot start with [?], define
| the predecessor to [?], and then somehow get back to 0.
|
| In other words, if you want to work backwards and say
| that smaller sets (like the natural numbers) are a subset
| of the bigger sets (like complex numbers), then you have
| to pick a "biggest set" containing all numbers, which is
| unsatisfactory. Somebody always wants a bigger set.
| ysofunny wrote:
| > _There's a very deep problem with that--every time you
| invent a "superset", do you then have to redefine the
| subset to be a subset of that "superset"?_
|
| I have thought about this too, and I'd initially agree
| with you. but I thought at some point how mathematical
| history is not extremely dissimilar from this. put in
| very rough terms:
|
| at first humans discovered/invented numbers (i.e. the
| counting numbers); these started at number one -- the
| first number. later on, at some point we had to go back
| and realize that there was a zero before number one which
| "silently" redefined the first number as zero and this
| created the natural numbers a the modern set-based N
|
| edit: adding this alternative rendering of my intended
| comment triggered by a condescending reply: "mathematics
| silently redefines stuff all the time. deal with it"
| klodolph wrote:
| There is a different answer here which is more
| satisfactory... which is to use notions of equality other
| than set theoretic equality. Which is what the article is
| talking about.
| threatofrain wrote:
| I have the naive feeling that early counting may have
| included 0 as a primitive right from the get-go. The need
| to say "nothing" seems pretty primal.
| Izkata wrote:
| Zero entered western writing systems through India, with
| limited usage in math before that. It seems like it was
| invented/borrowed as part of switching from additive
| numbers (such as Roman numerals) to positional numbers.
| tsimionescu wrote:
| "Nothing" as a concept always existed of course. But it
| wasn't considered a number, generally. Certainly no one
| counted "nothing, one, two", and even today natural
| language doesn't include "nothing" or some equivalent as
| a numeral noun.
| NeoTar wrote:
| You need to be careful about the phrase "considered a
| number" since I believe one, or unity, was also not
| considered a number by some ancient civilisation - i.e. a
| number was only multiple copies of unity.
|
| [I believe this YouTube video goes into more detail in
| its discussion of why 1 was not considered Prime in the
| ancient world: https://youtu.be/R33RoMO6xeA]
| threatofrain wrote:
| That's where I'm quite skeptical. Imagine you are in
| charge of trade or rationing important village resources
| in the winter. It just seems to me almost necessary that
| people would have a way to symbolically indicate that all
| the sheep are gone. As opposed to just not having any
| symbol for that at all.
| Jaxan wrote:
| > There is an infinite chain of supersets of the rational
| numbers, real numbers, etc.
|
| No you only do it for all the sets (of numbers) that you
| are currently working with.
| klodolph wrote:
| You can work with infinitely many such sets at a time.
| sebtron wrote:
| > In other words, if you want to work backwards and say
| that smaller sets (like the natural numbers) are a subset
| of the bigger sets (like complex numbers), then you have
| to pick a "biggest set" containing all numbers, which is
| unsatisfactory. Somebody always wants a bigger set.
|
| Exactly what we did in the Analysis I course I attended
| during my bachelor: defined the reals axiomatically, and
| the N as smallest inductive(?) subset containing 0.
|
| Satisfactory or not, it worked well for the purpose. And
| I actually liked this definition, if anything because it
| was original. Mathematical definitions don't need to have
| some absolute philosophical value, as long as you prove
| that yours is equivalent to everyone else's it's fine.
| klodolph wrote:
| > as long as you prove that yours is equivalent to
| everyone else's it's fine
|
| That's exactly the point I was making in the first place.
|
| "Unsatisfactory" just means "unsatisfactory" in the sense
| that some mathematicians out there won't be able to use
| your definitions and still get the subset property. This
| means that you are, in all realities, forced to deal with
| the separate notions of "equivalence" and "equality".
| Which is what the article is talking about--all I'm
| really saying here is that you can't sidestep equivalence
| by being clever.
| tuatoru wrote:
| You're not redefining anything; you're adding a
| relationship.
| el_pollo_diablo wrote:
| Another way to see it is to prepend every mathematical
| text involving Z with "for every Z such that [essential
| properties omitted]", so that you can apply it to several
| definitions of Z, rather than awkwardly redefining it
| after the fact. This is the mathematical equivalent of
| "programming to the interface", and is actually how
| mathematics are often formalized in modern proof
| assistants: as huge functors that abstract these details
| away.
| _nalply wrote:
| This means similar to duck typing?
| jhanschoo wrote:
| You can't do this in general, and everywhere, so it's
| still not rigorous. Consider the embedding of the nats
| into the reals, where the reals are defined as a subset
| of the binary sequences (e.g. as the usual infinite
| binary expansion for (0,1] choosing those that do not
| terminate in the zeros sequence, but prefix with a Elias-
| gamma-coded, zigzag-encoded integer). But the usual
| definition of sequence is as a function from the nats; so
| are you again going to redefine your reals in terms of
| that?
|
| In the end you still need to maintain a correspondence
| between the embedding and the original set as in the
| typical way where you do that and consider the subset
| notation as a shorthand that requires you to "lift" or
| "wrap" through the correspondence wherever necessary.
| whyever wrote:
| I don't think you can define the reals as a mapping from
| natural numbers, reals are famously not countable.
| Tainnor wrote:
| You can't map the natural numbers to the set of real
| numbers, but you can map the natural numbers to the
| fractional part of a single real number.
| defrost wrote:
| How would this work when mapping them to the fractional
| part of the real number 2 ?
|
| Collapsing a countably infinite set to 0 doesn't seem
| useful or reversable.
| gizmo686 wrote:
| The integer part is easy, since we already have the
| integers. Once you have D=[0,1), then you can define
| R=ZxD. That is to say, this definition of R seperates out
| the integral and fractional components of every real
| number.
| robinhouston wrote:
| Fortunately functions from the natural numbers are not
| countable either. This is Cantor's theorem.
| danwills wrote:
| I'm not a set-theorist, but a set-theorist friend of mine
| once taught me that you can turn a countably-infinite set
| (such as the integers) into an uncountably-infinite one
| (like the reals) by applying the 'power set' operation
| (the set of all subsets).
|
| Not heaps sure what this really means with respect to
| whether 1 the integer is really completely related (as
| in, equal, or the-exact same-thing) to 1.0 the real
| though. Kinda seems like it might still need a bit more
| information to fully identify a real, even when it
| happens to be infinitely-close to an integer?
| housecarpenter wrote:
| I think you misunderstood the parent comment. They're not
| talking about defining the reals by setting up a mapping
| where each real number corresponds to a unique natural
| number. They're talking about defining the reals by
| setting up a mapping where each real number corresponds
| to a unique mapping from the natural numbers to {0, 1}
| (i.e. a unique binary sequence). The set of all binary
| sequences is isomorphic to the power set of the natural
| numbers, which is uncountable.
| zarzavat wrote:
| It makes more sense to define it the other way around:
|
| Q = Z u Q', where Q' is the set of all rational numbers
| that aren't integers.
|
| Redefining the smaller set can't work because there may
| be more than one larger set, e.g. split complex numbers
| vs regular complex numbers. But you can define a larger
| set to strictly extend a smaller set.
| trueismywork wrote:
| What the fuck is silently redefined? That's very self-
| referential reasoning.
| ysofunny wrote:
| I disagree but I'm being nitpicky
|
| I think the real funky business happens right between Q [?]
| R
|
| but maybe all I'm really trying to say is "hey, look at me,
| I understand how all of N [?] Z [?] Q"
|
| I'm very very sure that it's possible to give a fully ZF
| set-theoretic construction of the rationals using sets. in
| fact IMO the annoying thing is that there are in fact two
| trivially equivalent constructions that I can think of the
| top of my head, and I find that even worse than there being
| none at all
| klodolph wrote:
| What do you disagree with?
|
| Traditionally, you define Q as equivalence classes of
| pairs of integers. The integer 0 is an integer, it's not
| an "equivalence class of pairs of integers" and therefore
| it's not a rational, in the set-theoretic sense.
|
| Real numbers have lots more constructions.
|
| https://en.m.wikipedia.org/wiki/Construction_of_the_real_
| num...
| ysofunny wrote:
| so yes, to answer one of my own questions. I was only
| really saying that I don't really know any of those
| constructions; but know all the "preceding" ones.
|
| I gotta figure out dedekind cuts or at least learn
| tarski's fixed point theorem which I'm sure that would
| allow me to much better understand tarski's construction
|
| all in the slow lifelong process of understanding and
| learning to draw post's lattice
|
| finally, to answer your question, I disagree with saying
| that there's funky business between Z [?] Q because of my
| alleged claim that there is at least one construction
| which avoids the problem you describe, but as I was
| trying to say, these would have a non-unique way to
| construct number zero which nobody likes
| zeroonetwothree wrote:
| You could construct the larger set and then define the
| smaller sets as specific subsets. For example Conway's
| surreal numbers is a fun construction.
|
| If you do it that way then there is only one version of
| "1"
| anon291 wrote:
| This is a construction. The notion is the same. Not all
| math need be constructive. This is an implicit bias in
| most theorem provers.
| auggierose wrote:
| No funny notion of [?] at all, it is about how you
| construct Q, for example. You construct Q(Z), show that Z
| is embedded in Q(Z) via a monomorphism I, and then define Q
| as (Q(Z) \ I(Z)) [?] Z. For example. You are right that
| nobody cares about how this works in detail. It does assume
| though some notion of Q and Z as collections, but not
| necessarily sets from ZFC.
| anon291 wrote:
| Not at all. This is only a problem when doing formal
| verification due to how the theorem provers work (based on
| lambda calc).
|
| N is the set of zero and all its successors.
|
| Z is N extended with all additive inverses, which means it
| includes all of N.
|
| Q is Z with all multiplicative inverses, so it includes all
| Z.
|
| R is the set of Q plus all supremums and infinums of all
| bounded sets of Q.
|
| R is only not Q when you define R with dedekind cuts, which
| is a nice formal construction, but doesn't change what R
| is, up to isomorphism.
| nyssos wrote:
| > up to isomorphism
|
| Which is exactly the sort of more sophisticated notion of
| equivalence you end up needing in these cases.
| auggierose wrote:
| See my other comment. You can define R(Q) as Dedekind
| cuts, see that there is a monomorphism I from Q to R(Q),
| and then set R = (R(Q) \ I(Q)) [?] Q. Then you have Q [?]
| R and R [?] R(Q). No problem. Except of course if you
| work in a theorem prover that doesn't support a
| construction like that.
| anon291 wrote:
| Yeah, I'm very familiar. The 'up to isomorphism' applies
| to dedekind cuts et al.
|
| I'm pointing out that the nature of R is independent of
| its definition, and that any mathematical formal system
| you invent to construct R (up to isomorphism) is just a
| description. R exists independently on its own.
|
| The constructions of R are useful, because you can show
| things about them that could be applicable to R.
|
| However, the article gives a rhetorical question of
| whether you should be able to say 0 is in 3. No you
| should not, because while there are many constructions of
| the natural numbers, the universal property they all
| share (that there is a zero and a successor) does not
| permit any notion of inclusion. The construction of the
| naturals as sets would permit such notions, but these are
| not relevant to any discussion of the natural numbers.
|
| Put in homotopy type theory terms, the natural numbers
| are the equivalence class of all representations of the
| natural numbers, and all propositions over the natural
| numbers are the equivalence classes of all propositions
| over all representations of the natural numbers.
|
| Since one cannot draw an equivalence between '0 \in 3'
| and any proposition from another construction of the
| natural numbers (I believe), then the term '0 \in 3' is
| not a proposition over the natural numbers.
|
| Put another way, I posit that there are constructions
| isomorphic to the natural numbers whose propositions
| cannot be mapped onto the space of all propositions over
| the construction of the natural numbers as sets. Whereas,
| all constructions of the natural numbers will permit a
| proof of the associativity of addition, or the infinity
| of primes. So these proofs are what should be accepted as
| 'proofs' over the natural numbers, but '0 \in 3' would
| not, because it's missing in many systems. '0 \in 3'
| could be _used_ in the set representation to be the
| definition of less than, but it is not a statement that
| applies to all representations.
|
| Is that clearer?
| diffeomorphism wrote:
| You would usually use something like \hookrightarrow
| instead. The set is isomorphic to a subset.
|
| In the same way the real line is "included" in the plane
| (\R \times \\{0\\}) or the sphere is not only a subset of
| the whole space but a submanifold.
|
| Math uses lots of polymorphism and overloaded notation, but
| that is also part of the beauty, where "A=A" can actually
| be a deep result about concepts being compatible.
| paulddraper wrote:
| > You have to use a very funny notion of [?] for that to
| make sense
|
| ??
|
| Are you claiming that Z [?] Q
|
| This thread is wild.
| gus_massa wrote:
| There is a subset of Q that is canonicaly isomorph to Z.
| Probably the distiction is too technical unless you want
| to do some weird advanced algebra. (Note that in most
| weird advanced math the distiction doen't matter.)
|
| So in most case, mathematicians and non mathematicians
| just write Z [?] Q and live happily ever after. But if
| you get supertechnical you should use scare quotes Z
| "[?]" Q or to look more proffesional Z - Q (because tha
| inclusion is an injective funcion, and sometimes it's
| useful to think aboout it as a function.).
|
| ---
|
| To add some confussion: Imagine that you buy in the
| supermarket a copy of Z that is green and another copy of
| Z that is red.
|
| 1(red) + 2 (red) = 3(red)
|
| 1(green) + 2(green) = 3(green)
|
| (If I get super technical, I have to define a +(red)
| operation and a +(green) operation. And probably also a
| =(red) and =(green) as the article discuss.)
|
| Are they the same Z or just canonicaly isomorph or it
| doen't matter?
|
| ---
|
| To add even more confussion: You have a copy of abstract
| Z and a copy inside the rational written as n/1:
|
| 1 + 2 = 3
|
| 1/1 + 2/1 = 3/1
|
| Are they the same Z or just canonicaly isomorph or it
| doen't matter?
| interroboink wrote:
| Yeah I didn't get that comment, either.
|
| At least in my education, you first define the natural
| numbers (where 0 and 1 are special, and the rest are defined
| in terms of that (ie 2 = 1+1)), then you define negation,
| which gives you the negative numbers. Then you layer on
| multiplication and division, which gives you rational
| numbers, and so on.
|
| So, it's the same "0 and 1" definition all the way through,
| just with additional operations being added to the mix.
|
| Though maybe other approaches do it differently.
| klodolph wrote:
| I think you may have not gotten far enough to get a formal
| explanation of what 0 and 1 are.
|
| The definition taught to most mathematicians is that for
| the natural numbers, 0 = {} 1 = {{}}
|
| In general S(N) = N [?] {N}
|
| But this is not how the real numbers are constructed. You
| either use Dedekind cuts, Cauchy sequences, or something
| else.
| gus_massa wrote:
| Complex numbers are just pairs (real and imaginary) of
| Cauchy sequences of pairs (numerator and denominator) of
| pairs (positive and negative) of nested versions of the
| empty set. (modulo al the necesary equivalence to make
| this work).
|
| So the natural number {{}} is canonical included in the
| complex numbers as [something].
|
| Natural {{}}
|
| Integer ({{}},{})
|
| Rational (({{}},{}),({{}},{}))
|
| Real (({{}},{}),({{}},{})), (({{}},{}),({{}},{})),
| (({{}},{}),({{}},{})), ...
|
| Complex ((({{}},{}),({{}},{})), (({{}},{}),({{}},{})),
| (({{}},{}),({{}},{})), ... , (({},{}),({{}},{})),
| (({},{}),({{}},{})), (({},{}),({{}},{})), ... )
|
| (And there are a few alternative definition, but I think
| they are even more messy.)
| germanier wrote:
| The usual formal definition for the rational numbers is
| _equivalence classes of pairs of integers_. The zero is
| then the equivalence class of (0, 1) which is not the same
| as the integer 0.
|
| You could certainly somehow get it to work by starting with
| the closure of the division operation but would introduce a
| lot of unnecessary headache along the way.
| singularity2001 wrote:
| I came across this topic in lean, where you have different
| definitions of 0 and 1 within the same context and you can
| auto-convert using coercion. instance : One
| Hyper where one := <1, 0, 0, 0> scoped
| notation "1" => One.one -- doesn't work "invalid atom" and
| unnecessary instance : OfNat Bool 1 where
| ofNat := true instance : Coe Z Bool where
| coe z := z [?] 0 instance : Coe R R[?] where
| coe r := < r 0 0 0 >
|
| Basically all the fun of C++ casting just that you are always
| safe.
| auggierose wrote:
| It is a different story in Lean though, because Lean, as
| most other logics based on type systems, doesn't have
| subtypes. So all you have are coercions. That's actually a
| bad thing.
| staunton wrote:
| What do you mean by "subtype"? Lean defines a thing
| calles `Subtype`, members of which are constructed from a
| value and a property.
| auggierose wrote:
| That might be called Subtype, but is a disjoint type
| containing different values than the original type. If S
| is a subtype of T, and x : S, then also x : T.
| singularity2001 wrote:
| why would you say that this is a bad thing
| auggierose wrote:
| Because coercions are just a work-around, and more
| machinery hidden from you, but still there causing
| problems (like types). If you are coming from C++, then
| yes, Lean coercions are a step up. If you are coming from
| mathematics, then Lean coercions are just a cumbersome
| work-around.
| lupire wrote:
| Cumbersome compared to what? Ignoring the issue entirely?
| auggierose wrote:
| Cumbersome compared to just having N [?] Z, instead of
| having a coercion c from N to Z, with complicated
| algorithms of where to insert c automatically, and then
| hiding the result from you, because otherwise you would
| see with your own eyes what a mess you are in.
| markusde wrote:
| But with coercions you do have {|n | n [?] N} [?] Z,
| which is the subtype that you really want!
|
| The issue is that not all properties of subsets can be
| lifted to supersets. As an example from analysis, you can
| coerce the reals R to the extended reals R[?], but you
| lose some of your rewrite rules because you need to
| choose how to define edge cases like ([?] - [?]) in R[?].
| Making these choices is common in mathematics (at least
| in analysis) and in pencil and paper proofs it's usually
| just handwaved away.
|
| Using subtypes, a proof checker would have to be
| explicitly given which ambient superset you're going to
| rewrite something like ((a : R) - (b : R)) in... this is
| more or less the same as using coercions to distinguish
| between R and {|r | r [?] R} [?] R[?] except with subsets
| type inference is way harder.
|
| I'll admit that coercions are annoying, but subsets don't
| let you get around it: here there's an essential step up
| in complexity between sloppy pencil and paper proofs and
| verified code. Personally, I'm really interested in
| seeing how much of mathematical handwaving can be
| rigorously automated away. There's a lot of cool work in
| this area by I don't think the FM community has a
| definitive answer for it yet.
| auggierose wrote:
| Let's be clear, I am not arguing for subtypes. Subtypes
| are a mess, that is why no type system supports them. I
| am arguing against any types at all. So type inference
| being harder is not a problem, because _there won 't be
| any type inference_. I know, that is a tough pill to
| swallow, type inference is like a hard drug for computer
| scientists.
|
| Subsets or subcollections, on the other hand, are fine.
| Of course you will have proof obligations, but that is
| not a problem, and automation can take care of most of
| this (note that automation is much more flexibel than
| hardcoded type inference).
| markusde wrote:
| Fair enough, I haven't used many proof assistants without
| dependent types, and I probably should.
| math_dandy wrote:
| Absolutely right. If you keep worrying about whether 1 is
| actually 1, you'll never get any math done.
| Someone wrote:
| > I think pretty much every mathematician agrees that [...] 1
| the integer is the same as 1 the real number
|
| Yes and no.
|
| NO: there already are multiple ways to construct "1 the
| natural number", even if you restrict that to set-theoretic
| ones. See https://en.wikipedia.org/wiki/Set-
| theoretic_definition_of_na.... Von Neumann defined the
| natural number 1 as _{[?]}_ (the set with as only element the
| empty set), Frege and Russell as the equivalence class of all
| sets with a single element (and that's not a circular
| definition)
|
| Integers typically are constructed from those (See for
| example https://mathesis-online.com/integers, which defines
| an integer _i_ as the equivalence class of pairs _(a,b)_ of
| natural numbers such that _a = b + i_ )
|
| In this construction, "the integer 1" is the infinite set
| _{(1,0},{2,1},{3,2},...}_. That obviously (in the
| mathematical sense) is different from the one element set
| _{[?]}_
|
| Rationals and reals are constructed on top of that (see for
| example https://www.quora.com/How-is-the-set-of-real-numbers-
| constru... for a way to construct those)
|
| YES: when you decide to ignore the low-level stuff and just
| use the intuitive definition of reals and integers.
|
| (Alternatives:
|
| - don't ignore it, but start at the basis, calling the
| integers something else, then prove equivalence between a
| well-defined subset of the reals and the integers and then
| give that subset the name "integers".
|
| - directly construct the reals without first constructing the
| integers and then define the integers as a subset of them.
| I'm not aware of any way to define the reals without first
| defining integers, though. )
| auggierose wrote:
| You ellipsed ([...]) the "can assume" part of my statement.
| Every mathematician knows the different ways of
| constructing numbers. It really is a simple YES.
| Someone wrote:
| No, it isn't. Whether it is depends on what level the
| mathematician operates, and will differ on what they're
| working on. That's precisely the subject of this article:
| there's an intuitive idea that, upon close scrutiny,
| turns out to before complex than it appears to be.
|
| So, if you want to start from the basis in a proof
| assistant, you'll have to discriminate between them and
| either give them different names or introduce context
| from which the computer can infer what you mean.
|
| If, for example, you want to prove that two definitions
| of _integers_ are equivalent, you need two different
| names.
| auggierose wrote:
| It helps to state carefully what you are trying to
| achieve. I want a theorem prover where constructing
| numbers such that N [?] Z is easy. Doing this in a
| theorem prover is not trivial, for example none of the
| type based theorem provers allow that (although,
| Isabelle/ZF might qualify; it is based on set theory on
| top of a weak intuitionistic type theory; but here N and
| Z are not types, but sets of the same type). It is
| trivial though if you are a mathematician, no matter what
| you are working on. You know that these constructions can
| be done, and that as a result you can assume N [?] Z (if
| you want to). So as long as your theorem prover doesn't
| support something as trivial as that, it is lacking.
|
| And yes, that is exactly what Buzzard is talking about.
| For the case I am talking about here though, that is just
| table stakes: make sure your prover can do N [?] Z [?] R
| [?] C. If you can do that, you can start worrying about
| more advanced issues of equality, and you might find that
| you have already solved a significant amount of them.
| robinzfc wrote:
| I can confirm that in Isabelle/ZF one can set up a
| context (locale) with the meaning of the N Z R C symbols
| defined so that N [?] Z [?] R [?] C. However N for
| example will not be equal in such case to the canonical
| set of ZF natural numbers where 1 = {0}, 2 = {0,1} etc.
| dataflow wrote:
| The (principle) cube root of the integer -1 is -1, but the
| (principle) cube root of the complex number -1 is (1 + sqrt
| 3) / 2. They sure seem like different objects.
|
| Though I guess whether you want to blame that on the
| operators vs. the objects themselves can be left to your
| taste, but I'm not sure what "these objects are equivalent"
| would mean if the behaviors are left unspecified as
| characteristics of the objects (which would be the former
| case).
| auggierose wrote:
| That is indeed a nice feature of types: You can overload
| notions. In this case you overload the notion "principal
| cube root" (PCR) to mean different things for Z and for C.
|
| But really, "principal cube root" as you would like it to
| behave is not well-defined just for a number, you also need
| to provide the algebraic structure you consider it in, as
| in PCR(Z, -1) = -1, and PCR(C, -1) = (1 + sqrt 3) / 2.
|
| Alternatively, just set PCR(-1) = (1 + sqrt 3) / 2. That
| makes probably the most sense, as there is not much value
| in a PCR notion for integers in the first place.
| lupire wrote:
| "Principal" root isn't an interesting mathematical object.
| It's just an arbitrary way to choose a preferred element
| from an equivalence class, when you're too lazy to consider
| the whole class and you want to pretend that 'implies"
| ("only if") is is the same as " biconditional" ('if and
| only if").
| dataflow wrote:
| > when you're too lazy to consider the whole class
|
| Well then consider the whole class? The whole classes are
| different too, I don't get your point.
| im3w1l wrote:
| I think every mathematician are aware of both of those
| perspectives, and uses whichever is more convenient at the
| moment.
| auggierose wrote:
| Yes, but in a software like a theorem prover you must make
| the conscious decision whether you want your prover to be
| able to assume N [?] Z or not. All the type theory based
| ones say "not". That is not very convenient.
| vishnugupta wrote:
| > Every mathamatician knows that the integer 1 and the real
| number 1 different objects [0].
|
| This is quite interesting to me as I'm trying to understand,
| recreationally, these concepts.
|
| From what you've written it looks like there are several ways
| to construct numbers. I'm aware of some of them but I don't
| know if they are connected or related e.g., Dedikend cut, Van
| Neumann numbers etc., It'd be great if you could list down all
| such constructions.
| klodolph wrote:
| Wikipedia has a lot of resources. Naturally, it won't all be
| accessible (some of these constructions sit at the top of a
| mountain, and you have to climb the mountain first).
|
| https://en.m.wikipedia.org/wiki/Construction_of_the_real_num.
| ..
| gizmo686 wrote:
| All of the ways is quite the ask.
|
| There are 2 main main approaches: explicit constructions and
| axiomatic constructions.
|
| Dedikend cuts and Von Neuman numbers are both examples of
| explicit constructions. You can point to exactly what a given
| number "is", and then prove properties about you
| construction.
|
| The other approach is the axiomatic construction, where you
| define what properties you want your numbers to have. You
| then (hopefully) prove that such a system exists and is, in
| some sense unique.
|
| Taking the integers, the most common explicit construction is
| the set-theoretic Von Neumon construction, where 0={}, 1={0},
| 2={0,1}, 3={0,1,2}...
|
| You can also imagine defing 0={}, 1={0}, 2={1}, 3={2}
|
| Note that while we say these are equivalent definitions, they
| produce different results in the sense that, for example,
| 0[?]3 in the former, but not in the latter. [0].
|
| You can also define natural numbers as a subset of the
| cardinals. In this construction, 3 represents the collection
| of all sets that can be put in a 1-to-1 correspondance to the
| set { {}, {{}}, {{{}}} }. Here, the exlusion of various
| infinities is a rather arbitrary part of the definition.
|
| You can also define integers as a subset of combinatorical
| games, given by 0={|}, 1={0|}, 2={1|}. This naturally leads
| to negative numbers, -1={|0}, and a zoo of "numbers" not seen
| outside of combinatorical game theory, such as | = {0|{0|0}}.
| Still, if you restrict yourself to the integer looking
| numbers and follow the game theory rules of addition, you get
| something equivalent to the natural numbers.
|
| You can also define them as strings constructed from the
| alphabet of a single character, so 0="", 1="a", 2="aa". (This
| is the free monoid over a single set)
|
| Lambda Calculus gives us the church encoding, where:
| * 0 = lf.lx.x * 1 = lf.lx.f x * 2 = lf.lx.f (f x)
|
| Under the axiomatic definition of numbers, the classical
| definition is given by the 9 Peano axioms, which amount to
| assuming the existence of 0 and a "succesor" function S(n)
| informally corresponding to S(n) = n+1.
|
| All of the above examples are things I have actually seen and
| that arise naturally in their respective branch of
| mathametics.
|
| [0] This contradiction is not actually an issue, because no
| one ever actually says 0[?]3, even though it is technically
| true in some constructions.
| anon291 wrote:
| These are all constructions though. They don't say what the
| natural numbers are.
|
| The natural numbers is a set with a starting element and
| that has, for each element, a thing immediately following.
|
| Things like 0 in 3 make no sense since 0 refers to the
| first thing in whatever representation you have, not a
| particular one.
|
| I love formal theorem proving and provers, but this
| shouldnt lead us to believe that the natural numbers are
| fundamentally any particular representation
|
| N is defined by its properties not its representation.
| lmm wrote:
| > These are all constructions though. They don't say what
| the natural numbers are.
|
| A construction is exactly what would tell you what they
| are.
|
| > The natural numbers is a set with a starting element
| and that has, for each element, a thing immediately
| following.
|
| OK, but, like, which one? There are lots of sets that
| this describes.
|
| > Things like 0 in 3 make no sense since 0 refers to the
| first thing in whatever representation you have, not a
| particular one.
|
| If 0 and 3 are sets then we can legitimately ask whether
| 0 is a member of 3 or not. If 0 and 3 aren't sets then
| what are they? If the natural numbers are a set then 0
| and 3 should also be sets, since set theory only talks
| about sets.
|
| > N is defined by its properties not its representation.
|
| Then what is it? If you say it's a set with those
| properties, then it should be a set and we can ask set
| questions about it. If you say it's somehow all of the
| sets with those properties, or some other concept that
| somehow encompasses them, then you still haven't
| explained what it actually is.
| BalinKing wrote:
| Not a direct reply to your question, but it seems to me
| that GP is describing a "structuralist" view (cf. https:/
| /en.wikipedia.org/wiki/Structuralism_(philosophy_of_m...,
| on which I'd guess much has been written over the years
| (both for and against).
| anon291 wrote:
| I think so yes.
|
| The article here espouses a constructivist view of
| mathematics
|
| While I like that view personally, I think it's wrong to
| act as if it's the only one like this article does.
|
| Many people have different views.
| lupire wrote:
| If I choose to wear a fedora, is a fedora an essential
| part of who I am? Or an arbitrary choice that be changed?
|
| This question goes back to Plato.
|
| You use Von Neuman naturals. I use Peano naturals. Which
| are the real naturals? Can they both be the naturals,
| even though they are clearly different? The natural
| numbers are not any one construction. They are the
| abstract idea of whose properties are what all the
| constructiona have in common.
|
| Math is like God. We use feeble human language to
| approximately talk about something that is beyond our
| ability.
| anon291 wrote:
| Right and this is my point the view espoused in the
| article is not universal
| lmm wrote:
| > Math is like God. We use feeble human language to
| approximately talk about something that is beyond our
| ability.
|
| That sounds like giving up. The approach the article is
| describing is a lot more satisfying - forming this
| concept of equivalence, and then using it to give
| genuine, rigorous answers to questions like:
|
| > You use Von Neuman naturals. I use Peano naturals.
| Which are the real naturals? Can they both be the
| naturals, even though they are clearly different?
| anon291 wrote:
| > OK, but, like, which one? There are lots of sets that
| this describes.
|
| Any, and all. One can do the thinking without specifying
| what. I believe this is the notion of a 'universal
| property' in category theory.
|
| > If 0 and 3 aren't sets then what are they?
|
| I mean, if you want to give me a construct I would use,
| I'd say the following
|
| 0 = \s -> \z -> z 3 = \s -> \z -> s s s z
|
| If you say that these are akin to church numerals, that
| is correct if you look at it as a lambda calc term.
| However I'm saying something much stronger than just a
| lambda calculus term. That's just my notation.
|
| I'm saying that zero is the concept of taking two things
| (one an initial thing and the other a method to take one
| thing and get the next thing) and then returning the
| initial thing. While three is the concept of taking the
| same two things and then doing the method three times on
| the first thing. I used lambda notation because that is
| an easy way to convey the idea, not because that is what
| three _is_.
|
| > Then what is it? If you say it's a set with those
| properties, then it should be a set and we can ask set
| questions about it. If you say it's somehow all of the
| sets with those properties, or some other concept that
| somehow encompasses them, then you still haven't
| explained what it actually is.
|
| It's a set in the colloquial sense, not in the ZFC sense.
|
| There's an idea of a thing, and then the definition of
| the thing. Both are valid in my mind.
|
| For example, heat is the movement of atoms. It's also the
| energy in a thing. But it's also the feeling of hot that
| I cannot describe. It's also an idea in its own right.
| Things can be many things. There's an infinite hierarchy
| of description that one may apply to concepts, and, in my
| philosophy, at some level the description becomes unable
| to be expressed.
| lmm wrote:
| > One can do the thinking without specifying what.
|
| _After_ one has figured out a rigorous approach, one can
| generally ignore it in day-to-day work. But you need to
| have that foundation there or you can go horribly wrong.
| (Analogy: we don 't generally think about limits when
| doing day-to-day calculus. But when people tried to do
| calculus pre-Weierstrass, unless they were geniuses they
| "proved" all sorts of nonsense and got crazy results).
|
| > I believe this is the notion of a 'universal property'
| in category theory.
|
| That's one of the good answers to this problem. But you
| still need the constructions (if only to prove that an
| object with the required properties exists at all) and
| you need a lot of the kind of work the article is talking
| about, where you establish that these different
| constructions are equivalent and you can lift all your
| theorems along those equivalences.
|
| > I'm saying that zero is the concept of taking two
| things (one an initial thing and the other a method to
| take one thing and get the next thing) and then returning
| the initial thing. While three is the concept of taking
| the same two things and then doing the method three times
| on the first thing. I used lambda notation because that
| is an easy way to convey the idea, not because that is
| what three is.
|
| OK but then what kind of things are these "concepts"?
| What kind of questions can and can't we ask about them?
| If you care about "what the natural numbers are" then
| these kind of questions are worth asking.
| simpaticoder wrote:
| We must remember that these constructions retcon the actual
| human experience with numbers, which is firmly rooted in
| counting and measurement, that always come after this
| experiential basis. Formal definitions appear driven by an
| aesthetic consensus, mostly about minimalism and axiom
| flavor. Individual human experience with numbers reflects
| human history and at both scales 'counting and measurement'
| is more fundamental in the sense that it always comes
| first, and therefore all constructions derive from it, must
| maintain consistency with it, and conflicts must be
| resolved within it, and it is safe to ignore
| inconsistencies that can't be expressed within it.
| staunton wrote:
| In those terms, the foundations (of any topic or field)
| are never fundamental. I think people in this thread are
| using a different meaning of "fundamental".
| lupire wrote:
| Without formal constructions, humans have a nasty habit
| of proving things that wrong or not even wrong. Our
| ancestors dealt with this problem in the 19th Century by
| creating tools to help distinguish truth from balderdash.
| simpaticoder wrote:
| Your statement is consistent with my point which I mean
| to point out the psycho-social origin of such
| constructions and therefore the limits of their utility.
| I do not say they are not useful at all.
| ajsnigrutin wrote:
| Meh, php solves this with "$a === $b" :D
| paulddraper wrote:
| > Every mathamatician knows that the integer 1 and the real
| number 1 different objects
|
| !!!!!!
|
| The integer 1 is the same as the real number 1 ,is the same as
| the odd number 1, is the same as the perfect square 1, etc.
|
| Z [?] R
|
| That this is the top-voted comment on this thread.....
| r0uv3n wrote:
| > Z [?] R That is not at all obvious without some canonical
| isomorphism acting on Z, or at least is a behaviour strictly
| dependent on your particular set theoretic construction of
| the reals.
|
| E.g. for the cauchy sequence construction of the reals, the
| image of the integer 1 under this canonical isomorphism would
| be the equivalence class of the sequence (1,0,0,0,...), but
| these are of course not the same object in a set theoretic
| sense.
| chiefjosh wrote:
| I think he literally just demonstrated the problem you were
| trying to illustrate about software provers
| phlakaton wrote:
| As one of the high school geometers of all time, I was always
| rather partial to [?] which we used for congruence. I'm happy to
| share it with other mathematicians if they'll agree to keep their
| mitts off of ":=".
| vishnugupta wrote:
| Related
|
| https://www.quantamagazine.org/with-category-theory-mathemat...
| cesaref wrote:
| Is there a decent overview of what the aim of mathematics solvers
| is these days? In light of Hilbert's effort at formalism in the
| 1920s, and the incompleteness theorem, I was wondering where this
| was going, and what the known limitations are.
| klodolph wrote:
| The incompleteness theorem isn't an argument against formalism,
| it's just a bound on what you can do with it (you can't use one
| set of axioms and expect to prove everything). That's ok,
| because you are,
|
| 1. Not required to prove everything which is true, 2. Not
| limited to one set of axioms.
|
| The nice thing about formalism is that you can use a computer
| program to check whether a proof is sound or not. Isn't that
| nice? It has applications in e.g. computer science and
| engineering, where you can prove that a program does not crash,
| or prove that a traffic light never shows green in conflicting
| directions, or prove that a real-time kernel always provides
| enough computational time for your rocket computer to steer.
|
| Working math, there are more and more complex proofs that
| cannot reasonably be checked by humans. Having a computer check
| them is a nice alternative.
| ysofunny wrote:
| it's pretty much a competition between niche programming
| languages which are interesting to different powerful academics
| singularity2001 wrote:
| Current hopes (even by Terrence Tao) are that you give a sketch
| of a proof to GPT-X and it will give you a link to the formally
| confirmed proof.
|
| Others hope that the next AI will come up with a sketch of a
| proof itself.
|
| GPT-4 sucks at lean because lean had it's syntax changed too
| often, and GPT-4 shows limited reasoning capabilities
|
| However it did come up with the following proof for my little
| order of pairs instance LT : LT (N x N) where
| lt f g := f.1 < g.1 [?] (f.1 = g.1 [?] f.2 < g.2)
| instance : DecidableRel (LT.lt : N x N - N x N - Prop) :=
| fun (a,b) (c,d) => if h1 : a < c then isTrue (Or.inl
| h1) else if h2 : a = c then if h3 : b < d
| then isTrue (Or.inr <h2, h3> ) -- the
| rest is even more silly since we have to turn everything around
| else isFalse (l (h : a < c [?] (a = c [?] b < d)) =>
| Or.elim h (l hlt : a < c => absurd hlt h1)
| (l heq : a = c [?] b < d => absurd (And.right heq)
| h3)) else isFalse (l (h : a < c [?] (a = c [?] b < d))
| => Or.elim h (l hlt : a < c => absurd
| hlt h1) (l heq : a = c [?] b < d =>
| absurd (And.left heq) h2) )
|
| This may lead back to the original question because Bool [?]
| Prop and the formula for LT should ideally lead directly to
| decidability without all this redundancy?
| ganzuul wrote:
| https://en.wikipedia.org/wiki/The_Treachery_of_Images
|
| Leads to
|
| https://en.wikipedia.org/wiki/Ontology
|
| Which compares everything to a self which we won't agree on, so
| it is expedient if we just pin it down
|
| https://en.wikibooks.org/wiki/X86_Assembly/Control_Flow#Comp...
|
| This presumes a sequential model of computation but we are
| actually free to discover functional and concurrent models as
| they are equivalent, but give philosophical freedom and yet
| retain rigor.
| crsn wrote:
| I've been working on a glossary of "Notions of Equality &
| Sameness" every few months for the last ~8 years (and looking for
| collaborators: carson@carsonkahn.com) - surprised not to have had
| this one in my list already!
| voidUpdate wrote:
| I know it's not related to the content of the article but I hate
| when websites redirect me to a page of articles when I click the
| back button, if that isn't where I came from. I've already
| decided I want to go back to what I was looking at before,
| shoving a load of stuff that I didn't want into my face isn't
| going to make me change my mind
| lordnacho wrote:
| I don't think you need to go to higher level math to run into
| this sort of problem.
|
| When we're in school solving equations, getting to the initial
| stages of calculus, you start running into identities like
| sin^2(x) + cos^2(x) = 1, which sometimes but not often are
| written with three parallel lines instead of two.
|
| What this means is that the functions on either side of the sign
| are equivalent, any x you pick doesn't change the graph.
|
| At some point, you will be solving simultaneous equations, and
| someone will have the bright idea that you can just differentiate
| both sides and just solve that. This happens to be true if you
| have something like above, it's still valid that the derivative
| anywhere is the same, since they are the same function. But if
| you are actually just finding the crossing point of two graphs,
| like one normally does at that level, then the equality is only
| for a particular value of x, and there's no reason the derivative
| would be the same.
|
| In general there's a lot of these little notation things that
| creep up around that stage. The big one is treating dy/dx like a
| fraction, which you can do in certain cases to solve differential
| equations, but only in certain cases. If you don't understand
| why, you might get very confused about what the symbols actually
| mean.
| hilbert42 wrote:
| Leaving aside the more advanced definitions of equals, it'd be
| good if more emphasis were put on the difference between '=' and
| '[?]' early on in one's training. That is explaining why is
| _equivalent_ different to _equals._
|
| I recall the difference in the definitions being confusing for
| most of us kids.
| housecarpenter wrote:
| The way I see it, the distinction between = and [?] isn't
| really to do with equality having more than one meaning. An
| "identity" like sin^2 x + cos^2 x [?] 1 is really just
| shorthand for "for every real number x, we have sin^2 x + cos^2
| x = 1". The equals sign here has the same meaning as in a
| statement such as "there is a real number x such that sin^2 x +
| cos^2 x = 1"; the difference is in the surrounding language,
| and what meaning it assigns to the variable x.
|
| So perhaps rather than just emphasizing the difference between
| = and [?] more, it would be better to go further and emphasize
| the difference between universal and existential quantification
| more. Quantifiers can be confusing, but I think people also
| find having two different equals signs confusing; and it
| wouldn't be necessary to give a full account of predicate logic
| to high schoolers, I'm thinking more of just informally
| describing the difference between "for all" and "there exists"
| and reminding them that a bare variable has no meaning if you
| don't know what set it ranges over and how it's quantified.
|
| This is just my speculation, I have no experience with
| mathematical education whatsoever.
| hilbert42 wrote:
| _"...emphasize the difference between universal and
| existential quantification more. Quantifiers can be
| confusing... "_
|
| Right, I've uni math also formal logic so I've knowledge of
| _universal and existential quantification,_ etc. thus an
| understanding of the issues.
|
| You're right, that stuff's a bit too heavy for highschoolers.
| Perhaps all that's needed is to be told 'that at times these
| appear the same but later on you'll need to understand
| there's a mathematical distinction' then emphasize the
| difference aspect to drive the point home.
|
| Even though it was a long time ago I mostly recall what the
| teacher said and whilst he gave a few examples he never
| emphasized that there was a mathematical difference and that
| it was an important fact to know. Matters became more
| ambiguous from our science courses, the use of 'equivalent'
| was very loose.
|
| I reckon the same or similar should apply to other topics,
| calculus for example.
| sproutini wrote:
| This isn't news to any logician or people working in formal
| methods. More like a mathematician getting his head around what
| has been thought about for decades, if not centuries.
|
| Also, -1 for not mentioning Leibniz equality.
| vinnyvichy wrote:
| tl;dr as an acolyte is that sometimes the bug can be fixed by
| adding extra data (e.g. number of minus signs, or method to
| compute minus signs) to your declaration of equality.
|
| Concrete example from Kev Buzzard's "Lean proof of Fermat's Last
| Theorem" from yesterday (2024-06-19 UT)
|
| p34: "It is impossible to say which of the two canonical
| isomorphisms is "the most canonical"; people working in different
| areas make different choices in order to locally minimise the
| number of minus signs in their results."
|
| https://imperialcollegelondon.github.io/FLT/blueprint.pdf
|
| A lot of the subtleties seem to come from the pecularities of
| what is meant by "canonical" rather than by "isomorphic"
___________________________________________________________________
(page generated 2024-06-19 23:01 UTC)