[Zurück]

R. Kuznets:
"Through an Inference Rule, Darkly";
in: "Mathesis Universalis, Computability and Proof", S. Centrone, S. Negri, D. Sarikaya, P. Schuster (Hrg.); Springer International Publishing, Cham, 2019, ISBN: 978-3-030-20446-4, S. 131 - 158.

Mathematical logic provides a formal language to describe complex abstract phenomena whereby a finite formula written in a finite alphabet states a property of an object that may even be infinite. Thus, the complexity of the underlying objects is abstracted away to give way for a simple syntactic description, a kind of mathesis universalis. The complexity, however, continues affecting which ways of reasoning are valid.

Structural proof theory reasons using proof objects more complex than individual formulas. One of its goals is to find minimal additional structures, depending on the complexity of the underlying objects, sufficient for efficient and modular reasoning about them.

In this paper, we are primarily interested in both the global structure used for reasoning and the local part of this structure employed to justify single inference steps. We provide recently developed examples where adapting the global structure of the sequent to the local structure of (potentially infinite) Kripke models yielded both quantitative and qualitative benefits in establishing fundamental logical properties such as complexity and interpolation.

http://dx.doi.org/10.1007/978-3-030-20447-1_10

https://publik.tuwien.ac.at/files/publik_270741.pdf