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
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\cl L L be a
language consisting of a
constant symbol for each value in
N
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\bb N N as well as a
function symbol color
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\text{color} color of arity 3. Additionally,
fix ( up , right , down , left ) = ( 0 , 1 , 2 , 3 )
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
(\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
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
T T and a subset
S ⊆ N 2
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
S \subseteq \bb N^2 S ⊆ N 2 of cells we want to tile, we form a
set Ξ ( T , S )
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\Xi(T, S) Ξ ( T , S ) of axioms as follows:
For each
( a , a ′ ) ∈ N 2
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
(a, a') \in \bb N^2 ( a , a ′ ) ∈ N 2 we include the axiom
a ≠ a ′
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
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 ) }
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
(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
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
(n, m) \in \bb N^2 ( n , m ) ∈ N 2 we include the axiom
color ( n , m , d ) = color ( n + Δ n , m + Δ m , d ‾ )
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\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
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
t \in T t ∈ T , let
up ( t ) , right ( t ) , down ( t ) , left ( t )
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\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
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
t t , which we assume to be natural numbers. For each
( n , m ) ∈ S
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
(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 ) )
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\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
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
T T is
finite . These axioms ensure that we produce only tilings consisting of tiles from
T
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
T T . Note that we only constrain coordinates from
S
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
S S . The rest of the plane may easily be tiled by matching the edge of
S
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
S S and choosing some color to
uniformly fill the rest of the plane.
Our axiom
set Ξ = Ξ ( T , S )
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\Xi = \Xi(T, S) Ξ = Ξ ( T , S ) contains only
quantifier-free formulas , which is fun. Anyway, I claim that by construction
Ξ
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\Xi Ξ has a
model if and only if S ⊆ N
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
S \subseteq \bb N S ⊆ N can be tiled by
T
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
T T . A
model M
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\cl M M for
Ξ
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\Xi Ξ will include an interpretation
color M
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\text{color}^\cl M color M which will give the actual tiling; the axioms of
Ξ
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\Xi Ξ will ensure that the tiling is valid.
Then
compactness gives us what we want. Say we have a tile
set T
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
T T which can tile any square in
N 2
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\bb N^2 N 2 . Then
Ξ ( T , N )
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\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
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
S \subseteq \bb N^2 S ⊆ N 2 , which is satisfied by a tiling for some enclosing square. Hence by
compactness Ξ ( T , N )
% 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} }
% category names
\newcommand{\cat}[1]{{ \sf{#1} }}
% more shorthands
\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
\newcommand{\card}{ \t{cd} } % cardinality
\newcommand{\dcup}{ \sqcup } % disjoint untion
\newcommand{\tup}[1]{ \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}[1]{{ \small `{#1} }}
% hook arrows
\newcommand{\injects}{ \hookrightarrow }
\newcommand{\embeds}{ \hookrightarrow }
\newcommand{\surjects}{ \twoheadrightarrow }
\newcommand{\projects}{ \twoheadrightarrow }
% good enough definition of yoneda
\newcommand{\yo}{よ}
\Xi(T, \bb N) Ξ ( T , N ) is
satisfiable .