THE FIRST-ORDER LOGIC OF CZF IS INTUITIONISTIC FIRST-ORDER LOGIC

DOI10.1017/JSL.2022.51MaRDI QIDQ6203558zbMATH OpenFDO

Authors Robert Paßmann

Publication date 5 April 2024

Published in Journal of Symbolic Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

admissible rulesfirst-order logicconstructive set theoryintuitionistic set theorytautologies of a theory

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Intermediate logics (03B55) Nonclassical and second-order set theories (03E70) Metamathematics of constructive systems (03F50) Intuitionistic mathematics (03F55)

Abstract: We prove that the first-order logic of CZF is intuitionistic first-order logic. To do so, we introduce a new model of transfinite computation (Set Register Machines) and combine the resulting notion of realisability with Beth semantics. On the way, we also show that the propositional admissible rules of CZF are exactly those of intuitionistic propositional logic.

Recommendations

• Intuitionistic completeness of first-order logic
• On the quantificational logic of intuitionistic set theory
• A Lindström theorem for intuitionistic first-order logic
• The continuum and first-order intuitionistic logic
• A short introduction to intuitionistic logic

Cites work

• scientific article; zbMATH DE number 5064954 (Why is no real title available?)
• A quasi-intumonistic set theory
• A semantical proof of De Jongh's theorem
• Axiom of Choice and Complementation
• Choice Implies Excluded Middle
• Constructivism in mathematics. An introduction. Volume I
• Derived rules for predicative set theory: an application of sheaves
• Foundations of set theory. With the collaboration of Dirk van Dalen. 2nd revised ed
• Intermediate logics and Visser's rules
• Intermediate logics and the de Jongh property
• Logics of intuitionistic Kripke-Platek set theory
• On the admissible rules of intuitionistic propositional logic
• On the quantificational logic of intuitionistic set theory
• Rules and arithmetics
• Set Theory
• The formulae-as-classes interpretation of constructive set theory
• The upper semi-lattice of degrees of recursive unsolvability

Cited in

(10)

• Ideal presentations and numberings of some classes of effective quasi-Polish spaces
• On the Weihrauch degree of the additive Ramsey theorem
• On the first-order parts of problems in the Weihrauch degrees
• Hilbert's tenth problem for term algebras with a substitution operator
• Defining long words succinctly in FO and MSO
• Complemented subsets and Boolean-valued, partial functions
• Algorithmically random series
• Lower bounds on () and other properties of -register machines
• Conservativity of type theory over higher-order arithmetic
• Full generalized effective reducibility

This page was built for publication: THE FIRST-ORDER LOGIC OF CZF IS INTUITIONISTIC FIRST-ORDER LOGIC

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