Logic - 2019-09-15

6:49 AM

So I just completed the non-compactness, and incompleteness section of the Standford Introduction to logic online course, and I have developed a few questions.

When mentioning compactness, they also mention the notion of finite subsets of sentences. However in the logic they construct, called Herbrand logic (HL), there is no way to specify a finite subset of a Herbrand base, in the deductive system itself.

How to we define the notion of finite subset of sentences in HL?

Since they do not define what a finite subset of sentences in HL is, they must be reasoning in a meta system about HL.…

One more thing (a comment this time not a question).

The automated proof verifier tool appears to be broken, because one is able to write Skolem terms as a premise. Doing so allows for a contradiction to be derived from $p([c1])$ and $\exists x. (\lnot p(x))$, since the tool specifies to $[c1]$ by default from $\exists x. (\lnot p(x))$.

You can find the course link here:
http://logic.stanford.edu/intrologic/lessons/lessons.html

user21820

7:14 AM

@user400188 Every theorem about logic is necessarily a theorem of some meta-system. This includes the incompleteness theorems, compactness theorem, completeness theorem, and so on. If your meta-system is not able to reason about finite strings, you simply cannot study logic at all.

That said, it would be erroneous to think that the study of logic depends on set theory. One only needs a meta-system MS that is capable of a certain amount of reasoning about finite strings and finite sets of finite strings, to prove almost all basic facts about logic, such as the three I just mentioned.

Sorry, not just finite sets of finite strings. That is enough for the incompleteness theorem but not enough for the compactness theorem or completeness theorem, for which you need to be able to handle infinite (but rather nice) sets of finite strings.

user400188

Is there a general method for determining whether true statements about the meta system, are also true for the system it describes?

user21820

If you're interested in the precise technical details of what MS must be capable of, I can elaborate, but roughly you just need TC plus induction plus reification of each first-order predicate over TC, which means that we have one sort str for strings and one sort set for sets of strings, and for each first-order property Q over TC we have the axiom ∃S∈set ∀x∈str ( x∈S ⇔ Q(x) ).

Normally, when we actually study logic we assume not just basic string facts but also PA (with one more sort nat for natural numbers), and some function/predicate-symbols and axioms relating nat and str, such as len : str → nat so that we can express induction for strings simply as part of the full induction schema over the whole language.

But it turns out that you can with not too much work encode natural numbers in finite (binary) strings and therefore we don't need anything more than the second-order language of TC (i.e. with just str and set and + : str^2 → str).

Nevertheless, it is instructive to start with the more convenient system with nat, str and set, and prove your theorems about logic there.

I sketch these aspects of MS, not only because it is important to know what exactly you are relying on, but also because it is relevant to your other question about soundness of MS.

It should not come as a surprise that since MS itself is an FOL system, and since MS proves the incompleteness theorems, MS itself proves that itself cannot prove itself consistent unless itself is inconsistent.

That means that we do not have any non-circular way of justifying the consistency, much less soundness of MS, unless you a priori already accept the soundness of TC.

But that also means that it is not too bad, because almost every logician does accept the soundness of TC (mere basic facts about finite binary strings). Soundness of TC implies soundness of TC plus reification of FOL predicates over TC, and soundness of a system with nat implies soundness of the same system with the full induction schema.

@user400188 So to complete the answer to your question, the compactness theorem is true if MS is sound, which we believe is so. It is still relative to MS, and even the notion of "finite" is relative to MS, because MS has its own idea of what nat is.

user400188

7:36 AM

That's a shame, and it was going to be my next question (more or less).

I'll give it here anyway: We use a meta system that is already not compact, and apply it to HL. We then show using MS that HL is non-compact.

However, we knew a prior that MS is not compact, so what is so surprising about the fact that MS describing this particular system would also not be compact? Why do we conclude after this reasoning that HL is not compact?

user21820

@user400188 I don't understand what you mean by "system that is not compact". Compactness is about a logic, not a specific system over the logic.

