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 条
  • [31] A denotational semantics for first-order logic
    Apt, KR
    COMPUTATIONAL LOGIC - CL 2000, 2000, 1861 : 53 - 69
  • [32] Combining Probability and First-Order Logic
    Russell, Stuart
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (345): : 4 - 4
  • [33] Monitoring First-Order Interval Logic
    Havelund, Klaus
    Omer, Moran
    Peled, Doron
    SOFTWARE ENGINEERING AND FORMAL METHODS (SEFM 2021), 2021, 13085 : 66 - 83
  • [34] Relating Z and first-order logic
    Martin, A
    FM'99-FORMAL METHODS, VOL II, 1999, 1709 : 1266 - 1280
  • [35] GAME SEMANTICS FOR FIRST-ORDER LOGIC
    Laurent, Olivier
    LOGICAL METHODS IN COMPUTER SCIENCE, 2010, 6 (04) : 1 - 50
  • [36] Rigid First-Order Hybrid Logic
    Blackburn, Patrick
    Martins, Manuel
    Manzano, Maria
    Huertas, Antonia
    LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION (WOLLIC 2019), 2019, 11541 : 53 - 69
  • [37] Abductive equivalence in first-order logic
    Inoue, Katsumi
    Sakama, Chiaki
    LOGIC JOURNAL OF THE IGPL, 2006, 14 (02) : 333 - 346
  • [38] Keynote: The First-Order Logic of Signals
    Bakhirkin, Alexey
    Ferrere, Thomas
    Henzinger, Thomas A.
    Nickovic, Dejan
    2018 PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE (EMSOFT), 2018,
  • [39] First-order Logic with Connectivity Operators
    Schirrmacher, Nicole
    Siebertz, Sebastian
    Vigny, Alexandre
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2023, 24 (04)
  • [40] Anytime reasoning in first-order logic
    Vanderveen, KB
    Ramamoorthy, CV
    NINTH IEEE INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 1997, : 142 - 148
12345