Lý thuyết mô hình

Điều này gây kinh ngạc: $\Sigma$ có thể vô hạn, thậm chí mã hóa vô hạn ràng buộc, nhưng tính nhất quán chỉ cần kiểm từng hữu hạn ràng buộc một lúc. Đây là cầu nối từ chứng minh hữu hạn (một suy diễn hình thức luôn là đối tượng hữu hạn) tới ngữ nghĩa vô hạn (một mô hình có thể vô hạn), và là định lý duy nhất chịu trách nhiệm cho sự tồn tại của các mô hình vô hạn và phi chuẩn xuyên suốt lý thuyết mô hình.

Ta chứng minh mệnh đề phản đảo: nếu $\Sigma$ không có mô hình, thì có một $\Sigma_0 \subseteq \Sigma$ hữu hạn không có mô hình.

Giả sử $\Sigma$ không thỏa mãn được. Theo Định lý Đầy đủ Gödel cho logic bậc một (kéo theo ngữ nghĩa trùng với suy dẫn cú pháp: $\Sigma \models \bot$ khi và chỉ khi $\Sigma \vdash \bot$), việc $\Sigma$ không thỏa mãn được tương đương với $\Sigma$ không nhất quán về cú pháp, tức $\Sigma \vdash \bot$ — một mâu thuẫn suy dẫn được hình thức từ $\Sigma$.

Một suy dẫn hình thức theo định nghĩa là một dãy hữu hạn các công thức, mỗi công thức được biện minh bởi một tiên đề, một tiền đề từ $\Sigma$, hoặc một quy tắc suy luận áp dụng cho các dòng trước. Vì suy dẫn của $\bot$ hữu hạn, nó chỉ trích dẫn hữu hạn tiền đề từ $\Sigma$; gom chúng vào tập hữu hạn $\Sigma_0 = \{\sigma_1, \dots, \sigma_n\} \subseteq \Sigma$.

Chính suy dẫn hữu hạn đó, chỉ dùng tiền đề từ $\Sigma_0$, chứng thực $\Sigma_0 \vdash \bot$. Theo tính đúng đắn của logic bậc một (suy dẫn được kéo theo kéo theo ngữ nghĩa), $\Sigma_0 \models \bot$, tức $\Sigma_0$ không thỏa mãn được — nó không có mô hình.

Vậy ta đã tạo ra một $\Sigma_0 \subseteq \Sigma$ hữu hạn không có mô hình, chứng minh mệnh đề phản đảo. Tương đương: nếu mọi tập con hữu hạn của $\Sigma$ có mô hình, không thể tồn tại suy dẫn hữu hạn không nhất quán như vậy, nên $\Sigma$ không thể không thỏa mãn được, do đó $\Sigma$ có mô hình.

Điều này cho thấy logic bậc một không thể chốt được lực lượng: bất kỳ lý thuyết nào có mô hình vô hạn (ví dụ tiên đề trường, tiên đề lý thuyết tập hợp, ...) đã có sẵn một mô hình đếm được, dù mô hình gốc được xây "lớn" đến đâu. Kết hợp với chiều lên (mọi mô hình vô hạn đều có mở rộng sơ cấp ở mọi lực lượng lớn hơn), đây là nguồn gốc của Nghịch lý Skolem — một cấu trúc đếm được có thể thỏa mãn đúng các câu bậc một như một cấu trúc không đếm được, kể cả những câu "khẳng định" tính không đếm được từ bên trong.

Ta xây $N$ là hợp của một dãy tăng đếm được các tập con đếm được của $M$, dùng kiểm tra Tarski–Vaught: một tập con $N \subseteq M$ (như cấu trúc con) là sơ cấp khi và chỉ khi với mọi công thức $\mathcal{L}$ là $\psi(x, \bar{y})$ và mọi bộ $\bar{a}$ từ $N$, nếu có $b \in M$ nào đó với $\mathcal{M} \models \psi(b, \bar{a})$, thì đã có sẵn nhân chứng $b \in N$ như vậy.

Vì $\mathcal{L}$ đếm được, chỉ có đếm được nhiều công thức $\psi(x,\bar y)$. Bắt đầu với $X_0 \subseteq M$ đếm được vô hạn bất kỳ (có thể vì $M$ vô hạn). Cho $X_n$ đếm được, với mỗi công thức $\psi(x,\bar y)$ và mỗi bộ $\bar a$ từ $X_n$ (vẫn chỉ đếm được nhiều cặp, vì $X_n$ đếm được và $\mathcal{L}$ đếm được), nếu $\exists b \in M\, \mathcal{M} \models \psi(b,\bar a)$, chọn một nhân chứng $b$ như vậy (dùng Tiên đề Chọn) và thêm vào để tạo $X_{n+1}$; điều này chỉ thêm đếm được nhiều phần tử mới, nên $X_{n+1}$ vẫn đếm được.

Đặt $N = \bigcup_{n<\omega} X_n$; hợp đếm được của các tập đếm được, nên $N$ đếm được (và vô hạn, vì $X_0 \subseteq N$). Ta kiểm kiểm tra Tarski–Vaught cho $N$: cho $\psi(x,\bar y)$ và $\bar a$ từ $N$, vì $\bar a$ là bộ hữu hạn nên nó nằm trọn trong một $X_n$ nào đó (dãy tăng dần); nếu tồn tại nhân chứng $b \in M$ cho $\psi(b, \bar a)$, thì theo cách xây $X_{n+1}$, một nhân chứng đã được chọn và đặt vào $X_{n+1} \subseteq N$.

Theo kiểm tra Tarski–Vaught, $N$ (với cấu trúc $\mathcal{L}$ cảm sinh $\mathcal{N}$) thỏa mãn $\mathcal{N} \preceq \mathcal{M}$. Mô hình con sơ cấp thỏa mãn đúng cùng các câu như cấu trúc mẹ, nên $\mathcal{N}$ là một mô hình đếm được vô hạn chứng thực định lý.