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

DOI10.1017/JSL.2022.51arXiv2112.00486MaRDI QIDQ6203558FDOQ6203558

Robert Paßmann

Publication date: 5 April 2024

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

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.

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)

Cites Work

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

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)