-
Notifications
You must be signed in to change notification settings - Fork 22
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
880a991
commit cca5d81
Showing
4 changed files
with
95 additions
and
2 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,26 @@ | ||
--- | ||
title: Compactness Theorem | ||
date: 2024-12-15T16:09:38-05:00 | ||
references: [] | ||
tags: [In_Progress] | ||
--- | ||
|
||
# Statement and Proofs | ||
|
||
{{< env type="theorem" name="Compactness Thoerem; Gödel 1930 & Maltsev 1936" >}} | ||
|
||
Let $L$ be a first-order language. If an $L$-theory $T$ is finitely-satisfiable, then $T$ is satisfiable. In fact, $T$ admits a model $M\models T$ with $|M|\leq\max\l\\{|L|,\aleph_0\r\\}$.{{< /env >}} | ||
|
||
{{< env type="proof" hide="false" name="from Completeness" >}} | ||
|
||
Every $L$-theory is *syntactically-compact*, in the sense that $T$ is consistent iff every $T$ is finitely-consistent. | ||
> Indeed, if $\phi$ witnesses inconsistency of $T$, then there are finite subtheories $\Delta_0,\Delta_1\subseteq T$ such that $\Delta_0\proves\phi$ and $\Delta_1\proves\lnot\phi$. Their union $\Delta\coloneqq\Delta_0\cup\Delta_1$ is then an inconsistent finite subtheory of $T$, a contradiction. | ||
The {{< link file="completeness_theorem.md" display="Completeness Theorem" type="proved_by" >}} then applies, since if $T$ is finitely-satisfiable, it is finitely-consistent, and hence consistent by the above.<span style="float:right;">$\blacksquare$</span>{{< /env >}}<div class="space"></div> | ||
|
||
{{< env type="proof" hide="false" name="with Ultraproducts" >}} | ||
|
||
Suppose w.l.o.g. that $T$ is infinite and let $\mc{D}$ be the collection of all finite-subtheories of $T$. For each $\Delta\in\mc{D}$, let $M_\Delta\models\Delta$, and let $X_\Delta\subseteq\mc{D}$ be the subcollection of all finite-subtheories of $T$ containing $\Delta$. Since $X_{\Delta_1}\cap X_{\Delta_2}=X_{\Delta_1\cup\Delta_2}$ for any two $\Delta_i\in\mc{D}$, the collection $F\coloneqq\l\\{X\subseteq\mc{D}\st X\supseteq X_\Delta\textrm{ for some }\Delta\in\mc{D}\r\\}$ is a filter, which extends to an ultrafilter $U\supseteq F$. | ||
<br> | ||
  We claim that the {{< link file="ultraproduct.md" display="ultraproduct" type="references" >}} $M\coloneqq\prod_{\Delta\in\mc{D}}M_\Delta/U$ models $T$. Indeed, for any $\phi\in T$, we have $M_\Delta\models\phi$ for all $\Delta\in X_{\l\\{\phi\r\\}}$, and thus $X_{\l\\{\phi\r\\}}\subseteq\l\\{\Delta\in\mc{D}\st M_\Delta\models\phi\r\\}$. Since $X_{\l\\{\phi\r\\}}\in U$, we have $\l\\{\Delta\in\mc{D}\st M_\Delta\models\phi\r\\}\in U$, and hence $M\models\phi$ by {{< link file="ultraproduct.md" display="Łoś’s Theorem" type="proved_by" secID="los_theorem" secDisplay="Łoś’s Theorem" >}}.<span style="float:right;">$\blacksquare$</span> | ||
{{< /env >}} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,18 @@ | ||
--- | ||
title: Theory | ||
date: 2024-12-15T16:05:04-05:00 | ||
references: [] | ||
tags: [In_Progress] | ||
--- | ||
|
||
# Motivation & Definition | ||
|
||
{{< env type="definition" >}} | ||
|
||
Let $L$ be a first-order language. An *$L$-theory* $T$ is a collection of $L$-sentences. A *deductively-closed* theory is a theory that is closed under provability, i.e., $\phi\in T$ whenever $T\proves\phi$.{{< /env >}} | ||
|
||
## Complete theories | ||
|
||
## Consistent and satisfiable theories | ||
|
||
# The Category of Theories |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
--- | ||
title: Ultraproduct | ||
date: 2024-12-15T16:27:53-05:00 | ||
references: [] | ||
tags: [In_Progress] | ||
--- |