Equation form expr-002bf3eb1573e012

$k+1$

Read as: k plus one

Means: k plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019700

Equation form expr-00acf7ce579f67f3

$!A_{\Zero}(x,y) \ident \eq[y][\Obj 0]$

Read as: A subscript zero function of x and y is the formula y equals the object language constant zero

Means: A subscript zero function of x and y is the formula y equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019043

Equation form expr-00cf750d9cce40d2

$\Th{Q} \Proves \lnot !A(\num{n})$

Read as: Q proves that not A of the numeral for n

Means: Q proves that not A of the numeral for n

1 occurrence in this chapter

• Occurrence projected-formula-0019540

Equation form expr-00e3b80d5a90664e

$!A_f(z,y) \ident !A_g(y, z, \Obj 0) \land \lforall[w][(w < y \lif \lnot !A_g(w, z, \Obj 0))].$

Read as: A subscript f of z and y is the conjunction of A subscript g of y, z, and the object language constant zero, with the following universal statement: for every w, if w is less than y then not A subscript g of w, z, and the object language constant zero

Means: A subscript f of z and y is the conjunction of A subscript g of y, z, and the object language constant zero, with the following universal statement: for every w, if w is less than y then not A subscript g of w, z, and the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019244

Equation form expr-00fe9b383f124db5

$y_n$

Read as: y subscript n

Means: y subscript n

3 occurrences in this chapter

• Occurrence projected-formula-0018916
• Occurrence projected-formula-0018922
• Occurrence projected-formula-0018931

Equation form expr-0120f8b6ce4d3c14

