Split

Lipen · Lipen · commit 02c431afb5cb · 2026-03-11T21:59:49.000+03:00
diff --git a/lec-fol.typ b/lec-fol.typ
@@ -657,7 +657,8 @@ SMT solvers restrict to _decidable fragments_ of FOL --- theories where satisfia
   *Non-standard models of arithmetic:*
   Let $Gamma = op("Th")(NN) union {c > 0, c > 1, c > 2, dots}$ where $c$ is a fresh constant.
   Every finite subset is satisfiable (interpret $c$ as a large enough number).
-  By compactness, $Gamma$ is satisfiable --- in a model with an "infinite" element $c$ larger than all standard naturals. This is a _non-standard model_ of arithmetic.
+  By compactness, $Gamma$~is satisfiable --- in a model with an "infinite" element $c$ larger than all standard naturals. \
+  This is a _non-standard model_ of arithmetic.
 ]
 
 #Block(color: blue)[

Original file line number	Diff line number	Diff line change
`@@ -657,7 +657,8 @@ SMT solvers restrict to _decidable fragments_ of FOL --- theories where satisfia`
`657`	`657`	`Non-standard models of arithmetic:`
`658`	`658`	`Let $Gamma = op("Th")(NN) union {c > 0, c > 1, c > 2, dots}$ where $c$ is a fresh constant.`
`659`	`659`	`Every finite subset is satisfiable (interpret $c$ as a large enough number).`
`660`		`- By compactness, $Gamma$ is satisfiable --- in a model with an "infinite" element $c$ larger than all standard naturals. This is a _non-standard model_ of arithmetic.`
	`660`	`+ By compactness, $Gamma$~is satisfiable --- in a model with an "infinite" element $c$ larger than all standard naturals. \`
	`661`	`+ This is a _non-standard model_ of arithmetic.`
`661`	`662`	`]`
`662`	`663`
`663`	`664`	`#Block(color: blue)[`