Material Dialogues for First-Order Logic in Constructive Type Theory

Paper i proceeding, refereegranskad
Författare
Dominik Wehr | Institutionen för filosofi, lingvistik och vetenskapsteori
Dominik Kirst | Extern
Publikationsår
2022
Publicerad i
Logic, Language, Information, and Computation, 28th International Workshop, WoLLIC 2022, Iași, Romania, September 20–23, 2022, Proceedings / Editors: Agata Ciabattoni, Elaine Pimentel, Ruy J. G. B. de Queiroz
Sammanfattning
Material dialogues are turn taking games which model debates about the satisfaction of logical formulas. A novel variant played over first-order structures gives rise to a notion of first-order satisfaction. We study the induced notion of validity for classical and intuitionistic first-order logic in the constructive setting of the calculus of inductive constructions. We prove that such material dialogue semantics for classical first-order logic admits constructive soundness and completeness proofs, setting it apart from standard model theoretic semantics of first-order logic. Furthermore, we prove that completeness with regards to intuitionistic material dialogues fails in constructive and classical settings. The results concerning classical material dialogues have been mechanized using the Coq interactive theorem prover.
ISSN
0302-9743
E-ISSN
1611-3349
Ämnesord
  • NATURVETENSKAP | Matematik | Algebra och logik
Nyckelord
Constructive Type Theory, Dialogue Games, First-Order Logic, Game Semantics
Språk
Engelska
Ytterligare information
Lecture Notes in Computer Science, volume 13468
Publikations-ID
321060
Identifikatorer