Turing machines

Undecidability

Equation form expr-0022ffa6a3f66313

m<km < k

Read as: m is less than k

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: m is less than k

2 occurrences in this chapter

Equation form expr-002bf3eb1573e012

k+1k+1

Read as: k plus one

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: k plus one

2 occurrences in this chapter

Equation form expr-01208e159d2aec8c

∧\land

Read as: and

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: and

1 occurrence in this chapter

Equation form expr-0392a7f58dc6f6ba

0\Obj 0

Read as: object language symbol zero

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol zero

7 occurrences in this chapter

Equation form expr-043a718774c572bd

ss

Read as: s

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: s

10 occurrences in this chapter

Equation form expr-0485a455fa1f1209

Σ′={▷,0,A}\Sigma' = \{\TMendtape,\TMblank,A\}

Read as: capital sigma prime equals the set containing the left end marker, the blank symbol, and A

Means: An explicit finite-set expression or equation that preserves the source braces as set enclosure. Read as: capital sigma prime equals the set containing the left end marker, the blank symbol, and A.

1 occurrence in this chapter

Equation form expr-04ce27fdf5d2c493

Sσ(m¯,n¯)\Obj S_\sigma(\num{m}, \num{n})

Read as: object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for n close parenthesis

1 occurrence in this chapter

Equation form expr-05598a684835245e

<M′′={⟨0,1⟩,⟨1,1⟩,⟨2,2⟩}\Assign{<}{M''} = \{\tuple{0,1}, \tuple{1,1}, \tuple{2,2}\}

Read as: the interpretation of the less-than relation in structure M double prime equals the set containing the tuple zero comma one, the tuple one comma one, and the tuple two comma two

Means: An explicit finite-set expression or equation that preserves the source braces as set enclosure. Read as: the interpretation of the less-than relation in structure M double prime equals the set containing the tuple zero comma one, the tuple one comma one, and the tuple two comma two.

1 occurrence in this chapter

Equation form expr-089c421a1eee90aa

Sσi(i¯,n¯)\Obj S_{\sigma_i}(\num{i}, \num{n})

Read as: object language symbol S sub sigma sub i open parenthesis the numeral for i comma the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol S sub sigma sub i open parenthesis the numeral for i comma the numeral for n close parenthesis

1 occurrence in this chapter

Equation form expr-08f271887ce94707

MM

Read as: M

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: M

78 occurrences in this chapter

Equation form expr-0a1283c811f79f60

m=km=k

Read as: m equals k

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: m equals k

1 occurrence in this chapter

Equation form expr-0ac6f2ec0fc75966

k¯\num{k}

Read as: the numeral for k

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the numeral for k

1 occurrence in this chapter

Equation form expr-0b7e104051728a9a

T′(M,w)⊨C(M,w,n)∧B(n¯)!T'(M,w) \Entails !C(M, w, n) \land !B(\num{n})

Read as: T prime open parenthesis M comma w close parenthesis semantically entails C open parenthesis M comma w comma n close parenthesis and formula B open parenthesis the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T prime open parenthesis M comma w close parenthesis semantically entails C open parenthesis M comma w comma n close parenthesis and formula B open parenthesis the numeral for n close parenthesis

2 occurrences in this chapter

Equation form expr-0e05800e5244c124

S▷(0¯,0¯)∧Sσi1(1¯,0¯)∧…∧Sσik(k¯,0¯)\Obj S_\TMendtape(\num{0}, \num{0}) \land \Obj S_{\sigma_{i_1}}(\num{1}, \num{0}) \land \dots \land \Obj S_{\sigma_{i_k}}(\num{k}, \num{0})

Read as: object language symbol S sub left end marker open parenthesis the numeral for zero comma the numeral for zero close parenthesis and object language symbol S sub sigma sub i sub one open parenthesis the numeral for one comma the numeral for zero close parenthesis and and so on and object language symbol S sub sigma sub i sub k open parenthesis the numeral for k comma the numeral for zero close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol S sub left end marker open parenthesis the numeral for zero comma the numeral for zero close parenthesis and object language symbol S sub sigma sub i sub one open parenthesis the numeral for one comma the numeral for zero close parenthesis and and so on and object language symbol S sub sigma sub i sub k open parenthesis the numeral for k comma the numeral for zero close parenthesis

1 occurrence in this chapter

Equation form expr-0ed845e79c8d8e41

σi\sigma_i

Read as: sigma sub i

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: sigma sub i

1 occurrence in this chapter

Equation form expr-104da7f0527793ce

′M′(x)={x+1if x<nnotherwise,\Assign{\prime}{M'}(x) = \begin{cases} x + 1 &\text{if $x < n$}\\ n &\text{otherwise,} \end{cases}

Read as: the interpretation of successor symbol in structure M prime open parenthesis x close parenthesis equals cases begin; row one: x plus one, if x is less than n; row two: n, otherwise comma; cases end

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: the interpretation of successor symbol in structure M prime open parenthesis x close parenthesis equals cases begin; row one: x plus one, if x is less than n; row two: n, otherwise comma; cases end

1 occurrence in this chapter

Equation form expr-10d5524dfcfac13f

δ(q,σ)\delta(q, \sigma)

Read as: delta open parenthesis q comma sigma close parenthesis

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q comma sigma close parenthesis

3 occurrences in this chapter

Equation form expr-139c7c04318de35e

n=0n = 0

Read as: n equals zero

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: n equals zero

1 occurrence in this chapter

Equation form expr-155ee6a457533b5a

x=y=nx = y = n

Read as: x equals y equals n

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: x equals y equals n

1 occurrence in this chapter

Equation form expr-156f5402c1d0baa8

x+1x+1

Read as: x plus one

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: x plus one

4 occurrences in this chapter

Equation form expr-15fd307d7f46f8c3

2¯\num{2}

Read as: the numeral for two

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the numeral for two

1 occurrence in this chapter

Equation form expr-18ac3e7343f01689

dd

Read as: d

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: d

1 occurrence in this chapter

Equation form expr-18d6e1cac2a8adaf

1/01/0

Read as: one zero

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: one zero

1 occurrence in this chapter

Equation form expr-1b16b1df538ba12d

nn

Read as: n

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: n

53 occurrences in this chapter

Equation form expr-1ca7be4fe71cdda8

E(M,w)!E(M, w)

Read as: E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: E open parenthesis M comma w close parenthesis

6 occurrences in this chapter

Equation form expr-1d9411a61065e25b

S0M′′\Assign{\Obj S_{\TMblank}}{M''}

Read as: the interpretation of object language symbol S sub blank symbol in structure M prime prime

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: the interpretation of object language symbol S sub blank symbol in structure M prime prime

1 occurrence in this chapter

Equation form expr-1ed442ade7da8f5f

Qq(x,y)\Obj Q_q(x, y)

Read as: object language symbol Q sub q open parenthesis x comma y close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol Q sub q open parenthesis x comma y close parenthesis

1 occurrence in this chapter

Equation form expr-1f97d653b7ed2d2b

n+1n+1

Read as: n plus one

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: n plus one

2 occurrences in this chapter

Equation form expr-1fe07613f8be2bf9

E⌢DE \concat D

Read as: E concatenated with D

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: E concatenated with D

2 occurrences in this chapter

Equation form expr-20c0d70009cd33dd

T(M,w)⊢k¯<k¯′!T(M,w) \Proves \num{k} < \num{k}'

Read as: T open parenthesis M comma w close parenthesis proves the numeral for k is less than the numeral for k prime

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: T open parenthesis M comma w close parenthesis proves the numeral for k is less than the numeral for k prime

1 occurrence in this chapter

Equation form expr-2160509ff364e743

M\Struct M

Read as: structure M

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M

3 occurrences in this chapter

Equation form expr-21a3189658821b30

R\TMright

Read as: move right

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: move right

1 occurrence in this chapter

Equation form expr-241d1cd21689b8a9

y′y'

Read as: y prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: y prime

1 occurrence in this chapter

Equation form expr-2438c1075acdf774

0¯=0n+1¯=n¯′\num{0} & = \Obj 0 \\ \num{n+1} &= \num{n}'

Read as: the numeral for zero equals object language symbol zero next row the numeral for n plus one equals the numeral for n prime

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: the numeral for zero equals object language symbol zero next row the numeral for n plus one equals the numeral for n prime

1 occurrence in this chapter

Equation form expr-266ae6e58d62d965

T(M,w)⊨E(M,w)!T(M, w) \Entails !E(M, w)

Read as: T open parenthesis M comma w close parenthesis semantically entails E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis semantically entails E open parenthesis M comma w close parenthesis

3 occurrences in this chapter

Equation form expr-284c47be48fb0c66

¬\lnot

Read as: not

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: not

1 occurrence in this chapter

Equation form expr-285974d271093f47

∀x∀y((Qq(x,y)∧Sσ(x,y))→(Qq′(x′,y′)∧Sσ′(x,y′)∧A(x,y)))is a conjunct of T(M,w). This entails the following !!{sentence} (universal instantiation, m¯ for~x and n¯ for~y):(Qq(m¯,n¯)∧Sσ(m¯,n¯))→(Qq′(m¯′,n¯′)∧Sσ′(m¯,n¯′)∧A(m¯,n¯)).By induction hypothesis, T(M,w)⊨C(M,w,n), i.e.,Qq(m¯,n¯)∧Sσ0(0¯,n¯)∧…∧Sσk(k¯,n¯)∧∀x(k¯<x→S0(x,n¯))Since after n steps, tape square~m contains~σ, the corresponding conjunct is~Sσ(m¯,n¯), so this entails:Qq(m¯,n¯)∧Sσ(m¯,n¯)We now getQq′(m¯′,n¯′)∧Sσ′(m¯,n¯′)∧Sσ0(0¯,n¯′)∧…∧Sσk(k¯,n¯′)∧∀x(k¯<x→S0(x,n¯′))& \lforall[x][\lforall[y][((\Obj Q_{q}(x, y) \land \Obj S_\sigma(x, y)) \lif {}]]\\ & \qquad (\Obj Q_{q'}(x', y') \land \Obj S_{\sigma'}(x, y') \land !A(x, y))) \intertext{is a conjunct of $!T(M,w)$. This entails the following !!{sentence} (universal instantiation, $\num{m}$ for~$x$ and $\num{n}$ for~$y$):} & (\Obj Q_{q}(\num{m}, \num{n}) \land \Obj S_{\sigma}(\num{m}, \num{n})) \lif {}\\ & \qquad (\Obj Q_{q'}(\num{m}', \num{n}') \land \Obj S_{\sigma'}(\num{m}, \num{n}') \land !A(\num{m}, \num{n})). \intertext{By induction hypothesis, $!T(M, w) \Entails !C(M, w, n)$, i.e.,} & \Obj Q_q(\num{m}, \num{n}) \land \Obj S_{\sigma_0}(\num{0}, \num{n}) \land \dots \land \Obj S_{\sigma_k}(\num{k}, \num{n}) \land \\ & \qquad\lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}))]\\ \intertext{Since after $n$ steps, tape square~$m$ contains~$\sigma$, the corresponding conjunct is~$\Obj S_\sigma(\num{m}, \num{n})$, so this entails:} & \Obj Q_{q}(\num{m}, \num{n}) \land \Obj S_{\sigma}(\num{m}, \num{n}) \intertext{We now get} & \Obj Q_{q'}(\num{m}', \num{n}') \land \Obj S_{\sigma'}(\num{m}, \num{n}') \land {}\\ & \qquad\Obj S_{\sigma_0}(\num{0}, \num{n}') \land \dots \land \Obj S_{\sigma_k}(\num{k}, \num{n}') \land {}\\ & \qquad \lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}'))]

