Talk:Compactness Theorem

Wikipedia claims this theorem is actually equivalent to BPIT and Gödel's Completeness Theorem. --Dfeuer (talk) 07:58, 13 December 2012 (UTC)

Before posting up any more proofs using this claim, it would be good to post both BPIT and GCT up on this site. As it stands, with the crucial information missing, it makes us look embarrassingly lame. It makes us look like a bunch of amateurs pretending to be clever, which is one of the main criticisms which is brought against this site. --prime mover (talk) 22:55, 13 December 2012 (UTC)

Sure. I can try to do some, but a lot of the set theory is over my head. It disturbs me, however, to see "this theorem depends on AoC" when in fact it only depends on BPIT, AoCC, AoDC, etc., even if I don't personally know how to prove that. --Dfeuer (talk) 22:59, 13 December 2012 (UTC)

I hate to say this, but if all this is over your head, should you not leave well alone? Is all you know about this what you've picked up from wikipedia? --prime mover (talk) 07:25, 14 December 2012 (UTC)

Substantial error in proof with ultraproducts

As I noted with a questionable template, $\{\uparrow(E) \mid E \in T \}$ isn't actually a filter on $\Sigma$ as claimed. I just glanced over at Wikipedia and see that rather than looking at finite sets containing individual statements, their proof considers finite sets including finite sets of statements, which makes a lot more sense. Since I don't know anything about ultraproducts yet, I don't feel comfortable trying to fix this proof, but someone really should. --Dfeuer (talk) 21:08, 24 December 2012 (UTC)

I went back to look at the original page put up by some dude with the username qedetc who didn't stay around long (put off by my rudeness, I believe). His original posting did not provide any links (and consistently refused to do so, one of the reasons for my rudeness to him). (Or her, coulda been f, nobody knows.) So it's possible that "filter" as originally used here is not the same as the definition we provide on the website.

Please feel free to take all pages written by qedetc with suspicion. --prime mover (talk) 22:40, 24 December 2012 (UTC)

Rewrote that section. Proof is almost the same; it's just using finite collections of sentences rather than individual sentences. From this you can justify that the set defined is contained in an ultrafilter. (As it stood, the proof was nearly correct - $\{\uparrow(E) \mid E \in T \}$ is contained in an ultrafilter, but it's not clearly exactly why this should be. As I've rewritten it this is justified using the finite intersection property.) Bakkot (talk) 08:41, 26 December 2012 (UTC)

Thanks - this page and much of the stuff which was added at the time is up for a reorganisation so as to ensure that it adheres to house style. Your input is welcome. --prime mover (talk) 10:17, 26 December 2012 (UTC)

It's definitely better, but:

1. Can't the proof of the finite intersection property be simplified by proving it just for pairwise intersections and then applying induction?
2. We still need to show how FIP leads to ultrafilter. I'm no expert, but don't we need to show that $F$ is a filter on some set and then invoke the ultrafilter lemma?
3. I personally find the name $\Sigma_0$ confusingly similar to $\Sigma$. Would it break convention to rename it $\sigma_0$? --Dfeuer (talk) 20:43, 26 December 2012 (UTC)

1. I wouldn't call that simpler - as it stands, we're directly constructing an element contained in the intersection. Induction seems like overkill.
2. You're right that this invokes the ultrafilter lemma. In order to use said lemma, what we need is that $F$ can be extended to a filter (on $\Sigma$). This is true in general of collections of sets with FIP: the obvious choice is the collection of supersets of finite intersections of elements in $F$, that is, $\{ A \in \mathcal{P}(\Sigma) \mid F_{\Sigma_1} \cap \dots \cap F_{\Sigma_n} \subseteq A, F_{\Sigma_{i=1,2,\dots,n}} \in F \}$. This is a filter containing $F$, to which we can apply the ultrafilter lemma to obtain $U$. Feel free to add this to the main page, if you think it helps.
3. The use of `$\Sigma_0$' to refer to a finite collection of sentences is fairly standard, I think, and the use of the capital letter reminds us that the $\Sigma_0$ are themselves sets. If you want to change the notation, I'd suggest renaming $\Sigma$ to $I$, to emphasize that it's serving as an indexing set. --Bakkot (talk) 21:25, 26 December 2012 (UTC)

1. That's a matter of taste. I'm accustomed to seeing theorems like that proven pairwise. You don't need to get into details of induction because the same inductive pattern works for any associative, commutative binary operator. It's quite common, for example, to prove a function is finitely additive, or that a certain set is a base for a topology, by just looking at the two-element case.
2. As you showed, finite intersections of elements of $F$ are themselves elements of $F$, so supersets of such intersections are just supersets of elements of $F$, a slight simplification.

I'd like to propose splitting this page in two. There are two versions of the Compactness Theorem (as well as the Completeness Theorem) that need to be studied separately. They are (minus some formalism):

Every finitely satisfiable theory is satisfiable

and

Any finitely satisfiable theory with language $\LL$, where $\LL$ is well-orderable, has either:

A finite model

or

A model of cardinality $\alpha$ for every infinite well-orderable $\alpha \ge \size \LL$

I propose naming the second one the "Strong Compactness Theorem," and adding it as a subpage of the current one.

The first form (with no cardinalities) is equivalent to BPIT (see Jech's "The Axiom of Choice").

The second requires no more than ZF, but becomes much stronger in the presence of full AC, due to Zermelo's Theorem. It does, however, apply to all languages with a countable number of symbols. This form is most easily derived from a matching Strong Completeness Theorem, proved through Henkin's construction.

One last note, we can get full (cardinality-less) completeness with Compactness and Strong Completeness, since every finite subset of the language contains a countable number of symbols. --CircuitCraft (talk) 20:58, 17 July 2023 (UTC)