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?

$\endgroup$
4
  • 1
    $\begingroup$ See the following related question: mathoverflow.net/q/9309/1946 $\endgroup$ 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$ 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$ 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$ Dec 7, 2017 at 22:17

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.