Read as: Right move induction display. For every x and y, if the machine is in state q scanning square x and that square contains sigma at time y, then at time y prime it is in state q prime scanning square x prime, writes sigma prime at x, and leaves every other square unchanged. Instantiate x with numeral m and y with numeral n. Combine this transition with the represented current configuration to obtain state q prime at square m prime and time n prime, the updated symbol at square m, all unchanged listed tape symbols, and a blank tail beyond numeral k

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: Right move induction display. For every x and y, if the machine is in state q scanning square x and that square contains sigma at time y, then at time y prime it is in state q prime scanning square x prime, writes sigma prime at x, and leaves every other square unchanged. Instantiate x with numeral m and y with numeral n. Combine this transition with the represented current configuration to obtain state q prime at square m prime and time n prime, the updated symbol at square m, all unchanged listed tape symbols, and a blank tail beyond numeral k

1 occurrence in this chapter

Equation form expr-28e8ca6f819f726b

k<nk < n

Read as: k is less than n

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: k is less than n

2 occurrences in this chapter

Equation form expr-2adc9a0232f82eb1

w=σi1…σikw = \sigma_{i_1}\dots\sigma_{i_k}

Read as: w equals sigma sub i sub one and so on sigma sub i sub k

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: w equals sigma sub i sub one and so on sigma sub i sub k

2 occurrences in this chapter

Equation form expr-2b88573dfa91deef

