Predicate provability logic with non-modalized quantifiers

DOI10.1007/BF00370393MaRDI QIDQ1176101zbMATH OpenFDO

Authors Giorgie Dzhaparidze

Publication date 25 June 1992

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF00370393

zbMATH Keywords

Gödel numbersGödel-Löb's logic GLKripke modelsPeano arithmeticpredicate modal logicprovability logicprovably binumerablerecursive enumerabilitySolovay's logic S

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) First-order arithmetic and fragments (03F30) Gödel numberings and issues of incompleteness (03F40)

Review text

A modal predicate formula is called a \(Q'\)-formula if it has no quantifiers within the scope of \(\square\). Let \(T\) be an arithmetical theory extending Peano arithmetic \((PA)\); it is also supposed that all theorems of \(T\) are true, and Gödel numbers of axioms of \(T\) are given by a formula \(\alpha(x)\) which is provably binumerable in \(T\), that is \[ T\vdash\forall x(\alpha(x)\to Pr[\alpha(x)])\land\forall x(\neg\alpha(x)\to P_ 2[\neg\alpha(x)]) \] (\(Pr\) is based on \(\alpha\) and encodes provability in \(T\)). As usual, \(Q'\)-formulas can be interpreted as arithmetical ones if \(\square\) is transcribed as \(Pr\). \(Q'L(T)\) (resp. \(Q'L\)) denotes the set of all \(Q'\)-formulas whose interpretations are always provable in \(T\) (resp. true). It is known that if \(T\) is \(RE\) then \(Q'L(T)\) is \(\Pi^ 0_ 2\)-complete (Vardanyan) and \(Q'L\) is non-arithmetical (Artemov). The paper proves that nevertheless \(Q'L(T)\) and \(Q'L\) can be axiomatized in some other cases. Namely, let \(Q'GL\), \(Q'S\) be \(Q'\)-fragments of quantified versions of Gödel-Łöb's logic \(GL\) and Solovay's logic \(S\). The main theorem claims that \(Q'L(T)=Q'GL\) and \(Q'L=Q'S\) whenever \(Pr_{Q'GL}(x)\) is provably binumerable in \(T\).

Recommendations

• scientific article; zbMATH DE number 4204315
• Nonaxiomatizability of predicate logics of proofs
• Provability logics with quantifiers on proofs
• The predicate modal logic of provability
• Non-Fregean propositional logic with quantifiers
• scientific article; zbMATH DE number 3976994
• On propositional quantifiers in provability logic
• Quantification and predication in modal predicative propositional logic
• Provability in predicate product logic
• Propositional modal logic with implicit modal quantification

Cites work

• Arithmetization of metamathematics in a general setting
• Decidable and enumerable predicate logics of provability
• scientific article; zbMATH DE number 3635994 (Why is no real title available?)
• Omega-consistency and the diamond
• Provability interpretations of modal logic
• The degree of the set of sentences of predicate provability logic that are true under every interpretation
• The predicate modal logic of provability

Cited in

(7)

• Proof-irrelevant model of CC with predicative induction and judgmental equality
• On predicate provability logics and binumerations of fragments of Peano arithmetic
• scientific article; zbMATH DE number 2174393 (Why is no real title available?)
• Arithmetical interpretations and Kripke frames of predicate modal logic of provability
• scientific article; zbMATH DE number 4197983 (Why is no real title available?)
• The predicate modal logic of provability
• Provability in predicate product logic

This page was built for publication: Predicate provability logic with non-modalized quantifiers

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