We draw a correspondence between tiling problems and
first-order axiom
sets ; the desired result will fall out of
compactness of
first-order logic .
Let
L
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\cl L L be a
language consisting of a
constant symbol for each value in
N
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\bb N N as well as a
function symbol color
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\text{color} color of arity 3. Additionally,
fix ( up , right , down , left ) = ( 0 , 1 , 2 , 3 )
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
(\text{up}, \text{right}, \text{down}, \text{left}) = (0, 1, 2, 3) ( up , right , down , left ) = ( 0 , 1 , 2 , 3 )
Given a
set of wang tiles
T
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
T T and a subset
S ⊆ N 2
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
S \subseteq \bb N^2 S ⊆ N 2 of cells we want to tile, we form a
set Ξ ( T , S )
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\Xi(T, S) Ξ ( T , S ) of axioms as follows:
For each
( a , a ′ ) ∈ N 2
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
(a, a') \in \bb N^2 ( a , a ′ ) ∈ N 2 we include the axiom
a ≠ a ′
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
a \neq a' a = a ′
to ensure that tilings do not conflate two colors or coordinates
For each
( d , d ‾ , Δ n , Δ m ) ∈ { ( up , down , 0 , 1 ) , ( right , left , 1 , 0 ) }
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
(d, \ol d, \Delta n, \Delta m) \in \{ (\text{up}, \text{down}, 0, 1), (\text{right}, \text{left}, 1, 0) \} ( d , d , Δ n , Δ m ) ∈ {( up , down , 0 , 1 ) , ( right , left , 1 , 0 )} and each
( n , m ) ∈ N 2
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
(n, m) \in \bb N^2 ( n , m ) ∈ N 2 we include the axiom
color ( n , m , d ) = color ( n + Δ n , m + Δ m , d ‾ )
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\text{color}(n, m, d) = \text{color}(n + \Delta n, m + \Delta m, \ol d) color ( n , m , d ) = color ( n + Δ n , m + Δ m , d )
This demands that tilings are valid
For each tile
t ∈ T
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
t \in T t ∈ T , let
up ( t ) , right ( t ) , down ( t ) , left ( t )
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\text{up}(t), \text{right}(t), \text{down}(t), \text{left}(t) up ( t ) , right ( t ) , down ( t ) , left ( t ) denote the colors of
t
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
t t , which we assume to be natural numbers. For each
( n , m ) ∈ S
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
(n, m) \in S ( n , m ) ∈ S we include the axiom
⋁ t ∈ T ( color ( n , m , up ) = up ( t ) ∧ color ( n , m , right ) = right ( t ) ∧ color ( n , m , down ) = down ( t ) ∧ color ( n , m , left ) = left ( t ) )
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\bigvee_{t \in T} \left(
\begin{align*}
\t{color}(n, m, \t{up}) &= \t{up}(t)
\\ \land\ \t{color}(n, m, \t{right}) &= \t{right}(t)
\\ \land\ \t{color}(n, m, \t{down}) &= \t{down}(t)
\\ \land\ \t{color}(n, m, \t{left}) &= \t{left}(t)
\end{align*} \right)
t ∈ T ⋁ ⎝ ⎛ color ( n , m , up ) ∧ color ( n , m , right ) ∧ color ( n , m , down ) ∧ color ( n , m , left ) = up ( t ) = right ( t ) = down ( t ) = left ( t ) ⎠ ⎞
This is admissable because
T
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
T T is
finite . These axioms ensure that we produce only tilings consisting of tiles from
T
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
T T . Note that we only constrain coordinates from
S
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
S S . The rest of the plane may easily be tiled by matching the edge of
S
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
S S and choosing some color to
uniformly fill the rest of the plane.
Our axiom
set Ξ = Ξ ( T , S )
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\Xi = \Xi(T, S) Ξ = Ξ ( T , S ) contains only
quantifier-free formulas , which is fun. Anyway, I claim that by construction
Ξ
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\Xi Ξ has a
model if and only if S ⊆ N
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
S \subseteq \bb N S ⊆ N can be tiled by
T
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
T T . A
model M
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\cl M M for
Ξ
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\Xi Ξ will include an interpretation
color M
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\text{color}^\cl M color M which will give the actual tiling; the axioms of
Ξ
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\Xi Ξ will ensure that the tiling is valid.
Then
compactness gives us what we want. Say we have a tile
set T
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
T T which can tile any square in
N 2
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\bb N^2 N 2 . Then
Ξ ( T , N )
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\Xi(T, \bb N) Ξ ( T , N ) is
finitely satisfiable , because any
finite set of axioms demands at most a valid tiling up over some
finite S ⊆ N 2
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
S \subseteq \bb N^2 S ⊆ N 2 , which is satisfied by a tiling for some enclosing square. Hence by
compactness Ξ ( T , N )
%% general %%
% shorthands
\newcommand{\cl}[1]{ \mathcal{#1} }
\newcommand{\sc}[1]{ \mathscr{#1} }
\newcommand{\bb}[1]{ \mathbb{#1} }
\newcommand{\fk}[1]{ \mathfrak{#1} }
\renewcommand{\bf}[1]{ \mathbf{#1} }
\renewcommand{\sf}[1]{ \mathsf{#1} }
\renewcommand{\rm}[1]{ \mathrm{#1} }
\newcommand{\floor}[1]{ { \lfloor {#1} \rfloor } }
\newcommand{\ceil}[1]{ { \lceil {#1} \rceil } }
\newcommand{\ol}[1]{ \overline{#1} }
\newcommand{\t}[1]{ \text{#1} }
\newcommand{\norm}[1]{ { \lvert {#1} \rvert } } % norm/magnitude (REMOVE)
\newcommand{\mag}[1]{ { \left\lvert {#1} \right\rvert } } % magnitude
\newcommand{\smag}[1]{ { \lvert {#1} \rvert } } % short mag
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \langle {#1} \rangle } % tuples
\newcommand{\tl}{ \tilde }
\newcommand{\wt}{ \widetilde }
% f \onall X = { f(x) : x ∈ X }
\newcommand{\onall}[1]{ { \llbracket {#1} \rrbracket } }
% shorthands: various brackets
\newcommand{\tpar}[1]{ \left( {#1} \right) } % "tall parens"
\newcommand{\tbrak}[1]{ \left[ {#1} \right] } % "tall brackets"
\newcommand{\tbrac}[1]{ \left\{ {#1} \right\} } % "tall braces"
% reverse \mapsto (FIXME: make better)
\newcommand{\mapsfrom}{ \mathop{\leftarrow\!\mid} }
% reverse-order composition
\newcommand{\then}{ \operatorname{\ ;\ } }
% Like f' represents "f after modification", \pre{f}
% represents "f before modification"
% TODO: remove this?
\newcommand{\pre}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
\newcommand{\id}{ \,\mathrm d } % integration d
% derivatives: use {\ddn n x y} for (dy/dx)
\newcommand{\ddn}[3]{ \frac{ {\mathrm d}^{#1} {#2} }{ {\mathrm d} {#3}^{#1} } } % nth derivative
\newcommand{\dd}{ \ddn{} } % first derivative
\newcommand{\d}{ \dd{} } % first derivative (no numerator)
\newcommand{\dn}[1]{ \ddn{#1}{} } % nth derivative (no numerator)
% derivatives: use {\D n x y} for (∂_x y)
\newcommand{\Dn}[2]{ \partial^{#1}_{#2} }
\newcommand{\D}{ \Dn{} } % no power
\newcommand{\ig}[2]{ \int {#2} \, \mathrm d {#1} } % first integral
%% category theory %%
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% yoneda embedding
\newcommand{\yo}{よ}
% represents an anonymous parameter
% eg. $f(\apar)$ usually denotes the function $x \mapsto f(x)$
% TODO: remove this?
\newcommand{\apar}{ {-} }
%% computability %%
% turing machines
\newcommand{\halts}{ {\downarrow} }
\newcommand{\loops}{ {\uparrow} }
\Xi(T, \bb N) Ξ ( T , N ) is
satisfiable .