$\eq[(b'+a)][\Obj 0]$

Read as: the sum of the successor of b and a equals the object language constant zero

Means: the sum of the successor of b and a equals the object language constant zero

2 occurrences in this chapter

• Occurrence projected-formula-0019274
• Occurrence projected-formula-0019278

Equation form expr-0180ff76ea2f422f

$h(\vec x, y) = \beta(\hat h(\vec x, y), y),$

Read as: h of the tuple x and y equals beta of h hat of the tuple x and y, and y

Means: h of the tuple x and y equals beta of h hat of the tuple x and y, and y

1 occurrence in this chapter

• Occurrence projected-formula-0019026

Equation form expr-02d48ad3da1936b3

$\eq[z' + t_1][t_2]$

Read as: the sum of the successor of z and t subscript one equals t subscript two

Means: the sum of the successor of z and t subscript one equals t subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019666

Equation form expr-033c668a4e2817cd

$\Prov[\Th{Q}](y) \defiff \fn{Sent}(y) \land \lexists[x][\Prf[\Th{Q}](x, y)]$

Read as: Provability in Q holds of y by definition if and only if y is a sentence code and there exists x which codes a derivation in Q of the formula with code y

Means: Provability in Q holds of y by definition if and only if y is a sentence code and there exists x which codes a derivation in Q of the formula with code y

1 occurrence in this chapter

• Occurrence projected-formula-0019521

Equation form expr-0343067284e5822a

$!A \ident \lexists[x][!B(x)]$

Read as: A is the formula there exists x such that B of x

Means: A is the formula there exists x such that B of x

1 occurrence in this chapter

• Occurrence projected-formula-0019588

Equation form expr-03601b0ecb040012

$\eq[(b' + c)'][\Obj 0]$

Read as: the successor of the sum of the successor of b and c equals the object language constant zero

Means: the successor of the sum of the successor of b and c equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019290

Equation form expr-0407f4d79a43a272

$\Mult(x_0, x_1) = x_0 \cdot x_1$

Read as: the multiplication function applied to x subscript zero and x subscript one equals x subscript zero times x subscript one

Means: the multiplication function applied to x subscript zero and x subscript one equals x subscript zero times x subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0019159

Equation form expr-043a718774c572bd

$s$

Read as: s

Means: s

8 occurrences in this chapter

• Occurrence projected-formula-0018864
• Occurrence projected-formula-0018870
• Occurrence projected-formula-0018873
• Occurrence projected-formula-0019525
• Occurrence projected-formula-0019535
• Occurrence projected-formula-0019537
• Occurrence projected-formula-0019547
• Occurrence projected-formula-0019787

Equation form expr-043e4702cf309ada

$\Th{Q} \Proves !A_h(\num{n}, \num{m})$

Read as: Q proves that A subscript h of the numeral for n and the numeral for m

Means: Q proves that A subscript h of the numeral for n and the numeral for m

2 occurrences in this chapter

• Occurrence projected-formula-0019207
• Occurrence projected-formula-0019212

Equation form expr-0459187f686800bb

$\eq[(z' + \num{n - m - 1})'][\Obj 0]$

Read as: the successor of the sum of the successor of z and the numeral for n minus m minus one equals the object language constant zero

Means: the successor of the sum of the successor of z and the numeral for n minus m minus one equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019677

Equation form expr-046ab677882f254d

$n \neq k$

Read as: n does not equal k

Means: n does not equal k

1 occurrence in this chapter

• Occurrence projected-formula-0019086

Equation form expr-046b4724fc2febf0

$a_n$

Read as: a subscript n

Means: a subscript n

2 occurrences in this chapter

• Occurrence projected-formula-0018887
• Occurrence projected-formula-0018898

Equation form expr-046becba09a52afb

$\Th{Q} \Proves \lforall[w][(w < \num{m} \lif \lnot !A_g(w, \num{n}, \Obj 0))]$

Read as: Q proves that for every w, if w is less than the numeral for m then not A subscript g of w, the numeral for n, and the object language constant zero

Means: Q proves that for every w, if w is less than the numeral for m then not A subscript g of w, the numeral for n, and the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019436

Equation form expr-07587fdd1bdb1d42

$\Value{(t_1 + t_2)}{N} = \Value{t_1}{N} + \Value{t_2}{N} = n_1 + n_2.$

Read as: The value of the term t subscript one plus t subscript two in the standard model N equals the value of t subscript one in N plus the value of t subscript two in N. This equals n subscript one plus n subscript two

Means: The value of the term t subscript one plus t subscript two in the standard model N equals the value of t subscript one in N plus the value of t subscript two in N. This equals n subscript one plus n subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019613

Equation form expr-08a31aaffef905c3

$x_n$

Read as: x subscript n

Means: x subscript n

3 occurrences in this chapter

• Occurrence projected-formula-0018914
• Occurrence projected-formula-0018920
• Occurrence projected-formula-0018929

Equation form expr-08c6aa8d5824f2de

$\Succ$

Read as: the successor function

Means: the successor function

6 occurrences in this chapter

• Occurrence projected-formula-0018816
• Occurrence projected-formula-0019009
• Occurrence projected-formula-0019054
• Occurrence projected-formula-0019441
• Occurrence projected-formula-0019449
• Occurrence projected-formula-0019455

Equation form expr-0916713022826be9

$!A_=(\num{n}, \num{m}, \num{1})$

Read as: A subscript equality applied to the numerals for n and m, and the numeral for one

Means: A subscript equality applied to the numerals for n and m, and the numeral for one

1 occurrence in this chapter

• Occurrence projected-formula-0019105

Equation form expr-099959186b7f6cac

$n = m$

Read as: n equals m

Means: n equals m

3 occurrences in this chapter

• Occurrence projected-formula-0019100
• Occurrence projected-formula-0019111
• Occurrence projected-formula-0019640

Equation form expr-09bda5125a2f9e49

$\Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{m}) \quad\text{iff}\quad m = f(n_0, \dots, n_k).$

Read as: Q proves A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for m, if and only if m equals f of n subscript zero through n subscript k

Means: Q proves A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for m, if and only if m equals f of n subscript zero through n subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0018827

Equation form expr-09f5d3cdd4f61799

$p \mid 1 + (i+1) m$

Read as: p divides one plus the product of i plus one and m

Means: p divides one plus the product of i plus one and m

1 occurrence in this chapter

• Occurrence projected-formula-0018940

Equation form expr-0a2c809e671649ae

$\hat h(\vec x, y)$

Read as: h hat of the tuple x and y

Means: h hat of the tuple x and y

1 occurrence in this chapter

• Occurrence projected-formula-0019014

Equation form expr-0a566b1db5acde7f

$g_0$

Read as: g subscript zero

Means: g subscript zero

1 occurrence in this chapter

• Occurrence projected-formula-0019180

Equation form expr-0a5a0cdb7119bde3

$n \neq m$

Read as: n does not equal m

Means: n does not equal m

5 occurrences in this chapter

• Occurrence projected-formula-0019062
• Occurrence projected-formula-0019066
• Occurrence projected-formula-0019106
• Occurrence projected-formula-0019117
• Occurrence projected-formula-0019643

Equation form expr-0a731ae7784bab75

$R(n_0, \dots, n_k, s)$

Read as: R of n subscript zero through n subscript k, and s

Means: R of n subscript zero through n subscript k, and s

3 occurrences in this chapter

• Occurrence projected-formula-0018859
• Occurrence projected-formula-0018865
• Occurrence projected-formula-0018879

Equation form expr-0aaed6339b81f11f

$j &= \max(n, y_0 + 1, \dots, y_n + 1), \\ m &= \lcm(1,\dots,j),$

Read as: j equals the maximum of n, y subscript zero plus one, and so on through y subscript n plus one. m equals the least common multiple of the integers one through j

Means: j equals the maximum of n, y subscript zero plus one, and so on through y subscript n plus one. m equals the least common multiple of the integers one through j

1 occurrence in this chapter

• Occurrence projected-formula-0018932

Equation form expr-0ac6f2ec0fc75966

$\num{k}$

Read as: the numeral for k

Means: the numeral for k

1 occurrence in this chapter

• Occurrence projected-formula-0019149

Equation form expr-0b0fc5327dcecbe2

$a < \num 1$

Read as: a is less than the numeral for one

Means: a is less than the numeral for one

1 occurrence in this chapter

• Occurrence projected-formula-0019298

Equation form expr-0b9c5e137bc7261e

$h(n) = m$

Read as: h of n equals m

Means: h of n equals m

4 occurrences in this chapter

• Occurrence projected-formula-0019206
• Occurrence projected-formula-0019208
• Occurrence projected-formula-0019213
• Occurrence projected-formula-0019215

Equation form expr-0bde84c13896897b

$x < \num{k+1}$

Read as: x is less than the numeral for k plus one

Means: x is less than the numeral for k plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019705

Equation form expr-0c121de460f446f8

$\bforall{x<t}{\lnot!A(x)}$

Read as: for every x less than t, not A of x

Means: for every x less than t, not A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019763

Equation form expr-0c46538005b57adc

$!A_g(x, y)$

Read as: A subscript g of x and y

Means: A subscript g of x and y

1 occurrence in this chapter

• Occurrence projected-formula-0019188

Equation form expr-0c6150bf3a95a786

$m \leq n$

Read as: m is less than or equal to n

Means: m is less than or equal to n

1 occurrence in this chapter

• Occurrence projected-formula-0019661

Equation form expr-0c615cfc75a63a7d

$h(\vec x, 0) & = f(\vec x) \\ h(\vec x, y+1) & = g(\vec x, y, h(\vec x, y)).$

Read as: Base case: h of the tuple x and zero equals f of the tuple x. Recursion step: h of the tuple x and y plus one equals g of the tuple x, y, and h of the tuple x and y

Means: Base case: h of the tuple x and zero equals f of the tuple x. Recursion step: h of the tuple x and y plus one equals g of the tuple x, y, and h of the tuple x and y

1 occurrence in this chapter

• Occurrence projected-formula-0018998

Equation form expr-0ca087e027fea4f9

$!A_{\Add}(x_0, x_1, y) \ident \eq[y][(x_0 + x_1)].$

Read as: A subscript Add of x subscript zero, x subscript one, and y is the formula y equals the sum of x subscript zero and x subscript one

Means: A subscript Add of x subscript zero, x subscript one, and y is the formula y equals the sum of x subscript zero and x subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0019125

Equation form expr-0e895da1dde0af8b

$y_i < j \leq m < x_i$

Read as: y subscript i is less than j; j is less than or equal to m; and m is less than x subscript i

Means: y subscript i is less than j; j is less than or equal to m; and m is less than x subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0018958

Equation form expr-0ef4b2cb1fbfa584

$\lforall[x][\lforall[y][\eq[x'][y'] \lif \eq[x][y]]]$

Read as: for all x and y, if their successors are equal, then x equals y

Means: for all x and y, if their successors are equal, then x equals y

1 occurrence in this chapter

• Occurrence projected-formula-0019089

Equation form expr-0ef721aef4e4d1c4

$\Th{Q} \Proves \lforall[y][(!A_f(\num{n}, y) \lif \eq[y][\num{m}])]$

Read as: Q proves that for every y, if A subscript f holds of the numeral for n and y, then y equals the numeral for m

Means: Q proves that for every y, if A subscript f holds of the numeral for n and y, then y equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019421

Equation form expr-0f54ca49553849bd

$\eq/[z'][\Obj 0]$

Read as: the successor of z does not equal the object language constant zero

Means: the successor of z does not equal the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019674

Equation form expr-0f6a28bdfad5c884

$f(y_0, \dots, y_{k-1})$

Read as: f of y subscript zero through y subscript k minus one

Means: f of y subscript zero through y subscript k minus one

1 occurrence in this chapter

• Occurrence projected-formula-0019224

Equation form expr-10ae1238b3bedd73

$\num{m+1}$

Read as: the numeral for m plus one

Means: the numeral for m plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019134

Equation form expr-10d29b12563e1ccd

$!A_g(x, z, y)$

Read as: A subscript g of x, z, and y

Means: A subscript g of x, z, and y

2 occurrences in this chapter

• Occurrence projected-formula-0019234
• Occurrence projected-formula-0019411

Equation form expr-115ce48a5e1e2710

$\left|i-k\right|$

Read as: the absolute value of i minus k

Means: the absolute value of i minus k

1 occurrence in this chapter

• Occurrence projected-formula-0018952

Equation form expr-116a126b4adf26eb

$\lexists[y][\eq[(y'+a)][\Obj 0]]$

Read as: there exists y such that the sum of the successor of y and a equals the object language constant zero

Means: there exists y such that the sum of the successor of y and a equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019273

Equation form expr-11baa595827a4e0f

$\omega$

Read as: omega

Means: omega

1 occurrence in this chapter

• Occurrence projected-formula-0019539

Equation form expr-126ba9dbf35ba818

$\Th{Q} \Proves \eq[{\num k}' + t_1][t_2]$

Read as: Q proves that the sum of the successor of the numeral for k and t subscript one equals t subscript two

Means: Q proves that the sum of the successor of the numeral for k and t subscript one equals t subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019656

Equation form expr-12d9b1e9f8e5096a

$\Sat{N}{!A(x)}[s]$

Read as: the standard model N under assignment s satisfies A of x

Means: the standard model N under assignment s satisfies A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019789

Equation form expr-139c7c04318de35e

$n = 0$

Read as: n equals zero

Means: n equals zero

3 occurrences in this chapter

• Occurrence projected-formula-0019068
• Occurrence projected-formula-0019253
• Occurrence projected-formula-0019295

Equation form expr-13b7fc57566924a3

$\Th{Q} \Proves \eq[\num{l}][\num{m}]$

Read as: Q proves that the numeral for l equals the numeral for m

Means: Q proves that the numeral for l equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0018834

Equation form expr-13dcd97896f4422a

$\Succ(x) = x+1$

Read as: the successor function applied to x equals x plus one

Means: the successor function applied to x equals x plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019044

Equation form expr-147d8c41e77101cc

$\Th{Q} \Proves \lforall[x][(x < \num {n+1} \lif (\eq[x][\Obj 0] \lor \dots \lor \eq[x][\num n]))].$

Read as: Q proves that for every x, if x is less than the numeral for n plus one, then x equals one of the numerals from zero through n

Means: Q proves that for every x, if x is less than the numeral for n plus one, then x equals one of the numerals from zero through n

1 occurrence in this chapter

• Occurrence projected-formula-0019293

Equation form expr-148de9c5a7a44d19

$p$

Read as: p

Means: p

5 occurrences in this chapter

• Occurrence projected-formula-0018937
• Occurrence projected-formula-0018942
• Occurrence projected-formula-0018944
• Occurrence projected-formula-0018948
• Occurrence projected-formula-0018950

Equation form expr-149bf3c439e010d6

$c < \Obj 0$

Read as: c is less than the object language constant zero

Means: c is less than the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019317

Equation form expr-14adae10a93f394c

$!A_\Add(x_0, x_1, y)$

Read as: A subscript Add applied to x subscript zero, x subscript one, and y

Means: A subscript Add applied to x subscript zero, x subscript one, and y

1 occurrence in this chapter

• Occurrence projected-formula-0019142

Equation form expr-152fd4c0c212fbe9

$\Value{t_2}{N} \leq \Value{t_1}{N}$

Read as: the value of t subscript two in the standard model N is less than or equal to the value of t subscript one in the standard model N

Means: the value of t subscript two in the standard model N is less than or equal to the value of t subscript one in the standard model N

1 occurrence in this chapter

• Occurrence projected-formula-0019631

Equation form expr-1581d72466c85316

$x_k$

Read as: x subscript k

Means: x subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0018957

Equation form expr-15fd307d7f46f8c3

$\num{2}$

Read as: the numeral for two

Means: the numeral for two

1 occurrence in this chapter

• Occurrence projected-formula-0018785

Equation form expr-16905e3dcc56a2ae

$\Th{Q} \Proves \eq[(\num{n} + \num{m}')][\num{n+m}']$

Read as: Q proves that the sum of the numeral for n and the successor of the numeral for m equals the successor of the numeral for n plus m

Means: Q proves that the sum of the numeral for n and the successor of the numeral for m equals the successor of the numeral for n plus m

1 occurrence in this chapter

• Occurrence projected-formula-0019141

Equation form expr-173061a6aaa446d4

$\Th{Q} \Proves !A_=(\num{n}, \num{m}, \num{0})$

Read as: Q proves that A subscript equality applied to the numerals for n and m, and the numeral for zero

Means: Q proves that A subscript equality applied to the numerals for n and m, and the numeral for zero

1 occurrence in this chapter

• Occurrence projected-formula-0019110

Equation form expr-188f5e8c4839a80f

$b' < \num {n+2}$

Read as: the successor of b is less than the numeral for n plus two

Means: the successor of b is less than the numeral for n plus two

1 occurrence in this chapter

• Occurrence projected-formula-0019326

Equation form expr-18ac3e7343f01689

$d$

Read as: d

Means: d

7 occurrences in this chapter

• Occurrence projected-formula-0018850
• Occurrence projected-formula-0018871
• Occurrence projected-formula-0018888
• Occurrence projected-formula-0018892
• Occurrence projected-formula-0018896
• Occurrence projected-formula-0019015
• Occurrence projected-formula-0019016

Equation form expr-18e9a2ef1c0f5cb1

$\eq[(c' + \num{m}')][b']$

Read as: the sum of the successor of c and the successor of the numeral for m equals the successor of b

Means: the sum of the successor of c and the successor of the numeral for m equals the successor of b

1 occurrence in this chapter

• Occurrence projected-formula-0019398

Equation form expr-18ef0ae4db587e5b

$\Th{Q} \Proves/ \lexists[y][!A(y)]$

Read as: Q does not prove that there exists y such that A of y

Means: Q does not prove that there exists y such that A of y

1 occurrence in this chapter

• Occurrence projected-formula-0019542

Equation form expr-18fb187f6340634b

$\Th{Q} \Proves \eq[t_2][\num n]$

Read as: Q proves that t subscript two equals the numeral for n

Means: Q proves that t subscript two equals the numeral for n

1 occurrence in this chapter

• Occurrence projected-formula-0019639

Equation form expr-1922c19949fdd3f1

$\bexists{x < t}{!A(x)}$

Read as: there exists x less than t such that A of x

Means: there exists x less than t such that A of x

2 occurrences in this chapter

• Occurrence projected-formula-0019580
• Occurrence projected-formula-0019753

Equation form expr-19b2a8c282eaa008

$\fn{rem}(x,y)$

Read as: rem of x and y, the remainder when y is divided by x

Means: rem of x and y, the remainder when y is divided by x

2 occurrences in this chapter

• Occurrence projected-formula-0018967
• Occurrence projected-formula-0018990

Equation form expr-19e9c269d8cb4bcf

$s(x) = n$

Read as: assignment s sends x to n

Means: assignment s sends x to n

1 occurrence in this chapter

• Occurrence projected-formula-0019788

Equation form expr-1b16b1df538ba12d

$n$

Read as: n

Means: n

17 occurrences in this chapter

• Occurrence projected-formula-0018777
• Occurrence projected-formula-0018780
• Occurrence projected-formula-0018884
• Occurrence projected-formula-0018953
• Occurrence projected-formula-0019038
• Occurrence projected-formula-0019060
• Occurrence projected-formula-0019064
• Occurrence projected-formula-0019079
• Occurrence projected-formula-0019087
• Occurrence projected-formula-0019250
• Occurrence projected-formula-0019252
• Occurrence projected-formula-0019292
• Occurrence projected-formula-0019294
• Occurrence projected-formula-0019319
• Occurrence projected-formula-0019523
• Occurrence projected-formula-0019551
• Occurrence projected-formula-0019786

Equation form expr-1b8ddd311995c3e6

$\Th{Q} \Proves \eq/[\num{l}][\num{m}]$

Read as: Q proves that the numeral for l does not equal the numeral for m

Means: Q proves that the numeral for l does not equal the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0018835

Equation form expr-1ba1ebd4a3e5f2fa

$\bexists{x<t}{\lnot !A(x)}$

Read as: there exists x less than t such that not A of x

Means: there exists x less than t such that not A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019757

Equation form expr-1bf0def65cbf1cdf

$f(g(n)) = m$

Read as: f of g of n equals m

Means: f of g of n equals m

2 occurrences in this chapter

• Occurrence projected-formula-0019209
• Occurrence projected-formula-0019216

Equation form expr-1ebbf9f57552ec69

$m = f(n_0, \dots, n_k)$

Read as: m equals f of n subscript zero through n subscript k

Means: m equals f of n subscript zero through n subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0018845

Equation form expr-1f0b48345ddedcf2

$z_0$

Read as: z subscript zero

Means: z subscript zero

1 occurrence in this chapter

• Occurrence projected-formula-0019246

Equation form expr-1f3ab9cf428562d8

$\Th{Q} \Proves !A(\num 0) \lor \dots \lor !A(\num{k-1})$

Read as: Q proves that the finite disjunction of A applied to each numeral from zero through k minus one

Means: Q proves that the finite disjunction of A applied to each numeral from zero through k minus one

1 occurrence in this chapter

• Occurrence projected-formula-0019687

Equation form expr-1f97d653b7ed2d2b

$n+1$

Read as: n plus one

Means: n plus one

2 occurrences in this chapter

• Occurrence projected-formula-0019080
• Occurrence projected-formula-0019318

Equation form expr-20aa50a3a1186f9b

$a \equiv b \mod c$

Read as: a is congruent to b modulo c

Means: a is congruent to b modulo c

1 occurrence in this chapter

• Occurrence projected-formula-0018908

Equation form expr-20b07e4823cb2fb8

$\Gn{\lexists[y][!B_T(\num{e}, \num{n}, y)]}$

Read as: the Goedel number of the formula there exists y such that B subscript T holds of the numeral for e, the numeral for n, and y

Means: the Goedel number of the formula there exists y such that B subscript T holds of the numeral for e, the numeral for n, and y

1 occurrence in this chapter

• Occurrence projected-formula-0019552

Equation form expr-2243b195c00d21fb

$!B_T$

Read as: B subscript T

Means: B subscript T

1 occurrence in this chapter

• Occurrence projected-formula-0019530

Equation form expr-22ced2a4d81d280b

$\Th{Q} \Proves !A_f(\num n, \num m)$

Read as: Q proves that A subscript f of the numeral for n and the numeral for m

Means: Q proves that A subscript f of the numeral for n and the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019417

Equation form expr-23146883045d970e

$\num m$

Read as: the numeral for m

Means: the numeral for m

2 occurrences in this chapter

• Occurrence projected-formula-0019078
• Occurrence projected-formula-0019095

Equation form expr-2340230b2e0abc21

$\Value{\Obj 0}{N} = 0$

Read as: the value of the object language constant zero in the standard model N equals zero

Means: the value of the object language constant zero in the standard model N equals zero

1 occurrence in this chapter

• Occurrence projected-formula-0019600

Equation form expr-234ef32b30394a54

$(!A \lor !B)$

Read as: the disjunction of A and B

Means: the disjunction of A and B

1 occurrence in this chapter

• Occurrence projected-formula-0019728

Equation form expr-2355ecda4c890c45

$(1 + (i+1)m) - (1+ (k+1)m) = (i-k) m.$

Read as: the quantity one plus the product of i plus one and m, minus the quantity one plus the product of k plus one and m, equals the product of i minus k and m

Means: the quantity one plus the product of i plus one and m, minus the quantity one plus the product of k plus one and m, equals the product of i minus k and m

1 occurrence in this chapter

• Occurrence projected-formula-0018943

Equation form expr-236a9900efeb2107

$\eq[a][b']$

Read as: a equals the successor of b

Means: a equals the successor of b

7 occurrences in this chapter

• Occurrence projected-formula-0019324
• Occurrence projected-formula-0019340
• Occurrence projected-formula-0019350
• Occurrence projected-formula-0019352
• Occurrence projected-formula-0019369
• Occurrence projected-formula-0019374
• Occurrence projected-formula-0019399

Equation form expr-241d658a47ae5a64

$a_0$

Read as: a subscript zero

Means: a subscript zero

2 occurrences in this chapter

• Occurrence projected-formula-0018886
• Occurrence projected-formula-0018897

Equation form expr-24931e0795a913c5

$!A_{\Succ}(x,y) \ident \eq[y][x']$

Read as: A subscript successor function of x and y is the formula y equals the successor of x

Means: A subscript successor function of x and y is the formula y equals the successor of x

1 occurrence in this chapter

• Occurrence projected-formula-0019046

Equation form expr-250dc58ba799c9f2

$b' < \num{n+1}'$

Read as: the successor of b is less than the successor of the numeral for n plus one

Means: the successor of b is less than the successor of the numeral for n plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019327

Equation form expr-252f10c83610ebca

$f$

Read as: f

Means: f

17 occurrences in this chapter

• Occurrence projected-formula-0018840
• Occurrence projected-formula-0018843
• Occurrence projected-formula-0018846
• Occurrence projected-formula-0018855
• Occurrence projected-formula-0018856
• Occurrence projected-formula-0018881
• Occurrence projected-formula-0018996
• Occurrence projected-formula-0019000
• Occurrence projected-formula-0019004
• Occurrence projected-formula-0019006
• Occurrence projected-formula-0019179
• Occurrence projected-formula-0019187
• Occurrence projected-formula-0019220
• Occurrence projected-formula-0019235
• Occurrence projected-formula-0019238
• Occurrence projected-formula-0019444
• Occurrence projected-formula-0019446

Equation form expr-25c79bc25c22b1f3

$\Value{t_1}{N} < \Value{t_2}{N}$

Read as: the value of t subscript one in the standard model N is less than the value of t subscript two in the standard model N

Means: the value of t subscript one in the standard model N is less than the value of t subscript two in the standard model N

1 occurrence in this chapter

• Occurrence projected-formula-0019629

Equation form expr-2744a80ff53255bd

$k \in \Nat$

Read as: k is a natural number

Means: k is a natural number

1 occurrence in this chapter

• Occurrence projected-formula-0019651

Equation form expr-274ec82875bc15b2

$y_i$

Read as: y subscript i

Means: y subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0018925

Equation form expr-2808f40d73183bcd

$f(n_0,\dots,n_k) = m$

Read as: f of n subscript zero through n subscript k equals m

Means: f of n subscript zero through n subscript k equals m

1 occurrence in this chapter

• Occurrence projected-formula-0018807

Equation form expr-28ec9f481d74b678

$\Th{Q} \Proves \eq[\num{k}][(\num{n} + \num{m})]$

Read as: Q proves that the numeral for k equals the sum of the numeral for n and the numeral for m

Means: Q proves that the numeral for k equals the sum of the numeral for n and the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019147

Equation form expr-290f81ef5dc5dcca

$\hat h$

Read as: h hat

Means: h hat

2 occurrences in this chapter

• Occurrence projected-formula-0019022
• Occurrence projected-formula-0019024

Equation form expr-29123983a0cb6d1b

$z = f(y)$

Read as: z equals f of y

Means: z equals f of y

2 occurrences in this chapter

• Occurrence projected-formula-0019194
• Occurrence projected-formula-0019201

Equation form expr-2a2da3070718fdd9

$\Th{Q} \Proves \eq[t_1 + t_2][\num{n_1} + t_2]$

Read as: Q proves that the sum of t subscript one and t subscript two equals the sum of the numeral for n subscript one and t subscript two

Means: Q proves that the sum of t subscript one and t subscript two equals the sum of the numeral for n subscript one and t subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019614

Equation form expr-2adf4f17373d7d33

$!A_f(y, z)$

Read as: A subscript f of y and z

Means: A subscript f of y and z

1 occurrence in this chapter

• Occurrence projected-formula-0019186

Equation form expr-2c866df94f98ffce

$k = g(n)$

Read as: k equals g of n

Means: k equals g of n

2 occurrences in this chapter

• Occurrence projected-formula-0019210
• Occurrence projected-formula-0019217

Equation form expr-2cc7cd477953ceb2

$\lexists[u][\eq[(u' + b')][\num{m+1}]]$

Read as: there exists u such that the sum of the successor of u and the successor of b equals the numeral for m plus one

Means: there exists u such that the sum of the successor of u and the successor of b equals the numeral for m plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019385

Equation form expr-2d36cab8ffd2acf4

$\Th{Q} \Proves \lnot(t_1 < t_2)$

Read as: Q proves that it is not the case that t subscript one is less than t subscript two

Means: Q proves that it is not the case that t subscript one is less than t subscript two

2 occurrences in this chapter

• Occurrence projected-formula-0019632
• Occurrence projected-formula-0019680

Equation form expr-2d711642b726b044

$x$

Read as: x

Means: x

4 occurrences in this chapter

• Occurrence projected-formula-0018798
• Occurrence projected-formula-0018969
• Occurrence projected-formula-0019074
• Occurrence projected-formula-0019240

Equation form expr-2df9d6aad7e20fb7

$f(z) = \umin{x}{[g(x, z) = 0]}$

Read as: f of z equals the least x such that g of x and z equals zero

Means: f of z equals the least x such that g of x and z equals zero

2 occurrences in this chapter

• Occurrence projected-formula-0019236
• Occurrence projected-formula-0019415

Equation form expr-2e607d1da306b922

$\Char{R}(x_0, \dots, x_k)$

Read as: the characteristic function of R applied to x subscript zero through x subscript k

Means: the characteristic function of R applied to x subscript zero through x subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0019483

Equation form expr-2e7d2c03a9507ae2

$c$

Read as: c

Means: c

7 occurrences in this chapter

• Occurrence projected-formula-0018907
• Occurrence projected-formula-0018912
• Occurrence projected-formula-0019286
• Occurrence projected-formula-0019307
• Occurrence projected-formula-0019329
• Occurrence projected-formula-0019379
• Occurrence projected-formula-0019393

Equation form expr-2ec537e0c5458fb9

$!A_{\Char{=}}(x_0, x_1, y) \ident (\eq[x_0][x_1] \land \eq[y][\num{1}]) \lor (\eq/[x_0][x_1] \land \eq[y][\num{0}]).$

Read as: A subscript characteristic function of equality, applied to x subscript zero, x subscript one, and y, is the following disjunction. Either x subscript zero equals x subscript one and y equals the numeral for one; or x subscript zero does not equal x subscript one and y equals the numeral for zero

Means: A subscript characteristic function of equality, applied to x subscript zero, x subscript one, and y, is the following disjunction. Either x subscript zero equals x subscript one and y equals the numeral for one; or x subscript zero does not equal x subscript one and y equals the numeral for zero

1 occurrence in this chapter

• Occurrence projected-formula-0019059

Equation form expr-2f02fbff196b184d

$\lnot !A_{\Char{R}}(\num{n_0}, \dots, \num{n_k}, \num{1})$

Read as: not A subscript characteristic function of R, applied to the numerals for n subscript zero through n subscript k, and the numeral for one

Means: not A subscript characteristic function of R, applied to the numerals for n subscript zero through n subscript k, and the numeral for one

1 occurrence in this chapter

• Occurrence projected-formula-0019503

Equation form expr-2f6e2197f5458485

$\lnot \bexists{x<t}!A(x)$

Read as: the negation of the bounded existential formula with variable x, bound t, and matrix A of x

Means: the negation of the bounded existential formula with variable x, bound t, and matrix A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019759

Equation form expr-304c6693e2e2e163

$f(\vec x)$

Read as: f of the tuple x

Means: f of the tuple x

1 occurrence in this chapter

• Occurrence projected-formula-0018993

Equation form expr-3078a09641b0267f

$x_0$

Read as: x subscript zero

Means: x subscript zero

3 occurrences in this chapter

• Occurrence projected-formula-0018913
• Occurrence projected-formula-0018919
• Occurrence projected-formula-0018928

Equation form expr-30c655c7dac91d1c

$\Obj 0 < a$

Read as: the object language constant zero is less than a

Means: the object language constant zero is less than a

2 occurrences in this chapter

• Occurrence projected-formula-0019361
• Occurrence projected-formula-0019362

Equation form expr-32521462ae8ed713

$\Prf[\Th{Q}](d,y)$

Read as: d is the Goedel number of a derivation in Q of the formula with Goedel number y

Means: d is the Goedel number of a derivation in Q of the formula with Goedel number y

1 occurrence in this chapter

• Occurrence projected-formula-0018849

Equation form expr-33136afeecc76360

$\eq/[\num n][\num k] \lif \eq/[\num n'][\num k']$

Read as: if the numeral for n does not equal the numeral for k, then their successors do not equal each other

Means: if the numeral for n does not equal the numeral for k, then their successors do not equal each other

1 occurrence in this chapter

• Occurrence projected-formula-0019092

Equation form expr-332ee6e9f858154b

$h(x_0,\dots,x_{l-1}) = f(g_0(x_0,\dots,x_{l-1}), \dots, g_{k-1}(x_0,\dots,x_{l-1})).$

Read as: h of x subscript zero through x subscript l minus one equals f applied to the outputs of g subscript zero through g subscript k minus one, each evaluated on that same input tuple x subscript zero through x subscript l minus one

Means: h of x subscript zero through x subscript l minus one equals f applied to the outputs of g subscript zero through g subscript k minus one, each evaluated on that same input tuple x subscript zero through x subscript l minus one

1 occurrence in this chapter

• Occurrence projected-formula-0019177

Equation form expr-33c928be6532259f

$\eq[b][\Obj 0] \lor \dots \lor \eq[b][\num{n}]$

Read as: b equals one of the numerals from zero through n

Means: b equals one of the numerals from zero through n

1 occurrence in this chapter

• Occurrence projected-formula-0019337

Equation form expr-349ba76d907adfab

$\times$

Read as: the object language multiplication symbol

Means: the object language multiplication symbol

4 occurrences in this chapter

• Occurrence projected-formula-0019163
• Occurrence projected-formula-0019167
• Occurrence projected-formula-0019618
• Occurrence projected-formula-0019622

Equation form expr-34a408f1932d96be

$\lforall[x][\lforall[y][(x' + y) = (x + y)']]$

Read as: for all x and y, the sum of the successor of x and y equals the successor of the sum of x and y

Means: for all x and y, the sum of the successor of x and y equals the successor of the sum of x and y

1 occurrence in this chapter

• Occurrence projected-formula-0019264

Equation form expr-34b6db63031b8989

$\Th{Q} \Proves \lforall[z][(!A_h(\num{n}, z) \lif z = \num{m})]$

Read as: Q proves that for every z, if A subscript h holds of the numeral for n and z, then z equals the numeral for m

Means: Q proves that for every z, if A subscript h holds of the numeral for n and z, then z equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019214

Equation form expr-3509c2eb7a4f4f4a

$(i-k)m$

Read as: the quantity i minus k, times m

Means: the quantity i minus k, times m

1 occurrence in this chapter

• Occurrence projected-formula-0018951

Equation form expr-363cd42d5ac9f41a

$g_i(x_0, \dots, x_{l-1})$

Read as: g subscript i of x subscript zero through x subscript l minus one

Means: g subscript i of x subscript zero through x subscript l minus one

1 occurrence in this chapter

• Occurrence projected-formula-0019227

Equation form expr-36613f93d5f91b7d

$h(x) = f(g(x))$

Read as: h of x equals f of g of x

Means: h of x equals f of g of x

1 occurrence in this chapter

• Occurrence projected-formula-0019185

Equation form expr-369ed52f7eb96cb2

$1+2 d_1$

Read as: one plus two times d subscript one

Means: one plus two times d subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0018975

Equation form expr-36a9ee34765ec360

$\Th{Q} \Proves \eq[(\num{n} \times \num{m})][\num{n \cdot m}]$

Read as: Q proves that the object language product of the numeral for n and the numeral for m equals the numeral for n times m

Means: Q proves that the object language product of the numeral for n and the numeral for m equals the numeral for n times m

1 occurrence in this chapter

• Occurrence projected-formula-0019162

Equation form expr-36c99c0bb63416fc

$g_i$

Read as: g subscript i

Means: g subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0019221

Equation form expr-3748191a26c840ce

$g(x, z)$

Read as: g of x and z

Means: g of x and z

2 occurrences in this chapter

• Occurrence projected-formula-0019232
• Occurrence projected-formula-0019412

Equation form expr-3768367f8e78740f

$\lforall[w][(w < b \lif \lnot !A_g(w, \num{n}, \Obj 0))]$

Read as: for every w, if w is less than b then not A subscript g of w, the numeral for n, and the object language constant zero

Means: for every w, if w is less than b then not A subscript g of w, the numeral for n, and the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019424

Equation form expr-37a84ca5445df351

$\eq[(c' + b')][\num{m}']$

Read as: the sum of the successor of c and the successor of b equals the successor of the numeral for m

Means: the sum of the successor of c and the successor of b equals the successor of the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019384

Equation form expr-380918b946a52664

$=$

Read as: equality

Means: equality

1 occurrence in this chapter

• Occurrence projected-formula-0019056

Equation form expr-38207f98f811b79b

$x<\num 0$

Read as: x is less than the numeral for zero

Means: x is less than the numeral for zero

1 occurrence in this chapter

• Occurrence projected-formula-0019690

Equation form expr-3851442364e6f15c

$\Prov[\Th{Q}]$

Read as: the provability relation for Q

Means: the provability relation for Q

2 occurrences in this chapter

• Occurrence projected-formula-0019556
• Occurrence projected-formula-0019558

Equation form expr-38654273862c7252

$\Th{Q} \Proves \eq[t_1 + t_2][\num{n_1 + n_2}]$

Read as: Q proves that the sum of t subscript one and t subscript two equals the numeral for n subscript one plus n subscript two

Means: Q proves that the sum of t subscript one and t subscript two equals the numeral for n subscript one plus n subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019617

Equation form expr-393b89d1414d6ea3

$\Th{Q} \Proves \lnot !B_T(\num{e}, \num{n}, \num{s})$

Read as: Q proves that not B subscript T applied to the numerals for e, n, and s

Means: Q proves that not B subscript T applied to the numerals for e, n, and s

1 occurrence in this chapter

• Occurrence projected-formula-0019536

Equation form expr-3a8f1b078f3f2c11

$(d)_0 = f(\vec x)$

Read as: the entry beta of d and zero equals f of the tuple x

Means: the entry beta of d and zero equals f of the tuple x

1 occurrence in this chapter

• Occurrence projected-formula-0019017

Equation form expr-3ade0c4e814b7a10

$\beta(d,i)$

Read as: beta of d and i

Means: beta of d and i

3 occurrences in this chapter

• Occurrence projected-formula-0018885
• Occurrence projected-formula-0018894
• Occurrence projected-formula-0019021

Equation form expr-3b391ecd75985eba

$\Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{m})$

Read as: Q proves that A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for m

Means: Q proves that A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for m

2 occurrences in this chapter

• Occurrence projected-formula-0018828
• Occurrence projected-formula-0018833

Equation form expr-3cc31176550ef537

$\lexists[x][(x < t \land !A(x))]$

Read as: there exists x such that both x is less than t and A of x

Means: there exists x such that both x is less than t and A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019578

Equation form expr-3cd97a31b560be7d

$R(x_0,\dots,x_k)$

Read as: R of x subscript zero through x subscript k

Means: R of x subscript zero through x subscript k

2 occurrences in this chapter

• Occurrence projected-formula-0019465
• Occurrence projected-formula-0019475

Equation form expr-3cdee58aaa5ae70f

$\lforall[x][\lforall[y][(x + y) = (y + x)]]$

Read as: for all x and y, the sum of x and y equals the sum of y and x

Means: for all x and y, the sum of x and y equals the sum of y and x

1 occurrence in this chapter

• Occurrence projected-formula-0018789

Equation form expr-3d2df79065b6f165

$\Th{Q}$

Read as: Q

Means: Q

94 occurrences in this chapter

• Occurrence projected-formula-0018768
• Occurrence projected-formula-0018769
• Occurrence projected-formula-0018771
• Occurrence projected-formula-0018772
• Occurrence projected-formula-0018774
• Occurrence projected-formula-0018775
• Occurrence projected-formula-0018787
• Occurrence projected-formula-0018790
• Occurrence projected-formula-0018791
• Occurrence projected-formula-0018792
• Occurrence projected-formula-0018794
• Occurrence projected-formula-0018803
• Occurrence projected-formula-0018805
• Occurrence projected-formula-0018808
• Occurrence projected-formula-0018811
• Occurrence projected-formula-0018813
• Occurrence projected-formula-0018814
• Occurrence projected-formula-0018818
• Occurrence projected-formula-0018820
• Occurrence projected-formula-0018821
• Occurrence projected-formula-0018822
• Occurrence projected-formula-0018823
• Occurrence projected-formula-0018825
• Occurrence projected-formula-0018836
• Occurrence projected-formula-0018837
• Occurrence projected-formula-0018839
• Occurrence projected-formula-0018844
• Occurrence projected-formula-0018852
• Occurrence projected-formula-0018861
• Occurrence projected-formula-0019028
• Occurrence projected-formula-0019029
• Occurrence projected-formula-0019036
• Occurrence projected-formula-0019039
• Occurrence projected-formula-0019042
• Occurrence projected-formula-0019045
• Occurrence projected-formula-0019048
• Occurrence projected-formula-0019058
• Occurrence projected-formula-0019091
• Occurrence projected-formula-0019096
• Occurrence projected-formula-0019097
• Occurrence projected-formula-0019099
• Occurrence projected-formula-0019121
• Occurrence projected-formula-0019124
• Occurrence projected-formula-0019160
• Occurrence projected-formula-0019175
• Occurrence projected-formula-0019205
• Occurrence projected-formula-0019225
• Occurrence projected-formula-0019228
• Occurrence projected-formula-0019231
• Occurrence projected-formula-0019233
• Occurrence projected-formula-0019248
• Occurrence projected-formula-0019254
• Occurrence projected-formula-0019260
• Occurrence projected-formula-0019263
• Occurrence projected-formula-0019266
• Occurrence projected-formula-0019272
• Occurrence projected-formula-0019281
• Occurrence projected-formula-0019312
• Occurrence projected-formula-0019413
• Occurrence projected-formula-0019438
• Occurrence projected-formula-0019439
• Occurrence projected-formula-0019460
• Occurrence projected-formula-0019461
• Occurrence projected-formula-0019462
• Occurrence projected-formula-0019463
• Occurrence projected-formula-0019464
• Occurrence projected-formula-0019466
• Occurrence projected-formula-0019469
• Occurrence projected-formula-0019472
• Occurrence projected-formula-0019474
• Occurrence projected-formula-0019492
• Occurrence projected-formula-0019494
• Occurrence projected-formula-0019498
• Occurrence projected-formula-0019500
• Occurrence projected-formula-0019502
• Occurrence projected-formula-0019506
• Occurrence projected-formula-0019513
• Occurrence projected-formula-0019519
• Occurrence projected-formula-0019520
• Occurrence projected-formula-0019529
• Occurrence projected-formula-0019538
• Occurrence projected-formula-0019543
• Occurrence projected-formula-0019559
• Occurrence projected-formula-0019563
• Occurrence projected-formula-0019565
• Occurrence projected-formula-0019566
• Occurrence projected-formula-0019567
• Occurrence projected-formula-0019662
• Occurrence projected-formula-0019689
• Occurrence projected-formula-0019692
• Occurrence projected-formula-0019704
• Occurrence projected-formula-0019758
• Occurrence projected-formula-0019762
• Occurrence projected-formula-0019773

Equation form expr-3d8599ee1cdce5f5

$!A_h(x, z)$

Read as: A subscript h of x and z

Means: A subscript h of x and z

2 occurrences in this chapter

• Occurrence projected-formula-0019190
• Occurrence projected-formula-0019204

Equation form expr-3dc609ecaa989589

$\bforall{x<t}{!A(x)}$

Read as: the bounded universal formula with variable x, bound t, and matrix A of x

Means: the bounded universal formula with variable x, bound t, and matrix A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019744

Equation form expr-3ddc4c39050a4dea

$x < y \liff \lexists[z][\eq[z' + x][y]]$

Read as: x is less than y if and only if there exists z such that the sum of the successor of z and x equals y

Means: x is less than y if and only if there exists z such that the sum of the successor of z and x equals y

1 occurrence in this chapter

• Occurrence projected-formula-0019648

Equation form expr-3dddf911c3c51204

$\Obj{0}'$

Read as: the successor of the object language constant zero

Means: the successor of the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0018784

Equation form expr-3e23e8160039594a

$b$

Read as: b

Means: b

8 occurrences in this chapter

• Occurrence projected-formula-0018903
• Occurrence projected-formula-0018906
• Occurrence projected-formula-0018911
• Occurrence projected-formula-0019302
• Occurrence projected-formula-0019323
• Occurrence projected-formula-0019349
• Occurrence projected-formula-0019368
• Occurrence projected-formula-0019408

Equation form expr-3f79bb7b435b0532

$e$

Read as: e

Means: e

2 occurrences in this chapter

• Occurrence projected-formula-0019522
• Occurrence projected-formula-0019550

Equation form expr-3fedf4ba120fb495

$\Th{Q} & \Proves \eq[(a' + \Obj 0)][a'] \quad \text{by axiom $Q_4$} \ollabel{step1}\\ \Th{Q} & \Proves \eq[(a + \Obj 0)][a] \quad \text{by axiom $Q_4$} \ollabel{step2} \\ \Th{Q} & \Proves \eq[(a + \Obj 0)'][a'] \quad \text{by \olref{step2}} \ollabel{step3} \\ \Th{Q} & \Proves \eq[(a' + \Obj 0)][(a + \Obj 0)'] \quad \text{by \olref{step1} and \olref{step3}}\notag$

Read as: Step one. Q proves that the sum of the successor of a and the object language constant zero equals the successor of a, by axiom Q subscript four. Step two. Q proves that the sum of a and that constant zero equals a, by axiom Q subscript four. Step three. Q proves that the successor of the sum of a and that constant zero equals the successor of a, by step two of the successor and fixed numeral addition derivation. Therefore Q proves that the sum of the successor of a and that constant zero equals the successor of the sum of a and that constant zero, by step one of the successor and fixed numeral addition derivation and step three of the successor and fixed numeral addition derivation

Means: Step one. Q proves that the sum of the successor of a and the object language constant zero equals the successor of a, by axiom Q subscript four. Step two. Q proves that the sum of a and that constant zero equals a, by axiom Q subscript four. Step three. Q proves that the successor of the sum of a and that constant zero equals the successor of a, by step two of the successor and fixed numeral addition derivation. Therefore Q proves that the sum of the successor of a and that constant zero equals the successor of the sum of a and that constant zero, by step one of the successor and fixed numeral addition derivation and step three of the successor and fixed numeral addition derivation

1 occurrence in this chapter

• Occurrence projected-formula-0019256

Equation form expr-3ff6171e27f51820

$\hat h(\vec x, y) = \umin{d}{(\beta(d,0) = f(\vec x) \land \bforall{i < y}{\beta(d,i+1) = g(\vec x, i,\beta(d,i)})}.$

Read as: h hat of the tuple x and y equals the least d satisfying both of the following conditions. Beta of d and zero equals f of the tuple x. And for every i less than y, beta of d and i plus one equals g of the tuple x, i, and beta of d and i

Means: h hat of the tuple x and y equals the least d satisfying both of the following conditions. Beta of d and zero equals f of the tuple x. And for every i less than y, beta of d and i plus one equals g of the tuple x, i, and beta of d and i

1 occurrence in this chapter

• Occurrence projected-formula-0019025

Equation form expr-402bb770441080e5

$(d)_{i+1} = g(\vec x, i, (d)_i)$

Read as: the entry beta of d and i plus one equals g of the tuple x, i, and the entry beta of d and i

Means: the entry beta of d and i plus one equals g of the tuple x, i, and the entry beta of d and i

1 occurrence in this chapter

• Occurrence projected-formula-0019019

Equation form expr-40513eca3baf2791

$A_f(\num{n_0}, \dots, \num{n_k}, (s)_1)$

Read as: A subscript f applied to the numerals for n subscript zero through n subscript k, and the entry at position one in the prime power sequence coded by s

Means: A subscript f applied to the numerals for n subscript zero through n subscript k, and the entry at position one in the prime power sequence coded by s

1 occurrence in this chapter

• Occurrence projected-formula-0018869

Equation form expr-405fc868048fb039

$j \geq n$

Read as: j is greater than or equal to n

Means: j is greater than or equal to n

1 occurrence in this chapter

• Occurrence projected-formula-0018954

Equation form expr-40b384adfe07cde8

$\Char{R}(n_0, \dots, n_k) = 1$

Read as: the characteristic function of R applied to n subscript zero through n subscript k equals one

Means: the characteristic function of R applied to n subscript zero through n subscript k equals one

1 occurrence in this chapter

• Occurrence projected-formula-0019491

Equation form expr-40e658560924b03e

$0'' \neq 0'''$

Read as: the second successor of zero does not equal the third successor of zero

Means: the second successor of zero does not equal the third successor of zero

1 occurrence in this chapter

• Occurrence projected-formula-0019098

Equation form expr-41e97c9c1b01a30b

$\lexists{x}!A(x)$

Read as: the existential formula with bound variable x and matrix A of x

Means: the existential formula with bound variable x and matrix A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019783

Equation form expr-4219f3c92eb4e243

$m=0$

Read as: m equals zero

Means: m equals zero

1 occurrence in this chapter

• Occurrence projected-formula-0019344

Equation form expr-428459f7dd087b9a

$f(z)$

Read as: f of z

Means: f of z

1 occurrence in this chapter

• Occurrence projected-formula-0019239

Equation form expr-43fdb02cd8622dcd

$\eq[(b' + c')][\Obj 0]$

Read as: the sum of the successor of b and the successor of c equals the object language constant zero

Means: the sum of the successor of b and the successor of c equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019288

Equation form expr-4448ae754d014960

$\Prov[\Th{Q}](y)$

Read as: y is the Goedel number of a sentence provable in Q

Means: y is the Goedel number of a sentence provable in Q

1 occurrence in this chapter

• Occurrence projected-formula-0019516

Equation form expr-45098c9492fd6adf

$\eq[(a' + \Obj 0)][(a + \Obj 0)']$

Read as: the sum of the successor of a and the object language constant zero equals the successor of the sum of a and the object language constant zero

Means: the sum of the successor of a and the object language constant zero equals the successor of the sum of a and the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019255

Equation form expr-45b91e8acdd27f18

$\lnot !A \ident \lnot\lnot !B$

Read as: not A is the formula not not B

Means: not A is the formula not not B

2 occurrences in this chapter

• Occurrence projected-formula-0019767
• Occurrence projected-formula-0019772

Equation form expr-471e29e5dd963354

$\lnot(!A \lor !B)$

Read as: the negation of the disjunction of A and B

Means: the negation of the disjunction of A and B

1 occurrence in this chapter

• Occurrence projected-formula-0019736

Equation form expr-473a7956734d59c6

$A(n_0, \dots, n_k, m) = \Gn{!A_f(\num{n_0}, \dots, \num{n_k}, \num{m})}$

Read as: A of n subscript zero through n subscript k, and m, equals the Goedel number of A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for m

Means: A of n subscript zero through n subscript k, and m, equals the Goedel number of A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0018858

Equation form expr-479a0e6f2fb037ea

$g(w, z) \neq 0$

Read as: g of w and z does not equal zero

Means: g of w and z does not equal zero

1 occurrence in this chapter

• Occurrence projected-formula-0019243

Equation form expr-47f476387d43584a

$z & \equiv y_0 \mod x_0 \\ z & \equiv y_1 \mod x_1 \\ & \vdots \\ z & \equiv y_n \mod x_n.$

Read as: The simultaneous congruences are: z is congruent to y subscript zero modulo x subscript zero; z is congruent to y subscript one modulo x subscript one; and so on, through z congruent to y subscript n modulo x subscript n

Means: The simultaneous congruences are: z is congruent to y subscript zero modulo x subscript zero; z is congruent to y subscript one modulo x subscript one; and so on, through z congruent to y subscript n modulo x subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0018918

Equation form expr-487776d8c1feed21

$(\num{n} + \num{m})$

Read as: the sum of the numeral for n and the numeral for m

Means: the sum of the numeral for n and the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019170

Equation form expr-489be0a9ab11e480

$\Th{Q} \Proves \eq[(\num{n} + \Obj 0)][\num{n}]$

Read as: Q proves that the sum of the numeral for n and the object language constant zero equals the numeral for n

Means: Q proves that the sum of the numeral for n and the object language constant zero equals the numeral for n

1 occurrence in this chapter

• Occurrence projected-formula-0019129

Equation form expr-497d497fc35ba36e

$!Q_1$

Read as: Q subscript one

Means: Q subscript one

2 occurrences in this chapter

• Occurrence projected-formula-0019314
• Occurrence projected-formula-0019333

Equation form expr-49f23caa2a921188

$!A_f(\num{n}, b)$

Read as: A subscript f of the numeral for n and b

Means: A subscript f of the numeral for n and b

1 occurrence in this chapter

• Occurrence projected-formula-0019422

Equation form expr-4ad9c626769fce17

$A(n_0, \dots, n_k, m) = \\ \fn{Subst}(\fn{Subst}(\dots\fn{Subst}(\Gn{!A_f}, \fn{num}(n_0), \Gn{x_0}),\\ \dots), \fn{num}(n_k), \Gn{x_k}), \fn{num}(m), \Gn{y})$

Read as: A of n subscript zero through n subscript k, and m, equals the result of these nested calls to the substitution coding function Subst. Start with the Goedel number of A subscript f. Substitute the numeral code num of n subscript zero for the variable code of x subscript zero. Continue in order through substitution of num of n subscript k for the variable code of x subscript k. Finally substitute num of m for the variable code of y. Each call takes the current formula code, the replacement numeral code, and the selected variable code, in that order

Means: A of n subscript zero through n subscript k, and m, equals the result of these nested calls to the substitution coding function Subst. Start with the Goedel number of A subscript f. Substitute the numeral code num of n subscript zero for the variable code of x subscript zero. Continue in order through substitution of num of n subscript k for the variable code of x subscript k. Finally substitute num of m for the variable code of y. Each call takes the current formula code, the replacement numeral code, and the selected variable code, in that order

1 occurrence in this chapter

• Occurrence projected-formula-0018857

Equation form expr-4ae81572f06e1b88

$Q$

Read as: Q

Means: Q

1 occurrence in this chapter

• Occurrence projected-formula-0018770

Equation form expr-4c9998b6a2629683

$\Th{Q} \Proves \eq[\num n][\num m]$

Read as: Q proves that the numeral for n equals the numeral for m

Means: Q proves that the numeral for n equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019641

Equation form expr-4dc4e01def696af8

$\Proj{n}{i}$

Read as: the n argument projection function with index i

Means: the n argument projection function with index i

6 occurrences in this chapter

• Occurrence projected-formula-0018817
• Occurrence projected-formula-0019010
• Occurrence projected-formula-0019055
• Occurrence projected-formula-0019442
• Occurrence projected-formula-0019450
• Occurrence projected-formula-0019456

Equation form expr-4e01c892379ba40e

$a_0,\dots,a_n$

Read as: a subscript zero through a subscript n

Means: a subscript zero through a subscript n

2 occurrences in this chapter

• Occurrence projected-formula-0018971
• Occurrence projected-formula-0018977

Equation form expr-4f0f1e4a3167d257

$x_i$

Read as: x subscript i

Means: x subscript i

2 occurrences in this chapter

• Occurrence projected-formula-0018927
• Occurrence projected-formula-0018956

Equation form expr-4fc68cff6de5c66b

$\Th{Q} \Proves \eq[t_1'][\num{n_1 + 1}]$

Read as: Q proves that the successor of t subscript one equals the numeral for n subscript one plus one

Means: Q proves that the successor of t subscript one equals the numeral for n subscript one plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019612

Equation form expr-5081cbc657fe24bd

$\num{m}$

Read as: the numeral for m

Means: the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019102

Equation form expr-50f6f70226bbab06

$\eq[(\num{n} + \num{m})][y]$

Read as: the sum of the numeral for n and the numeral for m equals y

Means: the sum of the numeral for n and the numeral for m equals y

1 occurrence in this chapter

• Occurrence projected-formula-0019154

Equation form expr-511e94877bb38a7b

$\num 0 \ident \Obj 0$

Read as: the numeral for zero is the object language constant zero

Means: the numeral for zero is the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019602

Equation form expr-5160b22457af7ef4

$f(n_0,\dots,n_{k}) = (\umin{s}{R(n_0, \dots, n_k, s)})_1.$

Read as: f of n subscript zero through n subscript k equals the entry at position one in the prime power sequence whose code is the least s such that R holds of n subscript zero through n subscript k, and s

Means: f of n subscript zero through n subscript k equals the entry at position one in the prime power sequence whose code is the least s such that R holds of n subscript zero through n subscript k, and s

1 occurrence in this chapter

• Occurrence projected-formula-0018882

Equation form expr-523e00ddd2c165db

$\eq[\num{n}][\num{n}]$

Read as: the numeral for n equals the numeral for n

Means: the numeral for n equals the numeral for n

1 occurrence in this chapter

• Occurrence projected-formula-0019116

Equation form expr-5280c8f9e471df51

$\ltrue$

Read as: truth

Means: truth

1 occurrence in this chapter

• Occurrence projected-formula-0019691

Equation form expr-534b34da02a3744c

$\eq[(b' + \Obj 0)][(a + \Obj 0)]$

Read as: the sum of the successor of b and the object language constant zero equals the sum of a and the object language constant zero

Means: the sum of the successor of b and the object language constant zero equals the sum of a and the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019353

Equation form expr-539a22491471bd29

$x_0,\dots,x_n$

Read as: x subscript zero through x subscript n

Means: x subscript zero through x subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0018934

Equation form expr-54e5cc297fef9e74

$(!A(\Obj 0) \land \lforall[x][(!A(x) \lif !A(x'))]) \lif \lforall[x][!A(x)]$

Read as: If both A holds of the object language constant zero, and for every x, A of x implies A of the successor of x, then A holds of every x

Means: If both A holds of the object language constant zero, and for every x, A of x implies A of the successor of x, then A holds of every x

1 occurrence in this chapter

• Occurrence projected-formula-0018795

Equation form expr-55154da3ffef0cbc

$\Th{Q} \Proves \eq/[\num n][\num k]$

Read as: Q proves that the numeral for n does not equal the numeral for k

Means: Q proves that the numeral for n does not equal the numeral for k

1 occurrence in this chapter

• Occurrence projected-formula-0019088

Equation form expr-553c7c9c2360e2c5

$!A_g$

Read as: A subscript g

Means: A subscript g

1 occurrence in this chapter

• Occurrence projected-formula-0019433

Equation form expr-5553c013c717e9a8

$!Q_5$

Read as: Q subscript five

Means: Q subscript five

8 occurrences in this chapter

• Occurrence projected-formula-0019138
• Occurrence projected-formula-0019289
• Occurrence projected-formula-0019311
• Occurrence projected-formula-0019331
• Occurrence projected-formula-0019382
• Occurrence projected-formula-0019397
• Occurrence projected-formula-0019671
• Occurrence projected-formula-0019678

Equation form expr-55ac8244d52de7d0

$i-k$

Read as: i minus k

Means: i minus k

1 occurrence in this chapter

• Occurrence projected-formula-0018949

Equation form expr-57953c2c25755935

$\lforall[y][(!A_f(\num{n_0}, \dots, \num{n_k}, y) \liff \eq[y][\num{m}])]$

Read as: for every y, A subscript f holds of the numerals for n subscript zero through n subscript k, and y, if and only if y equals the numeral for m

Means: for every y, A subscript f holds of the numerals for n subscript zero through n subscript k, and y, if and only if y equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0018812

Equation form expr-57aca383a1921bbe

$\Char{=}(n, m) = 1$

Read as: the characteristic function of equality applied to n and m equals one

Means: the characteristic function of equality applied to n and m equals one

1 occurrence in this chapter

• Occurrence projected-formula-0019103

Equation form expr-5810ea365f11a260

$\Char{R}(n_0, \dots, n_k) = 0$

Read as: the characteristic function of R applied to n subscript zero through n subscript k equals zero

Means: the characteristic function of R applied to n subscript zero through n subscript k equals zero

1 occurrence in this chapter

• Occurrence projected-formula-0019497

Equation form expr-58c0b6979bc3f4c1

$\eq[y][x']$

Read as: y equals the successor of x

Means: y equals the successor of x

1 occurrence in this chapter

• Occurrence projected-formula-0019051

Equation form expr-58ee3d3914bcad7c

$\eq[a][\Obj 0]$

Read as: a equals the object language constant zero

Means: a equals the object language constant zero

6 occurrences in this chapter

• Occurrence projected-formula-0019277
• Occurrence projected-formula-0019304
• Occurrence projected-formula-0019306
• Occurrence projected-formula-0019322
• Occurrence projected-formula-0019348
• Occurrence projected-formula-0019367

Equation form expr-594e519ae499312b

$z$

Read as: z

Means: z

6 occurrences in this chapter

• Occurrence projected-formula-0018917
• Occurrence projected-formula-0018923
• Occurrence projected-formula-0018926
• Occurrence projected-formula-0019245
• Occurrence projected-formula-0019394
• Occurrence projected-formula-0019665

Equation form expr-59c3bcebf9d9b194

$\eq[a][\Obj 0] \lor \lexists[y][\eq[a][y']]$

Read as: either a equals the object language constant zero, or there exists y such that a is the successor of y

Means: either a equals the object language constant zero, or there exists y such that a is the successor of y

1 occurrence in this chapter

• Occurrence projected-formula-0019276

Equation form expr-5afa20230f875253

$n \in \Nat$

Read as: n is a natural number

Means: n is a natural number

1 occurrence in this chapter

• Occurrence projected-formula-0019541

Equation form expr-5b63a60fdb499c3a

$\Struct{N}$

Read as: the standard model N

Means: the standard model N

22 occurrences in this chapter

• Occurrence projected-formula-0019265
• Occurrence projected-formula-0019544
• Occurrence projected-formula-0019576
• Occurrence projected-formula-0019711
• Occurrence projected-formula-0019714
• Occurrence projected-formula-0019717
• Occurrence projected-formula-0019722
• Occurrence projected-formula-0019725
• Occurrence projected-formula-0019729
• Occurrence projected-formula-0019731
• Occurrence projected-formula-0019733
• Occurrence projected-formula-0019737
• Occurrence projected-formula-0019740
• Occurrence projected-formula-0019745
• Occurrence projected-formula-0019749
• Occurrence projected-formula-0019755
• Occurrence projected-formula-0019760
• Occurrence projected-formula-0019765
• Occurrence projected-formula-0019775
• Occurrence projected-formula-0019777
• Occurrence projected-formula-0019781
• Occurrence projected-formula-0019785

Equation form expr-5bea4caf3b95f01e

$f(x_0,\dots,x_{k-1})$

Read as: f of x subscript zero through x subscript k minus one

Means: f of x subscript zero through x subscript k minus one

1 occurrence in this chapter

• Occurrence projected-formula-0019031

Equation form expr-5c37345158ceafa2

$c'$

Read as: the successor of c

Means: the successor of c

1 occurrence in this chapter

• Occurrence projected-formula-0019386

Equation form expr-5d08324acb961fcf

$t_2$

Read as: t subscript two

Means: t subscript two

3 occurrences in this chapter

• Occurrence projected-formula-0019604
• Occurrence projected-formula-0019624
• Occurrence projected-formula-0019634

Equation form expr-5f8d517bbaf86a44

$m = f(n)$

Read as: m equals f of n

Means: m equals f of n

1 occurrence in this chapter

• Occurrence projected-formula-0019430

Equation form expr-5fe6dc6b2281b3d2

$\Zero$

Read as: the zero function

Means: the zero function

6 occurrences in this chapter

• Occurrence projected-formula-0018815
• Occurrence projected-formula-0019008
• Occurrence projected-formula-0019053
• Occurrence projected-formula-0019440
• Occurrence projected-formula-0019448
• Occurrence projected-formula-0019454

Equation form expr-5feceb66ffc86f38

$0$

Read as: zero

Means: zero

3 occurrences in this chapter

• Occurrence projected-formula-0018960
• Occurrence projected-formula-0018991
• Occurrence projected-formula-0019070

Equation form expr-6009a1b65f58066f

$!A \ident t_1 = t_2$

Read as: A is the formula t subscript one equals t subscript two

Means: A is the formula t subscript one equals t subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019637

Equation form expr-607df55404d282ad

$\eq[y][x_i]$

Read as: y equals x subscript i

Means: y equals x subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0019052

Equation form expr-613f9747239d288b

$\eq[(c'+b)'][\num{n+1}']$

Read as: the successor of the sum of the successor of c and b equals the successor of the numeral for n plus one

Means: the successor of the sum of the successor of c and b equals the successor of the numeral for n plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019332

Equation form expr-61d2d6985fbd6781

$\Proj{n}{i}(x_0, \dots, x_{n-1}) = x_i$

Read as: the n argument projection function with index i, applied to x subscript zero through x subscript n minus one, equals x subscript i

Means: the n argument projection function with index i, applied to x subscript zero through x subscript n minus one, equals x subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0019047

Equation form expr-620d2aa6c7003f41

$!A_h$

Read as: A subscript h

Means: A subscript h

1 occurrence in this chapter

• Occurrence projected-formula-0019182

Equation form expr-62c66a7a5dd70c31

$m$

Read as: m

Means: m

13 occurrences in this chapter

• Occurrence projected-formula-0018872
• Occurrence projected-formula-0018946
• Occurrence projected-formula-0019037
• Occurrence projected-formula-0019061
• Occurrence projected-formula-0019065
• Occurrence projected-formula-0019069
• Occurrence projected-formula-0019081
• Occurrence projected-formula-0019127
• Occurrence projected-formula-0019131
• Occurrence projected-formula-0019341
• Occurrence projected-formula-0019343
• Occurrence projected-formula-0019407
• Occurrence projected-formula-0019670

Equation form expr-630bea13ff0c157d

$\eq[(b'+a)][\Obj 0']$

Read as: the sum of the successor of b and a equals the successor of the object language constant zero

Means: the sum of the successor of b and a equals the successor of the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019303

Equation form expr-63cf3cedc3938049

$!A_=(\num{n}, \num{m}, y)$

Read as: A subscript equality applied to the numerals for n and m, and y

Means: A subscript equality applied to the numerals for n and m, and y

2 occurrences in this chapter

• Occurrence projected-formula-0019113
• Occurrence projected-formula-0019118

Equation form expr-642a159103b087da

$\eq/[0][\num k']$

Read as: zero does not equal the successor of the numeral for k

Means: zero does not equal the successor of the numeral for k

1 occurrence in this chapter

• Occurrence projected-formula-0019076

Equation form expr-675020bea20828e6

$!A_f, !A_{g_0}, \dots, !A_{g_{k-1}}$

Read as: A subscript f, and A subscript g subscript zero through A subscript g subscript k minus one

Means: A subscript f, and A subscript g subscript zero through A subscript g subscript k minus one

1 occurrence in this chapter

• Occurrence projected-formula-0019178

Equation form expr-67d70b7414d21313

$\Th{Q} \Proves t_1 < t_2$

Read as: Q proves that t subscript one is less than t subscript two

Means: Q proves that t subscript one is less than t subscript two

2 occurrences in this chapter

• Occurrence projected-formula-0019630
• Occurrence projected-formula-0019659

Equation form expr-67eceadb93cd5af9

$\Value{t_1}{N} = n_1$

Read as: the value of t subscript one in the standard model N equals n subscript one

Means: the value of t subscript one in the standard model N equals n subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0019605

Equation form expr-686820eb63ee5ceb

$\Add(x_0, x_1) = x_0+x_1$

Read as: the addition function applied to x subscript zero and x subscript one equals the sum of x subscript zero and x subscript one

Means: the addition function applied to x subscript zero and x subscript one equals the sum of x subscript zero and x subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0019123

Equation form expr-68f9f7b7f15365cc

$!A_R(\num{n_0}, \dots, \num{n_k})$

Read as: A subscript R applied to the numerals for n subscript zero through n subscript k

Means: A subscript R applied to the numerals for n subscript zero through n subscript k

2 occurrences in this chapter

• Occurrence projected-formula-0019480
• Occurrence projected-formula-0019495

Equation form expr-6a67af47077a19dd

$\Th{Q} \Proves \lforall[y][(!A_\Add(\num{n}, \num{m}, y) \lif \eq[y][\num{k}])].$

Read as: Q proves that for every y, if A subscript Add holds of the numeral for n, the numeral for m, and y, then y equals the numeral for k

Means: Q proves that for every y, if A subscript Add holds of the numeral for n, the numeral for m, and y, then y equals the numeral for k

1 occurrence in this chapter

• Occurrence projected-formula-0019153

Equation form expr-6a766438d1de2cc9

$n+m$

Read as: n plus m

Means: n plus m

2 occurrences in this chapter

• Occurrence projected-formula-0019172
• Occurrence projected-formula-0019174

Equation form expr-6a85c216edb611d1

$\Th{Q} \Proves !A$

Read as: Q proves that A

Means: Q proves that A

7 occurrences in this chapter

• Occurrence projected-formula-0019515
• Occurrence projected-formula-0019560
• Occurrence projected-formula-0019577
• Occurrence projected-formula-0019712
• Occurrence projected-formula-0019718
• Occurrence projected-formula-0019734
• Occurrence projected-formula-0019782

Equation form expr-6aff617426baec7a

$\tuple{a_0, \dots, a_n}$

Read as: the sequence a subscript zero through a subscript n

Means: the sequence a subscript zero through a subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0018893

Equation form expr-6b81665d4120803d

$\Th{Q} \Proves \lforall[y][(!A_h(\num n, y) \lif \eq[y][\num m])]$

Read as: Q proves that for every y, if A subscript h holds of the numeral for n and y, then y equals the numeral for m

Means: Q proves that for every y, if A subscript h holds of the numeral for n and y, then y equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019219

Equation form expr-6b86b273ff34fce1

$1$

Read as: one

Means: one

4 occurrences in this chapter

• Occurrence projected-formula-0018904
• Occurrence projected-formula-0018947
• Occurrence projected-formula-0019184
• Occurrence projected-formula-0019222

Equation form expr-6c5efc1231f47515

$z = f(g(x))$

Read as: z equals f of g of x

Means: z equals f of g of x

1 occurrence in this chapter

• Occurrence projected-formula-0019202

Equation form expr-6cd9609ccf118909

$\num{n+m}'$

Read as: the successor of the numeral for n plus m

Means: the successor of the numeral for n plus m

1 occurrence in this chapter

• Occurrence projected-formula-0019137

Equation form expr-6d64cdb17c30935b

$1+(n+1) d_1$

Read as: one plus the product of n plus one and d subscript one

Means: one plus the product of n plus one and d subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0018976

Equation form expr-6d7097da4387177a

$a_i$

Read as: a subscript i

Means: a subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0018982

Equation form expr-6e601bf84d5d4eda

$!A_{\Char{R}}(x_0, \dots, x_k, \num{1})$

Read as: A subscript characteristic function of R, applied to x subscript zero through x subscript k, and the numeral for one

Means: A subscript characteristic function of R, applied to x subscript zero through x subscript k, and the numeral for one

1 occurrence in this chapter

• Occurrence projected-formula-0019487

Equation form expr-6ee3034ebd427cec

$g(x, z) = 0$

Read as: g of x and z equals zero

Means: g of x and z equals zero

1 occurrence in this chapter

• Occurrence projected-formula-0019241

Equation form expr-6f7ced04d6bee707

$\lnot \lexists[y][\eq[(y'+a)][\Obj 0]]$

Read as: there does not exist y such that the sum of the successor of y and a equals the object language constant zero

Means: there does not exist y such that the sum of the successor of y and a equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019271

Equation form expr-70514654ed0ce01b

$\num{m}'$

Read as: the successor of the numeral for m

Means: the successor of the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019135

Equation form expr-7199461c674714a8

$\eq[y][\Obj 0]$

Read as: y equals the object language constant zero

Means: y equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019050

Equation form expr-71c45e53665b252d

$\Th{Q} \Proves \eq[t][\num n]$

Read as: Q proves that t equals the numeral for n

Means: Q proves that t equals the numeral for n

2 occurrences in this chapter

• Occurrence projected-formula-0019598
• Occurrence projected-formula-0019619

Equation form expr-722f97d7125f3aac

$\lnot !A_g(b, \num{n}, \Obj 0)$

Read as: not A subscript g of b, the numeral for n, and the object language constant zero

Means: not A subscript g of b, the numeral for n, and the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019437

Equation form expr-72fcd7dafa1f7007

$\num{n+1}$

Read as: the numeral for n plus one

Means: the numeral for n plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019258

Equation form expr-72fe42cd2b8d2e97

$\eq/[\num{n}][\num{m}]$

Read as: the numeral for n does not equal the numeral for m

Means: the numeral for n does not equal the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019120

Equation form expr-73353f7ce9a444a4

$!A_f(y_0, \dots, y_{k-1}, z)$

Read as: A subscript f applied to y subscript zero through y subscript k minus one, and z

Means: A subscript f applied to y subscript zero through y subscript k minus one, and z

1 occurrence in this chapter

• Occurrence projected-formula-0019223

Equation form expr-7338240bcff9771d

$\num k'$

Read as: the successor of the numeral for k

Means: the successor of the numeral for k

2 occurrences in this chapter

• Occurrence projected-formula-0019077
• Occurrence projected-formula-0019094

Equation form expr-735c7fab3bc7df2a

$\Th{Q} & \Proves \lforall[y][((y < \num{m} \lor \num{m} < y) \lor \eq[y][\num{m}])] \intertext{and we want to show} \Th{Q} & \Proves \lforall[y][((y < \num{m+1} \lor \num{m+1} < y) \lor \eq[y][\num{m+1}])]$

Read as: Assume Q proves: for every y, either y is less than the numeral for m, or the numeral for m is less than y, or y equals the numeral for m. We want to show that Q proves: for every y, either y is less than the numeral for m plus one, or that numeral is less than y, or y equals that numeral

Means: Assume Q proves: for every y, either y is less than the numeral for m, or the numeral for m is less than y, or y equals the numeral for m. We want to show that Q proves: for every y, either y is less than the numeral for m plus one, or that numeral is less than y, or y equals that numeral

1 occurrence in this chapter

• Occurrence projected-formula-0019364

Equation form expr-73a9aa343d96822e

$(\Obj 0 < a \lor a < \Obj 0) \lor \eq[a][\Obj 0]$

Read as: either the object language constant zero is less than a, or a is less than that constant, or a equals that constant

Means: either the object language constant zero is less than a, or a is less than that constant, or a equals that constant

1 occurrence in this chapter

• Occurrence projected-formula-0019363

Equation form expr-73ad6360c4b0473c

$\Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{f(n_0, \dots, n_k)})$

Read as: Q proves that A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for the value of f at n subscript zero through n subscript k

Means: Q proves that A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for the value of f at n subscript zero through n subscript k

2 occurrences in this chapter

• Occurrence projected-formula-0018847
• Occurrence projected-formula-0018878

Equation form expr-7485ac02a69c12f0

$\Th{Q} & \Proves !A_g(\num{n}, \num{k}) \intertext{since $!A_g$ represents~$g$, and} \Th{Q} & \Proves !A_f(\num{k}, \num{m}) \intertext{since $!A_f$ represents~$f$. Thus,} \Th{Q} & \Proves !A_g(\num{n}, \num{k}) \land !A_f(\num{k}, \num{m}) \intertext{and consequently also} \Th{Q} & \Proves \lexists[y][(!A_g(\num{n}, y) \land !A_f(y, \num{m}))],$

Read as: Q proves A subscript g of the numeral for n and the numeral for k, since A subscript g represents g. And Q proves A subscript f of the numeral for k and the numeral for m, since A subscript f represents f. Thus Q proves their conjunction. Consequently Q also proves that there exists y such that both A subscript g of the numeral for n and y, and A subscript f of y and the numeral for m

Means: Q proves A subscript g of the numeral for n and the numeral for k, since A subscript g represents g. And Q proves A subscript f of the numeral for k and the numeral for m, since A subscript f represents f. Thus Q proves their conjunction. Consequently Q also proves that there exists y such that both A subscript g of the numeral for n and y, and A subscript f of y and the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019211

Equation form expr-74c0e74537bf75aa

$& \lforall[x][\lforall[y][(\eq[x'][y'] \lif \eq[x][y])]] \tag{$!Q_1$}\\ & \lforall[x][\eq/[\Obj 0][x']] \tag{$!Q_2$}\\ & \lforall[x][(\eq[x][\Obj 0] \lor \lexists[y][\eq[x][y']])] \tag{$!Q_3$}\\ & \lforall[x][\eq[(x + \Obj 0)][x]] \tag{$!Q_4$}\\ & \lforall[x][\lforall[y][\eq[(x + y')][(x + y)']]] \tag{$!Q_5$}\\ & \lforall[x][\eq[(x \times \Obj 0)][\Obj 0]] \tag{$!Q_6$}\\ & \lforall[x][\lforall[y][\eq[(x \times y')][((x \times y) + x)]]] \tag{$!Q_7$}\\ & \lforall[x][\lforall[y][(x < y \liff \lexists[z][\eq[(z' + x)][y]])]] \tag{$!Q_8$}$

Read as: Eight axioms for Q. Q subscript one: for all x and y, if the successor of x equals the successor of y, then x equals y. Q subscript two: for every x, the object language constant zero does not equal the successor of x. Q subscript three: for every x, either x equals the object language constant zero, or there exists y such that x equals the successor of y. Q subscript four: for every x, the sum of x and the object language constant zero equals x. Q subscript five: for all x and y, the sum of x and the successor of y equals the successor of the sum of x and y. Q subscript six: for every x, the object language product of x and the constant zero equals that constant zero. Q subscript seven: for all x and y, the object language product of x and the successor of y equals the sum of the object language product of x and y, and x. Q subscript eight: for all x and y, x is less than y if and only if there exists z such that the sum of the successor of z and x equals y. End of the eight axioms.

Means: Eight axioms for Q. Q subscript one: for all x and y, if the successor of x equals the successor of y, then x equals y. Q subscript two: for every x, the object language constant zero does not equal the successor of x. Q subscript three: for every x, either x equals the object language constant zero, or there exists y such that x equals the successor of y. Q subscript four: for every x, the sum of x and the object language constant zero equals x. Q subscript five: for all x and y, the sum of x and the successor of y equals the successor of the sum of x and y. Q subscript six: for every x, the object language product of x and the constant zero equals that constant zero. Q subscript seven: for all x and y, the object language product of x and the successor of y equals the sum of the object language product of x and y, and x. Q subscript eight: for all x and y, x is less than y if and only if there exists z such that the sum of the successor of z and x equals y. End of the eight axioms.

1 occurrence in this chapter

• Occurrence projected-formula-0018776

Equation form expr-74e0eb883b673576

$z_k$

Read as: z subscript k

Means: z subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0019247

Equation form expr-74f4567a6896230a

$\eq$

Read as: the equality symbol

Means: the equality symbol

1 occurrence in this chapter

• Occurrence projected-formula-0019354

Equation form expr-74fff1f3fc3ccc0c

$\eq[\num{m}' + a][\num{m+1}]$

Read as: the sum of the successor of the numeral for m and a equals the numeral for m plus one

Means: the sum of the successor of the numeral for m and a equals the numeral for m plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019370

Equation form expr-754fcd9ec52e8861

$d = J(d_0,d_1)$

Read as: d equals J of d subscript zero and d subscript one

Means: d equals J of d subscript zero and d subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0018984

Equation form expr-75ed6f448c24d8db

$k = n + m$

Read as: k equals n plus m

Means: k equals n plus m

1 occurrence in this chapter

• Occurrence projected-formula-0019148

Equation form expr-765c65ac668314de

$\lnot !A_g(\num{m}, \num{n}, \Obj 0)$

Read as: not A subscript g of the numeral for m, the numeral for n, and the object language constant zero

Means: not A subscript g of the numeral for m, the numeral for n, and the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019429

Equation form expr-76611dd34d50f93b

$f(n) = m$

Read as: f of n equals m

Means: f of n equals m

2 occurrences in this chapter

• Occurrence projected-formula-0019416
• Occurrence projected-formula-0019420

Equation form expr-76690a2632c6c282

$!A(x_0, \dots, x_k, y)$

Read as: A applied to x subscript zero through x subscript k, and y

Means: A applied to x subscript zero through x subscript k, and y

1 occurrence in this chapter

• Occurrence projected-formula-0018826

Equation form expr-76cbfc0766d6c646

$b' < \num{m+1}$

Read as: the successor of b is less than the numeral for m plus one

Means: the successor of b is less than the numeral for m plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019389

Equation form expr-7778045033568a46

$\Th{Q} \Proves !A_f(\num{n_0}, \dots, \num{n_k}, \num{l})$

Read as: Q proves that A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for l

Means: Q proves that A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for l

1 occurrence in this chapter

• Occurrence projected-formula-0018831

Equation form expr-77ece9c7795ab0b2

$\lexists[z][\eq[(z' + \num{m})][b]]$

Read as: there exists z such that the sum of the successor of z and the numeral for m equals b

Means: there exists z such that the sum of the successor of z and the numeral for m equals b

1 occurrence in this chapter

• Occurrence projected-formula-0019392

Equation form expr-77f918d83ed74656

$\eq[\num{n+m}][y]$

Read as: the numeral for n plus m equals y

Means: the numeral for n plus m equals y

1 occurrence in this chapter

• Occurrence projected-formula-0019157

Equation form expr-783819f2e7b1882c

$\Sat{N}{\Th{Q}}$

Read as: the standard model N satisfies Q

Means: the standard model N satisfies Q

1 occurrence in this chapter

• Occurrence projected-formula-0018838

Equation form expr-792de17cc1ae3441

$!A_{g_i}(x_0, \dots, x_{l-1}, y)$

Read as: A subscript g subscript i applied to x subscript zero through x subscript l minus one, and y

Means: A subscript g subscript i applied to x subscript zero through x subscript l minus one, and y

1 occurrence in this chapter

• Occurrence projected-formula-0019226

Equation form expr-7a5bbe0fc2709653

$\eq[(c' + \num{m})][b]$

Read as: the sum of the successor of c and the numeral for m equals b

Means: the sum of the successor of c and the numeral for m equals b

1 occurrence in this chapter

• Occurrence projected-formula-0019395

Equation form expr-7b8ba390a71f512b

$\Zero(x) = 0$

Read as: the zero function applied to x equals zero

Means: the zero function applied to x equals zero

1 occurrence in this chapter

• Occurrence projected-formula-0019041

Equation form expr-7d282b412739ae71

$(a < \Obj 0 \lor \Obj 0 < a) \lor \eq[a][\Obj 0]$

Read as: either a is less than the object language constant zero, or that constant is less than a, or a equals that constant

Means: either a is less than the object language constant zero, or that constant is less than a, or a equals that constant

1 occurrence in this chapter

• Occurrence projected-formula-0019351

Equation form expr-7d5aa605dde1dd9d

$\Th{Q} \Proves !A(\num 0) \land \dots \land !A(\num{k-1})$

Read as: Q proves that the finite conjunction of A applied to each numeral from zero through k minus one

Means: Q proves that the finite conjunction of A applied to each numeral from zero through k minus one

2 occurrences in this chapter

• Occurrence projected-formula-0019685
• Occurrence projected-formula-0019751

Equation form expr-7d7a67425bb66671

$\Proves !T \lif !A$

Read as: the implication from T to A is provable with no nonlogical premises

Means: the implication from T to A is provable with no nonlogical premises

1 occurrence in this chapter

• Occurrence projected-formula-0019561

Equation form expr-7d7eadee71a7e564

$m+1$

Read as: m plus one

Means: m plus one

2 occurrences in this chapter

• Occurrence projected-formula-0019132
• Occurrence projected-formula-0019409

Equation form expr-7dd2e78c28fc35bf

$m = k+1$

Read as: m equals k plus one

Means: m equals k plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019084

Equation form expr-7e2770a26fc50a59

$w < x$

Read as: w is less than x

Means: w is less than x

1 occurrence in this chapter

• Occurrence projected-formula-0019242

Equation form expr-7f024b2d7f1db4d4

$\num{n}$

Read as: the numeral for n

Means: the numeral for n

2 occurrences in this chapter

• Occurrence projected-formula-0018778
• Occurrence projected-formula-0019101

Equation form expr-801318c363bd13ba

$b < \num{m}$

Read as: b is less than the numeral for m

Means: b is less than the numeral for m

4 occurrences in this chapter

• Occurrence projected-formula-0019376
• Occurrence projected-formula-0019388
• Occurrence projected-formula-0019426
• Occurrence projected-formula-0019435

Equation form expr-8022b4c1dd18ddb5

$\Value{t_1}{N} \neq \Value{t_2}{N}$

Read as: the value of t subscript one in the standard model N does not equal the value of t subscript two in the standard model N

Means: the value of t subscript one in the standard model N does not equal the value of t subscript two in the standard model N

1 occurrence in this chapter

• Occurrence projected-formula-0019627

Equation form expr-8071422cd3693781

$\Th{Q} \Proves \bexists{x<t}{!A(x)}$

Read as: Q proves that there exists x less than t such that A of x

Means: Q proves that there exists x less than t such that A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019686

Equation form expr-80b17a5f996cbf72

$!A_f(x_0,\dots,x_k,y)$

Read as: A subscript f applied to x subscript zero through x subscript k, and y

Means: A subscript f applied to x subscript zero through x subscript k, and y

1 occurrence in this chapter

• Occurrence projected-formula-0018806

Equation form expr-80fce15b99d444a5

$\Th{Q} \Proves \eq/[\num{n}][\num{m}]$

Read as: Q proves that the numeral for n does not equal the numeral for m

Means: Q proves that the numeral for n does not equal the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019108

Equation form expr-81aa5a490db29cc9

$!A(x)$

Read as: A of x

Means: A of x

3 occurrences in this chapter

• Occurrence projected-formula-0018796
• Occurrence projected-formula-0018797
• Occurrence projected-formula-0019707

Equation form expr-8238c028f61fc0f7

$!A$

Read as: A

Means: A

13 occurrences in this chapter

• Occurrence projected-formula-0019510
• Occurrence projected-formula-0019511
• Occurrence projected-formula-0019514
• Occurrence projected-formula-0019574
• Occurrence projected-formula-0019586
• Occurrence projected-formula-0019591
• Occurrence projected-formula-0019681
• Occurrence projected-formula-0019709
• Occurrence projected-formula-0019715
• Occurrence projected-formula-0019730
• Occurrence projected-formula-0019766
• Occurrence projected-formula-0019770
• Occurrence projected-formula-0019779

Equation form expr-8254c329a92850f6

$k$

Read as: k

Means: k

4 occurrences in this chapter

• Occurrence projected-formula-0019030
• Occurrence projected-formula-0019072
• Occurrence projected-formula-0019083
• Occurrence projected-formula-0019694

Equation form expr-8288accffcbf319e

$g(m, n) = 0$

Read as: g of m and n equals zero

Means: g of m and n equals zero

1 occurrence in this chapter

• Occurrence projected-formula-0019431

Equation form expr-83c29a4e8dc685fc

$1 + (i+1)m$

Read as: one plus the product of i plus one and m

Means: one plus the product of i plus one and m

1 occurrence in this chapter

• Occurrence projected-formula-0018945

Equation form expr-83ffd5dcb893e03c

$\eq[(c' + b)'][(c' + b')]$

Read as: the successor of the sum of the successor of c and b equals the sum of the successor of c and the successor of b

Means: the successor of the sum of the successor of c and b equals the sum of the successor of c and the successor of b

1 occurrence in this chapter

• Occurrence projected-formula-0019383

Equation form expr-841c7796b253f8c4

$\Char=(n, m) = 0$

Read as: the characteristic function of equality applied to n and m equals zero

Means: the characteristic function of equality applied to n and m equals zero

1 occurrence in this chapter

• Occurrence projected-formula-0019107

Equation form expr-84c4519d1afda28e

$\Th{Q} \Proves \eq[(\num{n} + \num{m+1})][\num{n+m+1}]$

Read as: Q proves that the sum of the numeral for n and the numeral for m plus one equals the numeral for n plus m plus one

Means: Q proves that the sum of the numeral for n and the numeral for m plus one equals the numeral for n plus m plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019133

Equation form expr-866007381d5c48a8

$d_1$

Read as: d subscript one

Means: d subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0018981

Equation form expr-86bc40a9dfa0a3bf

$d_0$

Read as: d subscript zero

Means: d subscript zero

1 occurrence in this chapter

• Occurrence projected-formula-0018978

Equation form expr-86c174ef8f52728a

$\Th{Q} \Proves/ \lexists[y][!B_T(\num{e}, \num{n}, y)]$

Read as: Q does not prove that there exists y such that B subscript T holds of the numeral for e, the numeral for n, and y

Means: Q does not prove that there exists y such that B subscript T holds of the numeral for e, the numeral for n, and y

1 occurrence in this chapter

• Occurrence projected-formula-0019545

Equation form expr-86d0ea318fb5f9be

$R(n_0, \dots, n_k, s) \quad\text{iff}\quad \Prf[\Th{Q}]((s)_0, A(n_0, \dots, n_k, (s)_1))$

Read as: R holds of n subscript zero through n subscript k, and s, if and only if the entry at position zero in the prime power sequence coded by s is a derivation code in Q for the formula with code A of n subscript zero through n subscript k, and the entry at position one in that sequence

Means: R holds of n subscript zero through n subscript k, and s, if and only if the entry at position zero in the prime power sequence coded by s is a derivation code in Q for the formula with code A of n subscript zero through n subscript k, and the entry at position one in that sequence

1 occurrence in this chapter

• Occurrence projected-formula-0018863

Equation form expr-8779068734acaece

$\cdot$

Read as: the numerical multiplication operation

Means: the numerical multiplication operation

2 occurrences in this chapter

• Occurrence projected-formula-0019164
• Occurrence projected-formula-0019165

Equation form expr-87cc3fc5bd5779da

$\Th{Q} \Proves \eq[t_2][\num m]$

Read as: Q proves that t subscript two equals the numeral for m

Means: Q proves that t subscript two equals the numeral for m

2 occurrences in this chapter

• Occurrence projected-formula-0019654
• Occurrence projected-formula-0019668

Equation form expr-88a51162b7219690

$(s)_0$

Read as: the entry at position zero in the prime power sequence coded by s

Means: the entry at position zero in the prime power sequence coded by s

3 occurrences in this chapter

• Occurrence projected-formula-0018860
• Occurrence projected-formula-0018866
• Occurrence projected-formula-0018868

Equation form expr-893489f0e6d4eb45

$\Sat{N}{t_1 < t_2}$

Read as: in the standard model N, t subscript one is less than t subscript two

Means: in the standard model N, t subscript one is less than t subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019650

Equation form expr-8a08932817a94ba5

$b < \num{n+1}$

Read as: b is less than the numeral for n plus one

Means: b is less than the numeral for n plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019335

Equation form expr-8a15984a78d67748

$\Value{t_1}{N} = \Value{t_2}{N}$

Read as: the value of t subscript one in the standard model N equals the value of t subscript two in the standard model N

Means: the value of t subscript one in the standard model N equals the value of t subscript two in the standard model N

1 occurrence in this chapter

• Occurrence projected-formula-0019625

Equation form expr-8a4fc85668fc8882

$p \mid x_k$

Read as: p divides x subscript k

Means: p divides x subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0018939

Equation form expr-8ab9ee2cb0c96a7a

$\eq[(b' + \Obj 0)][\Obj 0]$

Read as: the sum of the successor of b and the object language constant zero equals the object language constant zero

Means: the sum of the successor of b and the object language constant zero equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019279

Equation form expr-8abffd0e59bff9dd

$!A_R(\num{n_0},\dots,\num{n_k})$

Read as: A subscript R applied to the numerals for n subscript zero through n subscript k

Means: A subscript R applied to the numerals for n subscript zero through n subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0019470

Equation form expr-8b2aa30dd4cbfbef

$p \mid m$

Read as: p divides m

Means: p divides m

1 occurrence in this chapter

• Occurrence projected-formula-0018955

Equation form expr-8b6c08b49f493c4b

$\lforall[x][(x < t \lif !A(x))]$

Read as: for every x, if x is less than t then A of x

Means: for every x, if x is less than t then A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019581

Equation form expr-8b99f1e835f81e5d

$!A_g(b, \num{n}, \Obj 0)$

Read as: A subscript g of b, the numeral for n, and the object language constant zero

Means: A subscript g of b, the numeral for n, and the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019423

Equation form expr-8ba33efa103d1d43

$!A_f(z, y)$

Read as: A subscript f of z and y

Means: A subscript f of z and y

1 occurrence in this chapter

• Occurrence projected-formula-0019237

Equation form expr-8c2574892063f995

$R$

Read as: R

Means: R

3 occurrences in this chapter

• Occurrence projected-formula-0018874
• Occurrence projected-formula-0019477
• Occurrence projected-formula-0019505

Equation form expr-8c531a72c7fe2655

$m = 0$

Read as: m equals zero

Means: m equals zero

3 occurrences in this chapter

• Occurrence projected-formula-0019082
• Occurrence projected-formula-0019128
• Occurrence projected-formula-0019419

Equation form expr-8c76422868ff432e

$\eq[b'][\Obj 0]$

Read as: the successor of b equals the object language constant zero

Means: the successor of b equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019283

Equation form expr-8e30179df74cc60a

$!Q_8$

Read as: Q subscript eight

Means: Q subscript eight

10 occurrences in this chapter

• Occurrence projected-formula-0019316
• Occurrence projected-formula-0019328
• Occurrence projected-formula-0019336
• Occurrence projected-formula-0019360
• Occurrence projected-formula-0019373
• Occurrence projected-formula-0019377
• Occurrence projected-formula-0019402
• Occurrence projected-formula-0019647
• Occurrence projected-formula-0019658
• Occurrence projected-formula-0019664

Equation form expr-8e6aea830823dc37

$\Th{Q} \Proves \eq[t_2][\num n_2]$

Read as: Q proves that t subscript two equals the numeral for n subscript two

Means: Q proves that t subscript two equals the numeral for n subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019608

Equation form expr-8ef7d16bdf52cb52

$\eq[(c'+b')][\num{n+1}']$

Read as: the sum of the successor of c and the successor of b equals the successor of the numeral for n plus one

Means: the sum of the successor of c and the successor of b equals the successor of the numeral for n plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019330

Equation form expr-91b4c578b18b4766

$a < \num{m+1}$

Read as: a is less than the numeral for m plus one

Means: a is less than the numeral for m plus one

2 occurrences in this chapter

• Occurrence projected-formula-0019372
• Occurrence projected-formula-0019390

Equation form expr-930ba382516e4117

$m = n$

Read as: m equals n

Means: m equals n

1 occurrence in this chapter

• Occurrence projected-formula-0019673

Equation form expr-9332333c95b92b1a

$\Th{Q} \Proves \eq[t_1'][{\num n_1}']$

Read as: Q proves that the successor of t subscript one equals the successor of the numeral for n subscript one

Means: Q proves that the successor of t subscript one equals the successor of the numeral for n subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0019610

Equation form expr-93d82ea1ce9d4511

$x = \num 0 \lor \dots \lor x = \num k$

Read as: x equals one of the numerals from zero through k

Means: x equals one of the numerals from zero through k

1 occurrence in this chapter

• Occurrence projected-formula-0019706

Equation form expr-94505e429fe1baae

$\num{m} < b$

Read as: the numeral for m is less than b

Means: the numeral for m is less than b

3 occurrences in this chapter

• Occurrence projected-formula-0019391
• Occurrence projected-formula-0019427
• Occurrence projected-formula-0019428

Equation form expr-94c266908603cc20

$\eq[(b' + \Obj 0)][b']$

Read as: the sum of the successor of b and the object language constant zero equals the successor of b

Means: the sum of the successor of b and the object language constant zero equals the successor of b

1 occurrence in this chapter

• Occurrence projected-formula-0019282

Equation form expr-94d55460ef707d5e

$\eq[(a + \Obj 0)][a]$

Read as: the sum of a and the object language constant zero equals a

Means: the sum of a and the object language constant zero equals a

1 occurrence in this chapter

• Occurrence projected-formula-0019356

Equation form expr-94ebc8441ce25a95

$n < \Value{t}{N}$

Read as: n is less than the value of t in the standard model N

Means: n is less than the value of t in the standard model N

1 occurrence in this chapter

• Occurrence projected-formula-0019750

Equation form expr-9521e1b505384499

$!A_R(x_0,\dots,x_k)$

Read as: A subscript R applied to x subscript zero through x subscript k

Means: A subscript R applied to x subscript zero through x subscript k

2 occurrences in this chapter

• Occurrence projected-formula-0019467
• Occurrence projected-formula-0019476

Equation form expr-968e772cf168b7f1

$x,y$

Read as: x and y

Means: x and y

1 occurrence in this chapter

• Occurrence projected-formula-0019649

Equation form expr-970988c031322f17

$\Th{Q} \Proves \eq[(\num{n} + \num{m})][\num{n+m}]$

Read as: Q proves that the sum of the numeral for n and the numeral for m equals the numeral for n plus m

Means: Q proves that the sum of the numeral for n and the numeral for m equals the numeral for n plus m

3 occurrences in this chapter

• Occurrence projected-formula-0019126
• Occurrence projected-formula-0019140
• Occurrence projected-formula-0019151

Equation form expr-9739d6e0c9f5971c

$\lexists[x][!B(x)]$

Read as: there exists x such that B of x

Means: there exists x such that B of x

1 occurrence in this chapter

• Occurrence projected-formula-0019572

Equation form expr-976c5f41c4507aea

$\Th{Q} \Proves \eq[(\num{n} + \num{m}')][(\num{n}+\num{m})']$

Read as: Q proves that the sum of the numeral for n and the successor of the numeral for m equals the successor of the sum of the numeral for n and the numeral for m

Means: Q proves that the sum of the numeral for n and the successor of the numeral for m equals the successor of the sum of the numeral for n and the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019139

Equation form expr-97785cf468546005

$\lnot (!A \land !B)$

Read as: the negation of the conjunction of A and B

Means: the negation of the conjunction of A and B

1 occurrence in this chapter

• Occurrence projected-formula-0019721

Equation form expr-97e8e4bcf0e37115

$\Th{Q} \Proves \eq[\num n + {\num k}'][\num m]$

Read as: Q proves that the sum of the numeral for n and the successor of the numeral for k equals the numeral for m

Means: Q proves that the sum of the numeral for n and the successor of the numeral for k equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019655

Equation form expr-97ea19d02577e8a3

$!A_f(\num{n_0}, \dots, \num{n_k}, \num{m})$

Read as: A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for m

Means: A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for m

2 occurrences in this chapter

• Occurrence projected-formula-0018809
• Occurrence projected-formula-0018842

Equation form expr-9829f2e34e8f0b11

$\num{1}$

Read as: the numeral for one

Means: the numeral for one

1 occurrence in this chapter

• Occurrence projected-formula-0018783

Equation form expr-984fa2e59cd0d0c7

$\Value{(t_1')}{N} = n_1 + 1$

Read as: the value of the successor of t subscript one in the standard model N equals n subscript one plus one

Means: the value of the successor of t subscript one in the standard model N equals n subscript one plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019609

Equation form expr-9863b00bde618db4

$\bforall{x<\num{k+1}}{!A(x)}$

Read as: for every x less than the numeral for k plus one, A of x

Means: for every x less than the numeral for k plus one, A of x

2 occurrences in this chapter

• Occurrence projected-formula-0019695
• Occurrence projected-formula-0019708

Equation form expr-9872759fd3b4ac8d

$\eq[a][\num{m+1}]$

Read as: a equals the numeral for m plus one

Means: a equals the numeral for m plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019406

Equation form expr-98f0455530b5b3d8

$g_{k-1}$

Read as: g subscript k minus one

Means: g subscript k minus one

1 occurrence in this chapter

• Occurrence projected-formula-0019181

Equation form expr-9936aa9b7ddc35fc

$\lforall[y][(!A_f(\num{n_0}, \dots, \num{n_k}, y) \lif \num{l} = y)]$

Read as: for every y, if A subscript f holds of the numerals for n subscript zero through n subscript k, and y, then the numeral for l equals y

Means: for every y, if A subscript f holds of the numerals for n subscript zero through n subscript k, and y, then the numeral for l equals y

1 occurrence in this chapter

• Occurrence projected-formula-0018832

Equation form expr-99530d605f8f40ba

$(\eq/[\num{n}][\num{m}] \land \Obj 0 = \Obj 0)$

Read as: both the numeral for n does not equal the numeral for m, and the object language constant zero equals itself

Means: both the numeral for n does not equal the numeral for m, and the object language constant zero equals itself

1 occurrence in this chapter

• Occurrence projected-formula-0019109

Equation form expr-997b5f48ec78691e

$Q \Proves \eq/[\num n][\num m]$

Read as: Q proves that the numeral for n does not equal the numeral for m

Means: Q proves that the numeral for n does not equal the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019067

Equation form expr-99c79ec8f502f506

$h(x,\vec z)$

Read as: h of x and the tuple z

Means: h of x and the tuple z

1 occurrence in this chapter

• Occurrence projected-formula-0018995

Equation form expr-99cd0a95829c8be4

$\Th{Q} \Proves !A(\num n)$

Read as: Q proves that A of the numeral for n

Means: Q proves that A of the numeral for n

2 occurrences in this chapter

• Occurrence projected-formula-0019699
• Occurrence projected-formula-0019793

Equation form expr-99deeccf026a5fbb

$c \mid (a-b)$

Read as: c divides the difference a minus b

Means: c divides the difference a minus b

1 occurrence in this chapter

• Occurrence projected-formula-0018909

Equation form expr-99eaba70cc483016

$\eq[(c' + b)][\num{m}]$

Read as: the sum of the successor of c and b equals the numeral for m

Means: the sum of the successor of c and b equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019380

Equation form expr-9a1bfbe943988e5d

$\lexists[z][\eq[(z' + \Obj 0)][a]]$

Read as: there exists z such that the sum of the successor of z and the object language constant zero equals a

Means: there exists z such that the sum of the successor of z and the object language constant zero equals a

1 occurrence in this chapter

• Occurrence projected-formula-0019358

Equation form expr-9a60b2b0354496bd

$!A_f(x_0,\dots,x_{k-1},y)$

Read as: A subscript f applied to x subscript zero through x subscript k minus one, and y

Means: A subscript f applied to x subscript zero through x subscript k minus one, and y

1 occurrence in this chapter

• Occurrence projected-formula-0019032

Equation form expr-9ae03202d8082a50

$p \mid 1 + (k+1) m$

Read as: p divides one plus the product of k plus one and m

Means: p divides one plus the product of k plus one and m

1 occurrence in this chapter

• Occurrence projected-formula-0018941

Equation form expr-9b1130dee3faf818

$\Sigma_1$

Read as: Sigma one

Means: Sigma one

7 occurrences in this chapter

• Occurrence projected-formula-0019564
• Occurrence projected-formula-0019569
• Occurrence projected-formula-0019571
• Occurrence projected-formula-0019575
• Occurrence projected-formula-0019587
• Occurrence projected-formula-0019780
• Occurrence projected-formula-0019784

Equation form expr-9b306121bac7d91c

$a < \num {n+2}$

Read as: a is less than the numeral for n plus two

Means: a is less than the numeral for n plus two

1 occurrence in this chapter

• Occurrence projected-formula-0019320

Equation form expr-9b7ba6bb774a5ef4

$\Obj{0}''$

Read as: the second successor of the object language constant zero

Means: the second successor of the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0018786

Equation form expr-9ba6ff8b57246881

$\cfind{e}(n) \fdefined$

Read as: the partial computable function with index e is defined at n

Means: the partial computable function with index e is defined at n

2 occurrences in this chapter

• Occurrence projected-formula-0019524
• Occurrence projected-formula-0019549

Equation form expr-9c24810c7efa7b9d

$\lexists[y_0\dots][\lexists[y_{k-1}][(!A_{g_0}(x_0,\dots,x_{l-1},y_0) \land \dots \land {}]]\\ !A_{g_{k-1}}(x_0,\dots,x_{l-1},y_{k-1}) \land !A_f(y_0,\dots,y_{k-1},z))$

Read as: There exist y subscript zero through y subscript k minus one such that all of the following hold. A subscript g subscript zero holds of x subscript zero through x subscript l minus one, and y subscript zero. Continue this conjunction through A subscript g subscript k minus one, applied to the same input tuple and y subscript k minus one. Finally A subscript f holds of y subscript zero through y subscript k minus one, and z

Means: There exist y subscript zero through y subscript k minus one such that all of the following hold. A subscript g subscript zero holds of x subscript zero through x subscript l minus one, and y subscript zero. Continue this conjunction through A subscript g subscript k minus one, applied to the same input tuple and y subscript k minus one. Finally A subscript f holds of y subscript zero through y subscript k minus one, and z

1 occurrence in this chapter

• Occurrence projected-formula-0019229

Equation form expr-9c407114b462de60

$g(e, n)$

Read as: g of e and n

Means: g of e and n

1 occurrence in this chapter

• Occurrence projected-formula-0019553

Equation form expr-9d0c6534a53aea21

$\Value{t}{N} = 0$

Read as: the value of t in the standard model N equals zero

Means: the value of t in the standard model N equals zero

1 occurrence in this chapter

• Occurrence projected-formula-0019688

Equation form expr-9d93aac1dee956be

$\Th{Q} \Proves \lforall[y][(\eq[y][\Obj 0] \lor \lexists[z][\eq[y][z']])]$

Read as: Q proves that for every y, either y equals the object language constant zero, or there exists z such that y is the successor of z

Means: Q proves that for every y, either y equals the object language constant zero, or there exists z such that y is the successor of z

1 occurrence in this chapter

• Occurrence projected-formula-0019345

Equation form expr-9ee230f22d8cf57f

$x \mid y$

Read as: x divides y

Means: x divides y

2 occurrences in this chapter

• Occurrence projected-formula-0018966
• Occurrence projected-formula-0018989

Equation form expr-9f13c5dc7a2b3efe

$\lforall[x][\eq/[0][x']]$

Read as: for every x, zero is not equal to the successor of x

Means: for every x, zero is not equal to the successor of x

1 occurrence in this chapter

• Occurrence projected-formula-0019073

Equation form expr-9f3504db545ac1c7

$!Q_3$

Read as: Q subscript three

Means: Q subscript three

7 occurrences in this chapter

• Occurrence projected-formula-0019275
• Occurrence projected-formula-0019305
• Occurrence projected-formula-0019321
• Occurrence projected-formula-0019346
• Occurrence projected-formula-0019366
• Occurrence projected-formula-0019675
• Occurrence projected-formula-0019679

Equation form expr-9f95de631c898c08

$\eq[(c' + \num{m})'][b']$

Read as: the successor of the sum of the successor of c and the numeral for m equals the successor of b

Means: the successor of the sum of the successor of c and the numeral for m equals the successor of b

1 occurrence in this chapter

• Occurrence projected-formula-0019396

Equation form expr-9fb0570ccfbbd6a2

$\Th{Q} \Proves \lforall[y][(!A_=(\num{n}, \num{m}, y) \lif \eq[y][\num{1}])]$

Read as: Q proves that for every y, if A subscript equality holds of the numeral for n, the numeral for m, and y, then y equals the numeral for one

Means: Q proves that for every y, if A subscript equality holds of the numeral for n, the numeral for m, and y, then y equals the numeral for one

1 occurrence in this chapter

• Occurrence projected-formula-0019112

Equation form expr-9ff21a3a6c7fede3

$\lforall[y][((!A(\Obj 0) \land \lforall[x][(!A(x) \lif !A(x'))]) \lif \lforall[x][!A(x)])]$

Read as: For every y: if both A holds of the object language constant zero, and for every x, A of x implies A of the successor of x, then A holds of every x. The occurrences of y as an additional parameter of A are suppressed in the displayed notation

Means: For every y: if both A holds of the object language constant zero, and for every x, A of x implies A of the successor of x, then A holds of every x. The occurrences of y as an additional parameter of A are suppressed in the displayed notation

1 occurrence in this chapter

• Occurrence projected-formula-0018801

Equation form expr-9ff870ac21c87903

$y_i < x_i$

Read as: y subscript i is less than x subscript i

Means: y subscript i is less than x subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0018936

Equation form expr-a0d5d7ad8b7c5f0f

$\Th{Q} \Proves \eq[\Obj 0][\num 0]$

Read as: Q proves that the object language constant zero equals the numeral for zero

Means: Q proves that the object language constant zero equals the numeral for zero

1 occurrence in this chapter

• Occurrence projected-formula-0019601

Equation form expr-a0f1d688b8d2c454

$\Th{Q} \Proves \lnot (!A \land !B)$

Read as: Q proves that not both A and B

Means: Q proves that not both A and B

1 occurrence in this chapter

• Occurrence projected-formula-0019727

Equation form expr-a13fad715d3d8f39

$f(x_0, \dots, x_k)$

Read as: f of x subscript zero through x subscript k

Means: f of x subscript zero through x subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0018824

Equation form expr-a180d671401aa95a

$R(n_0, \dots, n_k)$

Read as: R of n subscript zero through n subscript k

Means: R of n subscript zero through n subscript k

2 occurrences in this chapter

• Occurrence projected-formula-0019490
• Occurrence projected-formula-0019496

Equation form expr-a1fce4363854ff88

$y$

Read as: y

Means: y

9 occurrences in this chapter

• Occurrence projected-formula-0018800
• Occurrence projected-formula-0018851
• Occurrence projected-formula-0018968
• Occurrence projected-formula-0019158
• Occurrence projected-formula-0019193
• Occurrence projected-formula-0019198
• Occurrence projected-formula-0019199
• Occurrence projected-formula-0019517
• Occurrence projected-formula-0019518

Equation form expr-a2277e0b98ac28a5

$g(x)$

Read as: g of x

Means: g of x

1 occurrence in this chapter

• Occurrence projected-formula-0019197

Equation form expr-a271a4166cc5926a

$\lnot \bforall{x<t}{!A(x)}$

Read as: the negation of the bounded universal formula with variable x, bound t, and matrix A of x

Means: the negation of the bounded universal formula with variable x, bound t, and matrix A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019754

Equation form expr-a2930a4518e17ed7

$y = \Obj 0$

Read as: y equals the object language constant zero

Means: y equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019033

Equation form expr-a31439ad6799912e

$!Q_2$

Read as: Q subscript two

Means: Q subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019284

Equation form expr-a318c24216defe20

$+$

Read as: plus

Means: plus

1 occurrence in this chapter

• Occurrence projected-formula-0019169

Equation form expr-a3466b8f618426a2

$\Th{T}$

Read as: T

Means: T

3 occurrences in this chapter

• Occurrence projected-formula-0019508
• Occurrence projected-formula-0019509
• Occurrence projected-formula-0019512

Equation form expr-a37cb0fe7345926a

$\eq[y][\num{0}]$

Read as: y equals the numeral for zero

Means: y equals the numeral for zero

1 occurrence in this chapter

• Occurrence projected-formula-0019122

Equation form expr-a3a5c1aaeb0c0304

$\eq[y][(x_0 + x_1)]$

Read as: y equals the sum of x subscript zero and x subscript one

Means: y equals the sum of x subscript zero and x subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0019144

Equation form expr-a3a795ab86ae620b

$\eq[z' + \num n][\num m]$

Read as: the sum of the successor of z and the numeral for n equals the numeral for m

Means: the sum of the successor of z and the numeral for n equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019669

Equation form expr-a4cd1fc4fcb08699

$\lforall[x][\eq/[x][x']]$

Read as: for every x, x is not equal to its successor

Means: for every x, x is not equal to its successor

1 occurrence in this chapter

• Occurrence projected-formula-0018788

Equation form expr-a5b928f808bc85b6

$\Th{Q} & \Proves !A_g(\num{m}, \num{n}, \Obj 0) \land \lforall[w][(w < \num{m} \lif \lnot !A_g(w, \num{n}, \Obj 0))]. \notag \intertext{Since $!A_g(x, z, y)$ represents $g(x, z)$ and $g(m, n) = 0$ if $f(n) = m$, we have} \Th{Q} & \Proves !A_g(\num{m}, \num{n}, \Obj 0). \notag \intertext{If $f(n) = m$, then for every $k < m$, $g(k, n) \neq 0$. So} \Th{Q} & \Proves \lnot !A_g(\num{k}, \num{n}, \Obj 0). \notag \intertext{We get that} \Th{Q} & \Proves \lforall[w][(w < \num{m} \lif \lnot !A_g(w, \num{n}, \Obj 0))]. \ollabel{rep-less}$

Read as: We seek a proof in Q of the conjunction of A subscript g of the numeral for m, the numeral for n, and the object language constant zero, with the statement that every w less than the numeral for m fails to satisfy A subscript g of w, the numeral for n, and that constant zero. Since A subscript g of x, z, and y represents g of x and z, and g of m and n equals zero if f of n equals m, Q proves the first conjunct. If f of n equals m, then for every k less than m, g of k and n is not zero. So Q proves not A subscript g of the numeral for k, the numeral for n, and that constant zero. We obtain the final displayed claim: Q proves that for every w, if w is less than the numeral for m then not A subscript g of w, the numeral for n, and that constant zero

Means: We seek a proof in Q of the conjunction of A subscript g of the numeral for m, the numeral for n, and the object language constant zero, with the statement that every w less than the numeral for m fails to satisfy A subscript g of w, the numeral for n, and that constant zero. Since A subscript g of x, z, and y represents g of x and z, and g of m and n equals zero if f of n equals m, Q proves the first conjunct. If f of n equals m, then for every k less than m, g of k and n is not zero. So Q proves not A subscript g of the numeral for k, the numeral for n, and that constant zero. We obtain the final displayed claim: Q proves that for every w, if w is less than the numeral for m then not A subscript g of w, the numeral for n, and that constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019418

Equation form expr-a67fdb34453f737a

$\lexists[y][\eq[(y'+a)][\Obj 0']]$

Read as: there exists y such that the sum of the successor of y and a equals the successor of the object language constant zero

Means: there exists y such that the sum of the successor of y and a equals the successor of the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019300

Equation form expr-a6c0b99522e3fba2

$\eq[(b' + c)][\Obj 0]$

Read as: the sum of the successor of b and c equals the object language constant zero

Means: the sum of the successor of b and c equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019315

Equation form expr-a726dcd1f0fd3123

$T(e, n, s)$

Read as: Kleene T of e, n, and s

Means: Kleene T of e, n, and s

3 occurrences in this chapter

• Occurrence projected-formula-0019526
• Occurrence projected-formula-0019532
• Occurrence projected-formula-0019548

Equation form expr-a7799faa3faed46b

$\Th{Q} \Proves !B$

Read as: Q proves that B

Means: Q proves that B

1 occurrence in this chapter

• Occurrence projected-formula-0019719

Equation form expr-a92a1a72f6d79dff

$x_0 & = 1 + m \\ x_1 & = 1 + 2 \cdot m \\ x_2 & = 1 + 3 \cdot m \\ & \vdots \\ x_n & = 1 + (n+1) \cdot m$

Read as: x subscript zero equals one plus m. x subscript one equals one plus two times m. x subscript two equals one plus three times m. Continue in this pattern through x subscript n, which equals one plus the product of n plus one and m

Means: x subscript zero equals one plus m. x subscript one equals one plus two times m. x subscript two equals one plus three times m. Continue in this pattern through x subscript n, which equals one plus the product of n plus one and m

1 occurrence in this chapter

• Occurrence projected-formula-0018933

Equation form expr-a9ac716b2b2b6374

$\eq[b'][\num{m}']$

Read as: the successor of b equals the successor of the numeral for m

Means: the successor of b equals the successor of the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019405

Equation form expr-a9d343fbfceb6cbf

$(b < \num{m} \lor \num{m} < b) \lor \eq[b][\num{m}]$

Read as: either b is less than the numeral for m, or the numeral for m is less than b, or b equals the numeral for m

Means: either b is less than the numeral for m, or the numeral for m is less than b, or b equals the numeral for m

2 occurrences in this chapter

• Occurrence projected-formula-0019375
• Occurrence projected-formula-0019425

Equation form expr-aa311401800bb784

$\Th{Q} \Proves \eq[\num{n_1} + \num{n_2}][\num{n_1 + n_2}]$

Read as: Q proves that the sum of the numeral for n subscript one and the numeral for n subscript two equals the numeral for n subscript one plus n subscript two

Means: Q proves that the sum of the numeral for n subscript one and the numeral for n subscript two equals the numeral for n subscript one plus n subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019616

Equation form expr-aa3501e31cd10004

$\eq[a][\num{1}] \lor \dots \lor \eq[a][\num{n+1}]$

Read as: a equals one of the numerals from one through n plus one

Means: a equals one of the numerals from one through n plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019339

Equation form expr-aaa9402664f1a41f

$h$

Read as: h

Means: h

9 occurrences in this chapter

• Occurrence projected-formula-0018999
• Occurrence projected-formula-0019003
• Occurrence projected-formula-0019027
• Occurrence projected-formula-0019176
• Occurrence projected-formula-0019183
• Occurrence projected-formula-0019191
• Occurrence projected-formula-0019443
• Occurrence projected-formula-0019555
• Occurrence projected-formula-0019557

Equation form expr-ab0b4ea97abfc843

$\Th{Q} \Proves \eq[t_1 + t_2][\num{n_1} + \num{n_2}]$

Read as: Q proves that the sum of t subscript one and t subscript two equals the sum of the numeral for n subscript one and the numeral for n subscript two

Means: Q proves that the sum of t subscript one and t subscript two equals the sum of the numeral for n subscript one and the numeral for n subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019615

Equation form expr-acc4a828c3018e3e

$\eq[a][\Obj 0] \lor \dots \lor \eq[a][\num{n+1}]$

Read as: a equals one of the numerals from zero through n plus one

Means: a equals one of the numerals from zero through n plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019325

Equation form expr-ad82ed0b26185a19

$\Th{Q} \Proves \lnot(!A \lor !B)$

Read as: Q proves that not the disjunction of A and B

Means: Q proves that not the disjunction of A and B

1 occurrence in this chapter

• Occurrence projected-formula-0019743

Equation form expr-ad988faab4472ea6

$\tuple{y_0, \dots,y_n}$

Read as: the sequence y subscript zero through y subscript n

Means: the sequence y subscript zero through y subscript n

1 occurrence in this chapter

• Occurrence projected-formula-0018924

Equation form expr-adedc2ab1c653ff0

$\num{n}'$

Read as: the successor of the numeral for n

Means: the successor of the numeral for n

1 occurrence in this chapter

• Occurrence projected-formula-0019259

Equation form expr-aeba77fc8715af8d

$\Th{Q} \Proves \eq[t_1][\num n]$

Read as: Q proves that t subscript one equals the numeral for n

Means: Q proves that t subscript one equals the numeral for n

3 occurrences in this chapter

• Occurrence projected-formula-0019638
• Occurrence projected-formula-0019653
• Occurrence projected-formula-0019667

Equation form expr-af29e8d040e75ef3

$\fn{num}$

Read as: the numeral coding function num

Means: the numeral coding function num

1 occurrence in this chapter

• Occurrence projected-formula-0018853

Equation form expr-b030cfb307e9692e

$m = \Value{t_2}{N}$

Read as: m equals the value of t subscript two in the standard model N

Means: m equals the value of t subscript two in the standard model N

1 occurrence in this chapter

• Occurrence projected-formula-0019636

Equation form expr-b06799d3205fa44d

$\Delta_0$

Read as: Delta zero

Means: Delta zero

7 occurrences in this chapter

• Occurrence projected-formula-0019568
• Occurrence projected-formula-0019585
• Occurrence projected-formula-0019590
• Occurrence projected-formula-0019595
• Occurrence projected-formula-0019710
• Occurrence projected-formula-0019768
• Occurrence projected-formula-0019792

Equation form expr-b2ce9cd8bef51e4c

$!A \ident \lforall[x][!B(x)]$

Read as: A is the formula for every x, B of x

Means: A is the formula for every x, B of x

1 occurrence in this chapter

• Occurrence projected-formula-0019593

Equation form expr-b2daad0d82bb1fc2

$d_0 \equiv a_i \mod (1+(i+1)d_1)$

Read as: d subscript zero is congruent to a subscript i modulo one plus the product of i plus one and d subscript one

Means: d subscript zero is congruent to a subscript i modulo one plus the product of i plus one and d subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0018980

Equation form expr-b3f6ba5bad3f6071

$n_0$

Read as: n subscript zero

Means: n subscript zero

3 occurrences in this chapter

• Occurrence projected-formula-0018875
• Occurrence projected-formula-0019478
• Occurrence projected-formula-0019488

Equation form expr-b4e6bdbd4df9905c

$\Th{Q} \Proves (!A \land !B)$

Read as: Q proves that both A and B

Means: Q proves that both A and B

1 occurrence in this chapter

• Occurrence projected-formula-0019720

Equation form expr-b5348603f9f5b166

$\Sat/{N}{t_1 < t_2}$

Read as: the standard model N does not satisfy that t subscript one is less than t subscript two

Means: the standard model N does not satisfy that t subscript one is less than t subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019660

Equation form expr-b53fe84dcdb8d4ca

$m = k + 1$

Read as: m equals k plus one

Means: m equals k plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019071

Equation form expr-b620f7fd0a05aeb7

$\num{0}$

Read as: the numeral for zero

Means: the numeral for zero

1 occurrence in this chapter

• Occurrence projected-formula-0018781

Equation form expr-b70c52a65a4a70fb

$\Th{Q} \Proves \eq[t_1][t_2]$

Read as: Q proves that t subscript one equals t subscript two

Means: Q proves that t subscript one equals t subscript two

2 occurrences in this chapter

• Occurrence projected-formula-0019626
• Occurrence projected-formula-0019642

Equation form expr-b70e215b9e4d1e68

$\num{m}' \ident \num{m+1}$

Read as: the successor of the numeral for m is the numeral for m plus one

Means: the successor of the numeral for m is the numeral for m plus one

2 occurrences in this chapter

• Occurrence projected-formula-0019387
• Occurrence projected-formula-0019400

Equation form expr-b77b10aec6f1a7d2

$a_i = \fn{rem}(1+(i+1)d_1,d_0).$

Read as: a subscript i equals the remainder when d subscript zero is divided by one plus the product of i plus one and d subscript one

Means: a subscript i equals the remainder when d subscript zero is divided by one plus the product of i plus one and d subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0018983

Equation form expr-b9711ee2915de9c0

$\Add$

Read as: the addition function

Means: the addition function

4 occurrences in this chapter

• Occurrence projected-formula-0019011
• Occurrence projected-formula-0019143
• Occurrence projected-formula-0019451
• Occurrence projected-formula-0019457

Equation form expr-ba57289fd17703bd

$m \neq f(n_0, \dots, n_k)$

Read as: m does not equal f of n subscript zero through n subscript k

Means: m does not equal f of n subscript zero through n subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0018829

Equation form expr-ba6d58a2fdaae197

$\Th{Q} \Proves \bforall{x<\num{k+1}}{!A(x)}$

Read as: Q proves that for every x less than the numeral for k plus one, A of x

Means: Q proves that for every x less than the numeral for k plus one, A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019696

Equation form expr-ba7f9ad8e3be5eab

$\Th{Q} & \Proves \eq[(a' + \num n')][(a' + \num n)'] \quad \text{by axiom $!Q_5$} \ollabel{step5}\\ \Th{Q} & \Proves \eq[(a' + \num n')][(a + \num n')'] \quad \text{inductive hypothesis} \ollabel{step6}\\ \Th{Q} & \Proves \eq[(a' + \num n)'][(a + \num n')'] \quad \text{by \olref{step5} and \olref{step6}.} \notag$

Read as: Step five. Q proves that the sum of the successor of a and the successor of the numeral for n equals the successor of the sum of the successor of a and the numeral for n, by axiom Q subscript five. Step six, attributed in the source to the induction hypothesis. Q proves that the sum of the successor of a and the successor of the numeral for n equals the successor of the sum of a and the successor of the numeral for n. Final source line. Q proves that the successor of the sum of the successor of a and the numeral for n equals the successor of the sum of a and the successor of the numeral for n, by step five of the successor and fixed numeral addition derivation and step six of the successor and fixed numeral addition derivation

Means: Step five. Q proves that the sum of the successor of a and the successor of the numeral for n equals the successor of the sum of the successor of a and the numeral for n, by axiom Q subscript five. Step six, attributed in the source to the induction hypothesis. Q proves that the sum of the successor of a and the successor of the numeral for n equals the successor of the sum of a and the successor of the numeral for n. Final source line. Q proves that the successor of the sum of the successor of a and the numeral for n equals the successor of the sum of a and the successor of the numeral for n, by step five of the successor and fixed numeral addition derivation and step six of the successor and fixed numeral addition derivation

1 occurrence in this chapter

• Occurrence projected-formula-0019262

Equation form expr-bb4b3b3752cc45ed

$\bforall{x < t}{!A(x)}$

Read as: for every x less than t, A of x

Means: for every x less than t, A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019583

Equation form expr-bb73dc40dadf40d6

$\eq[\num n'][\num k'] \lif \eq[\num n][\num k]$

Read as: if the successor of the numeral for n equals the successor of the numeral for k, then the numeral for n equals the numeral for k

Means: if the successor of the numeral for n equals the successor of the numeral for k, then the numeral for n equals the numeral for k

1 occurrence in this chapter

• Occurrence projected-formula-0019090

Equation form expr-bbca117ccebff147

$\Sat{N}{!A(\num n)}$

Read as: the standard model N satisfies A of the numeral for n

Means: the standard model N satisfies A of the numeral for n

1 occurrence in this chapter

• Occurrence projected-formula-0019790

Equation form expr-bc0533ea2b50cd8b

$\Th{Q} \Proves !A_g(\num{m}, \num{n}, \Obj 0)$

Read as: Q proves that A subscript g of the numeral for m, the numeral for n, and the object language constant zero

Means: Q proves that A subscript g of the numeral for m, the numeral for n, and the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019432

Equation form expr-bc2ac1b4f5189864

$\num 1 \ident \Obj 0'$

Read as: the numeral for one is the successor of the object language constant zero

Means: the numeral for one is the successor of the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019301

Equation form expr-be58d8ae65b26403

$\Obj{0}$

Read as: the object language constant zero

Means: the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0018782

Equation form expr-be6439baf2b773eb

$\Th{Q} & \Proves \lforall[y][(!A_g(\num{n}, y) \lif \eq[y][\num{k}])] \intertext{since $!A_g$ represents~$g$, and} \Th{Q} & \Proves \lforall[z][(!A_f(\num{k}, z) \lif \eq[z][\num{m}])] \intertext{since $!A_f$ represents~$f$. Using just a little bit of logic, we can show that also} \Th{Q} & \Proves \lforall[z][(\lexists[y][(!A_g(\num{n}, y) \land !A_f(y, z))] \lif \eq[z][\num{m}])].$

Read as: Q proves: for every y, if A subscript g holds of the numeral for n and y, then y equals the numeral for k; since A subscript g represents g. And Q proves: for every z, if A subscript f holds of the numeral for k and z, then z equals the numeral for m; since A subscript f represents f. Using logic, Q also proves: for every z, if there exists y such that both A subscript g of the numeral for n and y, and A subscript f of y and z, then z equals the numeral for m

Means: Q proves: for every y, if A subscript g holds of the numeral for n and y, then y equals the numeral for k; since A subscript g represents g. And Q proves: for every z, if A subscript f holds of the numeral for k and z, then z equals the numeral for m; since A subscript f represents f. Using logic, Q also proves: for every z, if there exists y such that both A subscript g of the numeral for n and y, and A subscript f of y and z, then z equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019218

Equation form expr-be8dcefb61dddd9f

$t_1$

Read as: t subscript one

Means: t subscript one

3 occurrences in this chapter

• Occurrence projected-formula-0019603
• Occurrence projected-formula-0019623
• Occurrence projected-formula-0019633

Equation form expr-bf91a68806643b2d

$\eq[(b' + c')][\Obj 0']$

Read as: the sum of the successor of b and the successor of c equals the successor of the object language constant zero

Means: the sum of the successor of b and the successor of c equals the successor of the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019310

Equation form expr-bfd6ef7500b63b6e

$\Th{Q} \Proves \eq/[t_1][t_2]$

Read as: Q proves that t subscript one does not equal t subscript two

Means: Q proves that t subscript one does not equal t subscript two

2 occurrences in this chapter

• Occurrence projected-formula-0019628
• Occurrence projected-formula-0019645

Equation form expr-c0b85f68695529e7

$\Th{Q} \Proves (\eq[\num{n}][\num{m}] \land \eq[\num{1}][\num{1}])$

Read as: Q proves that both the numeral for n equals the numeral for m, and the numeral for one equals itself

Means: Q proves that both the numeral for n equals the numeral for m, and the numeral for one equals itself

1 occurrence in this chapter

• Occurrence projected-formula-0019104

Equation form expr-c130ae82020bfd16

$m < n$

Read as: m is less than n

Means: m is less than n

1 occurrence in this chapter

• Occurrence projected-formula-0019676

Equation form expr-c1ebb646a2c7db63

$d_1 = \lcm(1,\dots,j)$

Read as: d subscript one equals the least common multiple of the integers one through j

Means: d subscript one equals the least common multiple of the integers one through j

1 occurrence in this chapter

• Occurrence projected-formula-0018973

Equation form expr-c3acc8569f115745

$\Pi_1$

Read as: Pi one

Means: Pi one

2 occurrences in this chapter

• Occurrence projected-formula-0019570
• Occurrence projected-formula-0019592

Equation form expr-c42b3309bde3d651

$(\num{m} \times \num{n})$

Read as: the object language product of the numeral for m and the numeral for n

Means: the object language product of the numeral for m and the numeral for n

1 occurrence in this chapter

• Occurrence projected-formula-0019168

Equation form expr-c47201f62ece94f0

$!A_{\Mult}(x_0, x_1, y) \ident y = (x_0 \times x_1).$

Read as: A subscript Mult of x subscript zero, x subscript one, and y is the formula y equals the object language product of x subscript zero and x subscript one

Means: A subscript Mult of x subscript zero, x subscript one, and y is the formula y equals the object language product of x subscript zero and x subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0019161

Equation form expr-c4a123c8c48e6b9b

$\Th{Q} \Proves !B_T(\num{e}, \num{n}, \num{s})$

Read as: Q proves that B subscript T applied to the numerals for e, n, and s

Means: Q proves that B subscript T applied to the numerals for e, n, and s

2 occurrences in this chapter

• Occurrence projected-formula-0019531
• Occurrence projected-formula-0019533

Equation form expr-c4f0cb271cf766e6

$!A_{\Char{R}}(\num{n_0}, \dots, \num{n_k}, \num{1})$

Read as: A subscript characteristic function of R, applied to the numerals for n subscript zero through n subscript k, and the numeral for one

Means: A subscript characteristic function of R, applied to the numerals for n subscript zero through n subscript k, and the numeral for one

1 occurrence in this chapter

• Occurrence projected-formula-0019493

Equation form expr-c60dc090c13fb049

$\eq[\num{n_1}'][\num{n_1}']$

Read as: the successor of the numeral for n subscript one equals the successor of the numeral for n subscript one

Means: the successor of the numeral for n subscript one equals the successor of the numeral for n subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0019611

Equation form expr-c63f9557f464c93a

$\lnot !A$

Read as: not A

Means: not A

4 occurrences in this chapter

• Occurrence projected-formula-0019723
• Occurrence projected-formula-0019738
• Occurrence projected-formula-0019764
• Occurrence projected-formula-0019776

Equation form expr-c69517800513e472

$\Th{Q} \Proves !A_\Add(\num{n}, \num{m}, \num{k})$

Read as: Q proves that A subscript Add applied to the numeral for n, the numeral for m, and the numeral for k

Means: Q proves that A subscript Add applied to the numeral for n, the numeral for m, and the numeral for k

1 occurrence in this chapter

• Occurrence projected-formula-0019146

Equation form expr-c6af2de2cdedff23

$\Th{Q} \Proves \eq[(\num{n}+\num{m})][\num{n+m}],$

Read as: Q proves that the sum of the numeral for n and the numeral for m equals the numeral for n plus m

Means: Q proves that the sum of the numeral for n and the numeral for m equals the numeral for n plus m

1 occurrence in this chapter

• Occurrence projected-formula-0019155

Equation form expr-c6c006c35255f7a9

$K(z) & = \bmin{x \leq z}{\bexists{y \leq z}{z = J(x,y)}},\\ L(z) & = \bmin{y \leq z}{\bexists{x \leq z}{z = J(x,y)}};$

Read as: K of z equals the least x less than or equal to z such that there exists y less than or equal to z with z equal to J of x and y. L of z equals the least y less than or equal to z such that there exists x less than or equal to z with z equal to J of x and y

Means: K of z equals the least x less than or equal to z such that there exists y less than or equal to z with z equal to J of x and y. L of z equals the least y less than or equal to z such that there exists x less than or equal to z with z equal to J of x and y

1 occurrence in this chapter

• Occurrence projected-formula-0018964

Equation form expr-c6d8b66c8445862f

$\Th{Q} \Proves \lexists[x][!A(x)]$

Read as: Q proves that there exists x such that A of x

Means: Q proves that there exists x such that A of x

1 occurrence in this chapter

• Occurrence projected-formula-0019794

Equation form expr-c753fa04cc8febbe

$s = \tuple{\Gn{\delta}, f(n_0, \dots, n_k)}$

Read as: s equals the prime power code of the ordered pair consisting of the Goedel number of delta and the number f of n subscript zero through n subscript k

Means: s equals the prime power code of the ordered pair consisting of the Goedel number of delta and the number f of n subscript zero through n subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0018880

Equation form expr-c7d7dc4c87e87988

$R(x_0, \dots, x_k)$

Read as: R of x subscript zero through x subscript k

Means: R of x subscript zero through x subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0019482

Equation form expr-c8296fead254de67

$\Th{Q} \Proves \lforall[y][((y < \num{m} \lor \num{m} < y) \lor \eq[y][\num{m}])].$

Read as: Q proves that for every y, either y is less than the numeral for m, or the numeral for m is less than y, or y equals the numeral for m

Means: Q proves that for every y, either y is less than the numeral for m, or the numeral for m is less than y, or y equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019342

Equation form expr-c8cd3e05db71af27

$\Value{t}{N} = k+1$

Read as: the value of t in the standard model N equals k plus one

Means: the value of t in the standard model N equals k plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019693

Equation form expr-c94e90881ad97613

$!A_R(x_0, \dots, x_k)$

Read as: A subscript R applied to x subscript zero through x subscript k

Means: A subscript R applied to x subscript zero through x subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0019486

Equation form expr-c9da8b5c962314d2

$j = \max(n,a_0+1,\dots,a_n+1),$

Read as: j equals the maximum of n, a subscript zero plus one, and so on through a subscript n plus one

Means: j equals the maximum of n, a subscript zero plus one, and so on through a subscript n plus one

1 occurrence in this chapter

• Occurrence projected-formula-0018972

Equation form expr-ca52fdc0d544864c

$(s)_1$

Read as: the entry at position one in the prime power sequence coded by s

Means: the entry at position one in the prime power sequence coded by s

1 occurrence in this chapter

• Occurrence projected-formula-0018867

Equation form expr-ca978112ca1bbdca

$a$

Read as: a

Means: a

9 occurrences in this chapter

• Occurrence projected-formula-0018902
• Occurrence projected-formula-0018905
• Occurrence projected-formula-0018910
• Occurrence projected-formula-0019249
• Occurrence projected-formula-0019269
• Occurrence projected-formula-0019297
• Occurrence projected-formula-0019347
• Occurrence projected-formula-0019365
• Occurrence projected-formula-0019410

Equation form expr-caa2c3f5df4bcdee

$n+1 \neq k+1$

Read as: n plus one does not equal k plus one

Means: n plus one does not equal k plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019085

Equation form expr-cb38ea1ca94b6a4e

$\num{m+1} < a$

Read as: the numeral for m plus one is less than a

Means: the numeral for m plus one is less than a

1 occurrence in this chapter

• Occurrence projected-formula-0019403

Equation form expr-cb91d6f4cdc873bb

$!A_f(z,y) \ident !A_g(y, z, \Obj 0) \land \lforall[w][(w < y \lif \lnot !A_g(w, z, \Obj 0))]$

Read as: A subscript f of z and y is the conjunction of A subscript g of y, z, and the object language constant zero, with the following universal statement: for every w, if w is less than y then not A subscript g of w, z, and the object language constant zero

Means: A subscript f of z and y is the conjunction of A subscript g of y, z, and the object language constant zero, with the following universal statement: for every w, if w is less than y then not A subscript g of w, z, and the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019414

Equation form expr-cb9e98ffe227a219

$\Th{Q} \Proves \eq[(a' + \num n)][(a + \num n)'].$

Read as: Q proves that the sum of the successor of a and the numeral for n equals the successor of the sum of a and the numeral for n

Means: Q proves that the sum of the successor of a and the numeral for n equals the successor of the sum of a and the numeral for n

1 occurrence in this chapter

• Occurrence projected-formula-0019251

Equation form expr-cc7fd1eac73960bb

$\lforall[y][(!A_f(\num{n_0}, \dots, \num{n_k}, y) \lif \num{m} = y)]$

Read as: for every y, if A subscript f holds of the numerals for n subscript zero through n subscript k, and y, then the numeral for m equals y

Means: for every y, if A subscript f holds of the numerals for n subscript zero through n subscript k, and y, then the numeral for m equals y

1 occurrence in this chapter

• Occurrence projected-formula-0018810

Equation form expr-cd0aa9856147b6c5

$g$

Read as: g

Means: g

8 occurrences in this chapter

• Occurrence projected-formula-0018997
• Occurrence projected-formula-0019001
• Occurrence projected-formula-0019005
• Occurrence projected-formula-0019007
• Occurrence projected-formula-0019189
• Occurrence projected-formula-0019434
• Occurrence projected-formula-0019445
• Occurrence projected-formula-0019447

Equation form expr-cdd5f70c7ba98085

$g(\vec x, y, z)$

Read as: g of the tuple x, y, and z

Means: g of the tuple x, y, and z

1 occurrence in this chapter

• Occurrence projected-formula-0018994

Equation form expr-ce1dea246c115488

$!A(x, y)$

Read as: A of x and y

Means: A of x and y

1 occurrence in this chapter

• Occurrence projected-formula-0018799

Equation form expr-ce5499b301e3ff6e

$h(e, n) = \begin{cases} 1 & \text{if $\Prov[\Th{Q}](g(e, n))$}\\ 0 & \text{otherwise}. \end{cases}$

Read as: h of e and n equals one if g of e and n is the Goedel number of a sentence provable in Q, and equals zero otherwise

Means: h of e and n equals one if g of e and n is the Goedel number of a sentence provable in Q, and equals zero otherwise

1 occurrence in this chapter

• Occurrence projected-formula-0019554

Equation form expr-cf9404d3f534ee7e

$n_k$

Read as: n subscript k

Means: n subscript k

3 occurrences in this chapter

• Occurrence projected-formula-0018876
• Occurrence projected-formula-0019479
• Occurrence projected-formula-0019489

Equation form expr-cfed7d5e81fdcd14

$\Th{Q} \Proves \eq[(a' + \num n)][(a + \num n)']$

Read as: Q proves that the sum of the successor of a and the numeral for n equals the successor of the sum of a and the numeral for n

Means: Q proves that the sum of the successor of a and the numeral for n equals the successor of the sum of a and the numeral for n

1 occurrence in this chapter

• Occurrence projected-formula-0019257

Equation form expr-d055ee4dbcdd0c8b

$!B$

Read as: B

Means: B

8 occurrences in this chapter

• Occurrence projected-formula-0019573
• Occurrence projected-formula-0019584
• Occurrence projected-formula-0019589
• Occurrence projected-formula-0019594
• Occurrence projected-formula-0019716
• Occurrence projected-formula-0019732
• Occurrence projected-formula-0019769
• Occurrence projected-formula-0019774

Equation form expr-d09ed1e4ecd2d22e

$k=\Value{t}{N}$

Read as: k equals the value of t in the standard model N

Means: k equals the value of t in the standard model N

2 occurrences in this chapter

• Occurrence projected-formula-0019683
• Occurrence projected-formula-0019747

Equation form expr-d0c0747b792ead99

$R(n_0,\dots,n_k)$

Read as: R of n subscript zero through n subscript k

Means: R of n subscript zero through n subscript k

2 occurrences in this chapter

• Occurrence projected-formula-0019468
• Occurrence projected-formula-0019471

Equation form expr-d0f6b500e6a0f078

$a < \num 1 \lif \eq[a][\Obj 0]$

Read as: if a is less than the numeral for one, then a equals the object language constant zero

Means: if a is less than the numeral for one, then a equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019296

Equation form expr-d16e8ab6de59c4c0

$\beta(d,i) & = \beta^*(d_0,d_1,i) \\ & = \fn{rem}(1+(i+1) d_1,d_0) \\ & = a_i$

Read as: Beta of d and i equals beta star of d subscript zero, d subscript one, and i. This equals the remainder when d subscript zero is divided by one plus the product of i plus one and d subscript one. This equals a subscript i

Means: Beta of d and i equals beta star of d subscript zero, d subscript one, and i. This equals the remainder when d subscript zero is divided by one plus the product of i plus one and d subscript one. This equals a subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0018986

Equation form expr-d170031b3881cb44

$\Th{Q} \Proves \num n < \num{k+1}$

Read as: Q proves that the numeral for n is less than the numeral for k plus one

Means: Q proves that the numeral for n is less than the numeral for k plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019698

Equation form expr-d184b0662ef95fea

$J(x,y) = \frac{1}{2}[(x+y)(x+y+1)] + x$

Read as: J of x and y equals one half of the product of x plus y and x plus y plus one, plus x

Means: J of x and y equals one half of the product of x plus y and x plus y plus one, plus x

1 occurrence in this chapter

• Occurrence projected-formula-0018963

Equation form expr-d203ba01eef4198c

$\delta$

Read as: delta

Means: delta

3 occurrences in this chapter

• Occurrence projected-formula-0018841
• Occurrence projected-formula-0018848
• Occurrence projected-formula-0018877

Equation form expr-d2088115bb6beae8

$!T$

Read as: T

Means: T

1 occurrence in this chapter

• Occurrence projected-formula-0019562

Equation form expr-d216b49687a64c2b

$\Char{=}(x_0, x_1) = \begin{cases} 1 & \text{if } x_0 =x_1\\ 0 & otherwise \end{cases}$

Read as: The characteristic function of equality applied to x subscript zero and x subscript one has two cases: one if x subscript zero equals x subscript one; zero otherwise

Means: The characteristic function of equality applied to x subscript zero and x subscript one has two cases: one if x subscript zero equals x subscript one; zero otherwise

1 occurrence in this chapter

• Occurrence projected-formula-0019057

Equation form expr-d231f4622566655b

$\Add(n, m) = k$

Read as: the addition function applied to n and m equals k

Means: the addition function applied to n and m equals k

2 occurrences in this chapter

• Occurrence projected-formula-0019145
• Occurrence projected-formula-0019152

Equation form expr-d23482973ce32f15

$\eq[(c'+b)][\num{n+1}]$

Read as: the sum of the successor of c and b equals the numeral for n plus one

Means: the sum of the successor of c and b equals the numeral for n plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019334

Equation form expr-d30a1e55e70e9308

$\eq[z' + \num{n - m}][\Obj 0]$

Read as: the sum of the successor of z and the numeral for n minus m equals the object language constant zero

Means: the sum of the successor of z and the numeral for n minus m equals the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019672

Equation form expr-d33d5093ec487a6e

$!Q_4$

Read as: Q subscript four

Means: Q subscript four

4 occurrences in this chapter

• Occurrence projected-formula-0019130
• Occurrence projected-formula-0019280
• Occurrence projected-formula-0019355
• Occurrence projected-formula-0019371

Equation form expr-d3482b3a268726b8

$\num{n+m}$

Read as: the numeral for n plus m

Means: the numeral for n plus m

3 occurrences in this chapter

• Occurrence projected-formula-0019150
• Occurrence projected-formula-0019156
• Occurrence projected-formula-0019173

Equation form expr-d37ee030798fd9cd

$(d)_i$

Read as: the entry beta of d and i in the beta coding

Means: the entry beta of d and i in the beta coding

1 occurrence in this chapter

• Occurrence projected-formula-0019020

Equation form expr-d3a9668f550f81b4

$\beta(d,i) = a_i$

Read as: beta of d and i equals a subscript i

Means: beta of d and i equals a subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0018890

Equation form expr-d438a18a7da07bf0

$x < y$

Read as: x is less than y

Means: x is less than y

2 occurrences in this chapter

• Occurrence projected-formula-0018965
• Occurrence projected-formula-0018988

Equation form expr-d4735e3a265e16ee

$2$

Read as: two

Means: two

1 occurrence in this chapter

• Occurrence projected-formula-0019171

Equation form expr-d52d8099d5776fc7

$!A(\num n)$

Read as: A of the numeral for n

Means: A of the numeral for n

2 occurrences in this chapter

• Occurrence projected-formula-0019748
• Occurrence projected-formula-0019791

Equation form expr-d6a2d379cf7382cc

$y = g(x)$

Read as: y equals g of x

Means: y equals g of x

2 occurrences in this chapter

• Occurrence projected-formula-0019195
• Occurrence projected-formula-0019200

Equation form expr-d6c75f6e980ad53e

$(x_0 + x_1) = y$

Read as: the sum of x subscript zero and x subscript one equals y

Means: the sum of x subscript zero and x subscript one equals y

1 occurrence in this chapter

• Occurrence projected-formula-0019035

Equation form expr-d6e7de4c36623607

$\Th{Q} \Proves (!A \lor !B)$

Read as: Q proves that A or B

Means: Q proves that A or B

1 occurrence in this chapter

• Occurrence projected-formula-0019735

Equation form expr-d73ac5aa141ceef8

$\eq[(b' + \Obj 0)][a]$

Read as: the sum of the successor of b and the object language constant zero equals a

Means: the sum of the successor of b and the object language constant zero equals a

1 occurrence in this chapter

• Occurrence projected-formula-0019357

Equation form expr-d7716462fdf37ea7

$p \mid x_i$

Read as: p divides x subscript i

Means: p divides x subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0018938

Equation form expr-d826a37801d792cd

$i \le n$

Read as: i is less than or equal to n

Means: i is less than or equal to n

2 occurrences in this chapter

• Occurrence projected-formula-0018889
• Occurrence projected-formula-0018985

Equation form expr-d89ad7af62404a57

$\Th{PA}$

Read as: P A

Means: P A

2 occurrences in this chapter

• Occurrence projected-formula-0018793
• Occurrence projected-formula-0018802

Equation form expr-d99b5e7deabebeb1

$h(x_0, \dots, x_{l-1}) = f(g_0(x_0, \dots, x_{l-1}), \dots, g_{k-1}(x_0, \dots, x_{l-1})).$

Read as: h of x subscript zero through x subscript l minus one equals f applied to the outputs of g subscript zero through g subscript k minus one, each evaluated on that same input tuple x subscript zero through x subscript l minus one

Means: h of x subscript zero through x subscript l minus one equals f applied to the outputs of g subscript zero through g subscript k minus one, each evaluated on that same input tuple x subscript zero through x subscript l minus one

1 occurrence in this chapter

• Occurrence projected-formula-0019230

Equation form expr-dabd3aff769f07eb

$<$

Read as: less than

Means: less than

3 occurrences in this chapter

• Occurrence projected-formula-0019270
• Occurrence projected-formula-0019299
• Occurrence projected-formula-0019359

Equation form expr-daf18e7eb8ca32c3

$!A_f(\num{n_0}, \dots, \num{n_k}, \num{(s)_1})$

Read as: A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for the entry at position one in the prime power sequence coded by s

Means: A subscript f applied to the numerals for n subscript zero through n subscript k, and the numeral for the entry at position one in the prime power sequence coded by s

1 occurrence in this chapter

• Occurrence projected-formula-0018862

Equation form expr-dc0460d416b96ec6

$\eq[a][c']$

Read as: a equals the successor of c

Means: a equals the successor of c

3 occurrences in this chapter

• Occurrence projected-formula-0019287
• Occurrence projected-formula-0019308
• Occurrence projected-formula-0019309

Equation form expr-dc4f7e0ff5edebdc

$\beta^*(d_0,d_1,i) & = \fn{rem}(1+(i+1) d_1,d_0) \text{ and}\\ \beta(d,i) & = \beta^*(K(d),L(d),i).$

Read as: Beta star of d subscript zero, d subscript one, and i equals the remainder when d subscript zero is divided by one plus the product of i plus one and d subscript one. Beta of d and i equals beta star of K of d, L of d, and i

Means: Beta star of d subscript zero, d subscript one, and i equals the remainder when d subscript zero is divided by one plus the product of i plus one and d subscript one. Beta of d and i equals beta star of K of d, L of d, and i

1 occurrence in this chapter

• Occurrence projected-formula-0018970

Equation form expr-dcdf8b93520408f3

$y_0$

Read as: y subscript zero

Means: y subscript zero

3 occurrences in this chapter

• Occurrence projected-formula-0018915
• Occurrence projected-formula-0018921
• Occurrence projected-formula-0018930

Equation form expr-dddec4cec1599e3c

$\Mult$

Read as: the multiplication function

Means: the multiplication function

3 occurrences in this chapter

• Occurrence projected-formula-0019012
• Occurrence projected-formula-0019452
• Occurrence projected-formula-0019458

Equation form expr-ddfe3323228fd83c

$\Value{t}{N} = n$

Read as: the value of t in the standard model N equals n

Means: the value of t in the standard model N equals n

2 occurrences in this chapter

• Occurrence projected-formula-0019597
• Occurrence projected-formula-0019621

Equation form expr-de7d1b721a1e0632

$i$

Read as: i

Means: i

3 occurrences in this chapter

• Occurrence projected-formula-0018895
• Occurrence projected-formula-0018935
• Occurrence projected-formula-0018979

Equation form expr-deacb637cca1832d

$!A_{\Char{R}}(x_0, \dots, x_k, y)$

Read as: A subscript characteristic function of R, applied to x subscript zero through x subscript k, and y

Means: A subscript characteristic function of R, applied to x subscript zero through x subscript k, and y

1 occurrence in this chapter

• Occurrence projected-formula-0019485

Equation form expr-deee498cab971fab

$\Char{=}$

Read as: the characteristic function of equality

Means: the characteristic function of equality

8 occurrences in this chapter

• Occurrence projected-formula-0018819
• Occurrence projected-formula-0018883
• Occurrence projected-formula-0018901
• Occurrence projected-formula-0018961
• Occurrence projected-formula-0018992
• Occurrence projected-formula-0019013
• Occurrence projected-formula-0019453
• Occurrence projected-formula-0019459

Equation form expr-e0822a0f0cbced9e

$f(x_0,\ldots,x_k)$

Read as: f of x subscript zero through x subscript k

Means: f of x subscript zero through x subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0018804

Equation form expr-e1636b0d23d218c1

$n + k + 1 = m$

Read as: n plus k plus one equals m

Means: n plus k plus one equals m

1 occurrence in this chapter

• Occurrence projected-formula-0019652

Equation form expr-e1ff22673febf333

$\eq/[\num{0}][\num{1}]$

Read as: the numeral for zero does not equal the numeral for one

Means: the numeral for zero does not equal the numeral for one

1 occurrence in this chapter

• Occurrence projected-formula-0019501

Equation form expr-e246d1ddfd2bc6f7

$\Setabs{!A}{\Th{Q} \Proves !A}$

Read as: the set of formulas A such that Q proves A

Means: the set of formulas A such that Q proves A

1 occurrence in this chapter

• Occurrence projected-formula-0018773

Equation form expr-e30d2435124a07e9

$l = f(n_0, \dots, n_k)$

Read as: l equals f of n subscript zero through n subscript k

Means: l equals f of n subscript zero through n subscript k

1 occurrence in this chapter

• Occurrence projected-formula-0018830

Equation form expr-e3212229d200318d

$\lnot !B$

Read as: not B

Means: not B

2 occurrences in this chapter

• Occurrence projected-formula-0019724
• Occurrence projected-formula-0019739

Equation form expr-e35c9e414191ba7e

$(\eq[\num{n}][\num{m}] \land \eq[y][\num{1}]) \lor (\eq/[\num{n}][\num{m}] \land \eq[y][\num{0}])$

Read as: either the numeral for n equals the numeral for m and y equals the numeral for one; or the numeral for n does not equal the numeral for m and y equals the numeral for zero

Means: either the numeral for n equals the numeral for m and y equals the numeral for one; or the numeral for n does not equal the numeral for m and y equals the numeral for zero

1 occurrence in this chapter

• Occurrence projected-formula-0019119

Equation form expr-e3b98a4da31a127d

$t$

Read as: t

Means: t

9 occurrences in this chapter

• Occurrence projected-formula-0019579
• Occurrence projected-formula-0019582
• Occurrence projected-formula-0019596
• Occurrence projected-formula-0019599
• Occurrence projected-formula-0019620
• Occurrence projected-formula-0019682
• Occurrence projected-formula-0019746
• Occurrence projected-formula-0019756
• Occurrence projected-formula-0019761

Equation form expr-e49d8938325a43e0

$n = \Value{t_1}{N}$

Read as: n equals the value of t subscript one in the standard model N

Means: n equals the value of t subscript one in the standard model N

1 occurrence in this chapter

• Occurrence projected-formula-0019635

Equation form expr-e4c5ac9c0248aa1c

$t_1 < t_2$

Read as: t subscript one is less than t subscript two

Means: t subscript one is less than t subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019663

Equation form expr-e4d2363b6ce3190e

$h(x) = z$

Read as: h of x equals z

Means: h of x equals z

2 occurrences in this chapter

• Occurrence projected-formula-0019192
• Occurrence projected-formula-0019196

Equation form expr-e5f403ce29d1c8e6

$\eq[y][\num{1}]$

Read as: y equals the numeral for one

Means: y equals the numeral for one

1 occurrence in this chapter

• Occurrence projected-formula-0019115

Equation form expr-e632b7095b0bf32c

$T$

Read as: T

Means: T

2 occurrences in this chapter

• Occurrence projected-formula-0019527
• Occurrence projected-formula-0019528

Equation form expr-e6ac6aa77892e7e2

$\eq[(c' + \num{m+1})][a]$

Read as: the sum of the successor of c and the numeral for m plus one equals a

Means: the sum of the successor of c and the numeral for m plus one equals a

1 occurrence in this chapter

• Occurrence projected-formula-0019401

Equation form expr-e6c5f5f3979df938

$1+d_1$

Read as: one plus d subscript one

Means: one plus d subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0018974

Equation form expr-e6d166895851cb40

$\Th{Q} \Proves !A(\num 0) \land \dots \land !A(\num k)$

Read as: Q proves that A holds of every numeral from zero through k, as a finite conjunction

Means: Q proves that A holds of every numeral from zero through k, as a finite conjunction

2 occurrences in this chapter

• Occurrence projected-formula-0019702
• Occurrence projected-formula-0019703

Equation form expr-e71563ff05fb591e

$& \eq[\num n + \num m][\num {n+m}] \text{ and}\\ & \lforall[y][(\eq[(\num n + \num m)][y] \lif \eq[y][\num{n+m}])].$

Read as: The sum of the numeral for n and the numeral for m equals the numeral for the number n plus m. And for every y, if that sum equals y, then y equals the numeral for n plus m

Means: The sum of the numeral for n and the numeral for m equals the numeral for the number n plus m. And for every y, if that sum equals y, then y equals the numeral for n plus m

1 occurrence in this chapter

• Occurrence projected-formula-0019040

Equation form expr-e7e3a5dd1bed8a04

$\eq[(b'+c)'][\Obj 0']$

Read as: the successor of the sum of the successor of b and c equals the successor of the object language constant zero

Means: the successor of the sum of the successor of b and c equals the successor of the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019313

Equation form expr-e8c17252cf9632d5

$\Char{R}$

Read as: the characteristic function of R

Means: the characteristic function of R

2 occurrences in this chapter

• Occurrence projected-formula-0019484
• Occurrence projected-formula-0019507

Equation form expr-e9079c14e05d0693

$\Th{Q} \Proves \eq/[\num n][\num m]$

Read as: Q proves that the numeral for n does not equal the numeral for m

Means: Q proves that the numeral for n does not equal the numeral for m

2 occurrences in this chapter

• Occurrence projected-formula-0019063
• Occurrence projected-formula-0019644

Equation form expr-e9ccc382bd3f2395

$\lexists[z][\eq[(z' + b)][\num{m}]]$

Read as: there exists z such that the sum of the successor of z and b equals the numeral for m

Means: there exists z such that the sum of the successor of z and b equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019378

Equation form expr-e9ebe3576784cff0

$\num{n+m+1}$

Read as: the numeral for n plus m plus one

Means: the numeral for n plus m plus one

1 occurrence in this chapter

• Occurrence projected-formula-0019136

Equation form expr-ea1b0f85ed186853

$\Th{Q} \Proves \eq[t_1][\num n_1]$

Read as: Q proves that t subscript one equals the numeral for n subscript one

Means: Q proves that t subscript one equals the numeral for n subscript one

1 occurrence in this chapter

• Occurrence projected-formula-0019607

Equation form expr-ea2d8c8da4f6c79a

$\Th{Q} \Proves \bforall{x<t}{!A(x)}$

Read as: Q proves that for every x less than t, A of x

Means: Q proves that for every x less than t, A of x

2 occurrences in this chapter

• Occurrence projected-formula-0019684
• Occurrence projected-formula-0019752

Equation form expr-ea7df4bc96e2f1e1

$!A_{\Proj{n}{i}}(x_0, \dots, x_{n-1}, y) \ident \eq[y][x_i].$

Read as: A subscript projection function with arity n and index i, applied to x subscript zero through x subscript n minus one and y, is the formula y equals x subscript i

Means: A subscript projection function with arity n and index i, applied to x subscript zero through x subscript n minus one and y, is the formula y equals x subscript i

1 occurrence in this chapter

• Occurrence projected-formula-0019049

Equation form expr-eaea22e02f98a7a8

$x_0' = y$

Read as: the successor of x subscript zero equals y

Means: the successor of x subscript zero equals y

1 occurrence in this chapter

• Occurrence projected-formula-0019034

Equation form expr-eb2e661237ddf347

$\Value{t_2}{N} = n_2$

Read as: the value of t subscript two in the standard model N equals n subscript two

Means: the value of t subscript two in the standard model N equals n subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019606

Equation form expr-ec76e63a46b447fc

$i < y$

Read as: i is less than y

Means: i is less than y

1 occurrence in this chapter

• Occurrence projected-formula-0019018

Equation form expr-eda0b1a24e71fdef

$Q_2$

Read as: Q subscript two

Means: Q subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019291

Equation form expr-ee09bac82bcf2ecc

$\Th{Q} \Proves \lforall[x][\lnot x < \Obj 0]$

Read as: Q proves that for every x, it is not the case that x is less than the object language constant zero

Means: Q proves that for every x, it is not the case that x is less than the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019267

Equation form expr-ee3f045c61a5cba0

$n \leq k$

Read as: n is less than or equal to k

Means: n is less than or equal to k

2 occurrences in this chapter

• Occurrence projected-formula-0019697
• Occurrence projected-formula-0019701

Equation form expr-ef42aeac157b2180

$\Th{Q} \Proves \lexists[y][!B_T(\num{e}, \num{n}, y)]$

Read as: Q proves that there exists y such that B subscript T holds of the numeral for e, the numeral for n, and y

Means: Q proves that there exists y such that B subscript T holds of the numeral for e, the numeral for n, and y

2 occurrences in this chapter

• Occurrence projected-formula-0019534
• Occurrence projected-formula-0019546

Equation form expr-ef5d0009ab633762

$!A \ident t_1 < t_2$

Read as: A is the formula t subscript one is less than t subscript two

Means: A is the formula t subscript one is less than t subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019646

Equation form expr-f03c4223d0e0061d

$\Th{Q} \Proves \lnot !A$

Read as: Q proves that not A

Means: Q proves that not A

4 occurrences in this chapter

• Occurrence projected-formula-0019726
• Occurrence projected-formula-0019741
• Occurrence projected-formula-0019771
• Occurrence projected-formula-0019778

Equation form expr-f091204a20056317

$\eq[b'][\Obj 0'] \lor \dots \lor \eq[b'][\num{n}']$

Read as: the successor of b equals one of the successors of the numerals from zero through n

Means: the successor of b equals one of the successors of the numerals from zero through n

1 occurrence in this chapter

• Occurrence projected-formula-0019338

Equation form expr-f29d3f9eef64b9fd

$\eq/[b'][\Obj 0]$

Read as: the successor of b does not equal the object language constant zero

Means: the successor of b does not equal the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019285

Equation form expr-f345e4b35fa6a724

$\tuple{h(\vec x, 0), h(\vec x, 1), \dots, h(\vec x, y)}$

Read as: the sequence consisting of h of the tuple x and zero, h of the tuple x and one, and so on through h of the tuple x and y

Means: the sequence consisting of h of the tuple x and zero, h of the tuple x and one, and so on through h of the tuple x and y

1 occurrence in this chapter

• Occurrence projected-formula-0019023

Equation form expr-f3e60deab2094406

$\num k$

Read as: the numeral for k

Means: the numeral for k

1 occurrence in this chapter

• Occurrence projected-formula-0019075

Equation form expr-f3f3804480e8551a

$\beta$

Read as: beta

Means: beta

6 occurrences in this chapter

• Occurrence projected-formula-0018891
• Occurrence projected-formula-0018899
• Occurrence projected-formula-0018900
• Occurrence projected-formula-0018959
• Occurrence projected-formula-0018987
• Occurrence projected-formula-0019002

Equation form expr-f476b622c6193985

$\lforall[y][(!A_{\Char{R}}(\num{n_0}, \dots, \num{n_k}, y) \lif y = \num{0})].$

Read as: for every y, if A subscript characteristic function of R holds of the numerals for n subscript zero through n subscript k, and y, then y equals the numeral for zero

Means: for every y, if A subscript characteristic function of R holds of the numerals for n subscript zero through n subscript k, and y, then y equals the numeral for zero

1 occurrence in this chapter

• Occurrence projected-formula-0019499

Equation form expr-f47dcc537d15d65c

$\lexists[y][(!A_g(x, y) \land !A_f(y, z))]$

Read as: the existential formula with bound variable y and matrix consisting of A subscript g of x and y, conjoined with A subscript f of y and z

Means: the existential formula with bound variable y and matrix consisting of A subscript g of x and y, conjoined with A subscript f of y and z

1 occurrence in this chapter

• Occurrence projected-formula-0019203

Equation form expr-f54fef43dc45d2b2

$\eq[b][\num{m}]$

Read as: b equals the numeral for m

Means: b equals the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019404

Equation form expr-f6d7e6e92d70c039

$\Obj{0}^{\prime\prime\ldots\prime}$

Read as: the object language constant zero followed by the displayed sequence of successor marks

Means: the object language constant zero followed by the displayed sequence of successor marks

1 occurrence in this chapter

• Occurrence projected-formula-0018779

Equation form expr-f6e29a7cebc04e20

$m \cdot n$

Read as: m times n

Means: m times n

1 occurrence in this chapter

• Occurrence projected-formula-0019166

Equation form expr-f88d3cb081b9e7f7

$\Th{Q} \Proves \lexists[z][\eq[z' + t_1][t_2]]$

Read as: Q proves that there exists z such that the sum of the successor of z and t subscript one equals t subscript two

Means: Q proves that there exists z such that the sum of the successor of z and t subscript one equals t subscript two

1 occurrence in this chapter

• Occurrence projected-formula-0019657

Equation form expr-f891973c7e4f4f94

$(\eq[\num{n}][\num{n}] \land \eq[y][\num{1}]) \lor (\eq/[\num{n}][\num{n}] \land \eq[y][\num{0}])$

Read as: either the numeral for n equals itself and y equals the numeral for one; or the numeral for n does not equal itself and y equals the numeral for zero

Means: either the numeral for n equals itself and y equals the numeral for one; or the numeral for n does not equal itself and y equals the numeral for zero

1 occurrence in this chapter

• Occurrence projected-formula-0019114

Equation form expr-f921fe1caca7cb62

$\lnot a < \Obj 0$

Read as: it is not the case that a is less than the object language constant zero

Means: it is not the case that a is less than the object language constant zero

1 occurrence in this chapter

• Occurrence projected-formula-0019268

Equation form expr-f96d7ac361383f38

$\lnot !A_R(\num{n_0}, \dots, \num{n_k})$

Read as: not A subscript R applied to the numerals for n subscript zero through n subscript k

Means: not A subscript R applied to the numerals for n subscript zero through n subscript k

3 occurrences in this chapter

• Occurrence projected-formula-0019473
• Occurrence projected-formula-0019481
• Occurrence projected-formula-0019504

Equation form expr-fa3ca3612e44b977

$\eq[(c' + b)'][\num{m}']$

Read as: the successor of the sum of the successor of c and b equals the successor of the numeral for m

Means: the successor of the sum of the successor of c and b equals the successor of the numeral for m

1 occurrence in this chapter

• Occurrence projected-formula-0019381

Equation form expr-fa9afbb163c9a35d

$\eq[(a' + \num{n}')][(a + \num{n}')']$

Read as: the sum of the successor of a and the successor of the numeral for n equals the successor of the sum of a and the successor of the numeral for n

Means: the sum of the successor of a and the successor of the numeral for n equals the successor of the sum of a and the successor of the numeral for n

1 occurrence in this chapter

• Occurrence projected-formula-0019261

Equation form expr-fab1ef2eb664e0ce

$\fn{Subst}$

Read as: the substitution coding function Subst

Means: the substitution coding function Subst

1 occurrence in this chapter

• Occurrence projected-formula-0018854

Equation form expr-fcfea66fe1902321

$\fn{not}(x) & \defis \Char{=}(x,0)\\ \bmin{x \leq z}{R(x,y)} & \defis \umin{x}{(R(x,y) \lor x = z)}\\ \bexists{x \leq z}{R(x,y)} & \defiff R(\bmin{x \leq z}{R(x,y)}, y)$

Read as: Three definitions without primitive recursion. Not of x is defined to be the characteristic function of equality applied to x and zero. The bounded minimum of x less than or equal to z such that R of x and y is defined to be the least x such that either R of x and y or x equals z. The bounded existential statement that there is x less than or equal to z such that R of x and y holds is defined to mean that R holds of that bounded minimum and y. End of the three definitions

Means: Three definitions without primitive recursion. Not of x is defined to be the characteristic function of equality applied to x and zero. The bounded minimum of x less than or equal to z such that R of x and y is defined to be the least x such that either R of x and y or x equals z. The bounded existential statement that there is x less than or equal to z such that R of x and y holds is defined to mean that R holds of that bounded minimum and y. End of the three definitions

1 occurrence in this chapter

• Occurrence projected-formula-0018962

Equation form expr-fdc3cd2160233f3d

$\eq/[\num n'][\num k']$

Read as: the successor of the numeral for n does not equal the successor of the numeral for k

Means: the successor of the numeral for n does not equal the successor of the numeral for k

1 occurrence in this chapter

• Occurrence projected-formula-0019093

Equation form expr-fdc5b3ea336decbd

$\Th{Q} \Proves \lnot !B$

Read as: Q proves that not B

Means: Q proves that not B

1 occurrence in this chapter

• Occurrence projected-formula-0019742

Equation form expr-ff9ba27416d63e9a

$(!A \land !B)$

Read as: the conjunction of A and B

Means: the conjunction of A and B

1 occurrence in this chapter

• Occurrence projected-formula-0019713

Eight axioms of Robinson arithmetic Q

The eight universally quantified axioms govern successor injectivity, zero not being a successor, every nonzero object being a successor, recursive addition and multiplication, and less than. The associated expression reads every axiom and its label in order. There is no induction axiom here.

Source

Representability of a numerical function in Q

A formula with input variables and one output variable represents a function when, for each actual input tuple and output value, Q proves the formula on the corresponding numerals and proves that any output satisfying it equals that output numeral. Both clauses are required; the universal uniqueness clause is inside Q, while the choice of numerical inputs is metatheoretic.

Source

Functions representable in Q are exactly the computable functions

The theorem has two directions. The chapter first computes representable functions by searching through coded proofs, then represents all general recursive functions using basic arithmetic functions, composition, and regular minimization. The theorem is stated here and proved by the subsequent sections.

Source

Provable instances of a representing formula identify the correct value

For a function represented in Q, the instance of its representing formula on input and output numerals is provable exactly when that output is the actual function value. The source proof combines representability, uniqueness, provability of inequality of distinct numerals, and consistency of Q from its standard model.

Source

Every function representable in Q is computable

The proof first describes a search for a derivation of a numeral instance of the representing formula. It then makes the search numerical using substitution codes, the primitive recursive proof relation, and regular minimization of codes of proof and output pairs. A proof exists for every input, and the preceding lemma ensures that its output is correct.

Source

Nested substitutions defining the numeral instance code

Start with the Goedel number of the representing formula. Substitute the appropriate numeral code for each input variable in order, then the output numeral code for the output variable. The display is a nested functional definition, not a derivation tree. The associated speech preserves the distinction between each numerical input, its numeral, and that numeral code.

Source

The beta function lemma

There is a function beta such that every finite sequence can be decoded from some natural number d: beta of d and i returns the entry at position i. Beta is definable using basic functions, composition, and regular minimization, without primitive recursion. This coding is explicitly different from the earlier prime power coding. The lemma asserts existence of a suitable code, not an algorithm constructing that code within the restricted resources.

Source

Relatively prime natural numbers

Two natural numbers are relatively prime when their greatest common divisor is one. The definition concerns common divisors; it does not require that either number itself be prime.

Source

Congruence modulo a natural number

The definition says that a and b are congruent modulo c when c divides their difference, equivalently when they have the same remainder on division by c. The modular parameter and the direction of division are retained.

Source

Sunzi theorem on simultaneous congruences

Given pairwise relatively prime moduli x subscript zero through x subscript n and arbitrary residues y subscript zero through y subscript n, there exists a number z satisfying all the displayed congruences simultaneously. The source also identifies this as the theorem traditionally called the Chinese Remainder Theorem.

Source

System of simultaneous congruences

Every row uses the same unknown z. Row i says that z is congruent to y subscript i modulo x subscript i, for indices zero through n. The rows are simultaneous conditions, not successive transformations of z.

Source

Choice of bounds and common multiple for sequence coding

j is the maximum of n and one greater than each proposed residue. m is the least common multiple of the integers from one through j. These choices are used to construct moduli larger than their residues and pairwise relatively prime.

Source

The chosen family of moduli

The modulus with index i is one plus the product of i plus one and m. The display gives the first three members and the final member. Its continuation preserves both the index shift by one and the added one outside the product.

Source

Negation and bounded operations from minimization

Three displayed definitions express the numerical Boolean not function, a bounded minimum with endpoint fallback, and a bounded existential relation. The last definition tests R at the bounded minimum. The endpoint z ensures termination of the unbounded search used inside the bounded minimum.

Source

The two inverse coordinate functions of the pairing map

K searches for the first coordinate of a pair coded by z; L searches for the second. Each search and its witnessing quantifier is bounded by z. Both tests use the same pairing function J with its argument order x then y.

Source

Definitions of beta star and beta

Beta star takes a residue code, a modulus spacing parameter, and an index, and returns the remainder modulo one plus the product of the index plus one and the spacing parameter. Beta first extracts the two coordinates of d using K and L. The first argument of rem is the divisor, not the dividend.

Source

Verification that beta returns the chosen sequence entry

The three equal quantities are beta of d and i, beta star of the two coordinates and i, and the appropriate remainder, which equals a subscript i. Sunzi theorem and the previously selected bounds supply the final equality.

Source

Exercise defining order divisibility and remainder without primitive recursion

The source asks the reader to define less than, divisibility, and rem without primitive recursion. The permitted resources are zero, successor, addition, multiplication, the characteristic function of equality, projections, bounded minimization, and bounded quantification. No solution is supplied here.

Source

Primitive recursion equations for h

The base value at last argument zero is f of the parameter tuple. The value at last argument y plus one is g of the parameter tuple, y, and the previous value h at y. The parameter tuple is unchanged in both equations.

Source

Simulation of primitive recursion by regular minimization

A function defined by primitive recursion from f and g can instead be defined using those functions, zero, successor, projections, addition, multiplication, the characteristic function of equality, composition, and regular minimization. The proof searches for a beta code of a finite sequence satisfying the recursion and then decodes its last entry.

Source

Two requirements for representing addition

The first requirement states the correct sum of two numerals. The second universally quantifies the output variable and says any output equal to that sum equals the numeral of the numerical sum. These are the value and uniqueness conditions for representability.

Source

Representability of the zero function

The zero function maps every input to zero. Its representing formula says that the output variable equals the object language constant zero. The input variable need not occur in this formula.

Source

Representability of the successor function

The successor function maps x to x plus one. Its representing formula says that the output variable equals the successor term on the input variable.

Source

Representability of projection functions

The projection function with arity n and index i returns input coordinate i. Its representing formula states equality of the output variable with that coordinate. The indexing runs from zero to n minus one.

Source

Exercise proving representability of the three initial functions

Prove that the three displayed equality formulas represent zero, successor, and the indicated projection, respectively. The proof is left to the reader; no solution is added.

Source

Representability of the characteristic function of equality

The numerical function returns one for equal inputs and zero otherwise. The representing formula is a disjunction: equal input terms together with output numeral one, or unequal input terms together with output numeral zero. The proof separates the equal and unequal cases and verifies uniqueness in each.

Source

Q proves inequality of distinct numerals

For any two distinct natural numbers, Q proves that their numerals are unequal. The proof is by external induction on one of the numbers, using the successor axioms. It does not assert that Q internally proves a universally quantified inequality principle by induction.

Source

Representability of addition

The numerical addition function is represented by equality between the output variable and the object language sum of the two input variables. The following numerical evaluation lemma supplies the value condition, and equality reasoning supplies uniqueness.

Source

Q computes each sum of numerals

Q proves that the object language sum of the numeral for n and the numeral for m equals the numeral for the number n plus m. The proof uses external induction on m, with the zero and successor axioms for addition.

Source

Representability of multiplication

The numerical multiplication function is represented by equality between the output variable and the object language product of the input variables. The proof is marked Exercise in the source and remains unsolved.

Source

Q computes each product of numerals

Q proves that the object language product of the numerals for n and m equals the numeral for their numerical product. The proof is marked Exercise in the source and is not filled in.

Source

Exercise proving the numeral multiplication lemma

Prove the preceding lemma that Q evaluates products of numerals. The lemma reference is retained, and the source exercise remains unsolved.

Source

Exercise proving representability of multiplication

Use the numeral multiplication lemma to prove representability of multiplication. Both source references are retained; no new proof is supplied.

Source

Composition satisfies the value clause of representability

For the unary composition h of x equal to f of g of x, whenever h of n equals m, Q proves the proposed representing formula on the numerals for n and m. The proof uses the actual intermediate value k equal to g of n as an existential witness.

Source

Deriving the correct numeral instance for composition

Q proves the two representing instances for g and f, then their conjunction, then existentially quantifies the intermediate value. Interleaved source explanations identify which representing formula justifies each initial instance. The displayed steps form a linear derivation.

Source

Composition satisfies the uniqueness clause of representability

When h of n equals m, Q proves that every output z satisfying the proposed formula for h equals the numeral for m. The proof applies the uniqueness properties of g and f in sequence.

Source

Deriving uniqueness for a composition

The first universal statement forces the intermediate variable y to equal the numeral for k. The second forces z to equal the numeral for m. Logic then yields the universal uniqueness statement for the existentially composed formula. Quantifier scopes remain attached to their own conclusions.

Source

Representability is preserved under general composition

For a function f of k inputs and inner functions each of l inputs, existentially bind k intermediate variables. Conjoin every representing formula for the inner functions at the shared input tuple with the representing formula for f at those intermediate values and the output. The proof is marked Exercise and remains unsolved.

Source

Formula representing a general composition

There is one existential intermediate variable for each inner function. All inner representing formulas and the outer representing formula belong within the scope of all these quantifiers. The displayed ellipsis abbreviates the intervening conjunctions in index order.

Source

Exercise proving representability under general composition

Give the detailed proof of representability for general composition, using the preceding unary arguments as a guide. The source repeats the reference to the uniqueness proposition; that source reference defect is disclosed rather than silently changed. No solution is supplied.

Source

Moving successor past addition by a fixed numeral

For any constant a and natural number n, Q proves that the sum of the successor of a and the numeral for n equals the successor of the sum of a and that numeral. The parentheses are essential: the successor on the right applies to the whole sum. The source inductive derivation has a disclosed misidentified step and is preserved without a replacement proof.

Source

Base case of the fixed numeral successor identity

Two instances of the addition zero axiom identify the two sums. Applying successor to one equality and combining equalities gives the target base case. Four displayed lines retain their step labels and dependencies.

Source

Source inductive steps for the fixed numeral successor identity

The source presents step five from the addition successor axiom, step six attributed to induction, and a final equality attributed to both steps. The line labeled step six is already the desired successor case rather than the induction hypothesis. The source lines and this caveat are preserved; they are not treated as an independently verified proof.

Source

Q proves that nothing is less than zero

The lemma universally negates being less than the object language constant zero. The source proof expands the definition of less than, separates the zero and successor cases, and derives contradictions with the zero and successor axioms.

Source

Every object below a numeral is one of finitely many numerals

For every natural number n, Q proves that anything less than the numeral for n plus one equals one of the numerals zero through n. The external induction establishes a finite disjunction inside Q for each chosen bound.

Source

Trichotomy against each fixed numeral

For every natural number m, Q proves that each y is less than the numeral for m, greater than it, or equal to it. This is a separate provability claim for each numeral, proved by external induction; it is not stated as unrestricted internal trichotomy for two arbitrary variables.

Source

Induction hypothesis and target for fixed numeral trichotomy

The first displayed universal trichotomy is against the numeral for m. The second, introduced as the goal, is against the numeral for m plus one. Each has the same three alternatives in the same order.

Source

Representability is preserved under regular minimization

Given the representing formula for a regular function g, the formula for its least zero requires g to have value zero at the proposed output and not to have value zero at any smaller number. The universal bounded condition ensures leastness. The surrounding hypothesis of regularity ensures the numerical function is total.

Source

The value clause for the minimizing formula

The derivation combines the provable zero instance at the actual minimum with the negations of all smaller numeral instances. The finite numeral bound lemmas then yield the universal statement excluding every smaller object. Source explanations between rows are part of the linear reading, not omitted captions.

Source

Every computable function is representable in Q

Using general recursive functions as the precise model of computation, replace primitive recursion with the established simulation, represent each basic function, and apply closure under composition and regular minimization. The accompanying discussion distinguishes representability from the strength of a theory in proving arbitrary sentences.

Source

Representability of relations in Q

A formula represents a relation when Q proves its numeral instance whenever the relation holds, and proves the negation of that instance whenever the relation does not hold. Both positive and negative instances are required.

Source

Relations representable in Q are exactly the computable relations

The forward direction searches in parallel for a proof of the positive or negative instance. The backward direction represents the computable characteristic function and fixes its output argument to numeral one. Its unique output zero in the false case gives the required negative instance.

Source

Exercise relating representability of a relation and its characteristic function

Show that representability of R implies representability of its characteristic function. The source leaves this direction as an exercise, and no proof is added.

Source

Undecidability of Q

The provability relation restricts y to sentence codes and asserts existence of a derivation code in Q. The theorem says this relation is not recursive. The proof reduces halting to whether a sentence asserting a Kleene T witness is provable, using the standard model of Q to exclude false existential conclusions.

Source

Undecidability of first order logic

Because Q has finitely many axioms, provability from Q can be reduced to logical provability of an implication whose antecedent is the conjunction of those axioms. A decision procedure for first order logic would therefore decide Q, contradicting the preceding theorem.

Source

Bounded existential and universal formulas

A bounded existential requires both x less than its bound and A of x. A bounded universal says that x less than the bound implies A of x. Their compact bounded quantifier notations preserve these different connectives. The usual restriction that the bound not depend on the quantified variable is not stated in the source, and this omission is disclosed.

Source

Delta zero Sigma one and Pi one formulas

Delta zero formulas are built from atomic formulas by propositional connectives and bounded quantification. In the displayed definitions a Sigma one formula has an existential quantifier before a Delta zero formula, while a Pi one formula has a universal quantifier before a Delta zero formula.

Source

Q proves each closed term equal to its standard numeral

For a closed arithmetic term whose value in the standard model is n, Q proves its equality with the numeral for n. The proof uses structural induction on terms, the equality rules, and the previously established numeral arithmetic facts. The multiplication case is explicitly left for the following exercise.

Source

Exercise for the multiplication case of closed term evaluation

Give the detailed multiplication case of the closed term evaluation lemma. The source reference and the multiplication symbol are retained, and no solution is added.

Source

Atomic completeness for closed arithmetic terms

Four clauses cover equal standard values, unequal standard values, strict less than, and failure of strict less than. They conclude provability in Q of the corresponding equality, inequality, order statement, or negated order statement. The source proof contains a numeral index typo and incorrect contradiction axiom references; these are disclosed without claiming the printed steps are correct.

Source

Bounded quantification over a closed term reduces to a finite combination

If the closed bound has standard value k, a bounded universal is provable exactly when the conjunction of its numeral instances from zero through k minus one is provable. The existential counterpart uses their disjunction. The source proof treats the universal case and leaves the existential case to an exercise. Its zero bound paragraph misnames the empty conjunction as a disjunction; the mismatch is disclosed.

Source

Exercise proving the bounded existential equivalence

Give the detailed existential case of the bounded quantifier equivalence lemma. The exercise remains unsolved.

Source

Delta zero completeness of Q

Every Delta zero sentence true in the standard model is provable in Q. The source proof proceeds by formula complexity, separates positive and negated connective cases, reduces bounded quantifiers to finite combinations, and handles atomic negations and double negation. It leaves the detailed existential case for the following exercise.

Source

Exercise proving the existential case of Delta zero completeness

Give the detailed existential case of the Delta zero completeness lemma. No solution is supplied in the source or added by this edition.

Source

Sigma one completeness of Q

Every Sigma one sentence true in the standard model is provable in Q. Choose its standard numerical witness, substitute the corresponding numeral into the Delta zero matrix, apply Delta zero completeness, and introduce the existential quantifier. The source satisfaction statement explicitly uses assignment s for the free variable before numeral substitution.

Source

Cross-reference reference-000672

the definition of function representability in Q

Source occurrence

Cross-reference reference-000673

its first clause, proving the correct numeral instance

Source occurrence

Cross-reference reference-000674

the definition of function representability in Q

Source occurrence

Cross-reference reference-000675

its first clause, proving the correct numeral instance

Source occurrence

Cross-reference reference-000676

the definition of function representability in Q

Source occurrence

Cross-reference reference-000677

its second clause, proving uniqueness of the output

Source occurrence

Cross-reference reference-000678

the lemma that Q proves distinct numerals unequal

Source occurrence

Cross-reference reference-000679

the definition of the standard model of arithmetic

Source occurrence

Cross-reference reference-001840

the soundness corollary that satisfiable theories are consistent, for axiomatic derivations

Source occurrence

Cross-reference reference-001841

the soundness corollary that satisfiable theories are consistent, for sequent calculus

Source occurrence

Cross-reference reference-001842

the soundness corollary that satisfiable theories are consistent, for natural deduction

Source occurrence

Cross-reference reference-001843

the soundness corollary that satisfiable theories are consistent, for tableaux

Source occurrence

Cross-reference reference-000680

the lemma equating provable representing instances with correct function values

Source occurrence

Cross-reference reference-000681

the lemma equating provable representing instances with correct function values

Source occurrence

Cross-reference reference-000682

the proposition that numeral coding is primitive recursive

Source occurrence

Cross-reference reference-000683

the proposition that substitution coding is primitive recursive

Source occurrence

Cross-reference reference-000684

the first observation, that the chosen moduli are relatively prime

Source occurrence

Cross-reference reference-000685

the second observation, that each residue is smaller than its modulus

Source occurrence

Cross-reference reference-000686

the first observation, that the chosen moduli are relatively prime

Source occurrence

Cross-reference reference-000687

the second observation, that each residue is smaller than its modulus

Source occurrence

Cross-reference reference-000688

the beta function lemma

Source occurrence

Cross-reference reference-000689

the proposition representing the characteristic function of equality

Source occurrence

Cross-reference reference-000690

the lemma that Q proves distinct numerals unequal

Source occurrence

Cross-reference reference-000691

the lemma that Q proves distinct numerals unequal

Source occurrence

Cross-reference reference-000692

the proposition representing addition

Source occurrence

Cross-reference reference-000693

the lemma that Q computes sums of numerals

Source occurrence

Cross-reference reference-000694

the lemma that Q computes products of numerals

Source occurrence

Cross-reference reference-000695

the lemma that Q computes products of numerals

Source occurrence

Cross-reference reference-000696

the proposition representing multiplication

Source occurrence

Cross-reference reference-000697

the proposition giving the uniqueness clause for unary composition

Source occurrence

Cross-reference reference-000698

the proposition giving the uniqueness clause for unary composition

Source occurrence

Cross-reference reference-000699

the proposition representing general composition

Source occurrence

Cross-reference reference-000700

step two of the successor and fixed numeral addition derivation

Source occurrence

Cross-reference reference-000701

step one of the successor and fixed numeral addition derivation

Source occurrence

Cross-reference reference-000702

step three of the successor and fixed numeral addition derivation

Source occurrence

Cross-reference reference-000703

step five of the successor and fixed numeral addition derivation

Source occurrence

Cross-reference reference-000704

step six of the successor and fixed numeral addition derivation

Source occurrence

Cross-reference reference-000705

the lemma that Q proves nothing is less than zero

Source occurrence

Cross-reference reference-000706

the lemma that Q proves nothing is less than zero

Source occurrence

Cross-reference reference-000707

the lemma enumerating the objects less than a fixed numeral

Source occurrence

Cross-reference reference-000708

the lemma on trichotomy against each fixed numeral

Source occurrence

Cross-reference reference-000709

the displayed proof excluding all values below the minimum

Source occurrence

Cross-reference reference-000710

the lemma simulating primitive recursion by regular minimization

Source occurrence

Cross-reference reference-000711

the proposition representing the zero function

Source occurrence

Cross-reference reference-000712

the proposition representing the successor function

Source occurrence

Cross-reference reference-000713

the proposition representing projection functions

Source occurrence

Cross-reference reference-000714

the proposition representing the characteristic function of equality

Source occurrence

Cross-reference reference-000715

the proposition representing addition

Source occurrence

Cross-reference reference-000716

the proposition representing multiplication

Source occurrence

Cross-reference reference-000717

the proposition representing general composition

Source occurrence

Cross-reference reference-000718

the proposition representing regular minimization

Source occurrence

Cross-reference reference-000719

the theorem that function representability in Q is equivalent to computability

Source occurrence

Cross-reference reference-000720

Kleene normal form theorem

Source occurrence

Cross-reference reference-000721

the theorem that the halting problem is not computable

Source occurrence

Cross-reference reference-000722

the theorem on Sigma one completeness of Q

Source occurrence

Cross-reference reference-000723

the lemma that Q computes sums of numerals

Source occurrence

Cross-reference reference-000724

the lemma that Q computes products of numerals

Source occurrence

Cross-reference reference-000725

the closed term evaluation lemma

Source occurrence

Cross-reference reference-000726

the closed term evaluation lemma

Source occurrence

Cross-reference reference-000727

the closed term evaluation lemma

Source occurrence

Cross-reference reference-000728

the lemma that Q proves nothing is less than zero

Source occurrence

Cross-reference reference-000729

the closed term evaluation lemma

Source occurrence

Cross-reference reference-000730

the atomic completeness lemma

Source occurrence

Cross-reference reference-000731

the lemma enumerating the objects less than a fixed numeral

Source occurrence

Cross-reference reference-000732

the bounded quantifier equivalence lemma

Source occurrence

Cross-reference reference-000733

the atomic completeness lemma

Source occurrence

Cross-reference reference-000734

the bounded quantifier equivalence lemma

Source occurrence

Cross-reference reference-000735

the atomic completeness lemma

Source occurrence

Cross-reference reference-000736

the Delta zero completeness lemma

Source occurrence

Cross-reference reference-000737

the Delta zero completeness lemma

Source occurrence

Source disclosures

• TR036-SAR-001: The lemma introduces its representing formula as A and then writes A subscript f in the display. These are the same representing formula in this argument. The source notation is retained. source
• TR036-SAR-002: The last argument in this source occurrence is the numerical sequence entry, where a numeral for that entry is required as the syntactic argument of A subscript f. The earlier instance in the same paragraph uses that numeral. This notation omission is preserved and disclosed. source
• TR036-SAR-003: The introductory occurrence writes h of x and the tuple z, but the defining equations use h of the tuple x and the last recursion argument. The equations supply the parameter order used throughout the proof. The source mismatch is retained. source
• TR036-SAR-004: Here h hat returns a number coding the displayed sequence, not the sequence itself. This is the number minimized in the next display and passed to beta. The source calls it the sequence as shorthand. source
• TR036-SAR-005: The exercise cites the unary uniqueness proposition twice. Its two preceding unary proofs establish the value and uniqueness clauses, respectively. The repeated source reference is retained, and the exercise remains unsolved. source
• TR036-SAR-006: Step six is labeled induction hypothesis, but its displayed statement is the successor case being proved. The final line then combines that target with step five. These printed steps do not themselves establish the claimed induction step. The source derivation is preserved without an invented replacement proof. source
• TR036-SAR-007: The usual bounded quantifier convention also requires that the bounding term not contain the variable being quantified. The source says any term without stating that restriction. This qualification is disclosed while the original definition remains visible. source
• TR036-SAR-008: The source fixes m as the value of t subscript two but then writes that t subscript two equals the numeral for n. In that preliminary line the second numeral should be the numeral for m. The source index error is preserved and identified. source
• TR036-SAR-009: The two contradictions with a successor equaling zero cite Q subscript three. The axiom stating that zero is not a successor is Q subscript two. The original axiom labels remain in the source and reading, with this reference error disclosed. source
• TR036-SAR-010: This is the zero bound case for a universal quantifier, so the empty combination is a conjunction and is true. The source calls it an empty disjunction, which would instead be false. That word error is preserved and disclosed. source