?
Proof-theoretic analysis by iterated reflection
P. 225–270.
Beklemishev L. D.
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 book
Basel: Birkhauser/Springer, 2015.
Zaitsev I., Логические исследования 2025 Т. 31 № 2 С. 143–168
This article presents a labeled Fitch-style natural deduction system, 𝓕IntCK, for the basic propositional intuitionistic conditional logic IntCK introduced by G.K. Olkhovikov. The logic IntCK serves as a correct intuitionistic counterpart to Chellas' minimal conditional logic CK, designed to accommodate Lewis' strong and weak counterfactual conditionals within a single framework. In order to do this, IntCK features two independent logical connectives, namely □→ and ◇→, ...
Added: November 23, 2025
M.: [б.и.], 2021.
The Logical Perspectives Summer School and Workshop Series aims at giving advanced introductions into various branches of logic, and providing researchers — including early career scientists — with an opportunity to present their work.
In particular, LP 2021 Summer School (June 14–16) and Workshop (June 17–19) will focus on computational proof theory, broadly understood. The programme will comprise three ...
Added: December 14, 2021
Kanovich M., Kuznetsov S., Scedrov A., Journal of Logic and Computation 2020 Vol. 30 No. 1 P. 239–256
The Lambek calculus can be considered as a version of non-commutative intuitionistic linear logic. One of the interesting features of the Lambek calculus is the so-called ‘Lambek’s restriction’, i.e. the antecedent of any provable sequent should be non-empty. In this paper, we discuss ways of extending the Lambek calculus with the linear logic exponential modality ...
Added: July 1, 2020
Pavlova A., Lang T., Fermüller, C., , in: Information Processing and Management of Uncertainty in Knowledge-Based Systems 18th International Conference, IPMU 2020, Lisbon, Portugal, June 15–19, 2020, Proceedings, Part IVol. 1237. Issue 1.: Springer, 2020. P. 257–270.
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. ...
Added: June 3, 2020
Beklemishev L. D., Kolmakov E., Doklady Mathematics 2018 Vol. 98 No. 3 P. 582–585
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 ...
Added: June 24, 2019
Kolmakov E., Beklemishev L. D., Journal of Symbolic Logic 2019 Vol. Volume 84 No. Issue 2 P. 849–869
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 ...
Added: June 24, 2019
Max I. Kanovich, Mathematical Structures in Computer Science 2016 Vol. 26 No. 5 P. 719–744
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 ...
Added: September 1, 2016