Proving Infinitary Formulas
Amelia Harrison, Vladimir Lifschitz, and Julian Michael

TL;DR
This paper establishes a connection between the validity of infinitary formulas in the logic of here-and-there and their provability in finite deductive systems, enabling finite proofs for infinitary formulas.
Contribution
It introduces a method to use finite proofs to verify the validity of infinitary formulas in the logic of here-and-there.
Findings
Finite proofs can justify the validity of infinitary formulas.
A relationship between infinitary validity and finite provability is established.
This approach simplifies reasoning in infinitary propositional logic.
Abstract
The infinitary propositional logic of here-and-there is important for the theory of answer set programming in view of its relation to strongly equivalent transformations of logic programs. We know a formal system axiomatizing this logic exists, but a proof in that system may include infinitely many formulas. In this note we describe a relationship between the validity of infinitary formulas in the logic of here-and-there and the provability of formulas in some finite deductive systems. This relationship allows us to use finite proofs to justify the validity of infinitary formulas. This note is under consideration for publication in Theory and Practice of Logic Programming.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Multi-Agent Systems and Negotiation · Logic, programming, and type systems
