Beyond First-order Logic

Equation form expr-0392a7f58dc6f6ba

0

Read as: object language zero

Means: The object-language zero term of higher-order natural-number type; in the arithmetic instance it denotes zero.

1 occurrence in this chapter

Occurrence projected-formula-0012188

Equation form expr-043a718774c572bd

s

Read as: s

Means: The symbol s names a term, a variable assignment, or the base value of a recursive definition, as fixed by the local source sentence.

7 occurrences in this chapter

Equation form expr-05ed70c9ac00f1f2

λ x . s

Read as: lambda x dot s

Means: The function abstraction binds x in body s; when x has type tau and s has type sigma, the abstraction has type from tau to sigma. Its value may depend on x, and it is constant only if x is not free in s.

2 occurrences in this chapter

Equation form expr-071176c2ecd1d441

{\sqrt{2}}^{2} = 2

Read as: the square root of two squared equals two

Means: The standard calculation that squaring the positive square root of two gives two.

1 occurrence in this chapter

Occurrence projected-formula-0012253

Equation form expr-074378e6f960b402

\neg \neg A \to A

Read as: if not not A, then A

Means: The double-negation elimination schema, which is classically valid but not generally intuitionistically valid.

1 occurrence in this chapter

Occurrence projected-formula-0012293

Equation form expr-077e6ee303b5fa83

M, w ⊩ (A \to B)

Read as: model M forces if A then B at world w

Means: The Kripke forcing assertion for a conditional at world w.

1 occurrence in this chapter

Occurrence projected-formula-0012332

Equation form expr-0a8b1ea54e5be60e

A^{N}

Read as: the double negation translation of A

Means: Formula A superscript N is the recursively defined double-negation translation of A into intuitionistic logic.

5 occurrences in this chapter

Equation form expr-0bed48cb576984fd

\begin{matrix} R_{s t} (0) & = s \\ R_{s t} (x + 1) & = t (x, R_{s t} (x)), \end{matrix}

Read as: R sub s t at zero equals s; and R sub s t at x plus one equals t applied to x and R sub s t at x

Means: The two recursion equations defining the higher-type recursor R sub s t from base term s and step term t.

1 occurrence in this chapter

Occurrence projected-formula-0012223

Equation form expr-0bfe935e70c321c7

u

Read as: u

Means: The symbol u names a Kripke world in the intuitionistic forcing discussion.

3 occurrences in this chapter

Equation form expr-0f32ae3487ab888f

Γ \cup Δ ⊢ A

Read as: Gamma union Delta syntactically derives A

Means: Formula A is derivable when both the premises in Gamma and the comprehension axioms in Delta are available.

1 occurrence in this chapter

Occurrence projected-formula-0012141

Equation form expr-122181bf4dbc6fc4

T_{τ}

Read as: T sub tau

Means: The set of semantic values assigned to objects of type tau in a weak higher-type structure.

1 occurrence in this chapter

Occurrence projected-formula-0012241

Equation form expr-148de9c5a7a44d19

p

Read as: world p

Means: The symbol p names a possible world in the modal accessibility example.

2 occurrences in this chapter

Equation form expr-1581d72466c85316

x_{k}

Read as: x sub k

Means: The final member of an indexed list of first-order terms or arguments.

2 occurrences in this chapter

Equation form expr-162f1d040398ccb3

\forall x \neg (German (x) \land French (x))

Read as: for every x, it is not the case that x is both German and French

Means: The disjointness axiom separating the German and French sorts in the first-order encoding.

1 occurrence in this chapter

Occurrence projected-formula-0012049

Equation form expr-19581e27de7ced00

9

Read as: nine

Means: The natural number nine, used in the classically specified Riemann-hypothesis example.

1 occurrence in this chapter

Occurrence projected-formula-0012250

Equation form expr-2160509ff364e743

M

Read as: structure M

Means: The structure M fixed by context: an arithmetic structure in the categoricity argument or an arbitrary structure in the later definition of infinity.

6 occurrences in this chapter

Equation form expr-233478f0880b5b93

\begin{matrix} □ (A \to B) \to (□ A \to □ B) \\ □ A \to A \\ □ A \to □ □ A \\ as well as a rule, “from A conclude □ A .” S 5 adds the following axiom: \\ ◇ A \to □ ◇ A \end{matrix}

Read as: S four axioms: if it is necessary that A implies B, then necessary A implies necessary B; if A is necessary, then A; and if A is necessary, then necessarily necessary A. Necessitation permits inferring necessary A from A. S five also has: if A is possible, then it is necessarily possible

Means: The display lists the distribution, reflexivity, and positive-introspection axioms of S four, the necessitation rule, and the additional S five axiom.

1 occurrence in this chapter

Occurrence projected-formula-0012365

Equation form expr-2336e7fb467f4721

f (x + 1) ='^{M} (f (x))

Read as: f of x plus one equals the interpretation of successor in M applied to f of x

Means: The recursive step defining the comparison map from the natural numbers into a model of the second-order arithmetic axioms.

1 occurrence in this chapter

Occurrence projected-formula-0012105

Equation form expr-23fac266c08cc34b

p_{i}

Read as: propositional variable p sub i

