Comment by practal

> 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).