Academic Journal
The First-Order Logic of CZF is Intuitionistic First-Order Logic
| العنوان: | The First-Order Logic of CZF is Intuitionistic First-Order Logic |
|---|---|
| المؤلفون: | Passmann, R. |
| المصدر: | Passmann , R 2024 , ' The First-Order Logic of CZF is Intuitionistic First-Order Logic ' , Journal of Symbolic Logic , vol. 89 , no. 1 , pp. 308-330 . https://doi.org/10.1017/jsl.2022.51 |
| سنة النشر: | 2024 |
| المجموعة: | Universiteit van Amsterdam: Digital Academic Repository (UvA DARE) |
| الوصف: | 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. |
| نوع الوثيقة: | article in journal/newspaper |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | https://dare.uva.nl/personal/pure/en/publications/the-firstorder-logic-of-czf-is-intuitionistic-firstorder-logic(181ade77-af43-4789-b332-363cd0d7d760).html |
| DOI: | 10.1017/jsl.2022.51 |
| الاتاحة: | https://dare.uva.nl/personal/pure/en/publications/the-firstorder-logic-of-czf-is-intuitionistic-firstorder-logic(181ade77-af43-4789-b332-363cd0d7d760).html https://doi.org/10.1017/jsl.2022.51 https://hdl.handle.net/11245.1/181ade77-af43-4789-b332-363cd0d7d760 https://pure.uva.nl/ws/files/181213454/the-first-order-logic-of-czf-is-intuitionistic-first-order-logic.pdf http://www.scopus.com/inward/record.url?scp=85133952119&partnerID=8YFLogxK |
| Rights: | info:eu-repo/semantics/openAccess |
| رقم الانضمام: | edsbas.F979076F |
| قاعدة البيانات: | BASE |
| DOI: | 10.1017/jsl.2022.51 |
|---|