-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathmain.tex
More file actions
298 lines (248 loc) · 14.9 KB
/
main.tex
File metadata and controls
298 lines (248 loc) · 14.9 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
\documentclass[handout]{beamer}
% \documentclass{beamer}
\usepackage{lmodern}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{amsmath, amsthm, amsfonts, amssymb}
\usepackage{mathrsfs}
\usetheme{Madrid}
\usecolortheme{default}
\title{Applications of Compactness}
\author{Alexander Mayorov}
\institute{TU Kaiserslautern}
\def\N{\mathbb{N}_{\ge 0}}
\def\Npos{\mathbb{N}_{\ge 1}}
\def\Nsimpl{\mathbb{N}}
\def\R{\mathbb{R}}
\def\Z{\mathbb{Z}}
\def\Q{\mathbb{Q}}
\def\P{\mathcal{P}}
\DeclareMathOperator{\FO}{FO}
\makeatletter
\newenvironment<>{proofs}[1][\proofname]{%
\par
\def\insertproofname{#1\@addpunct{.}}%
\usebeamertemplate{proof begin}#2}
{\usebeamertemplate{proof end}}
\makeatother
\AtBeginSection[]
{
\begin{frame}
\frametitle{Table of Contents}
\tableofcontents[currentsection]
\end{frame}
}
\begin{document}
\frame{\titlepage}
\section{Compactness theorems}
\begin{frame}
\frametitle{The compactness theorem}
\begin{theorem}[Compactness for propositional logic]
A set of propositional formulas $ \Sigma $ is satisfiable if and only if every finite subset of $ \Sigma $ is satisfiable.
\end{theorem}
\begin{proof}
($ \Rightarrow $): If there exists $ \nu \models \Sigma $, then $ \nu $ will satisfy every finite subset of $ \Sigma $.
($ \Leftarrow $): proof of this direction is omitted
\end{proof}
\pause
\begin{theorem}[Contrapositive form of compactness]
$ \Sigma $ is unsatisfiable iff there exists some finite unsatisfiable subset of $ \Sigma $.
\end{theorem}
\end{frame}
\begin{frame}
\frametitle{Compactness for first-order logic}
\begin{theorem}[Compactness for first-order logic]
A set of closed first-order logic formulas $ \Sigma $ is satisfiable if and only if every finite subset of $ \Sigma $ is satisfiable.
\end{theorem}
\pause
\begin{proof}
($ \Rightarrow $): A model for $ \Sigma $ is also a model for every finite subset thereof.
($ \Leftarrow $): We can assume without loss of generality that all $ \varphi \in \Sigma $ are Skolem normal form sentences with matrix in CNF (via Tseitin's transformation). Suppose, for the sake of contradiction, $ \Sigma $ were unsatisfiable. Since $ \Sigma $ is satisfiable iff $ E(\Sigma) $ is satisfiable by the \textit{Gödel-Herbrand-Skolem theorem}, we conclude that $ E(\Sigma) $ is unsatisfiable. By the \textit{compactness theorem for propositional logic}, there must exist some finite unsatisfiable subset $ A \subseteq E(\Sigma) $. Taking formulas from $ \Sigma $ whose ground terms appear in $ A $ gives us a finite unsatisfiable subset of $ \Sigma $.
\end{proof}
\end{frame}
\section{Direct applications}
\begin{frame}
\frametitle{Compactness and entailment}
\begin{lemma}
Let $ \Sigma $ be a set of formulas and $ \alpha $ be a formula. Then, $ \Sigma \models \alpha $ iff there exists a finite $ \Sigma' \subseteq \Sigma $ such that $ \Sigma' \models \alpha $.
\end{lemma}
\pause
\begin{proof}
\begin{align*}
\Sigma \models \alpha &\Leftrightarrow \Sigma \cup \{\neg\alpha\} \text{ is unsatisfiable} \\
&\Leftrightarrow \text{There is a finite unsatisfiable } \Sigma' \subseteq \Sigma \cup \{\neg\alpha\} \\
&\Leftrightarrow \Sigma' \cup \{\neg\alpha\} \text{ is unsatisfiable}, \Sigma' \text{ is finite} \\
&\Leftrightarrow \Sigma' \models \alpha \text{ for some finite } \Sigma'
\end{align*}
Here, we use the contrapositive form of compactness in the second equivalence.
\end{proof}
\end{frame}
\begin{frame}
\frametitle{Arbitrary large finite models}
\begin{lemma}
Let $ \Sigma $ be a set of first-order sentences such that every $ \varphi \in \Sigma $ has an arbitrary large model. Then, $ \Sigma $ also has an infinite model.
\end{lemma}
\pause
\begin{proof}
Consider \begin{align*}
\lambda_k &:= \underbrace{\exists x_1, \dots, x_k : \bigwedge_{\substack{i,j = 1 \\ i \neq j}}^k x_i \neq x_j}_{\text{Universe has } \ge k \text{ elements}} \\
C &:= \underbrace{\underbrace{\Sigma}_{\forall n \in \N \text{ there is model of size n}} \cup \quad \underbrace{\{\lambda_k \mid k \in \N\}}_{\infty \text{ model}}}_{C \text{ finitely satisfiable } \Rightarrow \text{ } C \text{ satisfiable } \Rightarrow \text{ } \Sigma \text{ has an } \infty \text{ model}}
\end{align*}
\end{proof}
\end{frame}
\section{Proving non-expressibility using compactness}
\begin{frame}
\frametitle{Strategy for proving non-expressibility results}
Suppose we want to show that some \alert{property $ P $ is not expressible} in first-order logic. We can try proving this using the following technique:
\begin{itemize}[<+->]
\item \textit{Assume}, for the sake of contradiction, that there exists a formula $ \varphi $ expressing $ P $.
\item \textit{Construct} an infinite set of formulas (e.g., $ \{\lambda_k \mid k \in \Nsimpl\} $) enforcing the negation of $ P $.
\item \textit{Consider} the set $ C := \{\varphi\} \cup \{\lambda_k \mid k \in \Nsimpl\} $.
\item \textit{Argue} that $ C $ is unsatisfiable since every model of $ \varphi $ cannot be a model of $ \{\lambda_k \mid k \in \Nsimpl\} $.
\item \textit{Show} that for every finite $ M \subseteq C $ there exists a model $ \mathcal{A} \models M $ satisfying property $ P $. Hence, $ C $ is finitely satisfiable.
\item \textit{Conclude} that, by compactness, $ C $ is satisfiable, which is a contradiction to the unsatisfiability of $ C $.
\end{itemize}
\end{frame}
\section{Examples of non-expressibility results}
\begin{frame}
\frametitle{Finiteness is not first-order definable}
\begin{theorem}
There is no formula $ \varphi $ that is satisfied by structure $ A $ iff $ A $ is finite.
\end{theorem}
\pause
\begin{proofs}
\begin{itemize}
\item Suppose there were such a formula $ \varphi $. We describe infiniteness with $ \{\lambda_k \mid k \in \N\} $ where \[\lambda_k := \underbrace{\exists x_1, \dots, x_k : \bigwedge_{\substack{i,j = 1 \\ i \neq j}}^k x_i \neq x_j}_{\text{Universe has } \ge k \text{ elements}}\] \[
C := \underbrace{\underbrace{\{\varphi\}}_{\text{Finite model}} \cup \quad \underbrace{\{\lambda_k \mid k \in \N\}}_{\infty \text{ model}}}_{\Rightarrow \text{ unsatisfiable}}
\]
\end{itemize}
\end{proofs}
\end{frame}
\begin{frame}
\frametitle{Finiteness is not first-order definable}
\begin{proof}[\proofname\ (continued)]
\begin{itemize}[<+->]
\item Consider an arbitrary but finite $ M \subseteq C $ where, as we just defined, \[
C = \underbrace{\{\varphi\}}_{\text{Finite model}} \cup \quad \underbrace{\{\lambda_k \mid k \in \N\}}_{\infty \text{ model}}
\] Since $ M $ is finite, we can find a $ k \in \N $ such that $ M $ doesn't contain any $ \lambda_i $ for $ i \ge k $. Any structure with at least $ k $ elements is thus a model for $ M $.
\item By compactness, $ C $ is therefore satisfiable. However, $ C $ is unsatisfiable by construction (see previous slide). This is a contradiction.
\end{itemize}
\end{proof}
\end{frame}
\begin{frame}
\frametitle{Acyclicity is not first-order definable}
\begin{theorem}
Let $ \sigma = \{E_{/2}\} $ be a signature, where $ E $ is the predicate symbol representing the edge relation. There is no $ \varphi \in \FO(\sigma) $ expressing the fact that the graph is acyclic.
\end{theorem}
\pause
\begin{block}{Incorrect proof attempt}
\begin{itemize}
\item Suppose there were such a formula $ \varphi $. We describe the existence of some cycle with $ \{\lambda_k \mid k \in \Npos\} $ where \[\lambda_k := \underbrace{\exists x_1, \dots, x_k : \bigwedge_{\substack{i,j = 1 \\ i \neq j}}^k x_i \neq x_j \wedge \bigwedge_{i=1}^{k-1} E(x_i, x_{i+1}) \wedge E(x_k, x_1)}_{\text{There is a cycle of length } k}\]
\end{itemize}
\end{block}
\end{frame}
\begin{frame}
\begin{block}{Incorrect proof attempt -- continued}
\begin{itemize}
\item \[
C := \underbrace{\underbrace{\{\varphi\}}_{\text{Graph acyclic}} \cup \quad \underbrace{\{\lambda_k \mid k \in \Npos\}}_{\text{There is a cycle of every possible length}}}_{\Rightarrow \text{ unsatisfiable}}
\]
\item Consider some finite subset $ M \subseteq C $
\item \alert{Problem}: $ M $ may contain $ \varphi $ and some $ \lambda_i $-formulas, we cannot however construct a graph that is both acyclic and has a cycle of some specific length.
\end{itemize}
\end{block}
\pause
\textbf{Important observation}: in order for this proof technique to work, we need to ``approximate'' the negation of $ P $ using $ \{\lambda_k \mid k \in \Npos\} $ in a way, such that a finite subset of $ \{\lambda_k \mid k \in \Npos\} $ doesn't directly contradict $ \varphi $.
\textbf{In this example}: we could not ``approximate'' existence of cycles without contradicting acyclicity, because we described the existence of a cycle of a specific length with a single formula.
\end{frame}
\begin{frame}
\frametitle{Acyclicity is not first-order definable}
\textbf{Trick}: we can negate $ \varphi $ in the proof and thus show that the negation of acyclicity, namely the existence of a cycle, is not first-order definable. In other words, \alert{some property is first-order definable iff its negation is first-order definable}.
\begin{theorem}[restated]
Let $ \sigma = \{E_{/2}\} $ be a signature, where $ E $ is the predicate symbol representing the edge relation. There is no $ \varphi \in \FO(\sigma) $ expressing the fact that the graph is acyclic.
\end{theorem}
\end{frame}
\begin{frame}
\begin{proof}
\begin{itemize}[<+->]
\item Suppose there were such a formula $ \varphi $. We define \[\lambda_k := \underbrace{\neg \exists x_1, \dots, x_k : \bigwedge_{\substack{i,j = 1 \\ i \neq j}}^k x_i \neq x_j \wedge \bigwedge_{i=1}^{k-1} E(x_i, x_{i+1}) \wedge E(x_k, x_1)}_{\text{There is no cycle of length } k}\]\[
C := \underbrace{\underbrace{\{\neg\varphi\}}_{\exists\text{ cycle}} \quad \cup \quad \underbrace{\{\lambda_k \mid k \in \Npos\}}_{\text{There are no cycles}}}_{\Rightarrow \text{ unsatisfiable}}
\]
\item Consider an arbitrary but finite $ M \subseteq C $. Since $ M $ is finite, we can find a $ k \in \Npos $ such that $ M $ doesn't contain any $ \lambda_i $ for $ i \ge k $. We can easily construct a graph with a cycle of length $ k $ and without shorter cycles (how?), meaning that $ M $ is satisfiable.
\item By compactness, $ C $ is satisfiable, which is a contradiction.
\end{itemize}
\end{proof}
\end{frame}
\begin{frame}
\frametitle{Longest path has odd length is not first-order definable}
\begin{theorem}
There is no $ \varphi \in \FO(\{E_{/2}\}) $ expressing the property that the longest path in the graph has odd length.
\end{theorem}
\pause
\begin{proofs}
\begin{itemize}
\item Suppose there were such a formula $ \varphi $. We describe the property that \textit{the longest path is of even or infinite length} with $ \{\lambda_{2n+1} \mid n \in \N\} $: \begin{align*}
\psi_k &:= \underbrace{\exists x_1, \dots, x_{k+1} : \bigwedge_{\substack{i,j = 1 \\ i \neq j}}^{k+1} x_i \neq x_j \wedge \bigwedge_{i=1}^k E(x_i, x_{i+1})}_{\text{There exists a path of length } k} \\
\lambda_k &:= \neg(\underbrace{\psi_k \wedge \neg\psi_{k+1}}_{\text{Length of longest path } = k}) \equiv \neg\psi_k \vee \psi_{k+1}
\end{align*}
\end{itemize}
\end{proofs}
\end{frame}
\begin{frame}
\frametitle{Longest path has odd length is not first-order definable}
\begin{proof}[\proofname\ (continued)]
\begin{itemize}[<+->]
\item \[
C := \underbrace{\underbrace{\{\varphi\}}_{\text{Longest path is of odd length}} \cup \underbrace{\{\lambda_{2n+1} \mid n \in \N\}}_{\text{Longest path is of even or infinite length}}}_{\Rightarrow \text{ unsatisfiable}}
\]
\item Consider an arbitrary but finite $ M \subseteq C $. Since $ M $ is finite, we can find a $ k \in \N $ such that $ M $ doesn't contain any $ \lambda_i $ for $ i \ge k $. Let $ k' \ge k $ be some odd number. Any finite graph with length of longest path equal $ k' $ is a model for $ M $.
\item It follows that, by compactness, $ C $ is satisfiable. At the same time, $ C $ is unsatisfiable by construction. This is a contradiction.
\end{itemize}
\end{proof}
\end{frame}
\begin{frame}
\frametitle{Further examples of not first-order definable properties}
The same proof technique can be used to show the following results, exact proofs are left as an exercise.
\begin{theorem}
There is no $ \varphi \in \FO(\{E_{/2}\}) $ expressing the property that the graph is bipartite.
\end{theorem}
\textbf{Hint}: a graph is bipartite iff there are no cycles of odd length.
\begin{theorem}
Let $ \sigma = \{E_{/2}, a, b\} $ be a signature, where $ E $ is the predicate symbol representing the edge relation and $ a, b $ are constants. There is no $ \varphi \in \FO(\sigma) $ expressing the fact that there exists a path from $ a $ to $ b $.
\end{theorem}
\end{frame}
\section{Application: Finitary Ramsey Theorem}
\begin{frame}
\frametitle{Finitary Ramsey Theorem}
The following is a simplified version of the famous Ramsey's Theorem.
\begin{theorem}[Ramsey Theorem]
Every infinite graph has either an infinite clique or an infinite independent-set.
\end{theorem}
\pause
We can use compactness to show that this theorem implies the following finite version of it:
\begin{theorem}[Finitary Ramsey Theorem]
For every $ k \in \Nsimpl $ there is an $ n \in \Nsimpl $, such that every graph with $ n $ vertices has either a $ k $-clique or a $ k $-independent-set.
\end{theorem}
\end{frame}
\begin{frame}
\frametitle{Finitary Ramsey Theorem}
\begin{proofs}
Suppose, for the sake of contradiction, that $ \exists k \in \Nsimpl \quad \forall n \in \Nsimpl $ there exists a graph with $ n $ vertices that has no $ k $-clique and no $ k $-independent-set. We describe this using an infinite set of formulas $ \Sigma $: \begin{align*}
\alpha_k &:= \underbrace{\neg\exists v_1, \dots, v_k \Bigg(\bigwedge_{\substack{i,j = 1 \\ i \neq j}}^k v_i \neq v_j\Bigg) \wedge \Bigg(\bigwedge_{\substack{i,j = 1 \\ i \neq j}}^k E(v_i, v_j) \vee \bigwedge_{\substack{i,j = 1 \\ i \neq j}}^k \neg E(v_i, v_j)\Bigg)}_{\text{There is no clique or independent-set of size } k} \\
\beta_k &:= \underbrace{\exists v_1, \dots, v_k : \bigwedge_{\substack{i,j = 1 \\ i \neq j}}^k v_i \neq v_j}_{\text{Graph has at least } k \text{ vertices}} \\
\Sigma &:= \{\alpha_k\} \cup \{\beta_n \mid n \in \N\}
\end{align*}
\end{proofs}
\end{frame}
\begin{frame}
\frametitle{Finitary Ramsey Theorem}
\begin{proof}[\proofname\ (continued)]
\begin{itemize}[<+->]
\item Consider an arbitrary but finite $ M \subseteq \Sigma $. There exists an $ n \in \N $ such that there is no $ \beta_i \in M $ for $ i \ge n $. By our assumption, there exists a graph of size $ n $ with no $ k $-clique and no $ k $-independent-set. This graph satisfies $ M $.
\item Every finite subset of $ \Sigma $ has a model, so, by compactness, $ \Sigma $ is satisfiable.
\item This implies the existence of an infinite graph with no $ k $-clique and no $ k $-independent-set.
\item It follows that there exists an infinite graph with neither an infinite clique nor an infinite independent-set, which is a contradiction to Ramsey's Theorem.
\end{itemize}
\end{proof}
\end{frame}
\end{document}