Means: The indexed propositional variable whose forcing value is specified at a Kripke world.

1 occurrence in this chapter

Occurrence projected-formula-0012323

Equation form expr-240381337f804e9f

A \to B

Read as: if A then B

Means: The conditional with antecedent A and consequent B.

1 occurrence in this chapter

Occurrence projected-formula-0012282

Equation form expr-240e72e002c918ce

σ \to τ

Read as: the function type from sigma to tau

Means: The type whose objects are functions taking inputs of type sigma to outputs of type tau.

5 occurrences in this chapter

Equation form expr-252f10c83610ebca

f

Read as: f

Means: The symbol f names the function fixed by context: the recursive comparison map, an arbitrary unary function represented by a binary relation, a quantified function, or the function denoted by a lambda abstraction.

9 occurrences in this chapter

Equation form expr-27c6915250a4736d

\neg \exists A (\exists x A (x) \land \exists y \neg A (y) \land \forall w \forall z ((A (w) \land \neg A (z)) \to \neg R (w, z))) .

Read as: there does not exist a vertex property A such that some x has A, some y does not have A, and every w and z with A of w and not A of z fail to be related by R

Means: This second-order sentence states graph connectedness by ruling out a nontrivial partition with no R edge across it.

1 occurrence in this chapter

Occurrence projected-formula-0012134

Equation form expr-28a1475f37b0a34e

\forall x (x + 0) = x

Read as: for every x, x plus zero equals x

Means: The right-zero recursion axiom for addition in second-order arithmetic.

1 occurrence in this chapter

Occurrence projected-formula-0012093

Equation form expr-2affe4bb223283d3

\forall x \exists! y R (x, y)

Read as: for every x there exists exactly one y such that R holds of x and y

Means: The total single-valued condition that lets a binary relation R represent a unary function.

1 occurrence in this chapter

Occurrence projected-formula-0012129

Equation form expr-2b029b1e58a6db16

p_{2} (s)

Read as: the second projection of s

Means: The projection term selecting the second component of the pair denoted by s.

2 occurrences in this chapter

Equation form expr-2b84df7314786518

