3 ms·

You are probably confusing "automation" with "mechanisation" here, and maybe also with "computing". It is very easy to automate set theory, at least when it is

You are probably confusing "automation" with "mechanisation" here, and maybe also with "computing". It is very easy to automate set theory, at least when it is just embedded in first-order logic, and at least compared to type theory. Automation of first-order logic is MUCH further and MUCH easier than automation of type theory, which is usually not much automated at all apart from a few tactics here and there. Furthermore, the prevalent use of type theory for mechanised interactive theorem proving is based on the work of Church on simple type theory, and extensions of that into dependent types. Computer scientists like the lambda calculus and types, and it gives a nice and general way for implementing binding. It also is straightforward to compute in it, but that is also easy to implement for set theory if you are interested in it (most people doing set theory are not). Ultimately, though, both set theory and type theory are just specific mathematical theories. This became apparent to me after I discovered what is probably the best foundational logic, Abstraction Logic (AL) [1], in which you can represent both as mathematical theories. AL is like first-order logic, but plus operators (and therefore binding), and like higher-order logic, but minus static types. What is missing for AL is an actual system implementing it, but that is in the works. [1]: https://obua.com/publications/philosophy-of-abstraction-logic/2/ https://obua.com/publications/philosophy-of-abstraction-logi...

zozbot234 4y ago
> ...in which you can represent both as mathematical theories... There are many logical frameworks (LF's) that are targeted at this same space. They're especially useful for exploring automated conversions of high-level "theories" to different axiomatic systems.
- practal 4y ago
  Yes, I know. The reason why you call them "frameworks" instead of logics is because they don't have a model-theory based semantics, but are justified via proof theory. Abstraction logic on the other hand is a logic with its own model-theory based semantics. To further elaborate why this is important: When you implement a logic in some LF, then it is up to you to do a pen and paper argument of what the semantics of your logic is, and why it is faithfully represented via the constructs of the LF, which itself has no semantics. On the other hand, to implement a logic in AL, you just write down its axioms, and the semantics of AL automatically gives a semantics for your logic, including soundness and completeness results. Of course, you still need to do a pen and paper argument that the semantics of your logic via AL is faithful to the semantics of your standalone logic. But this will only be done for the first few logics you implement in AL, future logics will just inherit their semantics from AL, and that will be their semantics then by definition.

zozbot234 4y ago

> ...in which you can represent both as mathematical theories... There are many logical frameworks (LF's) that are targeted at this same space. They're especially useful for exploring automated conversions of high-level "theories" to different axiomatic systems.

practal 4y ago
Yes, I know. The reason why you call them "frameworks" instead of logics is because they don't have a model-theory based semantics, but are justified via proof theory. Abstraction logic on the other hand is a logic with its own model-theory based semantics. To further elaborate why this is important: When you implement a logic in some LF, then it is up to you to do a pen and paper argument of what the semantics of your logic is, and why it is faithfully represented via the constructs of the LF, which itself has no semantics. On the other hand, to implement a logic in AL, you just write down its axioms, and the semantics of AL automatically gives a semantics for your logic, including soundness and completeness results. Of course, you still need to do a pen and paper argument that the semantics of your logic via AL is faithful to the semantics of your standalone logic. But this will only be done for the first few logics you implement in AL, future logics will just inherit their semantics from AL, and that will be their semantics then by definition.