TITLE: Does every logic have sequent calculus, if not - what are alternatives to them? What prohibits to make general sequent calculus for universal logic?
QUESTION [1 upvotes]: Does every logic have sequent calculus, if not - what are alternatives to them? What prohibits to make general sequent calculus for universal logic?
The question arises in several application domains. E.g. as far as I know then logic can be encoded as categorical logic if logic admits sequent calculus. Therfore - is all logics have sequent calculus, then categorical logic can be made as universal logic. OpenCog project (open source implementation of CogPrime cognitive architecture) supports multiple reasoning styles and logics if those logics admit sequent calculus. Therefore - is OpenCog general enough framework if it only support logics having sequent calculus?

REPLY [4 votes]: It depends what you mean by "logic". Is second-order logic a logic? If so, then the answer to your question is no: second-order logic has no associated sequent calculus, since it is not compact (so in particular there is no way to represent entailment in second-order logic in a finitary way).

Note that there are other non-compact logics - say, infinitary logic $\mathcal{L}_{\omega_1\omega}$. However, second-order logic is a more compelling counterexample: unlike $\mathcal{L}_{\omega_1\omega}$, which does have a kind of proof system associated to it (via an infinitary sequent calculus, developed by Lopez-Escobar and later Barwise, if I recall correctly) which is reasonably set-theoretically absolute, second-order logic is just completely terrible.
Specifically, the question of validity in second-order logic - what second-order sentences are true in all models - is a fundamentally set-theoretic one. For example, there is a sentence $\varphi$ in second-order logic which is valid iff the Continuum Hypothesis holds, and similarly for many other set-theoretic statements (this general phenomenon is reflected in the ludicrous size of the Hanf number of second-order logic).

Maybe this suggests that you should restrict attention to compact logics. If so, though, you'll be hard pressed to find examples other than first-order logic (and its sublogics) without invoking some set-theoretic ideas. This is because of Lindstrom's theorem, which states that there is no logic strictly stronger than first-order logic which is compact and has the Lowenheim-Skolem property. So, if you want a logic stronger than first-order logic, it had better do something complicated with respect to uncountable structures, specifically. An example is first-order logic with a quantifier for "there are uncountably many," which was shown to be (countably) compact by Keisler if I recall correctly; there are other more technical examples known.
{"set_name": "stack_exchange", "score": 1, "question_id": 2063828}