\forall R ((R (0) \land \forall x (R (x) \to R (x^{'}))) \to \forall x R (x)) .

Read as: for every relation R, if R holds of zero and is closed under successor, then R holds of every x

Means: The full second-order induction axiom for the natural numbers.

1 occurrence in this chapter

Occurrence projected-formula-0012088

Equation form expr-2d0f1dd71d1f3097

ℕ \to Ω

Read as: the function type from the natural numbers to truth values

Means: The higher-order type of characteristic functions of subsets of the natural numbers.

1 occurrence in this chapter

Occurrence projected-formula-0012165

Equation form expr-2d711642b726b044

x

Read as: x

Means: The variable x names an individual, number, term argument, type variable, or Kripke-state witness as fixed by its occurrence context.

16 occurrences in this chapter

Equation form expr-2e7d2c03a9507ae2

c

Read as: c

Means: The variable c ranges over French citizens in the many-sorted example.

1 occurrence in this chapter

Occurrence projected-formula-0012039

Equation form expr-2f2669c71360e8cf

S

Read as: object language successor

Means: The distinguished successor constant of higher type from natural numbers to natural numbers.

1 occurrence in this chapter

Occurrence projected-formula-0012190

Equation form expr-2f7464f7da95c732

w^{'} \geq w

Read as: world w prime is at least world w

Means: World w prime is a future state extending world w in the Kripke partial order.

1 occurrence in this chapter

Occurrence projected-formula-0012333

Equation form expr-32a1f77ab6d24bbb

French (x)

Read as: x is French

Means: The unary first-order predicate marking membership in the French sort.

1 occurrence in this chapter

Occurrence projected-formula-0012050

Equation form expr-33a9c96304bcc292

| M |

Read as: the domain of structure M

Means: The first-order domain underlying structure M.

1 occurrence in this chapter

Occurrence projected-formula-0012111

Equation form expr-34ea3774f28a03cc

3^{\log_{3} x} = x

Read as: three to the logarithm base three of x equals x

Means: The inverse relation between base-three exponentiation and the base-three logarithm.

1 occurrence in this chapter

Occurrence projected-formula-0012269

Equation form expr-361740d1927f400f

a^{b}

Read as: a to the power b

Means: The real-number exponential whose base a and exponent b are chosen to be irrational.

1 occurrence in this chapter

Occurrence projected-formula-0012256

Equation form expr-363b76072bd6f50b

\forall x \forall y (x + y^{'}) = {(x + y)}^{'}

Read as: for every x and y, x plus the successor of y equals the successor of x plus y

Means: The successor recursion axiom for addition.

1 occurrence in this chapter

Occurrence projected-formula-0012094

Equation form expr-38b121987a673f8d

\forall a \forall x [(MarriedTo (a, x) \to (DrinksWine (a) \lor \neg EatsWurst (x))]]

Read as: for every French person a and every German person x, if a is married to x, then a drinks wine or x does not eat wurst

Means: A well-sorted example sentence whose quantifiers range over the French and German sorts respectively.

1 occurrence in this chapter

Occurrence projected-formula-0012043

Equation form expr-3a2254dc86e62be8

b = \log_{3} 4

Read as: b equals the logarithm base three of four

Means: The explicit irrational exponent chosen for the constructive witness pair.

1 occurrence in this chapter

Occurrence projected-formula-0012267

Equation form expr-3e23e8160039594a

b

Read as: b

Means: The symbol b is an irrational-number witness in the intuitionistic example or a variable ranging over French citizens in the many-sorted example.

4 occurrences in this chapter

Equation form expr-3f4d89655d2a221f

0,', +, \times

Read as: object language zero, object language successor, addition, and multiplication

Means: Four of the nonlogical symbols in the displayed second-order language of arithmetic; the surrounding prose adds strict order.

1 occurrence in this chapter

Occurrence projected-formula-0012089

Equation form expr-42b8f19ae63d24a4

M

Read as: structure M

Means: An arbitrary full second-order structure satisfying the categorical arithmetic axioms.

2 occurrences in this chapter

Equation form expr-435599bfdd587fb6

a = b = \sqrt{2}

Read as: a equals b equals the square root of two

Means: The first nonconstructive case chooses both irrational witnesses to be the square root of two.

1 occurrence in this chapter

Occurrence projected-formula-0012258

Equation form expr-448918e3f4404d43

a^{b} = {\sqrt{3}}^{\log_{3} 4} = 3^{1 / 2 \cdot \log_{3} 4} = {(3^{\log_{3} 4})}^{1 / 2} = 4^{1 / 2} = 2,

Read as: a to the power b equals the square root of three to the logarithm base three of four, equals three to one half times that logarithm, equals the quantity three to that logarithm raised to one half, equals four to one half, equals two

Means: The explicit calculation proving that the chosen irrational base and exponent have rational value two.

1 occurrence in this chapter

Occurrence projected-formula-0012268

Equation form expr-4509f530886a42f1

R (x_{1}, \dots, x_{k})

Read as: R holds of x sub one through x sub k

Means: A second-order atomic formula applying the k-ary relation variable R to k first-order terms.

1 occurrence in this chapter

Occurrence projected-formula-0012083

Equation form expr-46f433eef3ed2d83

\forall x A

Read as: for every x, A

Means: Universal quantification of formula A with respect to x.

1 occurrence in this chapter

Occurrence projected-formula-0012046

Equation form expr-4711bceed46b8379

German

Read as: the German sort predicate

Means: The unary predicate used to mark objects belonging to the German sort in the first-order translation.

1 occurrence in this chapter

Occurrence projected-formula-0012044

Equation form expr-4feaf0824cc8e0d1

⊨

Read as: semantic entailment

Means: The consequence relation evaluated using the weak second-order semantics in this occurrence.

1 occurrence in this chapter

Occurrence projected-formula-0012136

Equation form expr-50e721e49c013f00

w

Read as: world w

Means: The Kripke world w at which a formula is evaluated.

2 occurrences in this chapter

Equation form expr-5136fc4246e7d497

◇

Read as: the possibility operator

Means: The modal diamond operator, read as possibility.

1 occurrence in this chapter

Occurrence projected-formula-0012352

Equation form expr-531f1d8ca159fbe9

\sqrt{2}

Read as: the square root of two

Means: The positive square root of two.

1 occurrence in this chapter

Occurrence projected-formula-0012263

Equation form expr-537e40bfd7ec98eb

R (p, q)

Read as: world p accesses world q

Means: The modal accessibility relation R holds from possible world p to possible world q.

1 occurrence in this chapter

Occurrence projected-formula-0012346

Equation form expr-559aead08264d579

A

Read as: A

Means: The capital letter A names one of the basic higher-order types in this occurrence.

1 occurrence in this chapter

Occurrence projected-formula-0012154

Equation form expr-55d1823545b5b4c3

τ

Read as: type tau

Means: The Greek letter tau names a finite type, a function input type, or a semantic type index.

12 occurrences in this chapter

Equation form expr-57885e4c75965b23

Γ

Read as: Gamma

Means: Gamma denotes the current premise set in either the second-order completeness statement or the double-negation translation theorem.

1 occurrence in this chapter

Occurrence projected-formula-0012302

Equation form expr-57a641fd810b5a91

⊢

Read as: syntactic derivability

Means: The turnstile denotes derivability in the minimal second-order proof system.

1 occurrence in this chapter

Occurrence projected-formula-0012135

Equation form expr-57c1d36e705bef36

M = ⟨ W, R, V ⟩

Read as: Kripke model M equals the ordered triple W, R, V

Means: The propositional Kripke model consists of worlds W, an order R, and a monotone valuation V.

1 occurrence in this chapter

Occurrence projected-formula-0012308

Equation form expr-57dee22936161a96

R (t_{1}, \dots, t_{k})

Read as: R holds of t sub one through t sub k

Means: An atomic second-order formula applying the k-ary relation variable R to k first-order terms.

1 occurrence in this chapter

Occurrence projected-formula-0012059

Equation form expr-592836a5b6df2ca8

French

Read as: the French sort predicate

Means: The unary predicate used to mark objects belonging to the French sort in the first-order translation.

1 occurrence in this chapter

Occurrence projected-formula-0012045

Equation form expr-594e519ae499312b

z

Read as: z

Means: The variable z ranges over German citizens in the many-sorted example or is a variable of type sigma in the higher-order term grammar.

2 occurrences in this chapter

Equation form expr-5b63a60fdb499c3a

N

Read as: the standard natural number structure N

Means: The intended full second-order model of the displayed arithmetic axioms.

1 occurrence in this chapter

Occurrence projected-formula-0012098

Equation form expr-5c62e091b8c0565f

P

Read as: P

Means: The capital letter P names a unary second-order relation, the range set of f, or a set of possible worlds according to context.

7 occurrences in this chapter

Equation form expr-5da6eac60a718545

\neg (p \land q) \to (\neg p \lor \neg q)

Read as: if not both p and q, then not p or not q

Means: One direction of a De Morgan principle that is classically valid but not intuitionistically valid.

1 occurrence in this chapter

Occurrence projected-formula-0012336

Equation form expr-61531c2edf9f7391

{true}_{k} (R, x_{1}, \dots, x_{k})

Read as: the built in truth predicate of arity k holds of R and x sub one through x sub k

Means: The many-sorted relation symbol true sub k connects a k-ary relation object R with the k objects it relates.

1 occurrence in this chapter

Occurrence projected-formula-0012146

Equation form expr-623fc0387a93ef39

M, w ⊮ ⊥

Read as: model M does not force contradiction at world w

Means: The Kripke falsum clause says contradiction is forced at no world.

1 occurrence in this chapter

Occurrence projected-formula-0012325

Equation form expr-63a228d87ddf6698

S 4

Read as: modal system S four

Means: The normal modal logic S four, whose frames are reflexive and transitive.

2 occurrences in this chapter

Equation form expr-63b1870f9092ffa7

\forall x (German (x) \to A) .

Read as: for every x, if x is German then A

Means: The first-order relativization of a universal quantifier over the German sort.

1 occurrence in this chapter

Occurrence projected-formula-0012048

Equation form expr-64317005abd1642b

(ℕ \to ℕ) \to ℕ

Read as: the function type from natural number functions to natural numbers

Means: The higher type of functionals taking a natural-number function as input and returning a natural number.

1 occurrence in this chapter

Occurrence projected-formula-0012168

Equation form expr-69ef9ee2c45eb3b7

M, w^{'} ⊩ A

Read as: model M forces A at world w prime

Means: Formula A is forced at the future world w prime.

1 occurrence in this chapter

Occurrence projected-formula-0012334

Equation form expr-6b23c0d5f35d1b11

C

Read as: C

Means: The capital letter C names one of the basic higher-order types in the source list.

1 occurrence in this chapter

Occurrence projected-formula-0012156

Equation form expr-6d180803fdbffa50

a = \sqrt{3}

Read as: a equals the square root of three

Means: The explicit constructive witness uses square root of three for a.

1 occurrence in this chapter

Occurrence projected-formula-0012266

Equation form expr-705560e324570f60

M, w ⊩ (A \land B)

Read as: model M forces A and B at world w

Means: The Kripke forcing assertion for a conjunction at world w.

1 occurrence in this chapter

Occurrence projected-formula-0012326

Equation form expr-71983740200349d8

\forall x A (x)

Read as: for every x, A of x

Means: Universal quantification of the formula A of x.

1 occurrence in this chapter

Occurrence projected-formula-0012285

Equation form expr-75c15f3273bbd7da

\forall x (x \times 0) = 0

Read as: for every x, x times zero equals zero

Means: The right-zero recursion axiom for multiplication.

1 occurrence in this chapter

Occurrence projected-formula-0012095

Equation form expr-7607fe048956ea88

A (x_{1}, \dots, x_{k}) ⊢ \exists R R (x_{1}, \dots, x_{k})

Read as: A of x sub one through x sub k syntactically derives that some relation R holds of x sub one through x sub k

Means: A comprehension-style inference introducing a second-order relation that agrees with the given k-place formula at the displayed tuple.

1 occurrence in this chapter

Occurrence projected-formula-0012072

Equation form expr-78e6f2c71bd9642a

{({\sqrt{2}}^{\sqrt{2}})}^{\sqrt{2}} = {\sqrt{2}}^{\sqrt{2} \cdot \sqrt{2}} = {\sqrt{2}}^{2} = 2,

Read as: the square root of two to the square root of two, all raised to the square root of two, equals the square root of two to the product of those exponents, equals the square root of two squared, equals two

Means: The exponentiation calculation used in the second case of the nonconstructive irrational-exponent proof.

1 occurrence in this chapter

Occurrence projected-formula-0012259

Equation form expr-7902699be42c8a8e

7

Read as: seven

Means: The natural number seven, used in the classically specified Riemann-hypothesis example.

1 occurrence in this chapter

Occurrence projected-formula-0012249

Equation form expr-79763d9a3c4e5663

f (x) = s

Read as: f of x equals s

Means: The defining equation for the function denoted by lambda x dot s: under a corresponding assignment to x, application has the value of body s. It defines a constant function only if x is not free in s; the source's later word sigma is disclosed as a type mismatch.

1 occurrence in this chapter

Occurrence projected-formula-0012232

Equation form expr-79ccb820ca1adfb9

A [λ \vec{x} . B (\vec{x}) / R]

Read as: A with the relation expression lambda vector x dot B of vector x substituted for R

Means: The formula obtained by replacing each atomic occurrence of relation variable R in A by the formula B on the corresponding argument tuple.

1 occurrence in this chapter

Occurrence projected-formula-0012074

Equation form expr-79d4c7f9c8579543

ℕ

Read as: the natural numbers

Means: The standard type or set of natural numbers.

10 occurrences in this chapter

Equation form expr-79e9919e34db718e

A [λ \vec{x} . B (\vec{x}) / R] ⊢ \exists R A

Read as: A with lambda vector x dot B of vector x substituted for R syntactically derives that there exists R such that A

Means: The general relation-comprehension inference: a formula instance obtained from B yields an existential second-order witness R for A.

1 occurrence in this chapter

Occurrence projected-formula-0012073

Equation form expr-79f590d1ce563fc7

\neg □ \neg A

Read as: not necessarily not A

Means: The usual modal definition of possibility as the negation of the necessity of not A.

1 occurrence in this chapter

Occurrence projected-formula-0012342

Equation form expr-7cc21a3bda17828d

M, w ⊩ B

Read as: model M forces B at world w

Means: Formula B is forced at world w in the current Kripke clause.

2 occurrences in this chapter

Equation form expr-81aa5a490db29cc9

A (x)

Read as: A of x

Means: Formula A with the displayed argument x.

2 occurrences in this chapter

Equation form expr-8238c028f61fc0f7

A

Read as: formula A

Means: A denotes the current formula, schema instance, theorem conclusion, or modal proposition as fixed by its occurrence context.

28 occurrences in this chapter

Equation form expr-8254c329a92850f6

k

Read as: k

Means: The natural-number arity k of a second-order relation or the corresponding final argument index.

9 occurrences in this chapter

Equation form expr-830c9c56b4f2bf21

t_{k}

Read as: t sub k

Means: The final ordinary first-order term in a k-term argument list.

1 occurrence in this chapter

Occurrence projected-formula-0012058

Equation form expr-83f9ac616d005ed8

B (t_{1}, \dots, t_{k})

Read as: B of t sub one through t sub k

Means: Formula B instantiated with the k displayed first-order terms.

1 occurrence in this chapter

Occurrence projected-formula-0012077

Equation form expr-844b8e62f444c681

Γ^{N}

Read as: the pointwise double negation translation of Gamma

Means: Gamma superscript N is the set obtained by translating each hypothesis in Gamma.

1 occurrence in this chapter

Occurrence projected-formula-0012304

Equation form expr-87968c737ba8d4cb

σ \times τ

Read as: the product type sigma times tau

Means: The type of ordered pairs whose first component has type sigma and second component has type tau.

4 occurrences in this chapter

Equation form expr-8858f2939b554308

v \geq u

Read as: world v is at least world u

Means: World v is a possible future state extending world u in the Kripke order.

1 occurrence in this chapter

Occurrence projected-formula-0012314

Equation form expr-8b607ce39e12ce48

s = t

Read as: s equals t

Means: An identity formula between higher-order terms s and t of the same type.

1 occurrence in this chapter

Occurrence projected-formula-0012235

Equation form expr-8c2574892063f995

R

Read as: relation R

Means: The capital letter R names a second-order relation variable, an accessibility relation, or a recursion symbol as fixed by context.

10 occurrences in this chapter

Equation form expr-8de0b3c47f112c59

S

Read as: relation S

Means: The capital letter S names a second relation variable of the same arity as R.

1 occurrence in this chapter

Occurrence projected-formula-0012061

Equation form expr-8e35c2cd3bf6641b

q

Read as: world q

Means: The symbol q names a possible world in the modal accessibility example.

2 occurrences in this chapter

Equation form expr-8f6cf2521c9703a8

x < y ⊢ \exists R R (x, y)

Read as: x is less than y syntactically derives that some relation R holds of x and y

Means: The inference abstracts the fixed arithmetic order predicate into an existentially quantified binary relation variable.

1 occurrence in this chapter

Occurrence projected-formula-0012070

Equation form expr-8fc9b76e9eaa1f54

⟨ s, t ⟩

Read as: the ordered pair s comma t

Means: The higher-order pair term with first component s and second component t.

2 occurrences in this chapter

Equation form expr-9261a6b996e4ba08

{\sqrt{2}}^{\sqrt{2}}

Read as: the square root of two to the square root of two

Means: The real number whose rationality is split into cases in the nonconstructive proof.

2 occurrences in this chapter

Equation form expr-963aec90f53d4fd4

τ \to σ

Read as: the function type from tau to sigma

Means: The type of functions taking inputs of type tau to outputs of type sigma.

2 occurrences in this chapter

Equation form expr-9c3245dfb4ac54c1

σ

Read as: type sigma

Means: The Greek letter sigma names a finite type, a term type, or an output type.

15 occurrences in this chapter

Equation form expr-9dd4e4b646218a71

M, w^{'} ⊩ B

Read as: model M forces B at world w prime

Means: Formula B is forced at the future world w prime.

1 occurrence in this chapter

Occurrence projected-formula-0012335

Equation form expr-9ef0477687ad753d

p_{1} (s)

Read as: the first projection of s

Means: The projection term selecting the first component of the pair denoted by s.

2 occurrences in this chapter

Equation form expr-9ff72e6423da90e8

\forall P (\exists x P (x) \to \exists x (P (x) \land \forall y (y < x \to \neg P (y)))) .

Read as: for every property P, if something has P, then some x has P and every y below x does not have P

Means: The second-order least-element principle saying every nonempty unary relation has a least member under the ordering.

1 occurrence in this chapter

Occurrence projected-formula-0012133

Equation form expr-a05f5de3e5672324

A (R) ⊢ \exists R A (R)

Read as: A of R syntactically derives that there exists R such that A of R

Means: Existential introduction for a second-order relation variable.

1 occurrence in this chapter

Occurrence projected-formula-0012067

Equation form expr-a1fce4363854ff88

y

Read as: y

Means: The variable y names an individual, function value, arithmetic operand, or witness as fixed by context.

2 occurrences in this chapter

Equation form expr-a5cafe3dded670c0

M, w ⊩ p_{i}

Read as: model M forces propositional variable p sub i at world w

Means: The atomic Kripke forcing assertion for indexed propositional variable p sub i at w.

1 occurrence in this chapter

Occurrence projected-formula-0012322

Equation form expr-a96399d5a5cbd2a9

\begin{matrix} A^{N} & \equiv \neg \neg A for atomic formulas A \\ {(A \land B)}^{N} & \equiv (A^{N} \land B^{N}) \\ {(A \lor B)}^{N} & \equiv \neg \neg (A^{N} \lor B^{N}) \\ {(A \to B)}^{N} & \equiv (A^{N} \to B^{N}) \\ {(\forall x A)}^{N} & \equiv \forall x A^{N} \\ {(\exists x A)}^{N} & \equiv \neg \neg \exists x A^{N} \end{matrix}

Read as: double negation translation clauses: an atomic formula A translates as not not A; the conjunction of A and B translates componentwise; the disjunction of A and B translates as not not the disjunction of their translations; the conditional from A to B translates componentwise; the universal formula for every x, A keeps its quantifier and translates A; and the existential formula there exists x such that A translates as not not there exists x such that the translation of A

Means: The complete six-clause recursive definition of the Gödel Gentzen double-negation translation used in this chapter.

1 occurrence in this chapter

Occurrence projected-formula-0012296

Equation form expr-aa489f7eaaa53fde

R t_{1}, \dots, t_{k}

Read as: object language relation R applied to t sub one through t sub k

Means: The source's object-language notation for an atomic R formula with k term arguments.

1 occurrence in this chapter

Occurrence projected-formula-0012075

Equation form expr-ab733e02bed54e75

Γ ⊨ A

Read as: Gamma semantically entails A

Means: Every weak second-order structure satisfying Gamma also satisfies A.

1 occurrence in this chapter

Occurrence projected-formula-0012137

Equation form expr-b299a756fe5b9f2c

A \lor B

Read as: A or B

Means: The disjunction of formulas A and B.

1 occurrence in this chapter

Occurrence projected-formula-0012279

Equation form expr-b2cc1bf1631e546c

R (x, y)

Read as: R holds of x and y

Means: The binary relation variable R applies to x and y.

1 occurrence in this chapter

Occurrence projected-formula-0012345

Equation form expr-b4671760f70dc9d0

f (0) = 0^{M}

Read as: f of zero equals the interpretation of object language zero in M

Means: The base clause defining the comparison map from the natural numbers into structure M.

1 occurrence in this chapter

Occurrence projected-formula-0012104

Equation form expr-b50bb8940da5b931

L

Read as: language L

Means: The given first-order base language L whose predicates and formulas are being discussed and to which second-order relation variables may be added; one occurrence is specifically the first-order language of arithmetic.

4 occurrences in this chapter

Equation form expr-b5b446abb4d0323b

M, w ⊩ A

Read as: model M forces A at world w

Means: Formula A is true, or forced, at Kripke world w.

4 occurrences in this chapter

Equation form expr-b70d9440475516a8

ℕ \to ℕ

Read as: the function type from the natural numbers to the natural numbers

Means: The higher-order type of unary functions on natural numbers.

2 occurrences in this chapter

Equation form expr-ba9f5ad06bac23b1

A \leftrightarrow A^{N}

Read as: A if and only if its double negation translation

Means: The classical equivalence of a formula A with its double-negation translation.

1 occurrence in this chapter

Occurrence projected-formula-0012297

Equation form expr-baacfd9d189243cd

◇ A

Read as: possibly A

Means: The diamond formula applied to A; according to context, it says that A is possible, consistent, or sometimes true.

3 occurrences in this chapter

Equation form expr-bc08bdf8e6a2d207

R_{s t}

Read as: the recursor R sub s t

Means: The higher-order term denoting the natural-number recursion determined by base s and step t.

2 occurrences in this chapter

Equation form expr-be8dcefb61dddd9f

t_{1}

Read as: t sub one

Means: The first ordinary first-order term in a k-term argument list.

1 occurrence in this chapter

Occurrence projected-formula-0012057

Equation form expr-bf1df883a744abb3

A \land B

Read as: A and B

Means: The conjunction of formulas A and B.

1 occurrence in this chapter

Occurrence projected-formula-0012276

Equation form expr-c47ff2d918931e5d

\forall x \forall y (x \times y^{'}) = ((x \times y) + x)

Read as: for every x and y, x times the successor of y equals x times y plus x

Means: The successor recursion axiom for multiplication.

1 occurrence in this chapter

Occurrence projected-formula-0012096

Equation form expr-c571f4bf947b1523

\forall x_{1} \dots \forall x_{k} (R (x_{1}, \dots, x_{k}) \leftrightarrow S (x_{1}, \dots, x_{k})) .

Read as: for every x sub one through x sub k, R holds of them if and only if S holds of them

Means: The extensional equivalence condition used to define identity between two k-ary relation variables.

1 occurrence in this chapter

Occurrence projected-formula-0012064

Equation form expr-c63f9557f464c93a

\neg A

Read as: not A

Means: The negation of formula A.

1 occurrence in this chapter

Occurrence projected-formula-0012143

Equation form expr-c8b9bd8b45323b0c

\forall x \neg x^{'} = 0

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

Means: The arithmetic axiom that zero is not in the range of successor.

1 occurrence in this chapter

Occurrence projected-formula-0012091

Equation form expr-ca978112ca1bbdca

a

Read as: a

Means: The symbol a names the French-sorted variable or the first irrational witness, according to context.

4 occurrences in this chapter

Equation form expr-cbbba670a3f47b53

Γ ⊢ A

Read as: Gamma syntactically derives A

Means: Formula A is derivable from Gamma in the minimal second-order proof system.

1 occurrence in this chapter

Occurrence projected-formula-0012138

Equation form expr-cbede77419bcc57e

S 5

Read as: modal system S five

Means: The normal modal logic S five, whose Kripke accessibility relation is universal.

1 occurrence in this chapter

Occurrence projected-formula-0012367

Equation form expr-cd37871db1ba340f

A \lor \neg A

Read as: A or not A

Means: The law of excluded middle schema.

1 occurrence in this chapter

Occurrence projected-formula-0012292

Equation form expr-d055ee4dbcdd0c8b

B

Read as: formula B

Means: B denotes the second formula in a connective or translation clause.

4 occurrences in this chapter

Equation form expr-d112c3f30fc91b94

'^{M}

Read as: the interpretation of successor in M

Means: The unary function assigned to the object-language successor symbol by structure M.

1 occurrence in this chapter

Occurrence projected-formula-0012119

Equation form expr-d12d2db1d36c17ad

0^{M}

Read as: the interpretation of object language zero in M

Means: The domain element assigned to the zero constant by structure M.

1 occurrence in this chapter

Occurrence projected-formula-0012116

Equation form expr-d475527c5abd77f4

\exists x A (x)

Read as: there exists x such that A of x

Means: Existential quantification of formula A of x.

1 occurrence in this chapter

Occurrence projected-formula-0012288

Equation form expr-d5504fd61cfdf3b2

(\neg A \to ⊥) \to A

Read as: if not A implies contradiction, then A

Means: A classical reductio schema, intuitionistically equivalent to excluded middle and double-negation elimination.

1 occurrence in this chapter

Occurrence projected-formula-0012291

Equation form expr-d6aef031749de4a7

Ω

Read as: Omega

Means: The higher-order truth-value type whose intended values are true and false.

3 occurrences in this chapter

Equation form expr-d9b1567a52bb6c42

x_{1}

Read as: x sub one

Means: The first member of an indexed list of first-order terms or arguments.

2 occurrences in this chapter

Equation form expr-dabd3aff769f07eb

<

Read as: less than

Means: The strict order relation in arithmetic or a Kripke-world comparison rendered in the surrounding prose.

2 occurrences in this chapter

Equation form expr-df7e70e5021544f4

B

Read as: B

Means: The capital letter B names one of the basic higher-order types in this occurrence.

1 occurrence in this chapter

Occurrence projected-formula-0012155

Equation form expr-e3b98a4da31a127d

t

Read as: t

Means: The symbol t names a first-order term, a higher-order term, or the step functional in a recursion, as fixed by context.

4 occurrences in this chapter

Equation form expr-e7e35496e8ce02fb

\forall x \forall y (s (x) = s (y) \to x = y)

Read as: for every x and y, if successor of x equals successor of y, then x equals y

Means: The injectivity axiom for successor.

1 occurrence in this chapter

Occurrence projected-formula-0012092

Equation form expr-ea4cabc34cc43411

\exists f (\forall x \forall y (f (x) = f (y) \to x = y) \land \exists y \forall x f (x) \neq y) .

Read as: there exists a function f such that f is injective and some y is outside the range of f

Means: The second-order sentence asserting an injection of the domain into a proper subset of itself, and hence infinitude under full semantics.

1 occurrence in this chapter

Occurrence projected-formula-0012132

Equation form expr-ed1089a954ee910b

\exists R \forall x_{1}, \dots, x_{k} (A (x_{1}, \dots, x_{k}) \leftrightarrow R (x_{1}, \dots, x_{k})),

Read as: there exists a relation R such that for every x sub one through x sub k, A holds of that tuple if and only if R holds of it

Means: An instance of the second-order comprehension schema for a k-place formula A in which R is not free.

1 occurrence in this chapter

Occurrence projected-formula-0012078

Equation form expr-f157f71e0163a897

□

Read as: the necessity operator

Means: The modal box operator, read as necessity.

1 occurrence in this chapter

Occurrence projected-formula-0012351

Equation form expr-f1941b975ffcc891

Δ

Read as: Delta

Means: Delta denotes the selected set of second-order comprehension axioms.

1 occurrence in this chapter

Occurrence projected-formula-0012139

Equation form expr-f3f53d49901fff1a

M, w ⊩ (A \lor B)

Read as: model M forces A or B at world w

Means: The Kripke forcing assertion for a disjunction at world w.

1 occurrence in this chapter

Occurrence projected-formula-0012329

Equation form expr-f78d01e0e8c39041

ℕ \to (σ \to σ)

Read as: the type from natural numbers to functions from sigma to sigma

Means: The type of a recursion step term taking a number and returning an endofunction on sigma.

1 occurrence in this chapter

Occurrence projected-formula-0012195

Equation form expr-f7ed9e9808d36581

R = S

Read as: relation R equals relation S

Means: Defined extensional identity between relation variables R and S of the same arity.

1 occurrence in this chapter

Occurrence projected-formula-0012063

Equation form expr-f87a549f62a7a792

□ A

Read as: necessarily A

Means: The box formula applied to A; according to context, it says that A is necessary or true in every accessible world, provable, known or believed, or always true.

6 occurrences in this chapter

Equation form expr-fbc701a577760588

ℕ \to σ

Read as: the function type from the natural numbers to sigma

Means: The type of the recursively defined function R sub s t.

1 occurrence in this chapter

Occurrence projected-formula-0012197

Equation form expr-fc4a9077e91544fc

s (t)

Read as: s applied to t

Means: Application of higher-order function term s to argument term t.

1 occurrence in this chapter

Occurrence projected-formula-0012202

Equation form expr-fc81b70f63a0d8c8

Γ \cup Δ ⊨ A

Read as: Gamma union Delta semantically entails A

Means: Every weak second-order structure satisfying Gamma and all comprehension axioms in Delta satisfies A.

1 occurrence in this chapter

Occurrence projected-formula-0012140

Equation form expr-fcb5f40df9be6bae

W

Read as: the set of worlds W

Means: The carrier set W of worlds in a Kripke model.

4 occurrences in this chapter

Equation form expr-fe9c6c347eb9fd64

\forall x \forall y (x < y \leftrightarrow \exists z y = (x + z^{'}))

Read as: for every x and y, x is less than y if and only if some z makes y equal x plus the successor of z

Means: The arithmetic definition of strict order by a positive additive difference.

1 occurrence in this chapter

Occurrence projected-formula-0012097

Recursive equations for the higher-order recursor

A two-row display gives the base and successor clauses for R sub s t.

Source

Theorem on irrational powers with rational value

The theorem asserts existence of irrational a and b whose exponential a to the b is rational.

Source

Equivalent classical principles over intuitionistic logic

The theorem lists three classically characteristic schemata and says they are intuitionistically equivalent.

Source

Definition of the double-negation translation

A six-row display defines the translation for atoms, conjunction, disjunction, implication, universal quantification, and existential quantification.

Source

Theorem on the double-negation translation

The theorem states classical equivalence and preservation of classical provability by intuitionistic provability after translation.

Source

Theorem translating classical derivations from hypotheses

The theorem extends the double-negation result from theorems to derivations from a premise set Gamma.

Source

Axioms and rule for modal systems S four and S five

The display lists three S four axioms, necessitation, and the additional S five axiom.

Source

Source disclosures

TR025-SOURCE-FORMULA-002: The displayed language declares the object-language prime symbol as successor, but this injectivity axiom prints s as the function name. The reader identifies s here as successor while preserving the frozen formula. source
TR025-SOURCE-PROSE-001: The lambda clause at line sixty eight declares x to have type tau, so the function defined by lambda x dot s takes inputs of type tau. The later source sentence says sigma; the reader states tau while preserving the frozen source text. source
TR025-SOURCE-PROSE-003: The reader corrects the source phrase 'This following theorem' to 'The following theorem.' source
TR025-SOURCE-PROSE-004: The reader supplies the missing word 'as' in the definition lead-in. source
TR025-SOURCE-PROSE-005: The reader supplies the missing article before partial order and changes 'an monotone' to 'a monotone.' source
TR025-SOURCE-PROSE-006: The reader removes the extra article in 'create your own a syntax.' source
TR025-SOURCE-PROSE-007: The reader corrects 'creatures studies' to 'creatures studied.' source
TR025-SOURCE-PROSE-008: The reader changes 'in terms of' to 'in favor of' to preserve the stated contrast. source