Timeline for Compact formal semantics which is incompletable?
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 7, 2017 at 22:17 | comment | added | Noah Schweber | @AndreasBlass That might not be fully satisfying since the resulting logic applies to a smaller class of structures than first-order logic. Another fix in the same spirit is to add for each $a\in\mathbb{N}$ a new logical constant $\top_a$, which is interpreted as "true" if $a\in A$ and "false" if $a\not\in A$. This has the same "range of semantics" as first-order logic, and is compact since every sentence in it is equivalent to an FOL sentence, but again the validities aren't recursively enumerable. | |
| Dec 7, 2017 at 22:13 | comment | added | Noah Schweber | As Andreas' comment shows, it is trivially possible to have a compact logic with no recursive proof system. I think, though, that the question of whether there are any natural examples is a very good one. There are plenty of natural compact logics beyond first-order (the book Model-theoretic logics forms an excellent source on this point - while several chapters are quite technical, there are a number which focus on explicit natural examples), and I don't know if all of them are known to have an r.e. set of validities. | |
| Dec 7, 2017 at 17:37 | comment | added | Andreas Blass | Fix some non-r.e. set $A$ of positive integers, and extend first-order logic by building in the requirement that, if the underlying set of a structure is finite, then its cardinality must not be in $A$. This amounts to adding to first-order logic, the axioms expressing "the size of the universe is not $a$" for each $a\in A$. So compactness for this logic follows from compactness for ordinary first-order logic. But there's no effective, sound, complete proof system, because the set of valid statements is not computably enumerable. | |
| Dec 7, 2017 at 17:15 | comment | added | Joel David Hamkins | See the following related question: mathoverflow.net/q/9309/1946 | |
| Dec 7, 2017 at 16:37 | review | First posts | |||
| Dec 7, 2017 at 16:39 | |||||
| Dec 7, 2017 at 16:35 | history | asked | J. Short | CC BY-SA 3.0 |