> That the solution could lie in something as simple as Zermelo’s separation axiom and the conception of the cumulative hierarchy of sets was seemingly not anticipated. It was a miracle.
If you are a Platonist (I am), then it is not really a miracle. Mathematical objects are real, and logic is a tool to study them. The paradoxes can only exist, because math is real: a paradox shows that something is not real, and if there were no real mathematical objects to begin with, paradoxes would be meaningless. As it stands, a paradox is a tool to distinguish reality from that which is not real.
Have fun making any kind of sense if you are a formalist or intuitionist (hint: you can't).
It is indeed cool that something as simple as set theory covers so much. But it doesn't cover everything. The Banach-Tarski Paradox shows that sets are not what we imagine them to be (but they are still real): we need to add the property of measurability, which acts then as an additional axiom, to get closer to that. And in order to solve BB(748), ZFC is not enough [0, theorem 7]. So, one set theory is not enough. Depending on which properties we ascribe to sets, or in other words, which axioms we add to set theory, we also get different set theories.
> I give up.
Set theory is cool, but it is not special. In the end it describes a fragment of the (real) mathematical universe, but there is more to this universe than just set theory. And depending on which properties you pick for your sets, you get different fragments.
It is interesting that Larry says that Automath is not a Foundation, and that neither is Isabelle, which he created. Maybe I am putting words in his mouth here, but that is how I interpret his "Isabelle/Pure is in the same spirit". I think he is right. BUT, Isabelle is SO close to a foundation. All you have to do is to drop the types :-D. All of them. That's what I did, and you then basically get Abstraction Logic [1]. Abstraction Logic makes no assumptions whatsoever about your mathematical universe, except that it is non-empty, and it better have more than 1 object in it. It doesn't assume that sets exist, or types, or anything else. It doesn't force you to define natural numbers or other mathematical objects as sets. You can define any operator you want, and with each choice of axioms you are exposed to the risk of doing nonsense and creating paradoxes. And therefore I believe it is the right foundation for mathematics, and I think it is the only right one. Yes, there is a single logical foundation. Sounds too simple? So did set theory. Yes, I think Abstraction Logic is a miracle, but on the other hand, it simply manifests logic as it is.
> Abstraction Logic makes no assumptions whatsoever about your mathematical universe, except that it is non-empty, and it better have more than 1 object in it. It doesn't assume that sets exist, or types, or anything else.
This sounds kind of similar to something I've thought about, but which makes approximately one fewer assumption, while also remaining closer to set theory.
Namely, the theory of first order logic (without equality), with one binary relation symbol, and no axioms (unless you count the laws of inference of FOL, which you shouldn't).
If you name this binary relation symbol \in_0 , and are willing to use a "definition schema" to define, for each natural number in your meta-theory, binary relations \in_n and =_n (any sentence using these \in_n and =_n can be expanded out to a longer sentence in FOL using just quantifiers and \in_0),
then, in the meta theory, you can prove a fair number of nice things about "for all natural numbers n, it is provable in the object theory that [some statement which uses relations \in_n and/or =_n]".
For example, you can show that, for all n, you can show in the object-theory that =_n is transitive and reflexive, and that if x =_n y, then x =_{n+1} y as well,
and that for all A, B, if A \subseteq_n B , then A \subseteq_{n+1} B,
and you can define notions of one object being a power set of another object at level n (and any two power sets of an object at level n, will be equal at level n), and can show that, for all n, it is provable in the object theory that if A \subseteq_n B , and if PA is a powerset of A at level n, and PB is a powerset of B at level n, then PA \subseteq_n PB , and all sorts of similar things.
I'm a little skeptical of the "something between 1st order logic and 2nd order logic" claim, but I haven't looked closely.
Are you familiar with the metamath project? aiui, metamath is based in string rewrite rules, and is therefore fully general in the way it sounds like you are going for?
> I'm a little skeptical of the "something between 1st order logic and 2nd order logic" claim
And rightfully so. I've discovered Abstraction Logic (AL) over the course of the last two years, and in the beginning I didn't know exactly what I had there. In later papers on abstractionlogic.com I understand AL better, the latest being "Logic is Algebra". I would not say anymore that AL is in between first-order and second-order logic. Instead I would say that AL combines the benefits of first-order logic (one undivided mathematical universe U) with the benefits of higher-order logic (general binders). And there certainly is a second-order aspect to it, because an operator is a function that takes operations as arguments, and returns a value in the mathematical universe U; here an operation is a function that takes values in U as arguments, and also returns a value in U.
> Are you familiar with the metamath project
Yes, I know it. I would say the main difference is that metamath doesn't really have a proper semantics. It has some rules to manipulate syntax, but they don't mean anything on their own. Only by making the rules of metamath simulate the deduction rules of logics like first-order logic, meaning enters the picture, by inheriting meaning from the simulated logic. On the other hand, Abstraction Logic has a proper and simple semantics of its own.
> unless you count the laws of inference of FOL, which you shouldn't
So the laws for your quantifiers are not counted, I guess, but given as a built-in feature of FOL? In AL, quantifiers are just ordinary operators, and can be introduced via axioms (or not be introduced at all, if you prefer that for some reason).
If mathematics were the study of real objects, why didn't Platonists realize set theory was ill-founded a long time before Russell did? After all, Plato predates Russell by a few years.
The same reason it took so long to develop theories of gravity: nobody smart enough spent the time applying the tools needed to come to with it. The tools in this case being logic as the OP described.
Oh, it does give you special insight, but it doesn't make you infallible. It is easier to reach for something if you feel that it must be out there, and you just haven't got it right yet. That's how most mathematicians feel. Gödel was a Platonist, and I'd say he had really special insights.
So there's no actual advantage, since you can still be wrong and grasping for something that doesn't exist or that you can't define properly. It's just adding more mysticism to mathematics.
No, it is actually the opposite. It is removing mysticism (which I hate) and adds clarity. There are real things out there, and we can go and use them for our purposes. These things are so flexible that we can shape them into pretty much anything we want, bar inconsistency.
But yes, you need to state clearly the properties you are talking about. These can be axioms (and must be to a certain extent), but most of your math will consist of definitions (and theorems about them). And by doing all of this in a logic, on a computer, there is really no way to be much clearer and less mystic.
Thinking purely conceptual notions are real is mysticism. It's a confusion of layers, like in an Escher print: The hand is drawing itself, the water is going around infinitely, because the background is bleeding into the foreground and there's no consistent hierarchy. Well, an idea I have doesn't get to be as real as I am, too; I can't make a sphere be just as real as I am just because I imagined a sphere, any more than I can put a million dollars into my hand just because I imagined it to exist.
> But yes, you need to state clearly the properties you are talking about.
This is normal mathematics. It isn't unique to Platonism.
> And by doing all of this in a logic, on a computer, there is really no way to be much clearer and less mystic.
A software object, as a pattern of charge in memory circuits or in a storage device, isn't a Platonic form. It is real and it has all of the limits a real, physical object does, just like a bunch of marks on a blackboard or ink on a page. It is, conceptually, just notation, albeit one which is much more useful in some ways than paper notation. Platonism, as I understand it, posits that the purely conceptual is real, and partakes of forms, and all representations of those concepts are shadows of those forms.
Except... is Number a Form? If so, it would have one consistent set of properties, yet mathematicians have a lot of different kinds of numbers, with different properties, all useful and consistent within a given axiom system. Real numbers, Integers, Natural numbers, Complex numbers, Quaternions, Octonions, and Sedenions are all numbers, but no two of them are the same, and no two of them can, therefore, be of the same Form. In fact, we can apply what's called the Cayley-Dickson construction to create as many different kinds of numbers as we wish, to infinity, no two of which are the same but all of them are consistent and have some claim on Number-ness. If the form Number can be stretched that far, it isn't very good at predicting the properties things will have, and so it isn't all that useful, even aside from the objections I have to abstract concepts being real on the same level as me.
> Thinking purely conceptual notions are real is mysticism.
No, it is not. We just have to disagree here. What is 1? What is 2? Is it real? Of course it is. Is 3.5 + πi real? Yes, because what are you talking about if it is not? Something unreal?
> This is normal mathematics. It isn't unique to Platonism.
You can do mathematics without any philosophical grounding. In fact, most people do. It's just the way you study mathematics at university, it is pretty much platonic. Here is a vector space, deal with it. And it is pretty much the only philosophical grounding that makes sense to me. Of course a Turing machine is real. At the same time it is a purely mathematical object. So this mathematical object is real, and so are many others. You can make new concepts up as you go, and they are all real, if they are consistent. That's not mystic, it is a simple fact of life you should accept. It is not more mystic than life itself. Many concepts are real. That's why you can apply logic to them, and it works. And for some concepts, you can write them down, but they are inconsistent. And these are not real.
Writing down a concept in logic, I use a physical tool, the computer, but I really write it down in a mathematical object, represented on a computer. In my work, in Abstraction Logic. Abstraction Logic is real, even more real than the particular physical manifestation in form of software, for example. The software is just a shadow of the real Abstraction Logic. And only if I did not made a mistake implementing it. What is a mistake? Well, if my shadow doesn't match up to the real mathematical object that is Abstraction Logic.
> Fictionalism, on the other hand, is the view that (a) our mathematical sentences and theories do purport to be about abstract mathematical objects, as platonism suggests, but (b) there are no such things as abstract objects, and so (c) our mathematical theories are not true. Thus, the idea is that sentences like ‘3 is prime’ are false, or untrue, for the same reason that, say, ‘The tooth fairy is generous’ is false or untrue—because just as there is no such person as the tooth fairy, so too there is no such thing as the number 3.
Who knows, maybe they are right. For me personally, this view is not helpful, and it doesn't make sense to me.
The advantage of a robust philosophy of mathematics is that what you're doing actually makes sense. Some people care about conceptual clarity, and others don't. To each their own.
If you are a Platonist (I am), then it is not really a miracle. Mathematical objects are real, and logic is a tool to study them. The paradoxes can only exist, because math is real: a paradox shows that something is not real, and if there were no real mathematical objects to begin with, paradoxes would be meaningless. As it stands, a paradox is a tool to distinguish reality from that which is not real.
Have fun making any kind of sense if you are a formalist or intuitionist (hint: you can't).
It is indeed cool that something as simple as set theory covers so much. But it doesn't cover everything. The Banach-Tarski Paradox shows that sets are not what we imagine them to be (but they are still real): we need to add the property of measurability, which acts then as an additional axiom, to get closer to that. And in order to solve BB(748), ZFC is not enough [0, theorem 7]. So, one set theory is not enough. Depending on which properties we ascribe to sets, or in other words, which axioms we add to set theory, we also get different set theories.
> I give up.
Set theory is cool, but it is not special. In the end it describes a fragment of the (real) mathematical universe, but there is more to this universe than just set theory. And depending on which properties you pick for your sets, you get different fragments.
It is interesting that Larry says that Automath is not a Foundation, and that neither is Isabelle, which he created. Maybe I am putting words in his mouth here, but that is how I interpret his "Isabelle/Pure is in the same spirit". I think he is right. BUT, Isabelle is SO close to a foundation. All you have to do is to drop the types :-D. All of them. That's what I did, and you then basically get Abstraction Logic [1]. Abstraction Logic makes no assumptions whatsoever about your mathematical universe, except that it is non-empty, and it better have more than 1 object in it. It doesn't assume that sets exist, or types, or anything else. It doesn't force you to define natural numbers or other mathematical objects as sets. You can define any operator you want, and with each choice of axioms you are exposed to the risk of doing nonsense and creating paradoxes. And therefore I believe it is the right foundation for mathematics, and I think it is the only right one. Yes, there is a single logical foundation. Sounds too simple? So did set theory. Yes, I think Abstraction Logic is a miracle, but on the other hand, it simply manifests logic as it is.
[0] https://www.scottaaronson.com/papers/bb.pdf, page 12, theorem 7
[1] http://abstractionlogic.com