# Proof theory outside of structural proof theory (calculi)?

Is there proof theory for some more or less usual logics that is outside the scope of structural proof theory (Hilbert/natural deduction/sequent calculi)? E.g. proof theoy for adaptive logic (https://www.springer.com/gp/book/9783319007915) of defeasible logics that resembles logical programming or forward reasoning. What other proof techniques outside structural proof theory are available? Is it possible to classify and generalize them?

This question is concerned with more exotic theories such as ordinal analysis, mentioned in https://en.wikipedia.org/wiki/Proof_theory. I am more concerned with practical logics who are doing their proofs non-structural way.

Or maybe there are logics without proof theory (or any proof system) at all?

• Not very clear... Proof theory is the study of the properties of formalized proofs, considered as math objects. Thus, proof theory studies the properties of a proof system (or calculus): we may imagine a "logic" without a proof system, but if there is no proof system to consider, I cannot imagine a proof-theoretical study of it. – Mauro ALLEGRANZA Jul 3 '18 at 8:01
• Thanks! But what other branch of mathematics consider properties of other, non-formalized proofs? BTW what kind of mathematics is possible at all with non-formalized proofs? – TomR Jul 3 '18 at 8:04
• Structural proof theory is an approach to studying logics and their deductive systems. It is not a specific collection of logics or proof systems. It's a lens through which to view logic. Ordinal analysis is a different lens (and hardly a "more exotic" one). Model theory is yet another lens. They are all looking at the same thing. There aren't logics that are "out of scope" of structural proof theory. There are merely logics that may not yet have a compelling structural explanation. – Derek Elkins Jul 3 '18 at 8:08

## 1 Answer

A distinguished feature of what you have called structural proof theory deals with proof calculi that are monotonic. They share the property that:

$$\Gamma \vdash B \quad \Rightarrow \quad \Gamma, A \vdash B$$

In artificially intelligence and possibly also to some extend in philosophical logic, there is the field of non-monotonic logics.

Some of them work by translating back to a monotonic logic.