1
$\begingroup$

I am interested in the relationship between completeness and compactness of formal logical systems. I think it is pretty well known that if an effective proof system can be developed for a formal semantics, then that semantics must have the compactness property. In a slogan: "Completeness implies compactness".

But what about the other way? Is it possible for a formal semantics to have the compactness, but with respect to which an effective proof system which sound&complete cannot be produced?

If such a system could be produced, this would represent a counter example to the slogan "Compactness implies completeness".

Thus my question is: While compactness and completeness are clearly not identical properties (completeness involves proof theoretic notions, like computability), are they extensionally equivalent over formal systems?

Improve this question
$\endgroup$
4
  • 1
    $\begingroup$ See the following related question: mathoverflow.net/q/9309/1946 $\endgroup$
    – Joel David Hamkins
    Commented Dec 7, 2017 at 17:15
  • 7
    $\begingroup$ 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. $\endgroup$
    – Andreas Blass
    Commented Dec 7, 2017 at 17:37
  • $\begingroup$ 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. $\endgroup$
    – Noah Schweber
    Commented Dec 7, 2017 at 22:13
  • 2
    $\begingroup$ @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. $\endgroup$
    – Noah Schweber
    Commented Dec 7, 2017 at 22:17

0

Reset to default

You must log in to answer this question.

Browse other questions tagged .