Comment by practal
2 years ago
> 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.
[0] https://www.scottaaronson.com/papers/bb.pdf, page 12, theorem 7
> 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.
So if Platonism doesn't give you any special insight into mathematics, what good is it?
8 replies →