For example, the real numbers are not sets in the same sense that "the map is not the territory". Sets allow us to encode real numbers, but this encoding is mostly arbitrary. Is 3 an element of pi? If pi truly is a set, then this is a sensible question to ask, since sets are defined by their members. However, there is evidently an abstract concept of "real numbers" which exists without mentioning the elements of a real number. The technical reflection of this dilemma is the fact that in set theory there are multiple isomorphic copies of "the complete archimedean ordered field" which are all different as sets.
This is one reason why type theory is superior to set theory. In type theory we can actually capture the abstract concept of real number and work with it, instead of always working with an encoding. This might not matter so much for something as simple as a real number, but it matters a lot when you talk about more complicated structures.
Could you give a small example of how a simple bit of reasoning about a real (or even natural) number would work in both frameworks?
For example, we cannot represent the value of Pi in Hindu-Arabic notation; it stretches to some 'infinity' which is just bizarre and which we can't capture on paper. Saying it has a value opens up some interesting questions about what a number or a value actually is. I suspect people have very clear opinions which are all different from each other.
It is true that the fact that "there exists" (in a very nonconstructive sense) some unknowable, impenetrable encoding may offend the aesthetical sensibilities of some people, but type theory does not really "resolve" that in any way (and it is certainly not superior, just different, or rather, it is superior in some ways and inferior in others); it simply constructs its axioms at a higher level of abstraction. The axiomatic existence of inductive data types in type theory is just a theorem about well-founded sets in set theory, but those sets are really defined in exactly the same abstract way.
: So the natural numbers can be defined as "epsilon set N, s.t. N is the minimal set s.t. an element zero exists in N and there exists a function succ in the set N -> N, such that for all n in N, succ(n) is in n, and there is no n in N s.t. succ(n) = zero".
: For example, because most type theories are based on the lambda calculus, they are on the precipice of inconsistency due to Curry's paradox, which makes some aspects of working with them extremely unpleasant compared to set theory.
"The successor integer."
(==> int int))
A computer language is not just a way of getting a computer to perform operations but rather that it is a novel formal medium for expressing ideas about methodology. Thus, programs must be written for people to read, and only incidentally for machines to execute. - Preface, SICP 1st Ed. https://mitpress.mit.edu/sicp/front/node3.html
this is recursive, which is just how a function like succ works (with a bit more work, anyway) but the definition rather concernes a polymorph function.
You do work in a particular encoding when you mention yero, at least. and succ^x is also an encoding (where x is zero or succ^y, where y is zero or ...).
That encoding is completely opaque, though. You have no way of knowing what are the members of zero.
The main difference between type theories and set theories is that type theories have particular syntactic discipline. Everything else is or can be a feature of set theories, too.
Real numbers can actually be logically constructed as sets. So yes, Pi is a set.
For example, you can define the set of real numbers as the set of equivalent classes of rational cauchy sequences.
In order words, Pi is a set of rational cauchy sequences that are equivalent (this set is infinite).
In simple (non formal) words: Pi is the set of sequences of rational numbers that get closer and closer to the numerical value of Pi.
>>>> Is 3 an element of pi? If pi truly is a set
Pi being a set doesn't mean that it is a set of real numbers. In fact, that would be illogical (recursive). If Pi is a set, it must be a set of things that are not real numbers. So it is not logical to ask if 3 is an element of Pi. You can ask if 3 is equal to Pi, in which case the answer is no.
You missed the point. The point is that while X (e.g. the real numbers) can be encoded as Y (e.g. Cauchy sequences), this doesn't mean that X is literally Y. That would entail that Cauchy sequences and Dedekind cuts, for example, are the exact same thing, which they are not. Rather, they are two different ways of encoding the same abstract structure (a Dedekind-complete ordered field).
> Pi being a set doesn't mean that it is a set of real numbers.
This is dodging the question. Is the set containing the empty set a member of pi? Such a question is meaningless without fixing a particular encoding, and it has nothing to do with the intrinsic properties of a real number.
>The point is that while X (e.g. the real numbers) can be encoded as Y (e.g. Cauchy sequences), this doesn't mean that X is literally Y.
In my opinion, a mathematician does not know what the difference between "being literally" and "being encoded as" is - unless you assume that mathematics should aim to be a formal encoding of some pre-existing 'intrinsic reality', in which case what you're doing is physics and not math.
In physics, the debate is more open: Is the wave function literally the electron? Or is the wave function just an encoding of the electron, which is the intrinsic real thing? Or is the electron the way we humans perceive the wave function, which is the intrinsic real thing?
Anyway this is probably way too theoretical of a debate :)
Wrong. The real numbers are literally a Dedekind-complete ordered field. The real numbers are encoded as Cauchy sequences, or as Dedekind cuts. Cauchy sequences are not Dedekind cuts: The former are equivalence classes of sequences. The latter are downward-closed sets without a greatest element. They are literally different objects.
Regarding your electron comment, the answer is straightforward: the electron is an excitation of the electron spinor field, nothing more. Fields are more fundamental than particles.
The book is a non-academic tour of the history of mathematical foundations, and the way mathematicians struggled to rediscover "truth" or the purpose of their work when new crises were reached. For example, the book spends a good deal of time explaining the centrality of Euclidean geometry to people's worldviews, and the way that the discovery of non-Euclidean geometries shook people. Not just because they didn't assume other geometries could exist, but because people believed geometry to map onto Euclidean physical reality because it was God's way of revealing Himself to the world.
The other main crises that the book toured were the discovery of quaternions, Cantor's theories, and Godel's theorem.
Kline ends describing the arc over the last two hundred years of math as a splitting-off into four different schools: set theorists, intuitionists, formalists, and logicists. Each camp tried to reassert math on "solid ground". I hear echos of those debates in this thread, where some are asserting that there can possibly exist multiple foundations, which from my reading of the book is a very formalist idea (our rules of math are a formal system, and any internally consistent set of rules are just as valid as objects of study).
Not being a mathematician, I don't have a sense of where those schools played out to the current day. I'd be curious to hear if they're all still around in different forms, or whether some have more or less died out.
For this to be the case there have to demonstrable advantages over working with set theory. The main attraction of HoTT is that it allows people to do homotopy theory on computers using theorem provers. It is still a very open question whether this is an improvement over pen and paper math. It's still not clear if HoTT is just some neat technical gimmick that allows one to model homotopy theory using type theory.
This is still certainly worth investigating, but saying that HoTT "subsumes" set theory is a bit strong.
I would refer the interested reader to the discussion at https://mathematicswithoutapologies.wordpress.com/2015/05/13... (between Jacob Lurie, Shulman and Voevodsky).
Perhaps simply because it is older, set theory is way ahead of its competitors in developing a hierarchy of extremely strong (but apparently consistent) axioms to supplement its base theory ZFC.
I don't see a difference between precise definition and mathematical statement in this context, so your question would be paradox. Is it wrong to ask though? I think higher logic is supposed to deal with these types of paradoxes. Your question, if taken rhetorical, is a statement about mathematical statements, a metapher.
The in/-completeness theorems show that higher order logics like that are either inconsistent or incomplete. So a theory like you are asking for, is ab ever growing set of proofs that can't fit in a single book. Taken with a sense of philosophy in mind, a book can only be an introduction to think further.
I was glad to read at least the intro to Univalent foundations mentioned in a previous comment. Russels paradox defies a set of all sets in first order logic. FOL is otherwise said to be complete, by the way, a fact often overlooked when talking about the related liars paradox. I was pleasently surprised to read that they just avoid the paradox by embedding theory into theory (Universes, tbh). To me that means we can't draw elemens from an arch-set, but have to build facts from the ground up.