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 条
  • [21] A First-order Logic with Frames
    Murali, Adithya
    Pena, Lucas
    Loeding, Christof
    Madhusudan, P.
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2023, 45 (02):
  • [22] Indistinguishability and first-order logic
    Jordan, Skip
    Zeugmann, Thomas
    THEORY AND APPLICATIONS OF MODELS OF COMPUTATION, PROCEEDINGS, 2008, 4978 : 94 - 104
  • [23] From separation logic to first-order logic
    Calcagno, C
    Gardner, P
    Hague, M
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, PROCEEDINGS, 2005, 3441 : 395 - 409
  • [24] From First-Order Logic to Assertional Logic
    Zhou, Yi
    ARTIFICIAL GENERAL INTELLIGENCE: 10TH INTERNATIONAL CONFERENCE, AGI 2017, 2017, 10414 : 87 - 97
  • [25] Sperner spaces and first-order logic
    Blass, A
    Pambuccian, V
    MATHEMATICAL LOGIC QUARTERLY, 2003, 49 (02) : 111 - 114
  • [26] First-order conditional logic revisited
    Friedman, N
    Halpern, JY
    Koller, D
    PROCEEDINGS OF THE THIRTEENTH NATIONAL CONFERENCE ON ARTIFICIAL INTELLIGENCE AND THE EIGHTH INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE, VOLS 1 AND 2, 1996, : 1305 - 1312
  • [27] On First-Order Logic and CPDA Graphs
    Christopher H. Broadbent
    Theory of Computing Systems, 2014, 55 : 771 - 832
  • [28] DATALOG VS FIRST-ORDER LOGIC
    AJTAI, M
    GUREVICH, Y
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 1994, 49 (03) : 562 - 588
  • [29] First-Order da Costa Logic
    Graham Priest
    Studia Logica, 2011, 97 : 183 - 198
  • [30] First-order classical modal logic
    Arló-Costa H.
    Pacuit E.
    Studia Logica, 2006, 84 (2) : 171 - 210
12345