readme update

.gitignore

@@ -1 +1,2 @@
 /.lake
+.vscode

FormalTextbookModelTheory/ForMathlib/DLO.lean

@@ -14,7 +14,7 @@ open Cardinal
 open FirstOrder Language Structure Theory Order
 open Matrix (Vector_eq_VecNotation₂ comp_VecNotation₂)
 
-namespace FirstOrder.Language.Order --region
+namespace FirstOrder.Language.Order
 
 section
 
@@ -243,4 +243,4 @@ theorem aleph0_categorical_of_dlo : aleph0.Categorical Language.order.dlo := by
 
 end DLO --end
 
-end FirstOrder.Language.Order --end
+end FirstOrder.Language.Order

README.md

@@ -1 +1,5 @@
-# FormalTextbookModelTheory
+# FormalTextbookModelTheory
+
+The end goal is to formalize the famous textbook Model Theory: An Introduction by David Marker.
+
+* Right know, the aleph0 categoricity of the theory of dense linear orders are proved. The essential part of the proof, which is the back-and-forth argument, was already in Mathlib but it was in terms of the instances LinearOrder, Countable etc. We just provided the dictionary to carry the proof to the language of model theory.

blueprint/web/dep_graph_document.html

@@ -557,7 +557,7 @@ <h1 id="doc_title">Dependencies</h1>
     .width(width)
     .height(height)
     .fit(true)
