Comment by drdeca
2 years ago
> 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).