A Sound, Complete and Effective Second Order Game Semantics
Stefano Berardi

TL;DR
This paper introduces an effective game semantics for second order classical arithmetic PA2, ensuring soundness and completeness, with strategies that are primitive recursive and a novel approach to predicate interpretation.
Contribution
It presents a new game semantics for PA2 that is both sound and complete, with effective strategies and a novel interpretation of predicate variables as generic games.
Findings
Semantics is effective with finite move descriptions.
Winning strategies are primitive recursive.
Model ensures soundness and completeness for PA2.
Abstract
We define a game semantics for second order classical arithmetic PA2 (with quantifiers over predicates on integers and full comprehension axiom). Our semantics is effective: moves are described by a finite amount of information and whenever there is some winning strategy for the player defending the truth of the formula, then there is some primitive recursive winning strategy. Then we show that our game semantics is sound and complete for the truth assignment for formulas of PA2. In our game model, the value of a predicate variable is some family of "generic" games. This value is "unknown" during the play, but at the end of the play it is used by a "judge of the play" to decide who is the winner.
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
TopicsArtificial Intelligence in Games · Computability, Logic, AI Algorithms · Logic, Reasoning, and Knowledge
