Topological completeness of the provability logic GLP

Provability logic GLP is well-known to be incomplete w.r.t. Kripke semantics. A natural topological semantics of GLP interprets modalities as derivative operators of a polytopological space. Such spaces are called GLP-spaces whenever they satisfy all the axioms of GLP. We develop some constructions to build nontrivial GLP-spaces and show that GLP is complete w.r.t. the class of all GLP-spaces.     

Positive provability logic for uniform reflection principles

We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant ‘true’ by conjunction and diamonds only. The weaker language allows one to interpret the diamonds as the uniform reflection schemata in arithmetic, possibly of unrestricted logical complexity. We formulate an arithmetically complete calculus with modalities labeled by natural numbers and ω, where ω   corresponds to the full uniform reflection schema, whereas n<ω$n<\omega$ corresponds to its restriction to arithmetical _Πn+1${\Pi }_{n+1}$-formulas. This calculus is shown to be complete w.r.t. a suitable class of finite Kripke models and to be decidable in polynomial time.     

Around provability logic

We present some results on algebraic and modal analysis of polynomial (intrinsically definable) distortions of the standard provability predicate in Peano Arithmetic PA, and investigate three provability-like modal systems related to the Gödel-Löb modal system GL. We also present a short review of relational and topological semantics for these systems, and describe the dual category of algebraic models of our main modal system.     

Possible world semantics for first-order logic of proofs

In the tech report Artemov and Yavorskaya (Sidon) (2011) [4] an elegant formulation of the first-order logic of proofs was given, FOLP. This logic plays a fundamental role in providing an arithmetic semantics for first-order intuitionistic logic, as was shown. In particular, the tech report proved an arithmetic completeness theorem, and a realization theorem for FOLP. In this paper we provide a possible-world semantics for FOLP, based on the propositional semantics of Fitting (2005) [5]. We also give an Mkrtychev semantics. Motivation and intuition for FOLP can be found in Artemov and Yavorskaya (Sidon) (2011) [4], and are not fully discussed here.     

The omega-rule interpretation of transfinite provability logic

Given a computable ordinal Λ, the transfinite provability logic ${\mathsf{GLP}}_{\mathrm{\Lambda }}$ has for each $\xi <\mathrm{\Lambda }$ a modality $[\xi ]$ intended to represent a provability predicate within a chain of increasing strength. One possibility is to read $[\xi ]?$ as ? is provable in T using ω-rules of depth at most ξ, where T is a second-order theory extending ${\mathrm{ACA}}_0$.In this paper we will formalize such iterations of ω-rules in second-order arithmetic and show how it is a special case of what we call uniform provability predicates. Uniform provability predicates are similar to Ignatiev's strong provability predicates except that they can be iterated transfinitely. Finally, we show that ${\mathsf{GLP}}_{\mathrm{\Lambda }}$ is sound and complete for any uniform provability predicate.     

Kripke models for classical logic

We introduce a notion of the Kripke model for classical logic for which we constructively prove the soundness and cut-free completeness. We discuss the novelty of the notion and its potential applications.     

Proof internalization in generalized Frege systems for classical logic

We present a general method for inserting proofs in Frege systems for classical logic that produces systems that can internalize their own proofs.     

All finitely axiomatizable subframe logics containing the provability logic CSM_{0} are decidable

