docs(overview): Add overview of model theory (#12496)

Adds a subsection on model theory to the mathlib overview.
leanprover-community · Mar 7, 2022 · 85a415e · 85a415e
1 parent 3c3c3bc
commit 85a415e
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/docs/overview.yaml b/docs/overview.yaml
@@ -409,3 +409,10 @@ Logic and computation:
     ordinal: 'ordinal'
     cardinal: 'cardinal'
     model of ZFC: 'Set'
+  Model theory:
+    first-order structure: 'first_order.language.Structure'
+    first-order formula: 'first_order.language.formula'
+    satisfiability: 'first_order.language.Theory.is_satisfiable'
+    substructure: 'first_order.language.substructure'
+    definable set: 'first_order.language.definable_set'
+    elementary embedding: 'first_order.language.elementary_embedding'