Infinitary logic with infinite sequents: syntactic investigations

Summary: This paper investigates various non-contractive logical systems from a proof-theoretic perspective, aiming to avoid logical and semantic paradoxes. It introduces an additive quantifier first-order system and compares it with Grisin set theory. The reasons behind the inconsistency phenomenon of multiplicative quantifiers are analyzed. Additionally, the exponentials in affine logic are interpreted as vacuous quantifiers, and it is shown how such logic can be simulated within a truth-free fragment of a system with multiplicative quantifiers. Finally, it establishes the consistency of the logic for these multiplicative quantifiers without disquotational truth by eliminating an infinitary version of the cut rule, paving the way for a syntactic approach to the proof theory of infinitary logic with infinite sequents.

Summary: The Godel-McKinsey-Tarski embedding allows for a modal logic interpretation of intuitionistic logic. In this paper, an extension of the modal embedding to infinitary intuitionistic logic is introduced. The paper presents a neighborhood semantics for a family of axiomatically presented infinitary modal logics and proves soundness and completeness using canonical models. The paper also establishes the soundness and faithfulness of the embedding and employs it to relate classical, intuitionistic, and modal derivability in infinitary logic extended with axioms. ©2023 Elsevier B.V. All rights reserved.

Summary: The article discusses infinitary modal logic. It first addresses the challenges in developing a satisfactory proof theory and then proposes a solution by introducing a labelled sequent calculus that is sound and complete based on Kripke semantics. The article also explores the structural properties of the system and its extensions to handle common knowledge and first-order logic.

Summary: Neighbourhood semantics for intuitionistic logic extended with countable conjunctions and disjunctions is introduced and shown equivalent to topological semantics, with an indirect completeness proof as payoff. The new semantics is used to obtain a labelled sequent calculus with good structural properties, demonstrating admissibility of weakening and contraction, invertibility with preservation of height for each rule, and cut elimination. Finally, a direct Tait-Schutte-Takeuti style form of completeness via the extraction of a countermodel from a failed proof search is proved.