\documentclass[12pt,titlepage]{article} \usepackage{amsmath} \usepackage{mathrsfs} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsthm} \usepackage{mathtools} \usepackage{graphicx} \usepackage{color} \usepackage{ucs} \usepackage[utf8x]{inputenc} \usepackage{xparse} \usepackage{hyperref} %----Macros---------- % % Unresolved issues: % % \righttoleftarrow % \lefttorightarrow % % \color{} with HTML colorspec % \bgcolor % \array with options (without options, it's equivalent to the matrix environment) % Of the standard HTML named colors, white, black, red, green, blue and yellow % are predefined in the color package. Here are the rest. \definecolor{aqua}{rgb}{0, 1.0, 1.0} \definecolor{fuschia}{rgb}{1.0, 0, 1.0} \definecolor{gray}{rgb}{0.502, 0.502, 0.502} \definecolor{lime}{rgb}{0, 1.0, 0} \definecolor{maroon}{rgb}{0.502, 0, 0} \definecolor{navy}{rgb}{0, 0, 0.502} \definecolor{olive}{rgb}{0.502, 0.502, 0} \definecolor{purple}{rgb}{0.502, 0, 0.502} \definecolor{silver}{rgb}{0.753, 0.753, 0.753} \definecolor{teal}{rgb}{0, 0.502, 0.502} % Because of conflicts, \space and \mathop are converted to % \itexspace and \operatorname during preprocessing. % itex: \space{ht}{dp}{wd} % % Height and baseline depth measurements are in units of tenths of an ex while % the width is measured in tenths of an em. \makeatletter \newdimen\itex@wd% \newdimen\itex@dp% \newdimen\itex@thd% \def\itexspace#1#2#3{\itex@wd=#3em% \itex@wd=0.1\itex@wd% \itex@dp=#2ex% \itex@dp=0.1\itex@dp% \itex@thd=#1ex% \itex@thd=0.1\itex@thd% \advance\itex@thd\the\itex@dp% \makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}} \makeatother % \tensor and \multiscript \makeatletter \newif\if@sup \newtoks\@sups \def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}% \def\reset@sup{\@supfalse\@sups={}}% \def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else% \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}% \else \append@sup#2 \@suptrue \fi% \expandafter\mk@scripts\fi} \def\tensor#1#2{\reset@sup#1\mk@scripts#2_/} \def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2% \reset@sup\mk@scripts#3_/} \makeatother % \slash \makeatletter \newbox\slashbox \setbox\slashbox=\hbox{$/$} \def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$} \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa \copy\slashbox \kern-\@tempdima \box\@tempboxa} \def\slash{\protect\itex@pslash} \makeatother % math-mode versions of \rlap, etc % from Alexander Perlis, "A complement to \smash, \llap, and lap" % http://math.arizona.edu/~aprl/publications/mathclap/ \def\clap#1{\hbox to 0pt{\hss#1\hss}} \def\mathllap{\mathpalette\mathllapinternal} \def\mathrlap{\mathpalette\mathrlapinternal} \def\mathclap{\mathpalette\mathclapinternal} \def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}} \def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}} \def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}} % Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2} \let\oldroot\root \def\root#1#2{\oldroot #1 \of{#2}} \renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}} % Manually declare the txfonts symbolsC font \DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n} \SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n} \DeclareFontSubstitution{U}{txsyc}{m}{n} % Manually declare the stmaryrd font \DeclareSymbolFont{stmry}{U}{stmry}{m}{n} \SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n} % Manually declare the MnSymbolE font \DeclareFontFamily{OMX}{MnSymbolE}{} \DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n} \SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n} \DeclareFontShape{OMX}{MnSymbolE}{m}{n}{ <-6> MnSymbolE5 <6-7> MnSymbolE6 <7-8> MnSymbolE7 <8-9> MnSymbolE8 <9-10> MnSymbolE9 <10-12> MnSymbolE10 <12-> MnSymbolE12}{} % Declare specific arrows from txfonts without loading the full package \makeatletter \def\re@DeclareMathSymbol#1#2#3#4{% \let#1=\undefined \DeclareMathSymbol{#1}{#2}{#3}{#4}} \re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116} \re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117} \re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118} \re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119} \re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46} \re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121} \re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12} \re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64} \re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6} \re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77} \re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77} \makeatother % \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE \makeatletter \def\Decl@Mn@Delim#1#2#3#4{% \if\relax\noexpand#1% \let#1\undefined \fi \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}} \def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}} \def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}} \Decl@Mn@Open{\llangle}{mnomx}{'164} \Decl@Mn@Close{\rrangle}{mnomx}{'171} \Decl@Mn@Open{\lmoustache}{mnomx}{'245} \Decl@Mn@Close{\rmoustache}{mnomx}{'244} \makeatother % Widecheck \makeatletter \DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}} \def\@widecheck#1#2{% \setbox\z@\hbox{\m@th$#1#2$}% \setbox\tw@\hbox{\m@th$#1% \widehat{% \vrule\@width\z@\@height\ht\z@ \vrule\@height\z@\@width\wd\z@}$}% \dp\tw@-\ht\z@ \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@ \setbox\tw@\hbox{% \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box \tw@}}}% {\ooalign{\box\tw@ \cr \box\z@}}} \makeatother % \mathraisebox{voffset}[height][depth]{something} \makeatletter \NewDocumentCommand\mathraisebox{moom}{% \IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{% \IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}% }{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}% \mathpalette\@temp{#4}} \makeatletter % udots (taken from yhmath) \makeatletter \def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.} \mkern2mu\raise4\p@\hbox{.}\mkern1mu \raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}} \makeatother %% Fix array \newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}} %% \itexnum is a noop \newcommand{\itexnum}[1]{#1} %% Renaming existing commands \newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}} \newcommand{\widevec}{\overrightarrow} \newcommand{\darr}{\downarrow} \newcommand{\nearr}{\nearrow} \newcommand{\nwarr}{\nwarrow} \newcommand{\searr}{\searrow} \newcommand{\swarr}{\swarrow} \newcommand{\curvearrowbotright}{\curvearrowright} \newcommand{\uparr}{\uparrow} \newcommand{\downuparrow}{\updownarrow} \newcommand{\duparr}{\updownarrow} \newcommand{\updarr}{\updownarrow} \newcommand{\gt}{>} \newcommand{\lt}{<} \newcommand{\map}{\mapsto} \newcommand{\embedsin}{\hookrightarrow} \newcommand{\Alpha}{A} \newcommand{\Beta}{B} \newcommand{\Zeta}{Z} \newcommand{\Eta}{H} \newcommand{\Iota}{I} \newcommand{\Kappa}{K} \newcommand{\Mu}{M} \newcommand{\Nu}{N} \newcommand{\Rho}{P} \newcommand{\Tau}{T} \newcommand{\Upsi}{\Upsilon} \newcommand{\omicron}{o} \newcommand{\lang}{\langle} \newcommand{\rang}{\rangle} \newcommand{\Union}{\bigcup} \newcommand{\Intersection}{\bigcap} \newcommand{\Oplus}{\bigoplus} \newcommand{\Otimes}{\bigotimes} \newcommand{\Wedge}{\bigwedge} \newcommand{\Vee}{\bigvee} \newcommand{\coproduct}{\coprod} \newcommand{\product}{\prod} \newcommand{\closure}{\overline} \newcommand{\integral}{\int} \newcommand{\doubleintegral}{\iint} \newcommand{\tripleintegral}{\iiint} \newcommand{\quadrupleintegral}{\iiiint} \newcommand{\conint}{\oint} \newcommand{\contourintegral}{\oint} \newcommand{\infinity}{\infty} \newcommand{\bottom}{\bot} \newcommand{\minusb}{\boxminus} \newcommand{\plusb}{\boxplus} \newcommand{\timesb}{\boxtimes} \newcommand{\intersection}{\cap} \newcommand{\union}{\cup} \newcommand{\Del}{\nabla} \newcommand{\odash}{\circleddash} \newcommand{\negspace}{\!} \newcommand{\widebar}{\overline} \newcommand{\textsize}{\normalsize} \renewcommand{\scriptsize}{\scriptstyle} \newcommand{\scriptscriptsize}{\scriptscriptstyle} \newcommand{\mathfr}{\mathfrak} \newcommand{\statusline}[2]{#2} \newcommand{\tooltip}[2]{#2} \newcommand{\toggle}[2]{#2} % Theorem Environments \theoremstyle{plain} \newtheorem{theorem}{Theorem} \newtheorem{lemma}{Lemma} \newtheorem{prop}{Proposition} \newtheorem{cor}{Corollary} \newtheorem*{utheorem}{Theorem} \newtheorem*{ulemma}{Lemma} \newtheorem*{uprop}{Proposition} \newtheorem*{ucor}{Corollary} \theoremstyle{definition} \newtheorem{defn}{Definition} \newtheorem{example}{Example} \newtheorem*{udefn}{Definition} \newtheorem*{uexample}{Example} \theoremstyle{remark} \newtheorem{remark}{Remark} \newtheorem{note}{Note} \newtheorem*{uremark}{Remark} \newtheorem*{unote}{Note} %------------------------------------------------------------------- \begin{document} %------------------------------------------------------------------- \section*{model complete theory } [[!redirects model complete theory ]] [[!redirects model complete theory ]] \hypertarget{context}{}\subsubsection*{{Context}}\label{context} \hypertarget{model_theory}{}\paragraph*{{Model theory}}\label{model_theory} [[!include model theory - contents]] \hypertarget{contents}{}\section*{{Contents}}\label{contents} \noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak \noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak \noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak \noindent\hyperlink{remarks}{Remarks}\dotfill \pageref*{remarks} \linebreak \noindent\hyperlink{model_completeness__amalgamation_property_implies_substructure_completeness}{Model completeness + amalgamation property implies substructure completeness}\dotfill \pageref*{model_completeness__amalgamation_property_implies_substructure_completeness} \linebreak \noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak \noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak \hypertarget{idea}{}\subsection*{{Idea}}\label{idea} Model completeness is a [[property]] of [[first-order theories]] (in the same way that [[existential closedness]] is a [[property]] of [[first-order structures]]) meant to generalize the properties of the theory [[ACF]] of [[algebraically closed fields]]. As discussed in Hodges' \hyperlink{Hodges1993}{Model theory}: \begin{quote}% In the early 1950s [[Abraham Robinson]] noticed that certain maps studied by algebraists are in fact [[elementary embeddings]]. If you choose a map at random, the chances of it being an elementary embedding are negligible. So Robinson reckoned that there must be a systematic reason for the appearance of these elementary embeddings, and he set out to find what the reason was. In the course of this quest he introduced the notions of model complete theories, companionable theories and [[model companion|model companions]]. These notions have become essential tools for the model theory of algebra. \end{quote} \hypertarget{definition}{}\subsection*{{Definition}}\label{definition} We say a [[first-order theory]] $T$ is \emph{model complete} if every embedding (not necessarily elementary) between models of $T$ \emph{is} elementary. The following characterization appears as Theorem 8.3.1 in (\hyperlink{Hodges1993}{Hodges93}): \begin{theorem} \label{}\hypertarget{}{} Let $T$ be as above. The following are equivalent: \begin{enumerate}% \item $T$ is model complete. \item Every model of $T$ is [[existentially closed model|existentially closed]]. \item For every embedding $A \hookrightarrow B$ where $A$ and $B$ model $T$, there exists an [[elementary extension]] $D$ of $A$ and an embedding $g : B \to D$ such that the triangle commutes. \item Every [[existentially closed model|existential formula]] is equivalent (mod $T$) to a [[existentially closed model|universal formula]]. \item Every formula is equivalent (mod $T$) to a universal formula. \end{enumerate} \end{theorem} \hypertarget{examples}{}\subsection*{{Examples}}\label{examples} \begin{itemize}% \item Since [[quantifier elimination]] is equivalent to [[substructure completeness]], which is stronger than model completeness, every theory which eliminates quantifiers is model complete. So, for example, [[ACF]], [[DLO]], [[RCF]], and the theory of the [[countable random graph]] are all model complete (and so their models are [[existentially closed]].) \end{itemize} \hypertarget{remarks}{}\subsection*{{Remarks}}\label{remarks} \begin{itemize}% \item A theory $T$ is model complete if and only if for every \emph{model} $A$ of $T$, the [[quantifier-free diagram]] $T_{\mathsf{Diag}(A)}$ (whose models are precisely the models of $T$ containing $A$ as an embedded substructure) is \emph{complete}. \item Analogously, a theory $T$ is [[substructure complete]] if and only if for every model $A$ of $T$ and every \emph{substructure} $B \subseteq A$, the [[quantifier-free diagram]] $T_{\mathsf{Diag}(B)}$ is \emph{complete}. \item A model complete theory is an ``existentially closed theory'' in the sense that all of its models are [[existentially closed model|existentially closed models]]. \item As mentioned above, [[substructure completeness]] implies model completeness because every elementary submodel is also a substructure. The proposition below shows that the converse holds with some additional assumptions. \end{itemize} \hypertarget{model_completeness__amalgamation_property_implies_substructure_completeness}{}\subsection*{{Model completeness + amalgamation property implies substructure completeness}}\label{model_completeness__amalgamation_property_implies_substructure_completeness} \begin{prop} \label{substructureconverse}\hypertarget{substructureconverse}{} Suppose the [[first-order theory]] $T$ in the language $\mathcal{L}$ is model complete and has the property that for any two models $X,Y \models T$ and a mutual $\mathcal{L}$-substructure $A \hookrightarrow X,Y$, the latter [[span]] in the category of $\mathcal{L}$-structures and embeddings has a [[cocone]] $Z$ which is also a model of $T$. Then $T$ is [[substructure complete]]. \end{prop} This property of being able to ``amalgamate'' the models $X$ and $Y$ over the common substructure $A$ is sometimes called the \textbf{amalgamation property}, though this terminology is rather overloaded (c.f. [[Fraisse limit]]). \begin{proof} Let $A$ be a substructure of some model $M \models T$. Append the [[quantifier-free diagram]] of $A$ to $T$ to form $T_{\mathsf{Diag}(A)}$. Suppose towards a contradiction that $\varphi$ is a sentence which is undecided by $T_{\mathsf{Diag}(A)}$; let $X$ and $Y$ be models of $T_{\mathsf{Diag}(A)}$ which witness this, so that $X \models \varphi$ while $Y \models \neg \varphi$. Let $Z$ amalgamate $X$ and $Y$ over $A$. By [[model completeness]], the theory $T_{\mathsf{Diag}(X)}$ of $T$-models (not necessarily [[elementary embedding|elementarily]]) embedding $X$ is complete. Abuse notation and replace the instances of constants from $A$ in $\varphi$ with their images in $X$. Either $T_{\mathsf{Diag}(X)} \models \varphi$ or $T_{\mathsf{Diag}(X)} \models \neg \varphi$. Since $X$ certainly embeds itself and $X \models \varphi$, $T_{\mathsf{Diag}(X)} \models \varphi$. Similarly, $T_{\mathsf{Diag}(Y)} \models \neg \varphi.$ Now, on one hand, the theory $T_{\mathsf{Diag}(X)} \cup T_{\mathsf{Diag}(Y)}/A$ (where we glue along the copies of $A$ in $\mathsf{Diag}(X)$ and $\mathsf{Diag}(Y)$) entails both $\varphi$ and $\neg \varphi$, which makes it inconsistent. This theory therefore has no models. On the other hand, this theory axiomatizes the class of amalgams of $X$ and $Y$ over $A$ in the category of $\mathcal{L}$-structures and embeddings, so in particular is modelled by $Z$, a contradiction. \end{proof} \hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts} \begin{itemize}% \item [[quantifier elimination]] \item [[model companion]] \item [[substructure completeness]] \item [[existentially closed model]] \end{itemize} \hypertarget{references}{}\subsection*{{References}}\label{references} \begin{itemize}% \item Wilfrid Hodges, \emph{Model theory}, Cambridge Univ. Press 1993 \end{itemize} [[!redirects model completeness]] [[!redirects model-complete theory]] [[!redirects model-completeness]] [[!redirects model complete]] \end{document}