Proof-theoretic analysis by iterated reflection
Progressions of iterated reflection principles can be used as a tool for the ordinal analysis of formal systems. Moreover, they provide a uniform definition of a proof-theoretic ordinal for any arithmetical complexity Π0n
In their seminal paper:
Lincoln, P., Mitchell, J., Scedrov, A. and Shankar, N. (1992). Decision problems for propositional linear logic. Annals of Pure and Applied Logic 56 (1–3) 239–311,
LMSS have established an extremely surprising result that propositional linear logic is undecidable. Their proof is very complex and involves numerous nested inductions of different kinds. Later an alternative proof for the LL undecidability has been developed based on simulation Minsky machines in linear logic: Kanovich, M. (1995). The direct simulation of Minsky machines in linear logic. In: Girard, J.-Y., Lafont, Y. and Regnier, L. (eds.) Advances in Linear Logic, London Mathematical Society Lecture Notes, volume 222, Cambridge University Press 123–145. Notice that this direct simulation approach has been successfully applied for a large number of formal systems with resolving a number of open problems in computer science and even computational linguistics, e.g.,
James Brotherston, Max I. Kanovich: Undecidability of Propositional Separation Logic and Its Neighbours. J. ACM 61(2): 14:1-14:43 (2014), Max Kanovich, Stepan Kuznetsov, Andre Scedrov: Undecidability of the Lambek Calculus with a Relevant Modality. FG 2016: 240-256. Nevertheless, recently the undecidability of linear logic is questioned by some people. They claim that they have found lacunae in the LMSS 1992 paper, and, moreover, they have a proof that propositional linear logic is decidable!!! I have been asked to submit a paper, as clear as possible, to the Journal, in order to sort out such a confusing problem, once and for all.
Here, we give a fully self-contained, easy-to-follow, but fully detailed, direct and constructive proof of the undecidability of a very simple Horn-like fragment of linear logic, the proof is accessible to a wide range of people. Namely, we show that there is a direct correspondence between terminated computations of a Minsky machine M and cut-free linear logic derivations for a Horn-like sequent of the form \Phi_M, l1 |- l0 where \Phi_M consists only of Horn-like implications of the very simple forms. Neither negation, nor &, nor constants, nor embedded implications/bangs are used here. Furthermore, our particular correspondence constructed above provides decidability for some smaller Horn-like fragments along with the complexity bounds that come from the proof.
The set of all formulas whose n-provability in a given arithmetical theory S is provable in another arithmetical theory T is a recursively enumerable extension of S. We prove that such extensions can be naturally axiomatized in terms of transfinite progressions of iterated local reflection schemata over S. Specifically, the set of all provably 1-provable sentences in Peano arithmetic PA can be axiomatized by an epsilon(0)-times iterated local reflection schema over PA. The resulting characterizations provide additional information on the proof-theoretic strength of these theories and on the complexity of their axiomatization.
We introduce a game for (extended) Gödel logic where the players’ interaction stepwise reduces claims about the relative order of truth degrees of complex formulas to atomic truth comparison claims. Using the concept of disjunctive game states this semantic game is lifted to a provability game, where winning strategies correspond to proofs in a sequents-of-relations calculus.
A formula φ is called n-provable in a formal arithmetical theory S if φ is provable in S together with all true arithmetical Πn-sentences taken as additional axioms. While in general the set of all n-provable formulas, for a fixed n>0 , is not recursively enumerable, the set of formulas φ whose n-provability is provable in a given r.e. metatheory T is r.e. This set is deductively closed and will be, in general, an extension of S. We prove that these theories can be naturally axiomatized in terms of progressions of iterated local reflection principles. In particular, the set of provably 1-provable sentences of Peano arithmetic PA can be axiomatized by εo times iterated local reflection schema over PA . Our characterizations yield additional information on the proof-theoretic strength of these theories (w.r.t. various measures of it) and on their axiomatizability. We also study the question of speed-up of proofs and show that in some cases a proof of n-provability of a sentence can be much shorter than its proof from iterated reflection principles.