From 26b4b5843a44de05be7c6d851d52fadf20449434 Mon Sep 17 00:00:00 2001
From: Stan Ulbrych <stanulbrych@gmail.com>
Date: Sun, 30 Mar 2025 17:03:09 +0100
Subject: [PATCH] Add basic overview to model theory section

---
 content/model-theory/basics/basics.tex        |  2 ++
 content/model-theory/basics/overview.tex      | 20 +++++++++++++++++++
 .../basics/reducts-and-expansions.tex         |  4 ----
 content/model-theory/model-theory.tex         |  3 +--
 4 files changed, 23 insertions(+), 6 deletions(-)
 create mode 100644 content/model-theory/basics/overview.tex

diff --git a/content/model-theory/basics/basics.tex b/content/model-theory/basics/basics.tex
index f06b1fe3..6f5ad6c1 100644
--- a/content/model-theory/basics/basics.tex
+++ b/content/model-theory/basics/basics.tex
@@ -7,6 +7,8 @@
 
 \olchapter{mod}{bas}{Basics of Model Theory}
 
+\olimport{overview}
+
 \olimport{reducts-and-expansions}
 
 \olimport{substructures}
diff --git a/content/model-theory/basics/overview.tex b/content/model-theory/basics/overview.tex
new file mode 100644
index 00000000..be1aa52b
--- /dev/null
+++ b/content/model-theory/basics/overview.tex
@@ -0,0 +1,20 @@
+% Part: first-order-logic
+% Chapter: model-theory
+% Section: overview
+\documentclass[../../../include/open-logic-section]{subfiles}
+
+\begin{document}
+
+\olfileid{mod}{bas}{ovr}
+\olsection{Overview}
+
+\epigraph{Logic appears in a \textit{“sacred”} and in a \textit{“profane”} form;
+the sacred form is dominant in proof theory, the profane form in model theory}
+{\textit{Dirk van Dalen}}
+
+Model theory applies logic to the study of mathematical structures.
+While model theory has existed since the 20th century, the name was first
+coined by Alfred Tarski, a member of the Lwów–Warsaw school, in 1954.
+
+
+\end{document}
diff --git a/content/model-theory/basics/reducts-and-expansions.tex b/content/model-theory/basics/reducts-and-expansions.tex
index 65f26ce3..d8bb262b 100644
--- a/content/model-theory/basics/reducts-and-expansions.tex
+++ b/content/model-theory/basics/reducts-and-expansions.tex
@@ -48,10 +48,6 @@ \section{Reducts and Expansions}
 \]
 \end{prop}
 
-\begin{proof}
-  Exercise.
-\end{proof}
-
 \begin{prob}
 Prove \olref[mod][bas][red]{prop:reduct}.
 \end{prob}
diff --git a/content/model-theory/model-theory.tex b/content/model-theory/model-theory.tex
index b548caaa..6d0ab7c2 100644
--- a/content/model-theory/model-theory.tex
+++ b/content/model-theory/model-theory.tex
@@ -12,8 +12,7 @@
   theory, less those topics covered in the part on first-order logic
   (theories, completeness, compactness).  It requires much more
   introduction, motivation, and explanation, as well as exercises, to
-  be useful for a textbook.  Andy Arana is at planning to work on this
-  part specifically (\gitissue{65}).
+  be useful for a textbook.  The progress is tracked at \gitissue{65}.
 \end{editorial}
 
 \olimport[basics]{basics}