-    .renderDot(`strict digraph "" {	graph [bgcolor=transparent];	node [label="\N",		penwidth=1.8	];	edge [arrowhead=vee];	"lem:realize-reflexivity"	[color=green,		fillcolor="#1CAC78",		label="realize-reflexivity",		shape=ellipse,		style=filled];	"def:preorder-dlo"	[color=green,		fillcolor="#B0ECA3",		label="preorder-dlo",		shape=box,		style=filled];	"lem:realize-reflexivity" -> "def:preorder-dlo"	[style=dashed];	"def:linearorder-dlo"	[color=green,		fillcolor="#B0ECA3",		label="linearorder-dlo",		shape=box,		style=filled];	"def:preorder-dlo" -> "def:linearorder-dlo"	[style=dashed];	"thm:dlo-aleph0-categorical"	[color=green,		fillcolor="#1CAC78",		label="dlo-aleph0-categorical",		shape=ellipse,		style=filled];	"def:linearorder-dlo" -> "thm:dlo-aleph0-categorical";	"lem:realize-total"	[color=green,		fillcolor="#1CAC78",		label="realize-total",		shape=ellipse,		style=filled];	"lem:realize-total" -> "def:linearorder-dlo"	[style=dashed];	"lem:realize-no-min"	[color=green,		fillcolor="#1CAC78",		label="realize-no-min",		shape=ellipse,		style=filled];	"lem:to-embedding"	[color=green,		fillcolor="#1CAC78",		label="to-embedding",		shape=ellipse,		style=filled];	"lem:to-isomorphism"	[color=green,		fillcolor="#1CAC78",		label="to-isomorphism",		shape=ellipse,		style=filled];	"lem:to-embedding" -> "lem:to-isomorphism";	"lem:to-isomorphism" -> "thm:dlo-aleph0-categorical";	"def:le-instance-language-order"	[color=green,		fillcolor="#B0ECA3",		label="le-instance-language-order",		shape=box,		style=filled];	"def:le-instance-language-order" -> "def:preorder-dlo"	[style=dashed];	"def:le-instance-language-order" -> "lem:to-embedding"	[style=dashed];	"lem:order-structure-of-le"	[color=green,		fillcolor="#1CAC78",		label="order-structure-of-le",		shape=ellipse,		style=filled];	"def:le-instance-language-order" -> "lem:order-structure-of-le"	[style=dashed];	"lem:vector-notation"	[color=green,		fillcolor="#1CAC78",		label="vector-notation",		shape=ellipse,		style=filled];	"lem:vector-notation" -> "lem:to-embedding";	"lem:vector-notation" -> "lem:order-structure-of-le";	"lem:vector-notation-under-composition"	[color=green,		fillcolor="#1CAC78",		label="vector-notation-under-composition",		shape=ellipse,		style=filled];	"lem:vector-notation-under-composition" -> "lem:to-embedding";	"lem:realize-transitivity"	[color=green,		fillcolor="#1CAC78",		label="realize-transitivity",		shape=ellipse,		style=filled];	"lem:realize-transitivity" -> "def:preorder-dlo"	[style=dashed];	"lem:realize-antisymmetric"	[color=green,		fillcolor="#1CAC78",		label="realize-antisymmetric",		shape=ellipse,		style=filled];	"lem:realize-antisymmetric" -> "def:linearorder-dlo"	[style=dashed];	"lem:realize-densely-ordered"	[color=green,		fillcolor="#1CAC78",		label="realize-densely-ordered",		shape=ellipse,		style=filled];	"lem:realize-no-max"	[color=green,		fillcolor="#1CAC78",		label="realize-no-max",		shape=ellipse,		style=filled];}`)
+    .renderDot(`strict digraph "" {	graph [bgcolor=transparent];	node [label="\N",		penwidth=1.8	];	edge [arrowhead=vee];	"lem:vector-notation"	[color=green,		fillcolor="#1CAC78",		label="vector-notation",		shape=ellipse,		style=filled];	"lem:order-structure-of-le"	[color=green,		fillcolor="#1CAC78",		label="order-structure-of-le",		shape=ellipse,		style=filled];	"lem:vector-notation" -> "lem:order-structure-of-le";	"lem:to-embedding"	[color=green,		fillcolor="#1CAC78",		label="to-embedding",		shape=ellipse,		style=filled];	"lem:vector-notation" -> "lem:to-embedding";	"lem:to-isomorphism"	[color=green,		fillcolor="#1CAC78",		label="to-isomorphism",		shape=ellipse,		style=filled];	"lem:to-embedding" -> "lem:to-isomorphism";	"thm:dlo-aleph0-categorical"	[color=green,		fillcolor="#1CAC78",		label="dlo-aleph0-categorical",		shape=ellipse,		style=filled];	"lem:to-isomorphism" -> "thm:dlo-aleph0-categorical";	"lem:realize-reflexivity"	[color=green,		fillcolor="#1CAC78",		label="realize-reflexivity",		shape=ellipse,		style=filled];	"def:preorder-dlo"	[color=green,		fillcolor="#B0ECA3",		label="preorder-dlo",		shape=box,		style=filled];	"lem:realize-reflexivity" -> "def:preorder-dlo"	[style=dashed];	"def:linearorder-dlo"	[color=green,		fillcolor="#B0ECA3",		label="linearorder-dlo",		shape=box,		style=filled];	"def:preorder-dlo" -> "def:linearorder-dlo"	[style=dashed];	"def:linearorder-dlo" -> "thm:dlo-aleph0-categorical";	"lem:realize-no-min"	[color=green,		fillcolor="#1CAC78",		label="realize-no-min",		shape=ellipse,		style=filled];	"def:le-instance-language-order"	[color=green,		fillcolor="#B0ECA3",		label="le-instance-language-order",		shape=box,		style=filled];	"def:le-instance-language-order" -> "lem:order-structure-of-le"	[style=dashed];	"def:le-instance-language-order" -> "lem:to-embedding"	[style=dashed];	"def:le-instance-language-order" -> "def:preorder-dlo"	[style=dashed];	"lem:vector-notation-under-composition"	[color=green,		fillcolor="#1CAC78",		label="vector-notation-under-composition",		shape=ellipse,		style=filled];	"lem:vector-notation-under-composition" -> "lem:to-embedding";	"lem:realize-transitivity"	[color=green,		fillcolor="#1CAC78",		label="realize-transitivity",		shape=ellipse,		style=filled];	"lem:realize-transitivity" -> "def:preorder-dlo"	[style=dashed];	"lem:realize-antisymmetric"	[color=green,		fillcolor="#1CAC78",		label="realize-antisymmetric",		shape=ellipse,		style=filled];	"lem:realize-antisymmetric" -> "def:linearorder-dlo"	[style=dashed];	"lem:realize-total"	[color=green,		fillcolor="#1CAC78",		label="realize-total",		shape=ellipse,		style=filled];	"lem:realize-total" -> "def:linearorder-dlo"	[style=dashed];	"lem:realize-densely-ordered"	[color=green,		fillcolor="#1CAC78",		label="realize-densely-ordered",		shape=ellipse,		style=filled];	"lem:realize-no-max"	[color=green,		fillcolor="#1CAC78",		label="realize-no-max",		shape=ellipse,		style=filled];}`)
     .on("end", interactive);
 
 latexLabelEscaper = function(label) {