Computer Science – Logic in Computer Science
Scientific paper
2010-11-07
LMCS 6 (4:11) 2010
Computer Science
Logic in Computer Science
Scientific paper
10.2168/LMCS-6(4:11)2010
Goedel'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 [3], 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) P, either P is a proof of A or there is a model M of the orthogonal of A which defeats P. Compared with proofs of full completeness in game semantics, ours exhibits a striking similarity with proofs of Goedel's completeness, in that it explicitly constructs a countermodel essentially using Koenig's lemma, proceeds by induction on formulas, and implies an analogue of Loewenheim-Skolem theorem.
Basaldella Michele
Terui Kazushige
No associations
LandOfFree
On the meaning of logical completeness does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with On the meaning of logical completeness, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and On the meaning of logical completeness will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-245930