user400188

Ah, I see you answered the question in your next few comments.

user21820

FOL has compactness, and MS is an FOL system, so it enjoys the compactness property (for instance if MS is inconsistent then there is a finite set of axioms of MS that are inconsistent).

user400188

@user21820 Oh my reading is a bit behind here. To answer this, I was considering the MS to be a logic itself (since there is no restriction of what a logic can be, we might as well consider it as one to deduce certain things about where convenient.)

At the stage of writing, I did not know that MS was compact.

user21820

Again, it's not a system that is compact, but the logic. Every meta-system that is a first-order theory would satisfy what compactness of FOL implies about it.

user400188

7:41 AM

So there is a difference between MS possessing the compactness property, and MS been compact?

user21820

Nobody talks about systems being compact. I'm just following conventional definitions.

user400188

Ok, I'm just unfamiliar with them.

user21820

"Compactness" is an indivisible term describing certain logics.

FOL satisfies compactness (every finitely satisfiable set of formulae over a given language is satisfiable). Certain other logics don't.

Sorry I keep mixing up compactness and completeness because they are related.

What I just wrote is completeness...

Compactness for FOL follows from completeness for FOL.

Wait a minute, why does wikipedia say this is compactness...

user400188

The Intro to logic definition is this:

In light of the negative results described in the last section, namely that Herbrand Logic is inherently incomplete, it is not surprising that Herbrand Logic is not compact. Recall that Compactness says that if an infinite set of sentences is unsatisfiable, there is some finite subset that is unsatisfiable.

This definition has the form of A->B, so we can transpose this and get ~B->~A. Namely:
"If all finite subset of sentences are satisfiable, then the infinite set of sentences the subset is constructed from will also be satisfiable. "

I say consistent here, however the Wikipedia definition appears to be stricter, using a bi-conditional instead.

user21820

7:58 AM

Yes I mixed up later, because I remember the proof instead of the result. What I wrote at first was indeed compactness. Completeness is that ( S ⊨ Q ) implies ( S ⊢ Q ) for every set S of formulae and every formula Q.

The simplest proof of both theorems go via proving that if S is consistent then S has a model. This implies completeness, because if S does not prove Q then S∪{¬Q} is consistent and hence has a model, contradicting ( S ⊨ Q ).

It also implies compactness, because if S is finitely satisfiable then it is finitely consistent and hence consistent, which implies that S has a model.

Got to go for a while.

user400188

Alright, thank you for your time and help with my questions :)

user21820

9:17 AM

@user400188: Oh and in case it isn't obvious, completeness implies compactness because if S is not satisfiable then ( S ⊨ ⊥ ), which by completeness implies ( S ⊢ ⊥ ), contradicting consistency of S.

user21820

9:43 AM

I also took a look at what the link had to say about compactness and incompleteness, and I have to say that I am quite unsatisfied with their approach. They claim that Herbrand semantics is easier to understand than the (standard) semantics, but their anecdotal results with students is badly misleading, and their claim is in fact false. Students in general are incapable of assessing their understanding of a mathematical topic, so whether they think they do does not reflect whether they do.

user21820

10:23 AM

Maybe I should elaborate a bit. Their claim is false because everything is harder to do with Herbrand semantics than with standard semantics, and Herbrand semantics is easier to understand after the standard semantics has been understood. For example, you cannot capture the notion of "group" at all using Herbrand semantics, nor can you capture the reals in a mathematically productive way.

And once you understand standard semantics, a Herbrand model is simply conceptualized as a (standard-semantics) term model.

user21820

10:35 AM

This is not an idle distinction; standard semantics abstracts the domain from the structural properties, and this is crucial in FOL, even more so in many-sorted FOL, which every mathematically practical variant of FOL has to support.

Transcript for

♦ $Mathematics$ Logic

Transcript for

♦ Logic

♦ $Mathematics$ Logic