2 ms·
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
by 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.