Logic of proofs and provability

DOI10.1016/S0168-0072(01)00066-5MaRDI QIDQ5957921zbMATH OpenFDO

Authors Tatiana Yavorskaya

Publication date 11 December 2002

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0168-0072(01)00066-5

zbMATH Keywords

arithmetical provability interpretationfunctional completenesslogic of proofsmodal logic for provabilityoperations on proofs

Mathematics Subject Classification ID

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

Review text

Artemov's logic LP of proofs is extended by adjoining the GL modality so as to incorporate both the modality for provability and the operator representing the proof predicate ``is a proof of. To formalize the joint logic, two new operations on proof terms are required for the language in addition to the ``application, ``proof checker, and ``choice of LP. The author gives an axiomatization of the logic, which is shown to be complete, with respect to the intended arithmetical provability interpretations as well as to the Kripke-type semantics, to be decidable, and to enjoy a kind of functional completeness on proof terms meaning that any invariant operation on proofs admitting description in the modal propositional language can be realized by a proof polynomial.

Recommendations

• scientific article; zbMATH DE number 1320664
• scientific article; zbMATH DE number 1735872
• Logic of proofs
• The logic of proofs, semantically
• The basic intuitionistic logic of proofs

Cites work

• Explicit provability and constructive semantics
• scientific article; zbMATH DE number 1114340 (Why is no real title available?)
• scientific article; zbMATH DE number 1114356 (Why is no real title available?)
• scientific article; zbMATH DE number 1170091 (Why is no real title available?)
• Logic of proofs
• Provability interpretations of modal logic
• Self-reference and modal logic

Cited in

(52)

• Logic of proofs
• Provability logic and the completeness principle
• An operational logic of proofs with positive and negative information
• Hypothetical logic of proofs
• Justified common knowledge
• Referential logic of proofs
• scientific article; zbMATH DE number 1670490 (Why is no real title available?)
• scientific article; zbMATH DE number 1670501 (Why is no real title available?)
• Substructural logic of proofs
• Prefixed tableau systems for logic of proofs and provability
• scientific article; zbMATH DE number 5840915 (Why is no real title available?)
• On symbolic models for single-conclusion logic of proofs
• Systems of axioms and models for the first order theories with provability operator
• Analytic methods for the logic of proofs
• Reference Constructions in the Single-conclusion Proof Logic
• Logic of Proofs and Labels with a Complete Set of Operations
• Logic of Proofs for Bounded Arithmetic
• scientific article; zbMATH DE number 5157044 (Why is no real title available?)
• On two models of provability
• Topological Semantics of Justification Logic
• Tableaux and Hypersequents for Justification Logic
• 2008 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '08
• Operations on proofs and labels
• Extracting Information from Logical Proofs
• scientific article; zbMATH DE number 1320664 (Why is no real title available?)
• scientific article; zbMATH DE number 515725 (Why is no real title available?)
• scientific article; zbMATH DE number 1735872 (Why is no real title available?)
• scientific article; zbMATH DE number 1114348 (Why is no real title available?)
• scientific article; zbMATH DE number 1114356 (Why is no real title available?)
• scientific article; zbMATH DE number 1166301 (Why is no real title available?)
• Biological Perspectives Irreversible Lithium-Induced Neuropathy: Two Cases
• scientific article; zbMATH DE number 1751350 (Why is no real title available?)
• Kolmogorov and Gödel's approach to intuitionistic logic: current developments
• Proofs and Models in Philosophical Logic
• scientific article; zbMATH DE number 7241862 (Why is no real title available?)
• scientific article; zbMATH DE number 7288886 (Why is no real title available?)
• Stoic Sequent Logic and Proof Theory
• Logics of proofs and justifications
• The basic intuitionistic logic of proofs
• Decidability for some justification logics with negative introspection
• Rational proofs
• Explicit Proofs in Formal Provability Logic
• Symmetric Logic of Proofs
• scientific article; zbMATH DE number 5037198 (Why is no real title available?)
• Negative Operations on Proofs and Labels
• On Kripke-style Semantics for the Provability Logic of Gödel's Proof Predicate with Quantifiers on Proofs
• Provability logics with quantifiers on proofs
• A modal provability logic of explicit and implicit proofs
• Chair of Mathematical Logic and Theory of Algorithms
• The logic of proofs, semantically
• Derivability in certain subsystems of the logic of proofs is _2p-complete
• Feasible operations on proofs: the logic of proofs for bounded arithmetic

This page was built for publication: Logic of proofs and provability

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