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 rulesconstructive set theoryfirst-order logicintuitionistic 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

• 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
• scientific article; zbMATH DE number 5064954 (Why is no real title available?)
• Intermediate logics and the de Jongh property
• Intermediate logics and Visser's rules
• 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)

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

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)