Game semantics for first-order logic
Logic in Computer Science
2015-07-01 v2
Abstract
We refine HO/N game semantics with an additional notion of pointer (mu-pointers) and extend it to first-order classical logic with completeness results. We use a Church style extension of Parigot's lambda-mu-calculus to represent proofs of first-order classical logic. We present some relations with Krivine's classical realizability and applications to type isomorphisms.
Keywords
Cite
@article{arxiv.1009.4400,
title = {Game semantics for first-order logic},
author = {Olivier Laurent},
journal= {arXiv preprint arXiv:1009.4400},
year = {2015}
}