On the meaning of logical completeness
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 consid...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2010-12-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/1066/pdf |
| _version_ | 1827322950516211712 |
|---|---|
| author | Michele Basaldella Kazushige Terui |
| author_facet | Michele Basaldella Kazushige Terui |
| author_sort | Michele Basaldella |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:38:02Z |
| format | Article |
| id | doaj.art-bd48c62b3d154002948d5cf63c5c62e1 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:38:02Z |
| publishDate | 2010-12-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-bd48c62b3d154002948d5cf63c5c62e12024-03-08T09:14:02ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742010-12-01Volume 6, Issue 410.2168/LMCS-6(4:11)20101066On the meaning of logical completenessMichele BasaldellaKazushige TeruiGoedel'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.https://lmcs.episciences.org/1066/pdfcomputer science - logic in computer sciencef.3.2, f.4.1 |
| spellingShingle | Michele Basaldella Kazushige Terui On the meaning of logical completeness Logical Methods in Computer Science computer science - logic in computer science f.3.2, f.4.1 |
| title | On the meaning of logical completeness |
| title_full | On the meaning of logical completeness |
| title_fullStr | On the meaning of logical completeness |
| title_full_unstemmed | On the meaning of logical completeness |
| title_short | On the meaning of logical completeness |
| title_sort | on the meaning of logical completeness |
| topic | computer science - logic in computer science f.3.2, f.4.1 |
| url | https://lmcs.episciences.org/1066/pdf |
| work_keys_str_mv | AT michelebasaldella onthemeaningoflogicalcompleteness AT kazushigeterui onthemeaningoflogicalcompleteness |