Material Dialogues for First-Order Logic in Constructive Type Theory

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.