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

被引：3

作者：

Passmann, Robert ^{[1
]}

机构：

[1] Univ Amsterdam, Inst Logic Language & Computat, Fac Sci, POB 94242, NL-1090 GE Amsterdam, Netherlands

来源：

JOURNAL OF SYMBOLIC LOGIC | 2024年 / 89卷 / 01期

关键词：

intuitionistic set theory; constructive set theory; first-order logic; tautologies of a theory; admissible rules; CHOICE; RULES;

D O I：

10.1017/jsl.2022.51

中图分类号：

O1 [数学];

学科分类号：

0701 ; 070101 ;

摘要：

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.

引用

下载

页码：308 / 330

页数：23

共 50 条

[1] Intuitionistic completeness of first-order logic
Constable, Robert
Bickford, Mark
ANNALS OF PURE AND APPLIED LOGIC, 2014, 165 (01) : 164 - 198
[2] First-Order Logic and First-Order Functions
Freire, Rodrigo A.
LOGICA UNIVERSALIS, 2015, 9 (03) : 281 - 329
[3] ON THE MINTS HIERARCHY IN FIRST-ORDER INTUITIONISTIC LOGIC
Schubert, Aleksy
Urzyczyn, Pawel
Zdanowski, Konrad
LOGICAL METHODS IN COMPUTER SCIENCE, 2016, 12 (04)
[4] On the Mints Hierarchy in First-Order Intuitionistic Logic
Schubert, Aleksy
Urzyczyn, Pawel
Zdanowski, Konrad
FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES (FOSSACS 2015), 2015, 9034 : 451 - 465
[5] A Lindstrom theorem for intuitionistic first-order logic
Olkhovikov, Grigory
Badia, Guillermo
Zoghifard, Reihane
ANNALS OF PURE AND APPLIED LOGIC, 2023, 174 (10)
[6] Combining First-Order Classical and Intuitionistic Logic
Toyooka, Masanobu
Sano, Katsuhiko
ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2022, (358): : 25 - 40
[7] Embedding First-order Classical Logic into Gurevich’s Extended First-order Intuitionistic Logic: The Role of Strong Negation
Kamide, Norihiro
Journal of Applied Logics, 2023, 10 (06): : 1025 - 1058
[8] EMBEDDING FIRST-ORDER CLASSICAL LOGIC INTO GUREVICH'S EXTENDED FIRST-ORDER INTUITIONISTIC LOGIC: THE ROLE OF STRONG NEGATION
Kamide, Norihiro
JOURNAL OF APPLIED LOGICS-IFCOLOG JOURNAL OF LOGICS AND THEIR APPLICATIONS, 2023, 10 (06):
[9] A First-Order Logic with Frames
Murali, Adithya
Pena, Lucas
Loeding, Christof
Madhusudan, P.
PROGRAMMING LANGUAGES AND SYSTEMS ( ESOP 2020): 29TH EUROPEAN SYMPOSIUM ON PROGRAMMING, 2020, 12075 : 515 - 543
[10] Extended First-Order Logic
Brown, Chad E.
Smolka, Gert
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2009, 5674 : 164 - 179

← 1 2 3 4 5 →