Basic predicate calculus is not sound with respect to the strong variant of strictly primitive recursive realizability

DOI10.1134/S000143462201028XMaRDI QIDQ2113424zbMATH OpenOpenAlexWikidataFDO

Authors A. Yu. Konovalov

Publication date 14 March 2022

Published in Mathematical Notes (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1134/s000143462201028x

zbMATH Keywords

realizabilityconstructive semanticsbasic predicate calculus BQCstrictly primitive recursive realizability

Mathematics Subject Classification ID

Proof theory and constructive mathematics (03Fxx) Model theory (03Cxx) General logic (03Bxx)

Recommendations

• THE NONARITHMETICITY OF THE PREDICATE LOGIC OF STRICTLY PRIMITIVE RECURSIVE REALIZABILITY
• The nonarithmeticity of the predicate logic of primitive recursive realizability
• scientific article; zbMATH DE number 2019914
• Strictly primitive recursive realizability, I
• A Gentzen-style axiomatization for basic predicate calculus
• Strictly primitive recursive realizability. II: Completeness with respect to iterated reflection and a primitive recursive \(\omega\)-rule
• scientific article; zbMATH DE number 3557757
• General recursive realizability and basic logic
• On the strong semantical completeness of the intuitionistic predicate calculus
• Nonaxiomatizability of predicate logics of proofs

Cites work

• scientific article; zbMATH DE number 3083488 (Why is no real title available?)
• A propositional logic with explicit fixed points
• Basic predicate calculus
• Enumeration and the Grzegorczyk Hierarchy
• On the interpretation of intuitionistic number theory
• Provably total functions of Basic Arithmetic
• Strictly primitive recursive realizability, I

Cited in

(2)

• Basic predicate calculus is sound with respect to a modified version of strictly primitive recursive realizability
• A Generalized Realizability and Intuitionistic Logic

This page was built for publication: Basic predicate calculus is not sound with respect to the strong variant of strictly primitive recursive realizability

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