h(e,n)={0if machine~Me does not halt for input n1if machine~Me halts for input nh(e,n) = \begin{cases} \text{0} & \text{if machine~$M_e$ does not halt for input $n$} \\ \text{1} & \text{if machine~$M_e$ halts for input $n$} \end{cases}

Read as: h open parenthesis e comma n close parenthesis equals cases begin; row one: zero, if machine M sub e does not halt for input n; row two: one, if machine M sub e halts for input n; cases end

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: h open parenthesis e comma n close parenthesis equals cases begin; row one: zero, if machine M sub e does not halt for input n; row two: one, if machine M sub e halts for input n; cases end

1 occurrence in this chapter

Equation form expr-2d711642b726b044

xx

Read as: x

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: x

5 occurrences in this chapter

Equation form expr-2f9465b95c9e8e33

E(M,Λ)!E(M,\emptyseq)

Read as: E open parenthesis M comma the empty sequence code close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: E open parenthesis M comma the empty sequence code close parenthesis

1 occurrence in this chapter

Equation form expr-2fdfdde7570c43b1

qiq_i

Read as: q sub i

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: q sub i

2 occurrences in this chapter

Equation form expr-3072e8ef9af4e2b1

k¯<k¯′\num{k} < \num{k}'

Read as: the numeral for k is less than the numeral for k prime

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: the numeral for k is less than the numeral for k prime

1 occurrence in this chapter

Equation form expr-307ff218fecd14ae

N\TMstay

Read as: stay put

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: stay put

1 occurrence in this chapter

Equation form expr-3188150e34a0f671

T(M,w)⊢m¯<k¯!T(M,w) \Proves \num{m} < \num {k}

Read as: T open parenthesis M comma w close parenthesis proves the numeral for m is less than the numeral for k

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: T open parenthesis M comma w close parenthesis proves the numeral for m is less than the numeral for k

1 occurrence in this chapter

Equation form expr-31cef529d16bee5f

Sσ(x,y)\Obj S_\sigma(x, y)

Read as: object language symbol S sub sigma open parenthesis x comma y close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol S sub sigma open parenthesis x comma y close parenthesis

1 occurrence in this chapter

Equation form expr-3377aa50e30c85c9

Sσ(m¯,n¯)\Obj S_{\sigma}(\num{m}, \num{n})

Read as: object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for n close parenthesis

1 occurrence in this chapter

Equation form expr-33a9c96304bcc292

|M|\Domain{M}

Read as: the domain of structure M

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the domain of structure M

1 occurrence in this chapter

Equation form expr-34fd6d8fbebb6d5a

∀x∀y((Qqi(x′,y)∧Sσ(x′,y))→(Qqj(x,y′)∧Sσ′(x′,y′)∧A(x,y)))∧∀y((Qqi(0¯,y)∧Sσ(0¯,y))→(Qqj(0¯,y′)∧Sσ′(0¯,y′)∧A(0¯,y)))& \lforall[x][\lforall[y][ ((\Obj Q_{q_i}(x', y) \land \Obj S_{\sigma}(x', y)) \lif {}]]\\ & \qquad (\Obj Q_{q_j}(x, y') \land \Obj S_{\sigma'}(x', y') \land !A(x, y))) \land {}\\ & \lforall[y][((\Obj Q_{q_i}(\num{0}, y) \land \Obj S_{\sigma}(\num{0}, y)) \lif {}]\\ & \qquad (\Obj Q_{q_j}(\num{0}, y') \land \Obj S_{\sigma'}(\num{0}, y') \land !A(\num{0}, y)))

Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x prime comma y close parenthesis and object language symbol S sub sigma open parenthesis x prime comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x prime comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis close parenthesis close parenthesis and next row then for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis the numeral for zero comma y close parenthesis and object language symbol S sub sigma open parenthesis the numeral for zero comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis the numeral for zero comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis the numeral for zero comma y prime close parenthesis and formula A open parenthesis the numeral for zero comma y close parenthesis close parenthesis close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x prime comma y close parenthesis and object language symbol S sub sigma open parenthesis x prime comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x prime comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis close parenthesis close parenthesis and next row then for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis the numeral for zero comma y close parenthesis and object language symbol S sub sigma open parenthesis the numeral for zero comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis the numeral for zero comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis the numeral for zero comma y prime close parenthesis and formula A open parenthesis the numeral for zero comma y close parenthesis close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-35d3c1188d25a8a2

A(m,n)!A(m, n)

Read as: formula A open parenthesis m comma n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: formula A open parenthesis m comma n close parenthesis

1 occurrence in this chapter

Equation form expr-371bacbea5363456

M⊨B\Sat{M}{!B}

Read as: structure M satisfies formula B

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M satisfies formula B

1 occurrence in this chapter

Equation form expr-380172cff57049ab

w=Λw = \emptyseq

Read as: w equals the empty sequence code

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: w equals the empty sequence code

1 occurrence in this chapter

Equation form expr-39c0c06bf0f96fc1

Qq(m¯,k¯)\Obj Q_q(\num{m}, \num{k})

Read as: object language symbol Q sub q open parenthesis the numeral for m comma the numeral for k close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol Q sub q open parenthesis the numeral for m comma the numeral for k close parenthesis

1 occurrence in this chapter

Equation form expr-3c0042c07a5ab1bc

M′⊨T(M,w)\Sat{M'}{!T(M,w)}

Read as: structure M prime satisfies T open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M prime satisfies T open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-3c96c67cffcd3a70

∀x(k¯<x→S0(x,n¯′))\lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}'))]

Read as: for every x, open parenthesis the numeral for k is less than x implies object language symbol S sub blank symbol open parenthesis x comma the numeral for n prime close parenthesis close parenthesis

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: for every x, open parenthesis the numeral for k is less than x implies object language symbol S sub blank symbol open parenthesis x comma the numeral for n prime close parenthesis close parenthesis

2 occurrences in this chapter

Equation form expr-3d49f0278c584cab

δ(qi,σ)=⟨qj,σ′,N⟩\delta(q_i, \sigma) = \tuple{q_j, \sigma', \TMstay}

Read as: delta open parenthesis q sub i comma sigma close parenthesis equals the tuple q sub j comma sigma prime comma stay put

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q sub i comma sigma close parenthesis equals the tuple q sub j comma sigma prime comma stay put

2 occurrences in this chapter

Equation form expr-3e3cb3d5dc7f2dc5

1\TMstroke

Read as: stroke symbol

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: stroke symbol

35 occurrences in this chapter

Equation form expr-3f1b6dc519af96a7

′\prime

Read as: successor symbol

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: successor symbol

4 occurrences in this chapter

Equation form expr-3f39d5c348e5b79d

DD

Read as: D

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: D

6 occurrences in this chapter

Equation form expr-3f79bb7b435b0532

ee

Read as: e

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: e

27 occurrences in this chapter

Equation form expr-3fbd6815ef509046

B(y′)!B(y')

Read as: formula B open parenthesis y prime close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: formula B open parenthesis y prime close parenthesis

2 occurrences in this chapter

Equation form expr-3ffc6ab441a537ac

∀xx<x′\lforall[x][x < x']

Read as: for every x, x is less than x prime

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: for every x, x is less than x prime

3 occurrences in this chapter

Equation form expr-406f80d6fe2a10d6

S⌢JS \concat J

Read as: S concatenated with J

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: S concatenated with J

2 occurrences in this chapter

Equation form expr-418dd978c2c5d730

Q×ΣQ \times \Sigma

Read as: Q times capital sigma

Means: Notation for a machine prime s state set, tape alphabet, or defining tuple. Read as: Q times capital sigma

1 occurrence in this chapter

Equation form expr-4259230107adbba5

⊨T(M,w)→E(M,w)\Entails !T(M, w) \lif !E(M,w)

Read as: semantically entails T open parenthesis M comma w close parenthesis implies E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: semantically entails T open parenthesis M comma w close parenthesis implies E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-42b8f19ae63d24a4

M\Struct{M}

Read as: structure M

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M

7 occurrences in this chapter

Equation form expr-42e769a18fac6caa

⟨x,y⟩∈<M′\tuple{x,y} \in \Assign{<}{M'}

Read as: the tuple x comma y is in the interpretation of is less than in structure M prime

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: the tuple x comma y is in the interpretation of is less than in structure M prime

1 occurrence in this chapter

Equation form expr-440a949d16174f45

T(M,w)⊨C(M,w,n)!T(M,w) \Entails !C(M, w, n)

Read as: T open parenthesis M comma w close parenthesis semantically entails C open parenthesis M comma w comma n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis semantically entails C open parenthesis M comma w comma n close parenthesis

1 occurrence in this chapter

Equation form expr-44bd7ae60f478fae

HH

Read as: H

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: H

4 occurrences in this chapter

Equation form expr-45943e4f62da7355

s′(e)={1if machine~Me halts for input eundefinedif machine~Me does not halt for input es'(e) = \begin{cases} \text{1} & \text{if machine~$M_e$ halts for input $e$}\\ \text{undefined} & \text{if machine~$M_e$ does not halt for input $e$} \end{cases}

Read as: s prime open parenthesis e close parenthesis equals cases begin; row one: one, if machine M sub e halts for input e; row two: undefined, if machine M sub e does not halt for input e; cases end

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: s prime open parenthesis e close parenthesis equals cases begin; row one: one, if machine M sub e halts for input e; row two: undefined, if machine M sub e does not halt for input e; cases end

1 occurrence in this chapter

Equation form expr-46461bd80ef280f6

{s,h}\{s,h\}

Read as: the set containing s and h

Means: An explicit finite-set expression or equation that preserves the source braces as set enclosure. Read as: the set containing s and h.

1 occurrence in this chapter

Equation form expr-4657d6b3478ad20c

E⌢DE\concat D

Read as: E concatenated with D

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: E concatenated with D

1 occurrence in this chapter

Equation form expr-47ff73410fefc50c

f(e,n)=mf(e,n) = m

Read as: f open parenthesis e comma n close parenthesis equals m

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: f open parenthesis e comma n close parenthesis equals m

1 occurrence in this chapter

Equation form expr-4ad279bf4e4a8c22

f(n)f(n)

Read as: f open parenthesis n close parenthesis

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: f open parenthesis n close parenthesis

2 occurrences in this chapter

Equation form expr-4ae81572f06e1b88

QQ

Read as: Q

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: Q

1 occurrence in this chapter

Equation form expr-4b68ab3847feda7d

XX

Read as: X

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: X

1 occurrence in this chapter

Equation form expr-4ba54a6a818f6522

y+1y+1

Read as: y plus one

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: y plus one

2 occurrences in this chapter

Equation form expr-4bcc8b4ac4501fa9

i<mi < m

Read as: i is less than m

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: i is less than m

1 occurrence in this chapter

Equation form expr-4d5e2d82e9b73555

Sσm(m¯,n¯′)\Obj S_{\sigma_m}(\num{m},\num{n}')

Read as: object language symbol S sub sigma sub m open parenthesis the numeral for m comma the numeral for n prime close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol S sub sigma sub m open parenthesis the numeral for m comma the numeral for n prime close parenthesis

1 occurrence in this chapter

Equation form expr-4e07408562bedb8b

33

Read as: three

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: three

3 occurrences in this chapter

Equation form expr-4e3ed9256de1b698

⊨T(M,w)→E(M,w)\Entails !T(M, w) \lif !E(M, w)

Read as: semantically entails T open parenthesis M comma w close parenthesis implies E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: semantically entails T open parenthesis M comma w close parenthesis implies E open parenthesis M comma w close parenthesis

4 occurrences in this chapter

Equation form expr-5048c4b9123eb530

σ1\sigma_1

Read as: sigma sub one

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: sigma sub one

1 occurrence in this chapter

Equation form expr-50e721e49c013f00

ww

Read as: w

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: w

53 occurrences in this chapter

Equation form expr-5114954d49b039d0

T(Me,w)→E(Me,w)!T(M_e, w) \lif !E(M_e, w)

Read as: T open parenthesis M sub e comma w close parenthesis implies E open parenthesis M sub e comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M sub e comma w close parenthesis implies E open parenthesis M sub e comma w close parenthesis

4 occurrences in this chapter

Equation form expr-515233b84981c9db

m<km<k

Read as: m is less than k

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: m is less than k

1 occurrence in this chapter

Equation form expr-522d6ce4b07bfab0

Qq0M′′\Assign{\Obj Q_{q_0}}{M''}

Read as: the interpretation of object language symbol Q sub q sub zero in structure M prime prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the interpretation of object language symbol Q sub q sub zero in structure M prime prime

1 occurrence in this chapter

Equation form expr-5279731c117b6bc7

T(M,w)∧E(M,w)!T(M,w) \land !E(M,w)

Read as: T open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

3 occurrences in this chapter

Equation form expr-52c0b2d7d72a6fe8

l¯≡0¯\num{l} \ident \num{0}

Read as: the numeral for l is syntactically identical to the numeral for zero

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the numeral for l is syntactically identical to the numeral for zero

1 occurrence in this chapter

Equation form expr-5351bd0dfb10e404

∀z(((z<x∨x<z)∧Sσ(z,y))→Sσ(z,y′))\lforall[z][ (((z < x \lor x < z) \land \Obj S_\sigma(z, y)) \lif \Obj S_\sigma(z, y'))]

Read as: for every z, open parenthesis open parenthesis open parenthesis z is less than x or x is less than z close parenthesis and object language symbol S sub sigma open parenthesis z comma y close parenthesis close parenthesis implies object language symbol S sub sigma open parenthesis z comma y prime close parenthesis close parenthesis

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: for every z, open parenthesis open parenthesis open parenthesis z is less than x or x is less than z close parenthesis and object language symbol S sub sigma open parenthesis z comma y close parenthesis close parenthesis implies object language symbol S sub sigma open parenthesis z comma y prime close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-5499510e641b214f

0≤i≤k0 \le i \le k

Read as: zero is less than or equal to i is less than or equal to k

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: zero is less than or equal to i is less than or equal to k

1 occurrence in this chapter

Equation form expr-559aead08264d579

AA

Read as: capital A symbol

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: capital A symbol

2 occurrences in this chapter

Equation form expr-56552e66460416dc

M⊨Qq(m¯,n¯)\Sat{M}{\Obj Q_q(\num{m}, \num{n})}

Read as: structure M satisfies object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M satisfies object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis

1 occurrence in this chapter

Equation form expr-5a1eb28f9326ed82

Sσi(i¯,n¯′)\Obj S_{\sigma_i}(\num{i}, \num{n}')

Read as: object language symbol S sub sigma sub i open parenthesis the numeral for i comma the numeral for n prime close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol S sub sigma sub i open parenthesis the numeral for i comma the numeral for n prime close parenthesis

1 occurrence in this chapter

Equation form expr-5afa20230f875253

n∈ℕn \in \Nat

Read as: n is in the natural numbers

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: n is in the natural numbers

2 occurrences in this chapter

Equation form expr-5b81b8dff6f867f7

i≠mi \neq m

Read as: i is not equal to m

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: i is not equal to m

1 occurrence in this chapter

Equation form expr-5b85a600f1f160cd

s(e)=0s(e) = 0

Read as: s open parenthesis e close parenthesis equals zero

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: s open parenthesis e close parenthesis equals zero

1 occurrence in this chapter

Equation form expr-5cc45fd085fa0e67

∃x∃yQh(x,y)\lexists[x][\lexists[y][\Obj Q_h(x, y)]]

Read as: there exists x, there exists y, object language symbol Q sub h open parenthesis x comma y close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: there exists x, there exists y, object language symbol Q sub h open parenthesis x comma y close parenthesis

1 occurrence in this chapter

Equation form expr-5e769b89788d547a

s′s'

Read as: s prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: s prime

1 occurrence in this chapter

Equation form expr-5eecf8115f7c0078

C(M,w,n)⊨E(M,w)!C(M, w, n) \Entails !E(M,w)

Read as: C open parenthesis M comma w comma n close parenthesis semantically entails E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: C open parenthesis M comma w comma n close parenthesis semantically entails E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-5fc7567dc5f941ee

B(n¯)⊨k¯<n¯→k¯≠n¯!B(\num{n}) \Entails \num{k} < \num{n} \lif \eq/[\num{k}][\num{n}]

Read as: formula B open parenthesis the numeral for n close parenthesis semantically entails the numeral for k is less than the numeral for n implies the numeral for k is not equal to the numeral for n

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: formula B open parenthesis the numeral for n close parenthesis semantically entails the numeral for k is less than the numeral for n implies the numeral for k is not equal to the numeral for n

1 occurrence in this chapter

Equation form expr-5feceb66ffc86f38

00

Read as: zero

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: zero

20 occurrences in this chapter

Equation form expr-608b49002ed2f8f4

∀x(k¯<x→m¯<x)\lforall[x][(\num{k} < x \lif \num{m} < x)]

Read as: for every x, open parenthesis the numeral for k is less than x implies the numeral for m is less than x close parenthesis

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: for every x, open parenthesis the numeral for k is less than x implies the numeral for m is less than x close parenthesis

3 occurrences in this chapter

Equation form expr-61a45982430145d0

f:ℕ×ℕ⇀ℕf\colon \Nat \times \Nat \pto \Nat

Read as: f from the natural numbers times the natural numbers partially maps to the natural numbers

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: f from the natural numbers times the natural numbers partially maps to the natural numbers

1 occurrence in this chapter

Equation form expr-62c66a7a5dd70c31

mm

Read as: m

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: m

13 occurrences in this chapter

Equation form expr-638a8052d17cbaf3

0′\Obj 0'

Read as: object language symbol zero prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol zero prime

3 occurrences in this chapter

Equation form expr-66c370af1c7f93e0

|M′′|={0,1,2}\Domain{M''} = \{0, 1, 2\}

Read as: the domain of structure M double prime equals the set containing zero, one, and two

Means: An explicit finite-set expression or equation that preserves the source braces as set enclosure. Read as: the domain of structure M double prime equals the set containing zero, one, and two.

1 occurrence in this chapter

Equation form expr-66ff1e757c3aa9b2

Sσ(m¯,k¯)\Obj S_\sigma(\num{m}, \num{k})

Read as: object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for k close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for k close parenthesis

1 occurrence in this chapter

Equation form expr-6779c64ab17f04c5

T(M,w)→E(M,w)!T(M, w) \lif !E(M, w)

Read as: T open parenthesis M comma w close parenthesis implies E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis implies E open parenthesis M comma w close parenthesis

8 occurrences in this chapter

Equation form expr-67abbd486aaad55c

∀x(k¯′<x→S0(x,n¯′))\lforall[x][(\num{k}' < x \lif \Obj S_\TMblank(x, \num{n}'))]

Read as: for every x, open parenthesis the numeral for k prime is less than x implies object language symbol S sub blank symbol open parenthesis x comma the numeral for n prime close parenthesis close parenthesis

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: for every x, open parenthesis the numeral for k prime is less than x implies object language symbol S sub blank symbol open parenthesis x comma the numeral for n prime close parenthesis close parenthesis

3 occurrences in this chapter

Equation form expr-688eed70a27e98ff

q1q_1

Read as: q sub one

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: q sub one

2 occurrences in this chapter

Equation form expr-697c25e2e7186d2e

′M′′(2)=2\Assign{\prime}{M''}(2) = 2

Read as: the interpretation of successor symbol in structure M prime prime open parenthesis two close parenthesis equals two

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: the interpretation of successor symbol in structure M prime prime open parenthesis two close parenthesis equals two

1 occurrence in this chapter

Equation form expr-6b86b273ff34fce1

11

Read as: one

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: one

29 occurrences in this chapter

Equation form expr-6ba563d20e8fdc92

T(M,Λ)∧E(M,Λ)!T(M,\emptyseq) \land !E(M,\emptyseq)

Read as: T open parenthesis M comma the empty sequence code close parenthesis and E open parenthesis M comma the empty sequence code close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma the empty sequence code close parenthesis and E open parenthesis M comma the empty sequence code close parenthesis

1 occurrence in this chapter

Equation form expr-6d11835243989d93

σ∈Σ\sigma \in \Sigma

Read as: sigma is in capital sigma

Means: Notation for a machine prime s state set, tape alphabet, or defining tuple. Read as: sigma is in capital sigma

1 occurrence in this chapter

Equation form expr-6da43b944e494e88

JJ

Read as: J

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: J

7 occurrences in this chapter

Equation form expr-6f4a718317df8bd5

h(e,w)h(e,w)

Read as: h open parenthesis e comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: h open parenthesis e comma w close parenthesis

1 occurrence in this chapter

Equation form expr-724a316edcd71912

∀x∀y((Qqi(x′,y)∧Sσ(x′,y))→(Qqj(x,y′)∧Sσ′(x′,y′)∧A(x,y)))∧∀y((Qqi(0¯,y)∧Sσ(0¯,y))→(Qqj(0¯,y′)∧Sσ′(0¯,y′)∧A(0¯,y)∧B(y′)))& \lforall[x][\lforall[y][ ((\Obj Q_{q_i}(x', y) \land \Obj S_{\sigma}(x', y)) \lif {}]]\\ & \qquad (\Obj Q_{q_j}(x, y') \land \Obj S_{\sigma'}(x', y') \land !A(x, y))) \land {}\\ & \lforall[y][((\Obj Q_{q_i}(\num{0}, y) \land \Obj S_{\sigma}(\num{0}, y)) \lif {}]\\ & \qquad (\Obj Q_{q_j}(\num{0}, y') \land \Obj S_{\sigma'}(\num{0}, y') \land !A(\num{0}, y) \land !B(y')))

Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x prime comma y close parenthesis and object language symbol S sub sigma open parenthesis x prime comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x prime comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis close parenthesis close parenthesis and next row then for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis the numeral for zero comma y close parenthesis and object language symbol S sub sigma open parenthesis the numeral for zero comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis the numeral for zero comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis the numeral for zero comma y prime close parenthesis and formula A open parenthesis the numeral for zero comma y close parenthesis and formula B open parenthesis y prime close parenthesis close parenthesis close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x prime comma y close parenthesis and object language symbol S sub sigma open parenthesis x prime comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x prime comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis close parenthesis close parenthesis and next row then for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis the numeral for zero comma y close parenthesis and object language symbol S sub sigma open parenthesis the numeral for zero comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis the numeral for zero comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis the numeral for zero comma y prime close parenthesis and formula A open parenthesis the numeral for zero comma y close parenthesis and formula B open parenthesis y prime close parenthesis close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-72d3c432570c02f5

T′(M,w)∧E(M,w)!T'(M,w) \land !E(M, w)

Read as: T prime open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T prime open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-74728437b7963d0d

∀x(k¯<x→S0(x,0¯))\lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x, \num{0}))]

Read as: for every x, open parenthesis the numeral for k is less than x implies object language symbol S sub blank symbol open parenthesis x comma the numeral for zero close parenthesis close parenthesis

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: for every x, open parenthesis the numeral for k is less than x implies object language symbol S sub blank symbol open parenthesis x comma the numeral for zero close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-74c09e8f4b051811

M′⊨T′(M,w)∧E(M,w)\Sat{M'}{!T'(M,w) \land !E(M,w)}

Read as: structure M prime satisfies T prime open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M prime satisfies T prime open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-74ea488bf3852965

M⊨E(M,w)\Sat{M}{!E(M, w)}

Read as: structure M satisfies E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M satisfies E open parenthesis M comma w close parenthesis

3 occurrences in this chapter

Equation form expr-75dcf9c6552708e7

sM∈(Z+)*s_M \in (\PosInt)^*

Read as: s sub M is in open parenthesis positive integers close parenthesis superscript

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: s sub M is in open parenthesis positive integers close parenthesis superscript

1 occurrence in this chapter

Equation form expr-76956fb84940d91a

e≠ne \neq n

Read as: e is not equal to n

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: e is not equal to n

1 occurrence in this chapter

Equation form expr-76a8c8c02bf83b7a

M′M'

Read as: M prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: M prime

2 occurrences in this chapter

Equation form expr-780ad37cc2a9c734

e=ne = n

Read as: e equals n

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: e equals n

1 occurrence in this chapter

Equation form expr-7871e01579318cd3

⟨e,n⟩\tuple{e,n}

Read as: the tuple e comma n

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the tuple e comma n

1 occurrence in this chapter

Equation form expr-79c5e01e1ef895a2

f(e,n)f(e,n)

Read as: f open parenthesis e comma n close parenthesis

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: f open parenthesis e comma n close parenthesis

1 occurrence in this chapter

Equation form expr-79d4c7f9c8579543

ℕ\Nat

Read as: the natural numbers

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: the natural numbers

17 occurrences in this chapter

Equation form expr-7a6a9b174f4c80df

M⊨k¯≠n¯\Sat{M}{\eq/[\num{k}][\num{n}]}

Read as: structure M satisfies the numeral for k is not equal to the numeral for n

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M satisfies the numeral for k is not equal to the numeral for n

1 occurrence in this chapter

Equation form expr-7b5324c551330f48

S▷M′′\Assign{\Obj S_{\TMendtape}}{M''}

Read as: the interpretation of object language symbol S sub left end marker in structure M prime prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the interpretation of object language symbol S sub left end marker in structure M prime prime

1 occurrence in this chapter

Equation form expr-7c79a30577a3ee7b

Qq(m¯,n¯)∧Sσ(m¯,n¯)⊨⋁⟨q,σ⟩∈X(Qq(m¯,n¯)∧Sσ(m¯,n¯))\Obj Q_{q}(\num{m}, \num{n}) \land \Obj S_{\sigma}(\num{m}, \num{n}) \Entails \bigvee_{\tuple{q, \sigma} \in X} (\Obj Q_q(\num{m}, \num{n}) \land \Obj S_{\sigma}(\num{m}, \num{n}))

Read as: object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis and object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for n close parenthesis semantically entails the disjunction over sub the tuple q comma sigma is in X open parenthesis object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis and object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for n close parenthesis close parenthesis

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis and object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for n close parenthesis semantically entails the disjunction over sub the tuple q comma sigma is in X open parenthesis object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis and object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for n close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-7c7f989fbf767be7

T(M,w)⊨C(M,w,n+1)!T(M, w) \Entails !C(M, w, n+1)

Read as: T open parenthesis M comma w close parenthesis semantically entails C open parenthesis M comma w comma n plus one close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis semantically entails C open parenthesis M comma w comma n plus one close parenthesis

1 occurrence in this chapter

Equation form expr-7d342f063525a48d

QqM={⟨m,n⟩:started on~w, after~n steps,M is in state q scanning square~m}SσM={⟨m,n⟩:started on~w, after n steps,square~m of M contains symbol~σ}\Assign{\Obj Q_q}{M} & = \Setabs{\tuple{m, n}}{\begin{array}{ll}\text{started on~$w$, after~$n$ steps,}\\ \text{$M$ is in state $q$ scanning square~$m$}\end{array}} \\ \Assign{\Obj S_\sigma}{M} & = \Setabs{\tuple{m, n}}{\begin{array}{ll} \text{started on~$w$, after $n$ steps,}\\ \text{square~$m$ of $M$ contains symbol~$\sigma$}\end{array}}

Read as: Interpretation of the run structure. Predicate Q sub q contains exactly the pairs m and n for which machine M, started on input w, is in state q scanning square m after n steps. Predicate S sub sigma contains exactly the pairs m and n for which square m contains symbol sigma after n steps

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: Interpretation of the run structure. Predicate Q sub q contains exactly the pairs m and n for which machine M, started on input w, is in state q scanning square m after n steps. Predicate S sub sigma contains exactly the pairs m and n for which square m contains symbol sigma after n steps

1 occurrence in this chapter

Equation form expr-7dc44bba6fae9127

m<im < i

Read as: m is less than i

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: m is less than i

1 occurrence in this chapter

Equation form expr-7f024b2d7f1db4d4

n¯\num{n}

Read as: the numeral for n

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the numeral for n

1 occurrence in this chapter

Equation form expr-80812ec34d267e18

C(M,w,k)⊨E(M,w)!C(M, w, k) \Entails !E(M, w)

Read as: C open parenthesis M comma w comma k close parenthesis semantically entails E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: C open parenthesis M comma w comma k close parenthesis semantically entails E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-80c3541a77d62a0a

C(M,w,n)⊨E(M,w)!C(M, w, n) \Entails !E(M, w)

Read as: C open parenthesis M comma w comma n close parenthesis semantically entails E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: C open parenthesis M comma w comma n close parenthesis semantically entails E open parenthesis M comma w close parenthesis

3 occurrences in this chapter

Equation form expr-8188210924596030

∀x∀y((Qqi(x,y)∧Sσ(x,y))→(Qqj(x,y′)∧Sσ′(x,y′)∧A(x,y)∧B(y′)))& \lforall[x][\lforall[y][( (\Obj Q_{q_i}(x, y) \land \Obj S_{\sigma}(x, y)) \lif {}]] \\ &\qquad (\Obj Q_{q_j}(x, y') \land \Obj S_{\sigma'}(x, y') \land !A(x, y) \land !B(y')))

Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis and formula B open parenthesis y prime close parenthesis close parenthesis close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis and formula B open parenthesis y prime close parenthesis close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-81a36f1ac809b83f

M′′\Struct{M''}

Read as: structure M prime prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M prime prime

2 occurrences in this chapter

Equation form expr-8209a7659542ec35

T′(M,w)⊨k¯<n¯!T'(M,w) \Entails \num{k} < \num{n}

Read as: T prime open parenthesis M comma w close parenthesis semantically entails the numeral for k is less than the numeral for n

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: T prime open parenthesis M comma w close parenthesis semantically entails the numeral for k is less than the numeral for n

1 occurrence in this chapter

Equation form expr-8238c028f61fc0f7

A!A

Read as: formula A

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: formula A

3 occurrences in this chapter

Equation form expr-8254c329a92850f6

kk

Read as: k

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: k

9 occurrences in this chapter

Equation form expr-82ec871b4d33c4af

k−mk-m

Read as: k minus m

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: k minus m

1 occurrence in this chapter

Equation form expr-840e7fd7cd9f5514

M=⟨Q,Σ,q0,δ⟩M = \tuple{Q, \Sigma, q_0, \delta}

Read as: M equals the tuple Q comma capital sigma comma q sub zero comma delta

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: M equals the tuple Q comma capital sigma comma q sub zero comma delta

2 occurrences in this chapter

Equation form expr-8a5757e26e4e8c4a

T(M,w)⊨C(M,w,n)!T(M, w) \Entails !C(M, w, n)

Read as: T open parenthesis M comma w close parenthesis semantically entails C open parenthesis M comma w comma n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis semantically entails C open parenthesis M comma w comma n close parenthesis

5 occurrences in this chapter

Equation form expr-8b72c6bfaa480399

Qq(m¯,n¯)∧Sσ0(0¯,n¯)∧…∧Sσk(k¯,n¯)∧∀x(k¯<x→S0(x,n¯))\Obj Q_q(\num{m}, \num{n}) \land \Obj S_{\sigma_0}(\num{0}, \num{n}) \land \dots \land \Obj S_{\sigma_k}(\num{k}, \num{n}) \land \lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}))]

Read as: object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis and object language symbol S sub sigma sub zero open parenthesis the numeral for zero comma the numeral for n close parenthesis and and so on and object language symbol S sub sigma sub k open parenthesis the numeral for k comma the numeral for n close parenthesis and for every x, open parenthesis the numeral for k is less than x implies object language symbol S sub blank symbol open parenthesis x comma the numeral for n close parenthesis close parenthesis

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis and object language symbol S sub sigma sub zero open parenthesis the numeral for zero comma the numeral for n close parenthesis and and so on and object language symbol S sub sigma sub k open parenthesis the numeral for k comma the numeral for n close parenthesis and for every x, open parenthesis the numeral for k is less than x implies object language symbol S sub blank symbol open parenthesis x comma the numeral for n close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-8c5a7a352285148d

Sσ\Obj S_\sigma

Read as: object language symbol S sub sigma

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol S sub sigma

3 occurrences in this chapter

Equation form expr-8cc1fa30cfe84c12

δ(q0,0)=⟨q0,0,N⟩\delta(q_0,\TMblank) = \tuple{q_0,\TMblank,\TMstay}

Read as: delta open parenthesis q sub zero comma blank symbol close parenthesis equals the tuple q sub zero comma blank symbol comma stay put

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q sub zero comma blank symbol close parenthesis equals the tuple q sub zero comma blank symbol comma stay put

1 occurrence in this chapter

Equation form expr-8dcd00493487a032

l¯′≡l+1¯≡m¯\num{l}' \ident \num{l+1} \ident \num{m}

Read as: the numeral for l prime is syntactically identical to the numeral for l plus one is syntactically identical to the numeral for m

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the numeral for l prime is syntactically identical to the numeral for l plus one is syntactically identical to the numeral for m

1 occurrence in this chapter

Equation form expr-8de0b3c47f112c59

SS

Read as: S

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: S

10 occurrences in this chapter

Equation form expr-8e35c2cd3bf6641b

qq

Read as: q

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: q

9 occurrences in this chapter

Equation form expr-8eaa2441549873ae

n=max(k,len(w))n = \max(k,\len{w})

Read as: n equals maximum open parenthesis k comma the length of w close parenthesis

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: n equals maximum open parenthesis k comma the length of w close parenthesis

1 occurrence in this chapter

Equation form expr-8eac02e600ecb98f

(Z+)*(\PosInt)^*

Read as: open parenthesis positive integers close parenthesis superscript

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: open parenthesis positive integers close parenthesis superscript

2 occurrences in this chapter

Equation form expr-8ec6eaaccf7ca5db

T(M,w)!T(M,w)

Read as: T open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis

6 occurrences in this chapter

Equation form expr-925866ac94568d29

δ(q,σ)=⟨q′,σ′,L⟩\delta(q, \sigma) = \tuple{q', \sigma', \TMleft}

Read as: delta open parenthesis q comma sigma close parenthesis equals the tuple q prime comma sigma prime comma move left

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q comma sigma close parenthesis equals the tuple q prime comma sigma prime comma move left

1 occurrence in this chapter

Equation form expr-935dcc6e0812f3ef

∀x∀y((Qq(x′,y)∧Sσ(x′,y))→(Qq′(x,y′)∧Sσ′(x′,y′)∧A(x,y)))∧∀y((Qqi(0¯,y)∧Sσ(0¯,y))→(Qqj(0¯,y′)∧Sσ′(0¯,y′)∧A(0¯,y)))is a conjunct of T(M,w). If m>0, then let l=m−1 (i.e., m=l+1). The first conjunct of the above !!{sentence} entails the following:(Qq(l¯′,n¯)∧Sσ(l¯′,n¯))→(Qq′(l¯,n¯′)∧Sσ′(l¯′,n¯′)∧A(l¯,n¯))Otherwise, let l=m=0 and consider the following !!{sentence} entailed by the second conjunct:((Qqi(0¯,n¯)∧Sσ(0¯,n¯))→(Qqj(0¯,n¯′)∧Sσ′(0¯,n¯′)∧A(0¯,n¯)))Either sentence impliesQq′(l¯,n¯′)∧Sσ′(m¯,n¯′)∧Sσ0(0¯,n¯′)∧…∧Sσk(k¯,n¯′)∧∀x(k¯<x→S0(x,n¯′))& \lforall[x][\lforall[y][((\Obj Q_{q}(x', y) \land \Obj S_{\sigma}(x', y)) \lif {}]]\\ & \qquad (\Obj Q_{q'}(x, y') \land \Obj S_{\sigma'}(x', y') \land !A(x, y))) \land {}\\ & \lforall[y][((\Obj Q_{q_i}(\num{0}, y) \land \Obj S_{\sigma}(\num{0}, y)) \lif {}]\\ & \qquad (\Obj Q_{q_j}(\num{0}, y') \land \Obj S_{\sigma'}(\num{0}, y') \land !A(\num{0}, y))) \intertext{is a conjunct of $!T(M,w)$. If $m>0$, then let $l = m - 1$ (i.e., $m = l+1$). The first conjunct of the above !!{sentence} entails the following:} & (\Obj Q_{q}(\num{l}', \num{n}) \land \Obj S_{\sigma}(\num{l}', \num{n})) \lif {} \\ & \qquad (\Obj Q_{q'}(\num{l}, \num{n}') \land \Obj S_{\sigma'}(\num{l}', \num{n}') \land !A(\num{l}, \num{n})) \intertext{Otherwise, let $l = m = 0$ and consider the following !!{sentence} entailed by the second conjunct:} & ((\Obj Q_{q_i}(\num{0}, \num{n}) \land \Obj S_{\sigma}(\num{0}, \num{n})) \lif {}\\ & \qquad (\Obj Q_{q_j}(\num{0}, \num{n}') \land \Obj S_{\sigma'}(\num{0}, \num{n}') \land !A(\num{0}, \num{n}))) \intertext{Either sentence implies} & \Obj Q_{q'}(\num{l}, \num{n}') \land \Obj S_{\sigma'}(\num{m}, \num{n}') \land {}\\ &\qquad \Obj S_{\sigma_0}(\num{0}, \num{n}')\land \dots \land \Obj S_{\sigma_k}(\num{k}, \num{n}') \land {} \\ & \qquad \lforall[x][(\num{k} < x \lif \Obj S_\TMblank(x, \num{n}'))]

Read as: Left move induction display. For a positive head position m, let l be m minus one and instantiate the left move transition. The next configuration has state q prime scanning square l, writes sigma prime at square m, preserves every other listed square, and keeps the blank tail. At the leftmost square, use the boundary branch with current state q and successor state q prime, update square zero, and keep the head at square zero

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: Left move induction display. For a positive head position m, let l be m minus one and instantiate the left move transition. The next configuration has state q prime scanning square l, writes sigma prime at square m, preserves every other listed square, and keeps the blank tail. At the leftmost square, use the boundary branch with current state q and successor state q prime, update square zero, and keep the head at square zero

1 occurrence in this chapter

Equation form expr-93a4cd7eba9e5f60

M′\Struct M'

Read as: structure M prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M prime

1 occurrence in this chapter

Equation form expr-944399459793c1e1

T(M,w)⊨C(M,w,k)!T(M, w) \Entails !C(M, w, k)

Read as: T open parenthesis M comma w close parenthesis semantically entails C open parenthesis M comma w comma k close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis semantically entails C open parenthesis M comma w comma k close parenthesis

1 occurrence in this chapter

Equation form expr-9444f16c5f869824

T′(M,w)⊨B(n¯)!T'(M,w) \Entails !B(\num{n})

Read as: T prime open parenthesis M comma w close parenthesis semantically entails formula B open parenthesis the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T prime open parenthesis M comma w close parenthesis semantically entails formula B open parenthesis the numeral for n close parenthesis

1 occurrence in this chapter

Equation form expr-9489f1db06cfd09a

state diagram transition tablefrom statereadwritemovenext statestate onethreethreemove rightstate twostate twotwotwomove rightstate twostate twothreethreemove rightstate one\begin{tikzpicture}[->,>=stealth',shorten >=1pt,auto,node distance=2.8cm, semithick] \tikzstyle{every state}=[fill=none,draw=black,text=black] \node[initial,state] (A) {$1$}; \node[state] (B) [right of=A] {$2$}; \path (A) edge [bend left] node {\TMtrans{3}{3}{\TMright}} (B) (B) edge [loop above] node {\TMtrans{2}{2}{\TMright}} (B) edge [bend left] node {\TMtrans{3}{3}{\TMright}} (A); \end{tikzpicture}

Read as: State diagram. Purpose: Shows the same Even-machine behavior after replacing every state and symbol by a positive-integer code. Initial state: state one. States: state one, state two. Transition one: from state one, when reading three, write three, move right, and enter state two. Transition two: from state two, when reading two, write two, move right, and enter state two. Transition three: from state two, when reading three, write three, move right, and enter state one. Every displayed state has at least one outgoing transition

Means: A complete source-order transition linearization of the displayed state diagram. Read as: State diagram. Purpose: Shows the same Even-machine behavior after replacing every state and symbol by a positive-integer code. Initial state: state one. States: state one, state two. Transition one: from state one, when reading three, write three, move right, and enter state two. Transition two: from state two, when reading two, write two, move right, and enter state two. Transition three: from state two, when reading three, write three, move right, and enter state one. Every displayed state has at least one outgoing transition

1 occurrence in this chapter

Equation form expr-95ce48adb5325c33

∀x∀y((Qqi(x,y)∧Sσ(x,y))→(Qqj(x′,y′)∧Sσ′(x,y′)∧A(x,y)))& \lforall[x][\lforall[y][( (\Obj Q_{q_i}(x, y) \land \Obj S_{\sigma}(x, y)) \lif {}]] \\ &\qquad (\Obj Q_{q_j}(x', y') \land \Obj S_{\sigma'}(x, y') \land !A(x, y)))

Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x prime comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis close parenthesis close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x prime comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-966d35c33339efcc

C(M,w,n)!C(M, w, n)

Read as: C open parenthesis M comma w comma n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: C open parenthesis M comma w comma n close parenthesis

10 occurrences in this chapter

Equation form expr-979799be0c71fb64

Qq\Obj Q_q

Read as: object language symbol Q sub q

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol Q sub q

3 occurrences in this chapter

Equation form expr-9829f2e34e8f0b11

1¯\num{1}

Read as: the numeral for one

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the numeral for one

2 occurrences in this chapter

Equation form expr-9c3245dfb4ac54c1

σ\sigma

Read as: sigma

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: sigma

8 occurrences in this chapter

Equation form expr-9c5f8343c4fbdf71

C(M,w,n+1)!C(M, w, n+1)

Read as: C open parenthesis M comma w comma n plus one close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: C open parenthesis M comma w comma n plus one close parenthesis

3 occurrences in this chapter

Equation form expr-9ce8caa80a7a08e7

isprime(n)={1if n is prime0otherwise.\fn{isprime}(n) = \begin{cases} 1 & \text{if $n$ is prime}\\ 0 & \text{otherwise.} \end{cases}

Read as: the function isprime open parenthesis n close parenthesis equals cases begin; row one: one, if n is prime; row two: zero, otherwise; cases end

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: the function isprime open parenthesis n close parenthesis equals cases begin; row one: one, if n is prime; row two: zero, otherwise; cases end

1 occurrence in this chapter

Equation form expr-9d7103ac3526e8f6

m∈ℕm \in \Nat

Read as: m is in the natural numbers

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: m is in the natural numbers

1 occurrence in this chapter

Equation form expr-9f239d9ffb93e040

C(M,w,k)!C(M, w, k)

Read as: C open parenthesis M comma w comma k close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: C open parenthesis M comma w comma k close parenthesis

1 occurrence in this chapter

Equation form expr-a1fce4363854ff88

yy

Read as: y

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: y

4 occurrences in this chapter

Equation form expr-a25513c7e0f6eaa8

UU

Read as: U

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: U

14 occurrences in this chapter

Equation form expr-a319dec864e138a4

E(M,w)!E(M,w)

Read as: E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-a38ee6a67de22a3d

0\TMblank

Read as: blank symbol

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: blank symbol

8 occurrences in this chapter

Equation form expr-a4131995fca6d942

C(M,w,0)!C(M, w, 0)

Read as: C open parenthesis M comma w comma zero close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: C open parenthesis M comma w comma zero close parenthesis

1 occurrence in this chapter

Equation form expr-a5183e47a3207b2d

▷\TMendtape

Read as: left end marker

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: left end marker

5 occurrences in this chapter

Equation form expr-a603e6b6eedcb75f

MeM_e

Read as: M sub e

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: M sub e

31 occurrences in this chapter

Equation form expr-a66a0125fa15d041

σi1\sigma_{i_1}

Read as: sigma sub i sub one

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: sigma sub i sub one

1 occurrence in this chapter

Equation form expr-a6a377206f1cbcda

σ∈Σ\sigma\in \Sigma

Read as: sigma is in capital sigma

Means: Notation for a machine prime s state set, tape alphabet, or defining tuple. Read as: sigma is in capital sigma

1 occurrence in this chapter

Equation form expr-a7d5ad94a88ead6f

T(M,Λ)!T(M,\emptyseq)

Read as: T open parenthesis M comma the empty sequence code close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma the empty sequence code close parenthesis

1 occurrence in this chapter

Equation form expr-a899c3d06d4c0108

m=km = k

Read as: m equals k

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: m equals k

1 occurrence in this chapter

Equation form expr-a9799a71a6e8dcf7

{0,…,n}\{0, \dots, n\}

Read as: the set of integers from zero through n

Means: An explicit finite-set expression or equation that preserves the source braces as set enclosure. Read as: the set of integers from zero through n.

1 occurrence in this chapter

Equation form expr-a98ad2620c44dff1

Q×Σ×{L,R,N}Q \times \Sigma \times \{\TMleft, \TMright, \TMstay\}

Read as: Q Cartesian product capital sigma Cartesian product the set containing move left, move right, and stay put

Means: An explicit finite-set expression or equation that preserves the source braces as set enclosure. Read as: Q Cartesian product capital sigma Cartesian product the set containing move left, move right, and stay put.

1 occurrence in this chapter

Equation form expr-a9f51566bd6705f7

EE

Read as: E

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: E

6 occurrences in this chapter

Equation form expr-aa00709c3156cb92

∀x∀y∀z((x<y∧y<z)→x<z)\lforall[x][\lforall[y][\lforall[z][ ((x < y \land y < z) \lif x < z)]]]

Read as: for every x, for every y, for every z, open parenthesis open parenthesis x is less than y and y is less than z close parenthesis implies x is less than z close parenthesis

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: for every x, for every y, for every z, open parenthesis open parenthesis x is less than y and y is less than z close parenthesis implies x is less than z close parenthesis

2 occurrences in this chapter

Equation form expr-aaa9402664f1a41f

hh

Read as: h

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: h

10 occurrences in this chapter

Equation form expr-aabd5928c1d46b56

⟨q,σ,q′,σ′,d⟩\tuple{q, \sigma, q', \sigma', d}

Read as: the tuple q comma sigma comma q prime comma sigma prime comma d

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the tuple q comma sigma comma q prime comma sigma prime comma d

1 occurrence in this chapter

Equation form expr-aafda2cc5bdbea48

|M|=ℕ\Domain{M} = \Nat

Read as: the domain of structure M equals the natural numbers

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: the domain of structure M equals the natural numbers

1 occurrence in this chapter

Equation form expr-ad586e655c22273c

Qq0(1¯,0¯)\Obj Q_{q_0}(\num{1}, \num{0})

Read as: object language symbol Q sub q sub zero open parenthesis the numeral for one comma the numeral for zero close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol Q sub q sub zero open parenthesis the numeral for one comma the numeral for zero close parenthesis

1 occurrence in this chapter

Equation form expr-ae144eabc9f6e0b9

∀x∀y((Qqi(x,y)∧Sσ(x,y))→(Qqj(x′,y′)∧Sσ′(x,y′)∧A(x,y)∧B(y′)))& \lforall[x][\lforall[y][( (\Obj Q_{q_i}(x, y) \land \Obj S_{\sigma}(x, y)) \lif {}]] \\ &\qquad (\Obj Q_{q_j}(x', y') \land \Obj S_{\sigma'}(x, y') \land !A(x, y) \land !B(y')))

Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x prime comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis and formula B open parenthesis y prime close parenthesis close parenthesis close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x prime comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis and formula B open parenthesis y prime close parenthesis close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-b149f5c3c1e66912

T′(M,w)∧E(M,w)!T'(M,w) \land !E(M, w)

Read as: T prime open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T prime open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-b25388f04f22fb42

B(y)≡∀x(x<y→x≠y).!B(y) \ident \lforall[x][(x < y \lif \eq/[x][y])].

Read as: formula B open parenthesis y close parenthesis is syntactically identical to for every x, open parenthesis x is less than y implies x is not equal to y close parenthesis

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: formula B open parenthesis y close parenthesis is syntactically identical to for every x, open parenthesis x is less than y implies x is not equal to y close parenthesis

1 occurrence in this chapter

Equation form expr-b289b630c4ba9cc1

Qq(m¯,n¯)\Obj Q_{q}(\num{m}, \num{n})

Read as: object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis

1 occurrence in this chapter

Equation form expr-b2f2f3e1a76b3f91

M′⊨E(M,w)\Sat{M'}{!E(M,w)}

Read as: structure M prime satisfies E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M prime satisfies E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-b478ee213c6e39e6

n∈|M|=ℕn \in \Domain{M} = \Nat

Read as: n is in the domain of structure M equals the natural numbers

Means: A function type, value, or arithmetic relationship in the machine-computation convention. Read as: n is in the domain of structure M equals the natural numbers

1 occurrence in this chapter

Equation form expr-b488c0a338905f78

δ(q,σ)\delta(q,\sigma)

Read as: delta open parenthesis q comma sigma close parenthesis

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q comma sigma close parenthesis

1 occurrence in this chapter

Equation form expr-b5a2f52020d7aa61

T(M,w)!T(M, w)

Read as: T open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis

8 occurrences in this chapter

Equation form expr-b620f7fd0a05aeb7

0¯\num{0}

Read as: the numeral for zero

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the numeral for zero

2 occurrences in this chapter

Equation form expr-b659571f18ce34b0

|M′|={0,…,n},′M′(x)={x+1if x<nnotherwise,⟨x,y⟩∈<M′iff x<y or x=y=n,\Domain{M'} & = \{0, \dots, n\},\\ \Assign{\prime}{M'}(x) & = \begin{cases} x + 1 &\text{if $x < n$}\\ n &\text{otherwise,} \end{cases} \\ \tuple{x,y} \in \Assign{<}{M'} &\text{iff $x < y$ or $x = y = n$,}

Read as: the domain of structure M prime equals the set of integers from zero through n; next row, the interpretation of the successor symbol in structure M prime at x equals x plus one if x is less than n, and equals n otherwise; next row, the tuple x comma y belongs to the interpretation of the less-than relation in structure M prime if and only if x is less than y or x equals y equals n

Means: An explicit finite-set expression or equation that preserves the source braces as set enclosure. Read as: the domain of structure M prime equals the set of integers from zero through n; next row, the interpretation of the successor symbol in structure M prime at x equals x plus one if x is less than n, and equals n otherwise; next row, the tuple x comma y belongs to the interpretation of the less-than relation in structure M prime if and only if x is less than y or x equals y equals n.

1 occurrence in this chapter

Equation form expr-b6992d9da8d7da0a

δ(q,σ)=⟨q′,σ′,R⟩\delta(q, \sigma) = \tuple{q', \sigma', \TMright}

Read as: delta open parenthesis q comma sigma close parenthesis equals the tuple q prime comma sigma prime comma move right

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q comma sigma close parenthesis equals the tuple q prime comma sigma prime comma move right

1 occurrence in this chapter

Equation form expr-b85c44ecbea9a6b2

⟨q,σ⟩\tuple{q, \sigma}

Read as: the tuple q comma sigma

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the tuple q comma sigma

1 occurrence in this chapter

Equation form expr-b8a1bf1bab77ec11

σ′\sigma'

Read as: sigma prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: sigma prime

2 occurrences in this chapter

Equation form expr-b8b3491680dfd11b

A(m¯,n¯)!A(\num{m},\num{n})

Read as: formula A open parenthesis the numeral for m comma the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: formula A open parenthesis the numeral for m comma the numeral for n close parenthesis

1 occurrence in this chapter

Equation form expr-b8bbb3a7ebd17a45

q0q_0

Read as: q sub zero

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: q sub zero

5 occurrences in this chapter

Equation form expr-ba728bc2b688ea05

T(M,w)⊨m¯<k¯!T(M, w) \Entails \num{m} < \num{k}

Read as: T open parenthesis M comma w close parenthesis semantically entails the numeral for m is less than the numeral for k

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: T open parenthesis M comma w close parenthesis semantically entails the numeral for m is less than the numeral for k

1 occurrence in this chapter

Equation form expr-bf62a4e0cf8ea080

T′(M,w)!T'(M, w)

Read as: T prime open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T prime open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-bf9d04b95cd9408e

δ(qi,σ)=⟨qj,σ′,L⟩\delta(q_i, \sigma) = \tuple{q_j, \sigma', \TMleft}

Read as: delta open parenthesis q sub i comma sigma close parenthesis equals the tuple q sub j comma sigma prime comma move left

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q sub i comma sigma close parenthesis equals the tuple q sub j comma sigma prime comma move left

2 occurrences in this chapter

Equation form expr-c3c3a8fe03c53fac

M⊨∃x∃y(⋁⟨q,σ⟩∈X(Qq(x,y)∧Sσ(x,y))).\Sat{M}{\lexists[x][\lexists[y][(\bigvee_{\tuple{q, \sigma} \in X}(\Obj Q_q(x, y) \land \Obj S_\sigma(x, y)))]]}.

Read as: structure M satisfies there exists x, there exists y, open parenthesis the disjunction over sub the tuple q comma sigma is in X open parenthesis object language symbol Q sub q open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis close parenthesis

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: structure M satisfies there exists x, there exists y, open parenthesis the disjunction over sub the tuple q comma sigma is in X open parenthesis object language symbol Q sub q open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-c4e3858981cba4b9

M⊨T(M,w)\Sat{M}{!T(M, w)}

Read as: structure M satisfies T open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M satisfies T open parenthesis M comma w close parenthesis

2 occurrences in this chapter

Equation form expr-c6173ad7add4e2cd

⟨q,σ⟩\tuple{q,\sigma}

Read as: the tuple q comma sigma

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the tuple q comma sigma

1 occurrence in this chapter

Equation form expr-c63c8e0f289a448b

0≤n0 \le n

Read as: zero is less than or equal to n

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: zero is less than or equal to n

1 occurrence in this chapter

Equation form expr-c87721b01028b385

⊢B\Proves !B

Read as: proves formula B

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: proves formula B

4 occurrences in this chapter

Equation form expr-c8cffb66d974193d

δ(qi,σ)=⟨qj,σ′,R⟩\delta(q_i, \sigma) = \tuple{q_j, \sigma', \TMright}

Read as: delta open parenthesis q sub i comma sigma close parenthesis equals the tuple q sub j comma sigma prime comma move right

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q sub i comma sigma close parenthesis equals the tuple q sub j comma sigma prime comma move right

2 occurrences in this chapter

Equation form expr-cc097011c9aac4f0

q∈Qq \in Q

Read as: q is in Q

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: q is in Q

1 occurrence in this chapter

Equation form expr-cc35f5d773d01eaa

M⊨Qq(m¯,n¯)∧Sσ(m¯,n¯)\Sat{M}{\Obj Q_q(\num{m}, \num{n}) \land \Obj S_\sigma(\num{m}, \num{n})}

Read as: structure M satisfies object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis and object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M satisfies object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis and object language symbol S sub sigma open parenthesis the numeral for m comma the numeral for n close parenthesis

1 occurrence in this chapter

Equation form expr-ce1dea246c115488

A(x,y)!A(x, y)

Read as: formula A open parenthesis x comma y close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: formula A open parenthesis x comma y close parenthesis

2 occurrences in this chapter

Equation form expr-cef3e6639fe132be

M′\Struct{M'}

Read as: structure M prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M prime

4 occurrences in this chapter

Equation form expr-d0331456e52105eb

σ0\sigma_0

Read as: sigma sub zero

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: sigma sub zero

1 occurrence in this chapter

Equation form expr-d04ff80d9f6dc462

→\lif

Read as: implies

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: implies

1 occurrence in this chapter

Equation form expr-d055ee4dbcdd0c8b

B!B

Read as: formula B

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: formula B

9 occurrences in this chapter

Equation form expr-d203ba01eef4198c

δ\delta

Read as: delta

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta

2 occurrences in this chapter

Equation form expr-d255dc2863f32834

T′(M,w)∧E(M,w)!T'(M,w) \land !E(M,w)

Read as: T prime open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T prime open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

4 occurrences in this chapter

Equation form expr-d438a18a7da07bf0

x<yx < y

Read as: x is less than y

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: x is less than y

1 occurrence in this chapter

Equation form expr-d44275070c17fe89

|M′|\Domain{M'}

Read as: the domain of structure M prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: the domain of structure M prime

1 occurrence in this chapter

Equation form expr-d4735e3a265e16ee

22

Read as: two

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: two

7 occurrences in this chapter

Equation form expr-d56a2b36a6f91eac

δ(q,σ)=⟨q′,σ′,N⟩\delta(q, \sigma) = \tuple{q', \sigma', \TMstay}

Read as: delta open parenthesis q comma sigma close parenthesis equals the tuple q prime comma sigma prime comma stay put

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q comma sigma close parenthesis equals the tuple q prime comma sigma prime comma stay put

1 occurrence in this chapter

Equation form expr-d65d75b1e6562713

Σ\Sigma

Read as: capital sigma

Means: Notation for a machine prime s state set, tape alphabet, or defining tuple. Read as: capital sigma

1 occurrence in this chapter

Equation form expr-d69bb21f4e049d45

Σ={▷,0,1}\Sigma = \{\TMendtape,\TMblank,\TMstroke\}

Read as: capital sigma equals the set containing the left end marker, the blank symbol, and the stroke symbol

Means: An explicit finite-set expression or equation that preserves the source braces as set enclosure. Read as: capital sigma equals the set containing the left end marker, the blank symbol, and the stroke symbol.

1 occurrence in this chapter

Equation form expr-d8bd60c450507199

{0,1}\{0, 1\}

Read as: the set containing zero and one

Means: An explicit finite-set expression or equation that preserves the source braces as set enclosure. Read as: the set containing zero and one.

1 occurrence in this chapter

Equation form expr-da29c2da3a1713b4

2,1,2⏟Q,3,1,2,3⏞Σ,1,1,3,2,3,2⏟δ(1,3)=⟨2,3,R⟩,2,2,2,2,2⏞δ(2,2)=⟨2,2,R⟩,2,3,1,3,2⏟δ(2,3)=⟨1,3,R⟩.2, \underbrace{1, 2}_Q, 3, \overbrace{1, 2, 3}^\Sigma, 1, \underbrace{1, 3, 2, 3, 2}_{\delta(1,3) = \tuple{2,3,R}}, \overbrace{2, 2, 2, 2, 2}^{\delta(2,2) = \tuple{2,2,R}}, \underbrace{2, 3, 1, 3, 2}_{\delta(2,3) = \tuple{1,3,R}}.

Read as: two comma underbraced group one comma two sub Q comma three comma overbraced group one comma two comma three superscript capital sigma comma one comma underbraced group one comma three comma two comma three comma two sub delta open parenthesis one comma three close parenthesis equals the tuple two comma three comma move right comma overbraced group two comma two comma two comma two comma two superscript delta open parenthesis two comma two close parenthesis equals the tuple two comma two comma move right comma underbraced group two comma three comma one comma three comma two sub delta open parenthesis two comma three close parenthesis equals the tuple one comma three comma move right

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: two comma underbraced group one comma two sub Q comma three comma overbraced group one comma two comma three superscript capital sigma comma one comma underbraced group one comma three comma two comma three comma two sub delta open parenthesis one comma three close parenthesis equals the tuple two comma three comma move right comma overbraced group two comma two comma two comma two comma two superscript delta open parenthesis two comma two close parenthesis equals the tuple two comma two comma move right comma underbraced group two comma three comma one comma three comma two sub delta open parenthesis two comma three close parenthesis equals the tuple one comma three comma move right

1 occurrence in this chapter

Equation form expr-dabd3aff769f07eb

<<

Read as: is less than

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: is less than

9 occurrences in this chapter

Equation form expr-dac6ae08516007c6

s(e)={0if machine~Me does not halt for input e1if machine~Me halts for input es(e) = \begin{cases} \text{0} & \text{if machine~$M_e$ does not halt for input $e$} \\ \text{1} & \text{if machine~$M_e$ halts for input $e$} \end{cases}

Read as: s open parenthesis e close parenthesis equals cases begin; row one: zero, if machine M sub e does not halt for input e; row two: one, if machine M sub e halts for input e; cases end

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: s open parenthesis e close parenthesis equals cases begin; row one: zero, if machine M sub e does not halt for input e; row two: one, if machine M sub e halts for input e; cases end

1 occurrence in this chapter

Equation form expr-dc65a11ec486d432

σik\sigma_{i_k}

Read as: sigma sub i sub k

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: sigma sub i sub k

1 occurrence in this chapter

Equation form expr-dcdf5d4364f5256f

∀x∀y((Qqi(x,y)∧Sσ(x,y))→(Qqj(x,y′)∧Sσ′(x,y′)∧A(x,y)))& \lforall[x][\lforall[y][( (\Obj Q_{q_i}(x, y) \land \Obj S_{\sigma}(x, y)) \lif {}]] \\ &\qquad (\Obj Q_{q_j}(x, y') \land \Obj S_{\sigma'}(x, y') \land !A(x, y)))

Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis close parenthesis close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: for every x, for every y, open parenthesis open parenthesis object language symbol Q sub q sub i open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis implies next row then open parenthesis object language symbol Q sub q sub j open parenthesis x comma y prime close parenthesis and object language symbol S sub sigma prime open parenthesis x comma y prime close parenthesis and formula A open parenthesis x comma y close parenthesis close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-de7d1b721a1e0632

ii

Read as: i

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: i

1 occurrence in this chapter

Equation form expr-de8d9dcecaa89d17

S0(k¯′,n¯′)\Obj S_\TMblank(\num{k}',\num{n}')

Read as: object language symbol S sub blank symbol open parenthesis the numeral for k prime comma the numeral for n prime close parenthesis

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: object language symbol S sub blank symbol open parenthesis the numeral for k prime comma the numeral for n prime close parenthesis

2 occurrences in this chapter

Equation form expr-df701b27f24bbe71

M1M_1

Read as: M sub one

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: M sub one

1 occurrence in this chapter

Equation form expr-df7e70e5021544f4

B!B

Read as: formula B

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: formula B

1 occurrence in this chapter

Equation form expr-e3212229d200318d

¬B\lnot !B

Read as: not formula B

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: not formula B

5 occurrences in this chapter

Equation form expr-e632b7095b0bf32c

MM

Read as: M

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: M

1 occurrence in this chapter

Equation form expr-e6397ea8ead57cc7

0′′\Obj 0''

Read as: object language symbol zero prime prime

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol zero prime prime

1 occurrence in this chapter

Equation form expr-e650efe94b9a644f

δ(q0,▷)\delta(q_0, \TMendtape)

Read as: delta open parenthesis q sub zero comma left end marker close parenthesis

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q sub zero comma left end marker close parenthesis

1 occurrence in this chapter

Equation form expr-e7069b2e65a14ee6

Qq(m¯,n¯)\Obj Q_q(\num{m}, \num{n})

Read as: object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: object language symbol Q sub q open parenthesis the numeral for m comma the numeral for n close parenthesis

1 occurrence in this chapter

Equation form expr-e91d1317545e8c52

δ(q,σ)=⟨q′,σ′,D⟩\delta(q,\sigma) = \tuple{q', \sigma', D}

Read as: delta open parenthesis q comma sigma close parenthesis equals the tuple q prime comma sigma prime comma D

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q comma sigma close parenthesis equals the tuple q prime comma sigma prime comma D

1 occurrence in this chapter

Equation form expr-e945b5ddcecdc573

M2M_2

Read as: M sub two

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: M sub two

1 occurrence in this chapter

Equation form expr-e97689f41bba7a42

k¯<k¯′→S0(k¯′,n¯′)\num{k} < \num{k}' \lif \Obj S_\TMblank(\num{k}', \num{n}')

Read as: the numeral for k is less than the numeral for k prime implies object language symbol S sub blank symbol open parenthesis the numeral for k prime comma the numeral for n prime close parenthesis

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: the numeral for k is less than the numeral for k prime implies object language symbol S sub blank symbol open parenthesis the numeral for k prime comma the numeral for n prime close parenthesis

1 occurrence in this chapter

Equation form expr-eaa0e5d621cfcafd

⟨q,σ⟩∈X\tuple{q,\sigma} \in X

Read as: the tuple q comma sigma is in X

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: the tuple q comma sigma is in X

1 occurrence in this chapter

Equation form expr-ecfc6d63a3b68fb8

qjq_j

Read as: q sub j

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: q sub j

2 occurrences in this chapter

Equation form expr-ecfd3d94a98fb3e6

′M′′(0)=′M′′(1)=1\Assign{\prime}{M''}(0) = \Assign{\prime}{M''}(1) = 1

Read as: the interpretation of successor symbol in structure M prime prime open parenthesis zero close parenthesis equals the interpretation of successor symbol in structure M prime prime open parenthesis one close parenthesis equals one

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: the interpretation of successor symbol in structure M prime prime open parenthesis zero close parenthesis equals the interpretation of successor symbol in structure M prime prime open parenthesis one close parenthesis equals one

1 occurrence in this chapter

Equation form expr-ef2d127de37b942b

55

Read as: five

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: five

1 occurrence in this chapter

Equation form expr-ef8e079789f4bc01

⊨B\Entails !B

Read as: semantically entails formula B

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: semantically entails formula B

2 occurrences in this chapter

Equation form expr-f0f1f1a55365abbb

LM\Lang L_M

Read as: language move left sub M

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: language move left sub M

3 occurrences in this chapter

Equation form expr-f28fb26c476b73cd

T(M,w)⊨E(M,w)!T(M, w) \Entails !E(M, w)

Read as: T open parenthesis M comma w close parenthesis semantically entails E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis semantically entails E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-f39a4e236961a8b8

M′⊨T′(M,w)∧E(M,w)\Sat{M'}{!T'(M,w) \land !E(M,w)}

Read as: structure M prime satisfies T prime open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: structure M prime satisfies T prime open parenthesis M comma w close parenthesis and E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-f3e9982f3f4752a1

T(M,w)→E(M,w)!T(M,w) \lif !E(M,w)

Read as: T open parenthesis M comma w close parenthesis implies E open parenthesis M comma w close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: T open parenthesis M comma w close parenthesis implies E open parenthesis M comma w close parenthesis

1 occurrence in this chapter

Equation form expr-f54dd73a92f0a948

{q0,q1}\{q_0,q_1\}

Read as: the set containing q sub zero and q sub one

Means: An explicit finite-set expression or equation that preserves the source braces as set enclosure. Read as: the set containing q sub zero and q sub one.

1 occurrence in this chapter

Equation form expr-f5e609de0e757cd3

δ(q0,0)=⟨q0,0,N⟩\delta(q_0,\TMblank) = \tuple{q_0,\TMblank,\TMstay}

Read as: delta open parenthesis q sub zero comma blank symbol close parenthesis equals the tuple q sub zero comma blank symbol comma stay put

Means: Transition notation specifying a current state and symbol or the resulting state, written symbol, and head movement. Read as: delta open parenthesis q sub zero comma blank symbol close parenthesis equals the tuple q sub zero comma blank symbol comma stay put

1 occurrence in this chapter

Equation form expr-f67ab10ad4e4c531

FF

Read as: F

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: F

3 occurrences in this chapter

Equation form expr-f83a7cd34f377dcc

Qq0(1¯,n¯)∧S▷(0¯,n¯)∧∀x(0¯<x→S0(x,n¯))\quad for all n∈ℕ∃y(Qq0(0¯,y)∧S▷(0¯,y))& \Obj Q_{q_0}(\num{1}, \num{n}) \land \Obj S_{\TMendtape}(\num{0}, \num{n}) \land \lforall[x][(\num{0} < x \lif \Obj S_\TMblank(x, \num{n}))] \text{\quad for all $n \in \Nat$}\\ & \lexists[y][(\Obj Q_{q_0}(\num{0}, y) \land \Obj S_{\TMendtape}(\num{0}, y))]

Read as: object language symbol Q sub q sub zero open parenthesis the numeral for one comma the numeral for n close parenthesis and object language symbol S sub left end marker open parenthesis the numeral for zero comma the numeral for n close parenthesis and for every x, open parenthesis the numeral for zero is less than x implies object language symbol S sub blank symbol open parenthesis x comma the numeral for n close parenthesis close parenthesis quad for all n is in the natural numbers next row then there exists y, open parenthesis object language symbol Q sub q sub zero open parenthesis the numeral for zero comma y close parenthesis and object language symbol S sub left end marker open parenthesis the numeral for zero comma y close parenthesis close parenthesis

Means: Notation for tape symbols, concatenated strings, or unary blocks. Read as: object language symbol Q sub q sub zero open parenthesis the numeral for one comma the numeral for n close parenthesis and object language symbol S sub left end marker open parenthesis the numeral for zero comma the numeral for n close parenthesis and for every x, open parenthesis the numeral for zero is less than x implies object language symbol S sub blank symbol open parenthesis x comma the numeral for n close parenthesis close parenthesis quad for all n is in the natural numbers next row then there exists y, open parenthesis object language symbol Q sub q sub zero open parenthesis the numeral for zero comma y close parenthesis and object language symbol S sub left end marker open parenthesis the numeral for zero comma y close parenthesis close parenthesis

1 occurrence in this chapter

Equation form expr-f99ac7f5770eacfd

∃x∃y(⋁⟨q,σ⟩∈X(Qq(x,y)∧Sσ(x,y)))\lexists[x][\lexists[y][(\bigvee_{\tuple{q, \sigma} \in X}(\Obj Q_q(x, y) \land \Obj S_\sigma(x, y)))]]

Read as: there exists x, there exists y, open parenthesis the disjunction over sub the tuple q comma sigma is in X open parenthesis object language symbol Q sub q open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis close parenthesis

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: there exists x, there exists y, open parenthesis the disjunction over sub the tuple q comma sigma is in X open parenthesis object language symbol Q sub q open parenthesis x comma y close parenthesis and object language symbol S sub sigma open parenthesis x comma y close parenthesis close parenthesis close parenthesis

2 occurrences in this chapter

Equation form expr-f9a46065d2825cb5

s(e)=1s(e) = 1

Read as: s open parenthesis e close parenthesis equals one

Means: An equation, comparison, or membership claim fixed by the surrounding source sentence. Read as: s open parenthesis e close parenthesis equals one

1 occurrence in this chapter

Equation form expr-f9d5192eee9a80ca

L\TMleft

Read as: move left

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: move left

1 occurrence in this chapter

Equation form expr-fa02e26ac15b5f1d

M3M_3

Read as: M sub three

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: M sub three

1 occurrence in this chapter

Equation form expr-ff72e4f9ab549d6a

A(m¯,n¯)!A(\num{m}, \num{n})

Read as: formula A open parenthesis the numeral for m comma the numeral for n close parenthesis

Means: A Turing-machine variable or term whose role is fixed by its exact source context. Read as: formula A open parenthesis the numeral for m comma the numeral for n close parenthesis

2 occurrences in this chapter

Undecidability figure

Figure containing two behaviorally equivalent Even-machine diagrams with renamed states and tape symbols.

Source

Turing machine state diagram

First Even-machine variant, using states q zero and q one with stroke and blank tape symbols. State diagram. Purpose: Shows the Even-machine transition pattern before renaming, with initial state q zero and state q one. Initial state: state q sub zero. States: state q sub zero, state q sub one. Transition one: from state q sub zero, when reading stroke symbol, write stroke symbol, move right, and enter state q sub one. Transition two: from state q sub one, when reading blank symbol, write blank symbol, move right, and enter state q sub one. Transition three: from state q sub one, when reading stroke symbol, write stroke symbol, move right, and enter state q sub zero. Every displayed state has at least one outgoing transition

Source

Turing machine state diagram

Second Even-machine variant, using states s and h and capital A in place of the stroke symbol. State diagram. Purpose: Shows the same transition pattern after renaming the states and stroke symbol. Initial state: state s. States: state s, state h. Transition one: from state s, when reading capital A symbol, write capital A symbol, move right, and enter state h. Transition two: from state h, when reading blank symbol, write blank symbol, move right, and enter state h. Transition three: from state h, when reading capital A symbol, write capital A symbol, move right, and enter state s. Every displayed state has at least one outgoing transition

Source

Undecidability figure

Figure containing the standardized positive-integer encoding of the Even machine.

Source

Turing machine state diagram

Standard Even-machine diagram with states one and two and encoded tape symbols two and three. State diagram. Purpose: Shows the same Even-machine behavior after replacing every state and symbol by a positive-integer code. Initial state: state one. States: state one, state two. Transition one: from state one, when reading three, write three, move right, and enter state two. Transition two: from state two, when reading two, write two, move right, and enter state two. Transition three: from state two, when reading three, write three, move right, and enter state one. Every displayed state has at least one outgoing transition

Source

Undecidability theorem

States that some functions from the natural numbers to the natural numbers are not Turing computable.

Source

Unsolved undecidability exercise

Unsolved exercise asking for a different finite description convention for standard machines and a simulation justification. The exercise is preserved as a task and intentionally remains unsolved.

Source

Undecidability definition

Defines an index of a Turing machine in the fixed enumeration and introduces M sub e.

Source

Undecidability theorem

States the universal-machine simulation theorem and the associated partial function of a machine index and input.

Source

Undecidability definition

Defines the total halting function h on a machine index and input.

Source

Undecidability definition

Defines the Halting Problem as deciding whether indexed machine M sub e halts on unary input n.

Source

Undecidability definition

Defines the diagonal halting function s by running indexed machine M sub e on its own index.

Source

Undecidability lemma

States that the diagonal halting function s is not Turing computable.

Source

Undecidability theorem

States the unsolvability of the Halting Problem and noncomputability of h.

Source

Unsolved undecidability exercise

Unsolved exercise asking for a proof that deciding halting on the fixed unary input three is impossible. The exercise is preserved as a task and intentionally remains unsolved.

Source

Unsolved undecidability exercise

Unsolved exercise asking to reduce diagonal cases to off-diagonal halting cases. The exercise is preserved as a task and intentionally remains unsolved.

Source

Unsolved undecidability exercise

Unsolved exercise asking whether taking machine descriptions rather than indices changes halting undecidability. The exercise is preserved as a task and intentionally remains unsolved.

Source

Unsolved undecidability exercise

Unsolved exercise asking why the partial self-halting indicator is Turing computable. The exercise is preserved as a task and intentionally remains unsolved.

Source

Undecidability displayed formal object

Recursive definition of the numeral for zero and the successor numeral for n plus one.

Source

Undecidability definition

Defines the first-order language L sub M used to represent states, tape symbols, numerals, successor, and order.

Source

Undecidability displayed formal object

Universal transition sentence for a machine instruction that moves the head right.

Source

Undecidability displayed formal object

Two-part universal transition sentence for a left move, including the left-end boundary case.

Source

Undecidability displayed formal object

Universal transition sentence for an instruction that leaves the head in place.

Source

Undecidability proposition

States that the representation sentences entail numeral m is below numeral k whenever m is below k.

Source

Unsolved undecidability exercise

Unsolved exercise asking for a proof of the numeral-order proposition by induction. The exercise is preserved as a task and intentionally remains unsolved.

Source

Undecidability definition

Defines sentence C of M, w, and n describing the complete machine configuration after n steps.

Source

Undecidability lemma

States that a represented halting configuration entails sentence E expressing eventual halting.

Source

Undecidability lemma

States that T of M and w entails the correct configuration sentence at every nonhalting stage.

Source

Undecidability displayed formal object

Inductive right-move case deriving the next represented configuration from the current one.

Source

Undecidability displayed formal object

Inductive left-move case, including the special behavior at the leftmost tape square.

Source

Unsolved undecidability exercise

Unsolved exercise asking to complete the stay-put case of the configuration induction. The exercise is preserved as a task and intentionally remains unsolved.

Source

Unsolved undecidability exercise

Unsolved exercise asking for a derivation that unchanged non-scanned squares retain their tape symbols. The exercise is preserved as a task and intentionally remains unsolved.

Source

Unsolved undecidability exercise

Unsolved exercise asking for a derivation of the shifted blank-tail condition. The exercise is preserved as a task and intentionally remains unsolved.

Source

Undecidability lemma

States that if M halts on w, the implication from T of M and w to E of M and w is valid.

Source

Undecidability lemma

States the converse: validity of the representing implication entails that M halts on w.

Source

Undecidability displayed formal object

Defines the state and tape-symbol predicate interpretations in the structure built from an actual run.

Source

Undecidability theorem

States that no Turing machine decides validity of every first-order sentence.

Source

Undecidability corollary

States that satisfiability of arbitrary first-order sentences is undecidable.

Source

Undecidability theorem

States that first-order validity is semidecidable by enumerating derivations.

Source

Unsolved undecidability exercise

Unsolved exercise asking for a finite structure that makes the looping-machine representation and halting sentence true. The exercise is preserved as a task and intentionally remains unsolved.

Source

Undecidability displayed formal object

Two conditions the finite countermodel exercise asks the reader to make true.

Source

Undecidability displayed formal object

Modified right-move transition sentence with the freshness condition B of y prime.

Source

Undecidability displayed formal object

Modified left-move transition sentence with ordinary and left-boundary branches.

Source

Undecidability displayed formal object

Modified stay-put transition sentence with the freshness condition B of y prime.

Source

Undecidability lemma

States that a halting computation yields a finite model of T prime conjoined with E.

Source

Undecidability displayed formal object

Defines the finite run structure domain, capped successor, and modified order relation.

Source

Unsolved undecidability exercise

Unsolved exercise asking to verify the finite model in the forward Trakhtenbrot lemma. The exercise is preserved as a task and intentionally remains unsolved.

Source

Undecidability lemma

States that a finite model of T prime conjoined with E entails the represented machine halts.

Source

Unsolved undecidability exercise

Unsolved exercise asking to derive the freshness sentence B at each nonhalting step. The exercise is preserved as a task and intentionally remains unsolved.

Source

Undecidability theorem

States Trakhtenbrot's theorem: finite satisfiability of first-order sentences is undecidable.

Source

Undecidability corollary

States that no derivation system is both sound and complete for validity over finite structures.

Source

Unsolved undecidability exercise

Unsolved exercise asking for the corollary from semidecidability and the finite-satisfiability reduction. The exercise is preserved as a task and intentionally remains unsolved.

Source

Cross-reference reference-000619

link to figure Variants of the Even machine

Source occurrence

Cross-reference reference-000620

link to figure A standard Even machine

Source occurrence

Cross-reference reference-000621

link to exercise on enumerating finite sequences of positive integers

Source occurrence

Cross-reference reference-000622

link to exercise showing functions from natural numbers to natural numbers are nonenumerable

Source occurrence

Cross-reference reference-000623

link to section Enumerating Turing Machines

Source occurrence

Cross-reference reference-000624

link to the universal-machine simulation step that finds a matching instruction

Source occurrence

Cross-reference reference-000625

link to section Disciplined Machines

Source occurrence

Cross-reference reference-000626

link to section Combining Machines

Source occurrence

Cross-reference reference-000627

link to exercise asking for a disciplined copier machine

Source occurrence

Cross-reference reference-000628

link to section Enumerating Turing Machines

Source occurrence

Cross-reference reference-000629

link to proposition that represented numerals preserve strict order

Source occurrence

Cross-reference reference-000630

link to right-move case in the configuration induction

Source occurrence

Cross-reference reference-000631

link to definition of the first-order machine-description language

Source occurrence

Cross-reference reference-000632

link to right-move representation sentence

Source occurrence

Cross-reference reference-000633

link to proposition that represented numerals preserve strict order

Source occurrence

Cross-reference reference-000634

link to left-move case in the configuration induction

Source occurrence

Cross-reference reference-000635

link to definition of the first-order machine-description language

Source occurrence

Cross-reference reference-000636

link to left-move representation sentence

Source occurrence

Cross-reference reference-000637

link to stay-put case in the configuration induction

Source occurrence

Cross-reference reference-000638

link to stay-put case in the configuration induction

Source occurrence

Cross-reference reference-000639

link to configuration representation lemma

Source occurrence

Cross-reference reference-000640

link to configuration representation lemma

Source occurrence

Cross-reference reference-000641

link to lemma that a halting configuration entails the halting sentence

Source occurrence

Cross-reference reference-000642

link to lemma that validity of the representation implies halting

Source occurrence

Cross-reference reference-000643

link to lemma that halting implies validity of the representation

Source occurrence

Cross-reference reference-000644

link to theorem on unsolvability of the Halting Problem

Source occurrence

Cross-reference reference-000645

link to section Representing Turing Machines

Source occurrence

Cross-reference reference-000646

link to lemma that halting implies validity of the representation

Source occurrence

Cross-reference reference-000647

link to lemma that validity of the representation implies halting

Source occurrence

Cross-reference reference-000648

link to theorem that the decision problem is unsolvable

Source occurrence

Cross-reference reference-000649

link to corollary that first-order satisfiability is undecidable

Source occurrence

Cross-reference reference-000650

link to lemma that validity of the representation implies halting

Source occurrence

Cross-reference reference-000651

link to lemma that validity of the representation implies halting

Source occurrence

Cross-reference reference-000652

link to section Representing Turing Machines

Source occurrence

Cross-reference reference-000653

link to lemma that validity of the representation implies halting

Source occurrence

Cross-reference reference-000654

link to lemma that halting gives a finite model

Source occurrence

Cross-reference reference-000655

link to configuration representation lemma

Source occurrence

Cross-reference reference-000656

link to proposition that represented numerals preserve strict order

Source occurrence

Cross-reference reference-000657

link to lemma that a finite model gives halting

Source occurrence

Cross-reference reference-000658

link to lemma that halting gives a finite model

Source occurrence

Cross-reference reference-000659

link to lemma that a finite model gives halting

Source occurrence

Cross-reference reference-000660

link to corollary excluding a sound and complete proof system for finite validity

Source occurrence

Cross-reference reference-000661

link to theorem that first-order validity is semidecidable

Source occurrence

Source disclosures