In this paper we investigate those extensions of the bimodal provability logic (alias or which are subframe logics, i.e. whose general frames are closed under a certain type of substructures. Most bimodal provability logics are in this class. The main result states that all finitely axiomatizable subframe logics containing are decidable. We note that, as a rule, interesting systems in this class do not have the finite model property and are not even complete with respect to Kripke semantics. Received July 15, 1997     

Bounded linear-time temporal logic: A proof-theoretic investigation

Propositional and first-order bounded linear-time temporal logics (BLTL and FBLTL, respectively) are introduced by restricting Gentzen type sequent calculi for linear-time temporal logics. The corresponding Robinson type resolution calculi, RC and FRC for BLTL and FBLTL respectively are obtained. To prove the equivalence between FRC and FBLTL, a temporal version of Herbrand theorem is used. The completeness theorems for BLTL and FBLTL are proved for simple semantics with both a bounded time domain and some bounded valuation conditions on temporal operators. The cut-elimination theorems for BLTL and FBLTL are also proved using some theorems for embedding BLTL and FBLTL into propositional (first-order, respectively) classical logic. Although FBLTL is undecidable, its monadic fragment is shown to be decidable.     

First order logic without equality on relativized semantics

Let $\alpha \ge 2$ be any ordinal. We consider the class ${\mathsf{Drs}}_{\alpha }$ of relativized diagonal free set algebras of dimension α. With same technique, we prove several important results concerning this class. Among these results, we prove that almost all free algebras of ${\mathsf{Drs}}_{\alpha }$ are atomless, and none of these free algebras contains zero-dimensional elements other than zero and top element. The class ${\mathsf{Drs}}_{\alpha }$ corresponds to first order logic, without equality symbol, with α-many variables and on relativized semantics. Hence, in this variation of first order logic, there is no finitely axiomatizable, complete and consistent theory.     

On arithmetical completeness of the logic of proofs

In this paper, we establish a stronger version of Artemov's arithmetical completeness theorem of the Logic of Proofs ${\mathsf{LP}}_0$. Moreover, we prove a version of the uniform arithmetical completeness theorem of ${\mathsf{LP}}_0$.     

Provability logic and the completeness principle

The logic $\mathsf{iGLC}$ is the intuitionistic version of Löb's Logic plus the completeness principle $A\to \square A$. In this paper, we prove an arithmetical completeness theorems for $\mathsf{iGLC}$ for theories equipped with two provability predicates □ and △ that prove the schemes $A\to △A$ and $\square △S\to \square S$ for $S\in {\mathrm{\Sigma }}_1$. We provide two salient instances of the theorem. In the first, □ is fast provability and △ is ordinary provability and, in the second, □ is ordinary provability and △ is slow provability.Using the second instance, we reprove a theorem previously obtained by Mohammad Ardeshir and Mojtaba Mojtahedi [1] determining the ${\mathrm{\Sigma }}_1$-provability logic of Heyting Arithmetic.     

Prefixed tableaus and nested sequents

Nested sequent systems for modal logics are a relatively recent development, within the general area known as deep reasoning. The idea of deep reasoning is to create systems within which one operates at lower levels in formulas than just those involving the main connective or operator. Prefixed tableaus go back to 1972, and are modal tableau systems with extra machinery to represent accessibility in a purely syntactic way. We show that modal nested sequents and prefixed modal tableaus are notational variants of each other, roughly in the same way that Gentzen sequent calculi and tableaus are notational variants. This immediately gives rise to new modal nested sequent systems which may be of independent interest. We discuss some of these, including those for some justification logics that include standard modal operators.     

Normal deduction in the intuitionistic linear logic

We describe a natural deduction system NDIL for the second order intuitionistic linear logic which admits normalization and has a subformula property. NDIL is an extension of the system for !-free multiplicative linear logic constructed by the author and elaborated by A. Babaev. Main new feature here is the treatment of the modality !. It uses a device inspired by D. Prawitz' treatment of S4 combined with a construction introduced by the author to avoid cut-like constructions used in -elimination and global restrictions employed by Prawitz. Normal form for natural deduction is obtained by Prawitz translation of cut-free sequent derivations. Received: March 29, 1996     

A game semantics for disjunctive logic programming

Denotational semantics of logic programming and its extensions (by allowing negation, disjunctions, or both) have been studied thoroughly for many years. In 1998, a game semantics was given to definite logic programs by Di Cosmo, Loddo, and Nicolet, and a few years later it was extended to deal with negation by Rondogiannis and Wadge. Both approaches were proven equivalent to the traditional semantics. In this paper we define a game semantics for disjunctive logic programs and prove soundness and completeness with respect to the minimal model semantics of Minker. The overall development has been influenced by the games studied for PCF and functional programming in general, in the styles of Abramsky–Jagadeesan–Malacaria and Hyland–Ong–Nickau.     

No Escape from Vardanyan's theorem

Vardanyan's theorem states that the set of PA-valid principles of Quantified Modal Logic, QML, is complete Π⁰₂. We generalize this result to a wide class of theories. The crucial step in the generalization is avoiding the use of Tennenbaum's Theorem.     

A simplified proof of arithmetical completeness theorem for provability logic GLP

We present a simplified proof of Japaridze’s arithmetical completeness theorem for the well-known polymodal provability logic GLP. The simplification is achieved by employing a fragment J of GLP that enjoys a more convenient Kripke-style semantics than the logic considered in the papers by Ignatiev and Boolos. In particular, this allows us to simplify the arithmetical fixed point construction and to bring it closer to the standard construction due to Solovay.     

A modal logic framework for reasoning about comparative distances and topology

We propose and investigate a uniform modal logic framework for reasoning about topology and relative distance in metric and more general distance spaces, thus enabling the comparison and combination of logics from distinct research traditions such as Tarski’s S4 for topological closure and interior, conditional logics, and logics of comparative similarity. This framework is obtained by decomposing the underlying modal-like operators into first-order quantifier patterns. We then show that quite a powerful and natural fragment of the resulting first-order logic can be captured by one binary operator comparing distances between sets and one unary operator distinguishing between realised and limit distances (i.e., between minimum and infimum). Due to its greater expressive power, this logic turns out to behave quite differently from both S4 and conditional logics. We provide finite (Hilbert-style) axiomatisations and ExpTime-completeness proofs for the logics of various classes of distance spaces, in particular metric spaces. But we also show that the logic of the real line (and various other important metric spaces) is not recursively enumerable. This result is proved by an encoding of Diophantine equations.     

On the positive fragment of the polymodal provability logic GLP

The fragment of the polymodal provability logic GLP in the language with connectives ┬, Λ, and 〈n〉 for all n ∈ ω is considered. For this fragment, a deductive system is constructed, a Kripke semantics is proposed, and a polynomial bound for the complexity of a decision procedure is obtained.