$% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal L$-theories
Definition(s)
An $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal L$-theory is a set of sentences over the language $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal L$
Given an $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal L$-structure $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal M$, the theory of $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal M$, denoted $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \text{Th}(\mathcal M)$, is the set of sentences that $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal M$ satisfies; ie, the set $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \{ \mathcal L\text{-sentence}\ \phi : M \vDash \phi \}$
Terms
A theory $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } T$ is called:
satisfiable if there exists an $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal L$-structure $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal M$ where $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal M \vDash \phi$ for all $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \phi \in T$. Then we say that $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal M$ is a model for $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } T$
finitely satisfiable if for every finite subset $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } T_0 \subseteq T$ we have that $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } T_0$ is satisfiable.
maximal if for every $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal L$-sentence $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \phi$, either $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \phi \in T$ or $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \neg \phi \in T$. Note that all theories $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \text{Th}(\mathcal M)$ are maximal.
complete if for every $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal L$-sentence $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \phi$, either $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } T \vDash \phi$ or $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } T \vDash \neg \phi$, where by $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } T \vDash \psi$ we mean that for every $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal M$ modelling $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small {#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } T$ we have $% shorthands \newcommand{\cl}{ \mathcal{#1} } \newcommand{\sc}{ \mathscr{#1} } \newcommand{\bb}{ \mathbb{#1} } \newcommand{\fk}{ \mathfrak{#1} } \renewcommand{\bf}{ \mathbf{#1} } \renewcommand{\sf}{ \mathsf{#1} } % category names \newcommand{\cat}{{ \sf{#1} }} % more shorthands \newcommand{\floor}{ { \lfloor {#1} \rfloor } } \newcommand{\ceil}{ { \lceil {#1} \rceil } } \newcommand{\ol}{ \overline{#1} } \newcommand{\t}{ \text{#1} } \newcommand{\norm}{ { \lvert {#1} \rvert } } % norm/magnitude \newcommand{\card}{ \t{cd} } % cardinality \newcommand{\dcup}{ \sqcup } % disjoint untion \newcommand{\tup}{ \langle {#1} \rangle } % tuples % turing machines \newcommand{\halts}{ {\downarrow} } \newcommand{\loops}{ {\uparrow} } % represents an anonymous parameter % eg. f(\apar) usually denotes the function x \mapsto f(x) \newcommand{\apar}{ {-} } % reverse-order composition %\newcommand{\then}{ \operatorname{\ ;\ } } \newcommand{\then}{ {\scriptsize\ \rhd\ } } % Like f' represents "f after modification", \pre{f} % represents "f before modification" \newcommand{\pre}{{ \small `{#1} }} % hook arrows \newcommand{\injects}{ \hookrightarrow } \newcommand{\embeds}{ \hookrightarrow } \newcommand{\surjects}{ \twoheadrightarrow } \newcommand{\projects}{ \twoheadrightarrow } \mathcal M \vDash \psi$