On the share of closed IL formulas which are also in GL

DOI10.1007/S00153-015-0438-7MaRDI QIDQ892132zbMATH OpenOpenAlexWikidataFDO

Authors Vedran Čačić, Vjekoslav Kovač

Publication date 18 November 2015

Published in Archive for Mathematical Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1309.3408

zbMATH Keywords

asymptotic enumerationinterpretability logicnormal formsprovability logic

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45) Asymptotic enumeration (05A16)

Abstract: Normal forms for wide classes of closed IL formulas were given in [4]. Here we quantify asymptotically, in exact numbers, how wide those classes are. As a consequence, we show that the "majority" of closed IL formulas have GL-equivalents, and by that, they have the same normal forms as GL formulas. Our approach is entirely syntactical, except for applying the results of [4]. As a byproduct we devise a convenient way of computing asymptotic behaviors of somewhat general classes of formulas given by their grammar rules. Its applications do not require any knowledge of the recurrence relations, generating functions, or the asymptotic enumeration methods, as all these are incorporated into two fundamental parameters.

Review text

\(\mathsf{IL}\) is one of the basic systems in the family of interpretability logics which were founded on the analogy with Gödel and Löb provability logic \(\mathsf{GL}\). Whereas the latter introduces an unary modal operator formalizing provability, the former use a binary operator of interpretability. Thus we may evaluate not only an absolute strength of a formula against a theory but a relative strength with respect to some added formula. Researches on \(\mathsf{GL}\) profitably use methods devised for investigations on modal logics. Similarly, it seems that in the research on \(\mathsf{IL}\) it is valuable to use techniques applied sucessfully to \(\mathsf{GL}\). In particular, one of the nice features of \(\mathsf{GL}\) is the existence of regular normal forms for every closed formula. It was already shown by the first author and \textit{M. Vuković} [Math. Commun. 17, No. 1, 195--204 (2012; Zbl 1252.03138)] that such a result holds for a wide classes of \(\mathsf{IL}\) formulas; the main result of that work is recalled in Section 3. The aim of this article is to establish precisely how wide these classes are. In a purely syntactic way, the authors show that the ``majority of closed \(\mathsf{IL}\) formulas has equivalents in \(\mathsf{GL}\) and, consequently, the same normal forms as respective \(\mathsf{GL}\) formulas. Moreover, a convenient way of computing asymptotic behaviours of some general classes of formulas is provided; all considered classes are summarised in the tables closing the paper. The method of computation proposed by the authors seems to be of quite general use, in fact it is first described in Section 2 with no special reference to \(\mathsf{IL}\).

Recommendations

• A note on the normal form of closed formulas of interpretability logic
• A note on normal forms for the closed fragment of system IL
• Classical and Intuitionistic Logic Are Asymptotically Identical
• The closed fragment of IL is PSPACE hard
• Distribution of the equilibrium logic formulas in classical logic metric space

Cites work

• A new principle in the interpretability logic of all reasonable arithmetical theories
• A note on normal forms for the closed fragment of system IL
• A note on the normal form of closed formulas of interpretability logic
• Analytic combinatorics
• Arithmetically complete modal theories
• scientific article; zbMATH DE number 3539473 (Why is no real title available?)
• scientific article; zbMATH DE number 1215477 (Why is no real title available?)
• Singularity Analysis of Generating Functions
• The closed fragment of IL is PSPACE hard
• The On-Line Encyclopedia of Integer Sequences

Cited in

(3)

• The closed fragment of IL is PSPACE hard
• An overview of Verbrugge semantics, a.k.a. generalised Veltman semantics
• A note on the normal form of closed formulas of interpretability logic

Describes a project that uses

Uses Software

• Mathematica
• OEIS

This page was built for publication: On the share of closed \(\mathsf {IL}\) formulas which are also in \(\mathsf {GL}\)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q892132)