2014/09/09 by Michele Basaldella
Computer Science · Mathematics · #Algebra over a field #Calculus (dental) #Completeness (order theory) #Computer science #Conservative extension #Discrete mathematics #Extension (predicate logic) #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematical proof #Mathematics #Negation #Programming language #Propositional calculus #Pure mathematics #Semantics (computer science) #Sequent calculus #cs.LO
paper · pdf · doi:10.4204/eptcs.164.4
published as EPTCS 164, 2014, pp. 48-62 · In Proceedings CL&C 2014, arXiv:1409.2593
openalex publication_date 2014/09/09 · arxiv created 2014/09/11 · arxiv updated 2014/09/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
In this paper, we present an interactive semantics for derivations in an infinitary extension of classical logic. The formulas of our language are possibly infinitary trees labeled by propositional variables and logical connectives. We show that in our setting every recursive formula equation has a unique solution. As for derivations, we use an infinitary variant of Tait-calculus to derive sequents. The interactive semantics for derivations that we introduce in this article is presented as a debate (interaction tree) between a test << T >> (derivation candidate, Proponent) and an environment << not S >> (negation of a sequent, Opponent). We show a completeness theorem for derivations that we call interactive completeness theorem: the interaction between << T >> (test) and << not S >> (environment) does not produce errors (i.e., Proponent wins) just in case << T >> comes from a syntactical derivation of << S >>.