On the Meaning of Logical Completeness

G¨odel’s completeness theorem is concerned with provability, while Girard’s theorem in ludics (as well as full completeness theorems in game semantics) are concerned with proofs. Our purpose is to look for a connection between these two disciplines. Following a previous work [1], we consider an extension of the original ludics with contraction and universal nondeterminism, which play dual roles, in order to capture a polarized fragment of linear logic and thus a constructive variant of classical propositional logic. We then prove a completeness theorem for proofs in this extended setting: for any behaviour (formula) A and any design (proof attempt)

• Type: Conference
• Year: 2009
• Where: TLCA
• Authors: Michele Basaldella, Kazushige Terui
• Keywords: Completeness Theorem, Game Semantics, G¨odel’s Completeness Theorem, Theoretical Computer Science, TLCA 2009