Syntax of First-Order Logic — Explore equations

Expression 1

A [t / x]

Conventional reading: the result of substituting term t for variable x in the current formula

Meaning here: The formula obtained by replacing the relevant free occurrences of variable x by term t in the current formula.

5 occurrences

Expression 2

\land

Conventional reading: and sign

Meaning here: The binary logical connective and, used to form a conjunction.

3 occurrences

Expression 3

A_{k}

Conventional reading: A sub k

Meaning here: The formula at position k in an indexed sequence of formulas.

3 occurrences

Expression 4

0

Conventional reading: zero

Meaning here: The object-language constant used for zero in the language of arithmetic; officially it aliases constant c sub zero.

2 occurrences

Expression 5

A \in Frm (L)

Conventional reading: formula A is in the set of formulas of language L

Meaning here: Formula A belongs to the inductively defined set of well-formed formulas of first-order language L.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 183, column 15

Expression 6

P (t_{1} [t / x], \dots, t_{n} [t / x])

Conventional reading: P of t sub one with t substituted for x, through t sub n with t substituted for x

Meaning here: The atomic P-formula obtained by substituting term t for variable x in each of its n argument terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 57, column 38

Expression 7

s

Conventional reading: s

Meaning here: The source symbol s denotes a term being transformed or a formation sequence, as fixed by the surrounding definition.

7 occurrences

Expression 8

{f^{n}}_{0}

Conventional reading: f superscript n sub zero

Meaning here: The first indexed n-place function symbol in the standard first-order vocabulary.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 60, column 3

Expression 9

(A \lor B)

Conventional reading: open parenthesis A or B close parenthesis

Meaning here: The fully parenthesized disjunction of formulas A and B; the reader supplies the source table's delimiter-displaced closing parenthesis.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 91, column 24

Expression 10

\exists v_{0}

Conventional reading: the existential quantifier for variable v sub zero

Meaning here: The existential-quantifier prefix binding indexed variable v sub zero.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/free-vars-sentences.tex, line 72, column 30

Expression 11

\neg = (t_{1}, t_{2})

Conventional reading: not, t sub one is identical to t sub two

Meaning here: The negation of the atomic identity formula between terms t sub one and t sub two.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 104, column 35

Expression 12

A_{i} \equiv \neg A_{j}

Conventional reading: A sub i is syntactically identical to not A sub j

Meaning here: The indexed string A sub i is exactly the negation of the earlier string A sub j.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 71, column 22

Expression 13

⟨ B_{0}, \dots, B_{n}, \exists x B_{n} ⟩

Conventional reading: sequence B sub zero through B sub n, followed by there exists x such that B sub n

Meaning here: A formula formation sequence extended by existentially quantifying its final formula B sub n with variable x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 142, column 12

Expression 14

l (t)

Conventional reading: the number of left parentheses in term t

Meaning here: The function l applied to term t, counting its left parentheses.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 69, column 35

Expression 15

(\forall x)

Conventional reading: parenthesized universal quantifier for x

Meaning here: A traditional notation variant for universal quantification with variable x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 138, column 44

Expression 16

{\neg, \land}

Conventional reading: the set containing negation and conjunction

Meaning here: A truth-functionally complete set consisting of negation and conjunction.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 148, column 30

Expression 17

{f^{1}}_{0} ({f^{2}}_{0} (c_{0}, v_{0}))

Conventional reading: f superscript one sub zero of f superscript two sub zero of c sub zero and v sub zero

Meaning here: A compound term formed by applying the unary function symbol f superscript one sub zero to the binary-function term with arguments c sub zero and v sub zero.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 56, column 38

Expression 18

A [t / x]

Conventional reading: formula A with term t substituted for variable x

Meaning here: The result of substituting term t for all relevant free occurrences of variable x in formula A.

5 occurrences

Expression 19

s [t / x]

Conventional reading: term s with term t substituted for variable x

Meaning here: The result of substituting term t for every occurrence of variable x in term s.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 14, column 11

Expression 20

\exists x

Conventional reading: there exists x

Meaning here: A traditional existential-quantifier prefix for variable x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 139, column 48

Expression 21

n = 0

Conventional reading: n equals zero

Meaning here: The arity n is zero, so the zero-place function expression has no argument list.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 37, column 66

Expression 22

L_{Z}

Conventional reading: language L sub Z

Meaning here: The first-order language of set theory, whose sole nonlogical predicate is membership.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 77, column 28

Expression 23

(A_{j} \land A_{k})

Conventional reading: open parenthesis A sub j and A sub k close parenthesis

Meaning here: The conjunction of the two earlier indexed formulas A sub j and A sub k.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 208, column 1

Expression 24

{A^{2}}_{0} (t_{1}, t_{2})

Conventional reading: predicate A superscript two sub zero of t sub one and t sub two

Meaning here: The binary atomic formula obtained by applying the first indexed two-place predicate to terms t sub one and t sub two.

2 occurrences

Expression 25

n

Conventional reading: n

Meaning here: The source symbol n denotes an arity, final sequence index, or connective count, as fixed by its source packet.

9 occurrences

Expression 26

v_{8}

Conventional reading: v sub eight

Meaning here: The indexed individual variable v sub eight in the substitution example.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 37, column 7

Expression 27

A [t / x]

Conventional reading: the result of substituting term t for variable x in the current expression

Meaning here: The recursively transformed current term or formula after substituting t for x; the primed induction placeholder records the same current input.

10 occurrences

Expression 28

\neg

Conventional reading: not sign

Meaning here: A notation variant for logical negation.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 123, column 9

Expression 29

L_{\leq}

Conventional reading: language L sub less than or equal to

Meaning here: The language of orders containing only the binary predicate less than or equal to.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 82, column 24

Expression 30

n + 1

Conventional reading: n plus one

Meaning here: One more than n, used as the length of a sequence indexed from zero through n.

2 occurrences

Expression 31

l (A)

Conventional reading: the number of left parentheses in formula A

Meaning here: The function l applied to formula A, counting its left parentheses.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 68, column 5

Expression 32

⋀_{x}

Conventional reading: large conjunction indexed by x

Meaning here: A traditional notation variant for universal quantification over x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 139, column 1

Expression 33

(A \lor B)

Conventional reading: open parenthesis A or B close parenthesis

Meaning here: The fully parenthesized disjunction of formulas A and B.

3 occurrences

Expression 34

{A^{n}}_{2}

Conventional reading: A superscript n sub two

Meaning here: The third indexed n-place predicate symbol in the standard first-order vocabulary.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 56, column 25

Expression 35

l (A) = l (t_{1}) + l (t_{2}) = r (t_{1}) + r (t_{2}) = r (A)

Conventional reading: left parentheses in the current identity formula equals left parentheses in t sub one plus left parentheses in t sub two, equals right parentheses in t sub one plus right parentheses in t sub two, equals right parentheses in the current identity formula

Meaning here: The parenthesis-count chain for an atomic identity formula, using the induction hypothesis for its two terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 88, column 35

Expression 36

A \to B

Conventional reading: if A, then B

Meaning here: The conditional whose antecedent is formula A and whose consequent is formula B.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 29, column 47

Expression 37

f

Conventional reading: f

Meaning here: The object-language function symbol f, with arity supplied by the surrounding clause.

4 occurrences

Expression 38

\forall x B

Conventional reading: for every x, B

Meaning here: The universal quantification of formula B with respect to variable x.

4 occurrences

Expression 39

(A \land B)

Conventional reading: open parenthesis A and B close parenthesis

Meaning here: The fully parenthesized conjunction of formulas A and B; the reader supplies the source table's delimiter-displaced closing parenthesis.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 90, column 25

Expression 40

\neg

Conventional reading: not sign

Meaning here: The unary logical connective not.

5 occurrences

Expression 41

B [t / x]

Conventional reading: formula B with term t substituted for variable x

Meaning here: The result of substituting term t for all relevant free occurrences of x in formula B.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 106, column 34

Expression 42

B'

Conventional reading: B prime

Meaning here: A formula metavariable distinguished from B by a prime mark.

2 occurrences

Expression 43

{f^{n}}_{1}

Conventional reading: f superscript n sub one

Meaning here: The second indexed n-place function symbol in the standard first-order vocabulary.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 60, column 17

Expression 44

\exists v_{0} \underset{B}{{A^{2}}_{0} (v_{0}, v_{1})}

Conventional reading: there exists v sub zero such that predicate A superscript two sub zero holds of v sub zero and v sub one, with that atomic formula marked B

Meaning here: An existential formula whose displayed scope B is the binary atom A superscript two sub zero of v sub zero and v sub one.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/free-vars-sentences.tex, line 69, column 1

Expression 45

A \equiv t_{1} = t_{2}

Conventional reading: A is syntactically identical to t sub one equals t sub two

Meaning here: Formula string A is exactly the infix identity formula between terms t sub one and t sub two.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 141, column 7

Expression 46

\forall v_{2} {A^{2}}_{4} (v_{0}, v_{2})

Conventional reading: for every v sub two, predicate A superscript two sub four holds of v sub zero and v sub two

Meaning here: A universally quantified binary atomic formula binding v sub two while v sub zero remains available from the surrounding context.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 41, column 11

Expression 47

\Leftrightarrow

Conventional reading: double arrow biconditional symbol

Meaning here: A notation variant for the biconditional.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 128, column 3

Expression 48

x

Conventional reading: x

Meaning here: The individual variable x, including its free, bound, and substitution roles in the surrounding source packet.

26 occurrences

Expression 49

c

Conventional reading: c

Meaning here: The object-language constant symbol c in the surrounding term or substitution clause.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 134, column 63

Expression 50

\exists v_{0} ({A^{1}}_{1} (c_{1}) \land {A^{1}}_{0} (v_{0}))

Conventional reading: there exists v sub zero such that A superscript one sub one of c sub one and A superscript one sub zero of v sub zero

Meaning here: An existential conjunction in which the first atom is closed and the second atom contains the bound variable v sub zero.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 92, column 28

Expression 51

\supset

Conventional reading: horseshoe conditional symbol

Meaning here: A notation variant for the conditional.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 125, column 55

Expression 52

\exists y

Conventional reading: there exists y

Meaning here: The existential-quantifier prefix binding variable y.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 104, column 12

Expression 53

A \equiv ⊥

Conventional reading: A is syntactically identical to falsum

Meaning here: The formula string A consists exactly of the falsum symbol.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 136, column 20

Expression 54

= (t_{1}, t_{2})

Conventional reading: t sub one is identical to t sub two

Meaning here: The atomic identity formula whose two argument terms are t sub one and t sub two.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 54, column 55

Expression 55

C \equiv C'

Conventional reading: C is syntactically identical to C prime

Meaning here: Formula strings C and C prime contain exactly the same symbols in the same positions.

2 occurrences

Expression 56

j, k < i

Conventional reading: indices j and k are less than i

Meaning here: Both cited formula indices precede position i in a formation sequence.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 68, column 7

Expression 57

\times

Conventional reading: multiplication sign

Meaning here: The binary multiplication function symbol in the language of arithmetic.

2 occurrences

Expression 58

v_{1}

Conventional reading: v sub one

Meaning here: The indexed individual variable v sub one.

6 occurrences

Expression 59

\exists y y < y

Conventional reading: there exists y such that y is less than y

Meaning here: The false existential formula produced in the variable-capture example.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 102, column 52

Expression 60

Π x

Conventional reading: capital pi quantifier for x

Meaning here: A traditional notation variant for universal quantification over x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 138, column 66

Expression 61

\exists x

Conventional reading: the existential quantifier for x

Meaning here: The existential-quantifier prefix binding variable x.

2 occurrences

Expression 62

A \leftrightarrow B

Conventional reading: A if and only if B

Meaning here: The biconditional with formula A on the left and formula B on the right.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 150, column 18

Expression 63

⟨ {A^{1}}_{0} (v_{0}), {A^{1}}_{1} (c_{1}), ({A^{1}}_{1} (c_{1}) \land {A^{1}}_{0} (v_{0})), {A^{1}}_{1} (c_{1}), \forall v_{1} {A^{1}}_{0} (v_{0}), \exists v_{0} ({A^{1}}_{1} (c_{1}) \land {A^{1}}_{0} (v_{0})) ⟩ .

Conventional reading: sequence: A superscript one sub zero of v sub zero; A superscript one sub one of c sub one; their conjunction; A superscript one sub one of c sub one again; for every v sub one, A superscript one sub zero of v sub zero; and the existential conjunction binding v sub zero

Meaning here: A formula formation sequence that deliberately contains redundant material before its final existential formula.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 94, column 1

Expression 64

\exists y B [t / x]

Conventional reading: there exists y such that B with term t substituted for x

Meaning here: The existential formula obtained after substitution proceeds beneath a quantifier for a variable y distinct from x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 90, column 8

Expression 65

A \equiv \forall x B

Conventional reading: A is syntactically identical to: for every x, B

Meaning here: The formula string A has a universal quantifier for x and scope B.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 138, column 23

Expression 66

b

Conventional reading: b

Meaning here: The object-language constant symbol b.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 134, column 58

Expression 67

⟨ B_{0}, \dots, B_{n}, \forall x B_{n} ⟩

Conventional reading: sequence B sub zero through B sub n, followed by for every x, B sub n

Meaning here: A formula formation sequence extended by universally quantifying its final formula B sub n with variable x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 139, column 12

Expression 68

⟨ B_{0}, \dots, B_{n}, C_{0}, \dots, C_{m}, (B_{n} \to C_{m}) ⟩

Conventional reading: sequence B sub zero through B sub n, then C sub zero through C sub m, followed by: if B sub n then C sub m

Meaning here: Two formation sequences concatenated and extended by a conditional whose antecedent and consequent are their final formulas.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 133, column 12

Expression 69

{\neg, \to}

Conventional reading: the set containing negation and the conditional

Meaning here: A truth-functionally complete set consisting of negation and the conditional.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 148, column 56

Expression 70

'

Conventional reading: successor prime

Meaning here: The postfix unary successor-function symbol in the language of arithmetic.

2 occurrences

Expression 71

\forall v_{0} \underset{B}{({A^{1}}_{0} (v_{0}) \to {A^{2}}_{0} (v_{0}, v_{1}))} \to \exists v_{1} \underset{C}{({A^{2}}_{1} (v_{0}, v_{1}) \lor \forall v_{0} \overset{D}{\neg {A^{1}}_{1} (v_{0})})}

Conventional reading: a conditional whose complete antecedent is: for every v sub zero, scope B, where B is, if A superscript one sub zero of v sub zero then A superscript two sub zero of v sub zero and v sub one; and whose complete consequent is: there exists v sub one such that scope C, where C is, either A superscript two sub one of v sub zero and v sub one, or, for every v sub zero, scope D, where D is, not A superscript one sub one of v sub zero

Meaning here: The main operator is a conditional. Its complete antecedent is the universal formula for every v sub zero, B, with B marking that quantifier's inner conditional scope. Its complete consequent is the existential formula there exists v sub one, C, with C marking that quantifier's disjunctive scope. D marks the negated-atom scope of the inner universal quantifier.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/free-vars-sentences.tex, line 80, column 1

Expression 72

(A \to B)

Conventional reading: open parenthesis if A then B close parenthesis

Meaning here: The fully parenthesized conditional from A to B; the reader supplies the source table's delimiter-displaced closing parenthesis.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 92, column 28

Expression 73

= (t_{1}, t_{2})

Conventional reading: t sub one is identical to t sub two

Meaning here: The atomic identity formula between terms t sub one and t sub two.

2 occurrences

Expression 74

(B * C)

Conventional reading: open parenthesis B binary connective star C close parenthesis

Meaning here: The fully parenthesized result of applying an arbitrary binary connective to B and C.

3 occurrences

Expression 75

Frm (L) \subseteq F

Conventional reading: the set of formulas of language L is a subset of F

Meaning here: Every well-formed formula of language L belongs to the set F of strings having formation sequences.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 179, column 42

Expression 76

\forall x A

Conventional reading: for every x, A

Meaning here: The universal quantification of formula A with respect to variable x.

5 occurrences

Expression 77

t_{1} \in t_{2}

Conventional reading: t sub one is an element of t sub two

Meaning here: The set-theoretic membership atom written infix between two terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 163, column 19

Expression 78

{f^{2}}_{1} (v_{1}, v_{2})

Conventional reading: function f superscript two sub one of v sub one and v sub two

Meaning here: A binary function term with indexed variables v sub one and v sub two as arguments.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 40, column 7

Expression 79

⟨ A_{0}, \dots, A_{n} ⟩

Conventional reading: sequence A sub zero through A sub n

Meaning here: A finite sequence of strings indexed from zero through n.

3 occurrences

Expression 80

A \equiv (B * C)

Conventional reading: A is syntactically identical to open parenthesis B binary connective star C close parenthesis

Meaning here: Formula string A is exactly the result of enclosing B, an arbitrary binary connective, and C in parentheses.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 192, column 17

Expression 81

2 n + 1

Conventional reading: two times n plus one

Meaning here: The upper bound two times n plus one on the number of subformulas of a formula with n connectives and quantifiers.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/subformulas.tex, line 104, column 23

Expression 82

l (t) = r (t)

Conventional reading: left parentheses in term t equals right parentheses in term t

Meaning here: Term t has equally many left and right parentheses.

2 occurrences

Expression 83

v

Conventional reading: v

Meaning here: An arbitrary individual variable v.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 195, column 47

Expression 84

\forall x \exists y x < y

Conventional reading: for every x, there exists y such that x is less than y

Meaning here: A sentence asserting that every object has a greater object.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 107, column 1

Expression 85

l (A) = l (B) = r (B) = r (A)

Conventional reading: left parentheses in the current formula equals left parentheses in B, equals right parentheses in B, equals right parentheses in the current formula

Meaning here: The parenthesis-count chain for a unary or quantified formula built from B.

2 occurrences

Expression 86

(A \to B) \land (B \to A)

Conventional reading: if A then B, and if B then A

Meaning here: The conjunction of the conditional from A to B and its converse, used to define the biconditional.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 150, column 44

Expression 87

D \to D

Conventional reading: if D then D

Meaning here: The conditional from formula D to itself.

5 occurrences

Expression 88

v_{2}

Conventional reading: v sub two

Meaning here: The indexed individual variable v sub two.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 49, column 72

Expression 89

A_{i} \equiv \exists x A_{j}

Conventional reading: A sub i is syntactically identical to: there exists x such that A sub j

Meaning here: The indexed string A sub i is obtained by existentially quantifying the earlier formula A sub j with x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 77, column 21

Expression 90

⊤

Conventional reading: truth sign

Meaning here: The propositional truth constant used as an atomic first-order formula when included in the profile.

3 occurrences

Expression 91

\lor

Conventional reading: or sign

Meaning here: The binary logical connective or.

6 occurrences

Expression 92

⟨ t_{0}, \dots, t_{n} ⟩

Conventional reading: sequence t sub zero through t sub n

Meaning here: A finite sequence of term strings indexed from zero through n.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 42, column 40

Expression 93

(\exists x)

Conventional reading: parenthesized existential quantifier for x

Meaning here: A traditional notation variant for existential quantification with variable x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 139, column 61

Expression 94

{\neg, \lor}

Conventional reading: the set containing negation and disjunction

Meaning here: A truth-functionally complete set consisting of negation and disjunction.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 148, column 9

Expression 95

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

Conventional reading: predicate R of t sub one through t sub n

Meaning here: An n-place atomic formula formed by applying predicate symbol R to terms t sub one through t sub n.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 87, column 1

Expression 96

i \leq n

Conventional reading: i is less than or equal to n

Meaning here: Index i is within the sequence positions from zero through n.

2 occurrences

Expression 97

k \leq n

Conventional reading: k is less than or equal to n

Meaning here: Index k is within the sequence positions from zero through n.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 158, column 22

Expression 98

⋁_{x}

Conventional reading: large disjunction indexed by x

Meaning here: A traditional notation variant for existential quantification over x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 140, column 26

Expression 99

z

Conventional reading: z

Meaning here: The individual variable z.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 136, column 62

Expression 100

⟨ c_{0}, v_{0}, {f^{2}}_{0} (c_{0}, v_{0}), {f^{1}}_{0} ({f^{2}}_{0} (c_{0}, v_{0})) ⟩

Conventional reading: sequence c sub zero, v sub zero, f superscript two sub zero of c sub zero and v sub zero, then f superscript one sub zero of that binary term

Meaning here: A concrete term formation sequence ending in a unary-function application to an earlier binary-function term.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 53, column 1

Expression 101

c_{0}

Conventional reading: c sub zero

Meaning here: The first indexed constant symbol in the standard first-order vocabulary.

2 occurrences

Expression 102

r (t)

Conventional reading: the number of right parentheses in term t

Meaning here: The function r applied to term t, counting its right parentheses.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 69, column 46

Expression 103

P

Conventional reading: P

Meaning here: The symbol P denotes either a property used in structural induction or a predicate symbol in an atomic formula, as fixed by the source packet.

4 occurrences

Expression 104

t_{2}

Conventional reading: t sub two

Meaning here: The second indexed term metavariable.

2 occurrences

Expression 105

0

Conventional reading: zero

Meaning here: The number zero.

2 occurrences

Expression 106

\sim

Conventional reading: tilde negation symbol

Meaning here: A notation variant for logical negation.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 123, column 1

Expression 107

⟨ v_{0}, c_{0}, {f^{2}}_{0} (c_{0}, v_{0}), {f^{1}}_{0} ({f^{2}}_{0} (c_{0}, v_{0})) ⟩ .

Conventional reading: sequence v sub zero, c sub zero, f superscript two sub zero of c sub zero and v sub zero, then f superscript one sub zero of that binary term

Meaning here: A concrete term formation sequence with its first two entries reversed relative to the preceding valid sequence.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 58, column 1

Expression 108

c_{1}

Conventional reading: c sub one

Meaning here: The second indexed constant symbol in the standard first-order vocabulary.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 57, column 60

Expression 109

(A \leftrightarrow B)

Conventional reading: open parenthesis A if and only if B close parenthesis

Meaning here: The fully parenthesized biconditional between formulas A and B.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 93, column 31

Expression 110

l (B) = r (B)

Conventional reading: left parentheses in B equals right parentheses in B

Meaning here: Formula B has equally many left and right parentheses.

3 occurrences

Expression 111

A_{i}

Conventional reading: A sub i

Meaning here: The formula or string at index i in a formation sequence.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 67, column 28

Expression 112

⟨ A_{0}, \dots, A_{n} ⟩

Conventional reading: sequence A sub zero through A sub n

Meaning here: A finite sequence of formula strings indexed from zero through n.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 238, column 22

Expression 113

n > 0

Conventional reading: n is greater than zero

Meaning here: The arity n is positive, as required for indexed predicate and function symbols in the standard vocabulary.

2 occurrences

Expression 114

\forall v_{0}

Conventional reading: the universal quantifier for variable v sub zero

Meaning here: The universal-quantifier prefix binding indexed variable v sub zero.

4 occurrences

Expression 115

(B' \to C')

Conventional reading: open parenthesis if B prime then C prime close parenthesis

Meaning here: The fully parenthesized conditional from B prime to C prime.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 177, column 34

Expression 116

*

Conventional reading: binary connective star

Meaning here: A metavariable for an arbitrary binary logical connective.

2 occurrences

Expression 117

v_{0}

Conventional reading: v sub zero

Meaning here: The first indexed individual variable in the standard first-order vocabulary.

7 occurrences

Expression 118

D \to D \to D

Conventional reading: if D then D, then D

Meaning here: The unparenthesized string containing two conditionals whose two possible constructions illustrate ambiguity.

3 occurrences

Expression 119

\forall x A (x)

Conventional reading: for every x, A of x

Meaning here: The universal quantification of a formula displayed as depending on variable x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 122, column 4

Expression 120

Frm (L)

Conventional reading: formula set of L

Meaning here: The set of well-formed formulas of the fixed first-order language L; the reader corrects the source's copied L sub zero notation.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 206, column 52

Expression 121

\in

Conventional reading: membership sign

Meaning here: The membership relation between an object and a set.

2 occurrences

Expression 122

(B [t / x] \lor C [t / x])

Conventional reading: open parenthesis B with t substituted for x, or C with t substituted for x, close parenthesis

Meaning here: Substitution distributed through a disjunction of formulas B and C.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 71, column 38

Expression 123

=

Conventional reading: equals sign

Meaning here: The two-place logical identity predicate.

3 occurrences

Expression 124

⟨ B_{0}, \dots, B_{n}, C_{0}, \dots, C_{m}, (B_{n} \land C_{m}) ⟩

Conventional reading: sequence B sub zero through B sub n, then C sub zero through C sub m, followed by their final conjunction

Meaning here: Two formation sequences concatenated and extended by the conjunction of their final formulas.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 127, column 12

Expression 125

A_{j}

Conventional reading: A sub j

Meaning here: The formula or string at earlier index j in a formation sequence.

2 occurrences

Expression 126

t'

Conventional reading: term t prime

Meaning here: The successor of term t in the postfix notation of arithmetic.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 165, column 43

Expression 127

\leq

Conventional reading: less than or equal to sign

Meaning here: The non-strict order predicate used by the language of orders.

2 occurrences

Expression 128

\leftrightarrow

Conventional reading: left right arrow biconditional symbol

Meaning here: A notation variant for the biconditional.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 127, column 37

Expression 129

A_{i} \equiv (A_{j} \lor A_{k})

Conventional reading: A sub i is syntactically identical to open parenthesis A sub j or A sub k close parenthesis

Meaning here: The indexed string A sub i is the disjunction of the earlier indexed formulas A sub j and A sub k.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 73, column 21

Expression 130

\exists v_{1}

Conventional reading: the existential quantifier for variable v sub one

Meaning here: The existential-quantifier prefix binding indexed variable v sub one.

2 occurrences

Expression 131

m_{0}, \dots, m_{k} < i

Conventional reading: indices m sub zero through m sub k are less than i

Meaning here: Every cited argument index precedes position i in a term formation sequence.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 46, column 1

Expression 132

A_{i} \equiv (A_{j} \to A_{k})

Conventional reading: A sub i is syntactically identical to open parenthesis if A sub j then A sub k close parenthesis

Meaning here: The indexed string A sub i is the conditional from earlier formula A sub j to earlier formula A sub k.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 74, column 21

Expression 133

A (x)

Conventional reading: A of x

Meaning here: A formula displayed as possibly containing individual variable x free.

2 occurrences

Expression 134

A

Conventional reading: A

Meaning here: The metavariable A denotes an arbitrary first-order formula or formula string.

105 occurrences

Expression 135

k

Conventional reading: k

Meaning here: The source symbol k denotes a sequence index or a function arity, as fixed by its source packet.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 45, column 15

Expression 136

f (t_{1} [t / x], \dots, t_{n} [t / x])

Conventional reading: function f applied to t sub one with t substituted for x, through t sub n with t substituted for x

Meaning here: The function term obtained by recursively substituting t for x in every argument of f.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 25, column 3

Expression 137

A \equiv B

Conventional reading: A is syntactically identical to B

Meaning here: Formula strings A and B contain exactly the same symbols in the same positions.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 172, column 16

Expression 138

A \equiv A_{n}

Conventional reading: A is syntactically identical to A sub n

Meaning here: Formula string A is the final indexed string A sub n of its formation sequence.

2 occurrences

Expression 139

↓

Conventional reading: Peirce arrow nor symbol

Meaning here: Peirce's arrow, read nor, a truth-functionally complete binary connective.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 154, column 7

Expression 140

A \equiv \exists x B

Conventional reading: A is syntactically identical to: there exists x such that B

Meaning here: Formula string A has existential quantifier x and scope B.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 141, column 22

Expression 141

\cdot

Conventional reading: centered dot conjunction symbol

Meaning here: A notation variant for conjunction.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 123, column 51

Expression 142

{f^{2}}_{0}

Conventional reading: f superscript two sub zero

Meaning here: The first indexed binary function symbol, used as addition in arithmetic.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 88, column 48

Expression 143

\equiv

Conventional reading: syntactic identity sign

Meaning here: The metalinguistic relation of exact symbol-for-symbol string identity.

2 occurrences

Expression 144

A \equiv (B \lor C)

Conventional reading: A is syntactically identical to open parenthesis B or C close parenthesis

Meaning here: Formula string A is exactly the fully parenthesized disjunction of B and C.

2 occurrences

Expression 145

\exists

Conventional reading: there exists sign

Meaning here: The existential operator shown without a bound variable or scope in the main-operator table.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 95, column 1

Expression 146

\to

Conventional reading: right arrow conditional symbol

Meaning here: A notation variant for the conditional.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 125, column 21

Expression 147

R

Conventional reading: R

Meaning here: The n-place predicate symbol R used to form an atomic first-order formula.

3 occurrences

Expression 148

\forall y B [t / x]

Conventional reading: for every y, B with term t substituted for x

Meaning here: The universal formula obtained when substitution proceeds beneath a quantifier for y distinct from x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 84, column 8

Expression 149

f (t_{1}, \dots, t_{n})

Conventional reading: function f of terms t sub one through t sub n

Meaning here: An n-place function term formed from f and its n argument terms.

2 occurrences

Expression 150

&

Conventional reading: ampersand conjunction symbol

Meaning here: A notation variant for conjunction.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 123, column 63

Expression 151

(E \to D)

Conventional reading: open parenthesis if E then D close parenthesis

Meaning here: The conditional from formula E to formula D.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 55, column 36

Expression 152

⟨ C_{0}, \dots, C_{m} ⟩

Conventional reading: sequence C sub zero through C sub m

Meaning here: A finite formation sequence whose final formula is C sub m.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 119, column 32

Expression 153

\forall

Conventional reading: for every sign

Meaning here: The universal quantifier operator.

2 occurrences

Expression 154

(B \to C)

Conventional reading: open parenthesis if B then C close parenthesis

Meaning here: The fully parenthesized conditional from B to C.

3 occurrences

Expression 155

y ≢ x

Conventional reading: y is not syntactically identical to x

Meaning here: Variables y and x are distinct object-language symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 20, column 34

Expression 156

f (t_{1}, \dots, t_{n})

Conventional reading: function f of terms t sub one through t sub n

Meaning here: An n-place function term written with f followed by its argument list.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 199, column 28

Expression 157

t_{1} \neq t_{2}

Conventional reading: t sub one is not identical to t sub two

Meaning here: The abbreviated negation of the identity atom between terms t sub one and t sub two.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 105, column 16

Expression 158

⟨ A ⟩

Conventional reading: sequence containing A

Meaning here: The one-entry formation sequence for an atomic formula A.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 115, column 43

Expression 159

(D \to E)

Conventional reading: open parenthesis if D then E close parenthesis

Meaning here: The conditional from formula D to formula E.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 55, column 9

Expression 160

A \equiv (A_{j} \land A_{k})

Conventional reading: A is syntactically identical to open parenthesis A sub j and A sub k close parenthesis

Meaning here: Formula string A is exactly the conjunction of earlier formulas A sub j and A sub k.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 200, column 1

Expression 161

C

Conventional reading: C

Meaning here: The metavariable C denotes an arbitrary first-order formula or formula string.

19 occurrences

Expression 162

r (A)

Conventional reading: the number of right parentheses in formula A

Meaning here: The function r applied to formula A, counting its right parentheses.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 68, column 52

Expression 163

(B [t / x] \to C [t / x])

Conventional reading: open parenthesis if B with t substituted for x, then C with t substituted for x, close parenthesis

Meaning here: Substitution distributed through a conditional from B to C.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 75, column 38

Expression 164

B * C

Conventional reading: B binary connective star C

Meaning here: The result of applying an arbitrary binary connective to formulas B and C without displaying outer parentheses.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 108, column 8

Expression 165

t \equiv y

Conventional reading: term t is syntactically identical to variable y

Meaning here: The substitution term t is exactly the variable symbol y.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 102, column 5

Expression 166

y

Conventional reading: y

Meaning here: The individual variable y.

7 occurrences

Expression 167

+

Conventional reading: plus sign

Meaning here: The binary addition function symbol in the language of arithmetic.

2 occurrences

Expression 168

B ≢ B'

Conventional reading: B is not syntactically identical to B prime

Meaning here: Formula strings B and B prime differ at some symbol position or in length.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 196, column 28

Expression 169

A \equiv (A_{j} \to A_{k})

Conventional reading: A is syntactically identical to open parenthesis if A sub j then A sub k close parenthesis

Meaning here: Formula string A is the conditional from earlier formula A sub j to earlier formula A sub k.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 193, column 21

Expression 170

\exists x A

Conventional reading: there exists x such that A

Meaning here: The existential quantification of formula A with respect to variable x.

4 occurrences

Expression 171

A \equiv \exists x A_{j}

Conventional reading: A is syntactically identical to: there exists x such that A sub j

Meaning here: Formula string A is obtained by existentially quantifying earlier formula A sub j with x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 196, column 21

Expression 172

{f^{2}}_{1}

Conventional reading: f superscript two sub one

Meaning here: The second indexed binary function symbol, used as multiplication in arithmetic.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 89, column 1

Expression 173

) (v_{0} \to \exists

Conventional reading: close parenthesis, open parenthesis, v sub zero, conditional, existential quantifier

Meaning here: An intentionally ill-formed language string used to show that not every first-order-language string is a formula.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 36, column 26

Expression 174

A \equiv \exists y x < y

Conventional reading: A is syntactically identical to: there exists y such that x is less than y

Meaning here: Formula A is the existential formula used in the variable-capture example.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 101, column 38

Expression 175

⟨ A_{0}, \dots, A_{j} ⟩

Conventional reading: sequence A sub zero through A sub j

Meaning here: The initial subsequence ending at index j of a formula formation sequence.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 202, column 1

Expression 176

\Rightarrow

Conventional reading: double right arrow conditional symbol

Meaning here: A notation variant for the conditional.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 125, column 36

Expression 177

j, k < n

Conventional reading: indices j and k are less than n

Meaning here: Both cited formula indices precede the final position n in a formation sequence.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 187, column 28

Expression 178

A_{n} \in Frm (L)

Conventional reading: A sub n is in the set of formulas of language L

Meaning here: The final indexed string A sub n is a well-formed formula of the fixed first-order language L; the reader corrects the source's copied L sub zero notation.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 199, column 1

Expression 179

Trm (L)

Conventional reading: term set of L

Meaning here: The inductively defined set of well-formed terms of first-order language L.

3 occurrences

Expression 180

l (C) = r (C)

Conventional reading: left parentheses in C equals right parentheses in C

Meaning here: Formula C has equally many left and right parentheses.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 96, column 14

Expression 181

\leftrightarrow

Conventional reading: if and only if sign

Meaning here: The binary biconditional connective.

2 occurrences

Expression 182

A_{i} \equiv \forall x A_{j}

Conventional reading: A sub i is syntactically identical to: for every x, A sub j

Meaning here: The indexed string A sub i is obtained by universally quantifying earlier formula A sub j with x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 76, column 22

Expression 183

\forall x

Conventional reading: for every x

Meaning here: A traditional universal-quantifier prefix for variable x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 138, column 31

Expression 184

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

Conventional reading: predicate R of terms t sub one through t sub n

Meaning here: An n-place atomic formula formed by applying R to terms t sub one through t sub n.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 51, column 38

Expression 185

Σ x

Conventional reading: capital sigma quantifier for x

Meaning here: A traditional notation variant for existential quantification over x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 140, column 14

Expression 186

L

Conventional reading: L

Meaning here: The first-order language L whose nonlogical symbols determine its vocabulary.

2 occurrences

Expression 187

* = *'

Conventional reading: binary connective star equals binary connective star prime

Meaning here: The two displayed connective occurrences are the same connective symbol.

2 occurrences

Expression 188

A \equiv (B' *' C')

Conventional reading: A is syntactically identical to open parenthesis B prime, binary connective star prime, C prime, close parenthesis

Meaning here: Formula string A is decomposed using primed subformulas and a primed binary connective.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 192, column 46

Expression 189

⟨ B_{0}, \dots, B_{n}, \neg B_{n} ⟩

Conventional reading: sequence B sub zero through B sub n, followed by not B sub n

Meaning here: A formula formation sequence extended by negating its final formula B sub n.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 124, column 12

Expression 190

{A^{n}}_{1}

Conventional reading: A superscript n sub one

Meaning here: The second indexed n-place predicate symbol in the standard first-order vocabulary.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 56, column 11

Expression 191

⟨ A_{0}, \dots, A_{k} ⟩

Conventional reading: sequence A sub zero through A sub k

Meaning here: The initial subsequence ending at index k of a formula formation sequence.

2 occurrences

Expression 192

t_{1}

Conventional reading: t sub one

Meaning here: The first indexed term metavariable.

8 occurrences

Expression 193

(B \lor C)

Conventional reading: open parenthesis B or C close parenthesis

Meaning here: The fully parenthesized disjunction of formulas B and C.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 164, column 37

Expression 194

⟨ B_{0}, \dots, B_{n}, C_{0}, \dots, C_{m}, (B_{n} \lor C_{m}) ⟩

Conventional reading: sequence B sub zero through B sub n, then C sub zero through C sub m, followed by their final disjunction

Meaning here: Two formation sequences concatenated and extended by the disjunction of their final formulas.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 130, column 12

Expression 195

⟨ t_{0}, \dots, t_{n} ⟩

Conventional reading: sequence t sub zero through t sub n

Meaning here: A finite sequence of term strings indexed from zero through n.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 243, column 33

Expression 196

B [y / x] \equiv \exists y y < y

Conventional reading: formula B with y substituted for x is syntactically identical to: there exists y such that y is less than y

Meaning here: The captured substitution result in the counterexample, where a formerly free y becomes bound.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 111, column 1

Expression 197

\neg ⊥

Conventional reading: not falsum

Meaning here: The negation of falsum, used as a definition of the truth constant.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 130, column 20

Expression 198

m < n

Conventional reading: m is less than n

Meaning here: The corrected proof uses m and n as final sequence indices, with m smaller than n. Equivalently, it inducts on a sequence length of n plus one and applies the hypothesis to all shorter lengths.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 185, column 30

Expression 199

A \equiv (A_{j} \lor A_{k})

Conventional reading: A is syntactically identical to open parenthesis A sub j or A sub k close parenthesis

Meaning here: Formula string A is the disjunction of earlier formulas A sub j and A sub k.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 192, column 21

Expression 200

(E x)

Conventional reading: parenthesized E x existential quantifier

Meaning here: A traditional notation variant for existential quantification with variable x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 140, column 6

Expression 201

t_{n}

Conventional reading: t sub n

Meaning here: The final indexed term metavariable t sub n.

6 occurrences

Expression 202

A \equiv (B \land C)

Conventional reading: A is syntactically identical to open parenthesis B and C close parenthesis

Meaning here: Formula string A is exactly the fully parenthesized conjunction of B and C.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 126, column 23

Expression 203

c_{2}

Conventional reading: c sub two

Meaning here: The third indexed constant symbol in the standard first-order vocabulary.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 57, column 72

Expression 204

\exists x B

Conventional reading: there exists x such that B

Meaning here: The existential quantification of formula B with respect to x.

2 occurrences

Expression 205

\neg A

Conventional reading: not A

Meaning here: The negation of formula A.

4 occurrences

Expression 206

A \equiv (A_{j} \land A_{k})

Conventional reading: A is syntactically identical to open parenthesis A sub j and A sub k close parenthesis

Meaning here: Formula string A is the conjunction of earlier formulas A sub j and A sub k.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 191, column 22

Expression 207

A

Conventional reading: the current formula

Meaning here: The current formula selected by the surrounding induction case.

23 occurrences

Expression 208

⟨ B_{0}, \dots, B_{n} ⟩

Conventional reading: sequence B sub zero through B sub n

Meaning here: A finite formation sequence ending with formula B sub n.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 119, column 1

Expression 209

a

Conventional reading: a

Meaning here: The object-language constant symbol a, or the constant metavariable in the induction principle, as fixed by context.

2 occurrences

Expression 210

\forall

Conventional reading: for every sign

Meaning here: The universal operator shown without a bound variable or scope in the main-operator table.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 94, column 1

Expression 211

\land

Conventional reading: wedge conjunction symbol

Meaning here: A notation variant for conjunction.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 123, column 41

Expression 212

|

Conventional reading: Sheffer stroke nand symbol

Meaning here: The Sheffer stroke, read nand, a truth-functionally complete binary connective.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 153, column 8

Expression 213

t_{1} = t_{2}

Conventional reading: t sub one equals t sub two

Meaning here: The identity atom written in infix notation.

2 occurrences

Expression 214

(t_{1} + t_{2})

Conventional reading: open parenthesis t sub one plus t sub two close parenthesis

Meaning here: The arithmetic addition term with arguments t sub one and t sub two.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 162, column 41

Expression 215

⊥

Conventional reading: falsum sign

Meaning here: The propositional constant for falsity, used as an atomic first-order formula when included in the profile.

7 occurrences

Expression 216

t_{1} [t / x] = t_{2} [t / x]

Conventional reading: t sub one with t substituted for x equals t sub two with t substituted for x

Meaning here: The identity formula obtained by recursively substituting t for x in both argument terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 61, column 3

Expression 217

(A \to B)

Conventional reading: open parenthesis if A then B close parenthesis

Meaning here: The fully parenthesized conditional from A to B.

2 occurrences

Expression 218

\neg B [t / x]

Conventional reading: not, formula B with term t substituted for x

Meaning here: Substitution distributed through the negation of formula B.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 64, column 5

Expression 219

\to

Conventional reading: if then sign

Meaning here: The binary logical connective if then.

6 occurrences

Expression 220

B

Conventional reading: B

Meaning here: The metavariable B denotes an arbitrary first-order formula or formula string.

57 occurrences

Expression 221

\exists y x < y

Conventional reading: there exists y such that x is less than y

Meaning here: An existential formula whose free variable x lies outside the quantifier for y.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 107, column 49

Expression 222

{f^{1}}_{0}

Conventional reading: f superscript one sub zero

Meaning here: The first indexed unary function symbol, used as successor in arithmetic.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 88, column 26

Expression 223

{A^{n}}_{0}

Conventional reading: A superscript n sub zero

Meaning here: The first indexed n-place predicate symbol in the standard first-order vocabulary.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 55, column 74

Expression 224

\forall x

Conventional reading: the universal quantifier for x

Meaning here: The universal-quantifier prefix binding x.

2 occurrences

Expression 225

{f^{1}}_{0} (t)

Conventional reading: function f superscript one sub zero of t

Meaning here: The unary successor-function term applied to t.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 167, column 59

Expression 226

B \to C

Conventional reading: if B then C

Meaning here: The conditional whose antecedent is formula B and whose consequent is formula C.

4 occurrences

Expression 227

⟨ {A^{1}}_{0} (v_{0}), {A^{1}}_{1} (c_{1}), ({A^{1}}_{1} (c_{1}) \land {A^{1}}_{0} (v_{0})), \exists v_{0} ({A^{1}}_{1} (c_{1}) \land {A^{1}}_{0} (v_{0})) ⟩

Conventional reading: sequence: A superscript one sub zero of v sub zero; A superscript one sub one of c sub one; their conjunction; then the existential conjunction binding v sub zero

Meaning here: A concrete formula formation sequence ending in an existentially quantified conjunction.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 84, column 1

Expression 228

L_{A}

Conventional reading: language L sub A

Meaning here: The first-order language of arithmetic with its order, zero, successor, addition, and multiplication symbols.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 71, column 14

Expression 229

A \equiv \neg A_{j}

Conventional reading: A is syntactically identical to not A sub j

Meaning here: Formula string A is the negation of the earlier formula A sub j.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 190, column 22

Expression 230

<

Conventional reading: less than sign

Meaning here: The strict-order predicate used by the language of arithmetic.

2 occurrences

Expression 231

(B' *' C')

Conventional reading: open parenthesis B prime, binary connective star prime, C prime, close parenthesis

Meaning here: A formula built from primed subformulas B prime and C prime using the primed binary connective.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 189, column 27

Expression 232

t \equiv t_{n}

Conventional reading: term t is syntactically identical to term t sub n

Meaning here: Term t is the final entry t sub n of its formation sequence.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 43, column 45

Expression 233

t_{i}

Conventional reading: t sub i

Meaning here: The term string at index i in a term formation sequence.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 44, column 20

Expression 234

A_{n}

Conventional reading: A sub n

Meaning here: The final formula or string at index n in a formation sequence.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 158, column 5

Expression 235

A_{i} \equiv (A_{j} \land A_{k})

Conventional reading: A sub i is syntactically identical to open parenthesis A sub j and A sub k close parenthesis

Meaning here: The indexed string A sub i is the conjunction of earlier formulas A sub j and A sub k.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 72, column 22

Expression 236

((D \to E) \to (E \to D))

Conventional reading: open parenthesis, if: if D then E; then: if E then D; close parenthesis

Meaning here: A conditional whose antecedent is D implies E and whose consequent is E implies D; the middle conditional is its main operator.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/main-operator.tex, line 54, column 1

Expression 237

\neg B

Conventional reading: not B

Meaning here: The negation of formula B.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 160, column 38

Expression 238

t

Conventional reading: t

Meaning here: An arbitrary first-order term t.

19 occurrences

Expression 239

t_{1} < t_{2}

Conventional reading: t sub one is less than t sub two

Meaning here: The arithmetic strict-order atom written infix between two terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 162, column 25

Expression 240

A (t)

Conventional reading: A of t

Meaning here: The substitution instance obtained by replacing the relevant free x occurrences in A by term t.

2 occurrences

Expression 241

{f^{n}}_{2}

Conventional reading: f superscript n sub two

Meaning here: The third indexed n-place function symbol in the standard first-order vocabulary.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 60, column 31

Expression 242

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

Conventional reading: predicate R of terms t sub one through t sub n

Meaning here: An n-place atomic formula formed by applying predicate R to its argument terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 90, column 1

Expression 243

l (A) = 1 + l (t_{1}) + \dots + l (t_{n}) = 1 + r (t_{1}) + \dots + r (t_{n}) = r (A)

Conventional reading: left parentheses in the current atomic formula equals one plus the left-parenthesis counts of t sub one through t sub n, equals one plus their right-parenthesis counts, equals right parentheses in the current atomic formula

Meaning here: The parenthesis-count chain for an n-place predicate atom, including its one argument-list parenthesis pair.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 83, column 45

Expression 244

A \equiv R (t_{1}, \dots, t_{n})

Conventional reading: A is syntactically identical to predicate R of terms t sub one through t sub n

Meaning here: Formula string A is exactly the n-place atomic formula formed from R and the displayed terms.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 138, column 7

Expression 245

\equiv

Conventional reading: triple bar equivalence symbol

Meaning here: A historical notation variant for the biconditional or material-equivalence connective in this symbol list.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 128, column 26

Expression 246

\exists v_{3} {A^{2}}_{4} (v_{3}, v_{1})

Conventional reading: there exists v sub three such that predicate A superscript two sub four holds of v sub three and v sub one

Meaning here: An existential binary atomic formula binding v sub three while retaining v sub one.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 37, column 44

Expression 247

(x)

Conventional reading: parenthesized x quantifier

Meaning here: A traditional notation variant for universal quantification over x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 138, column 59

Expression 248

L

Conventional reading: L

Meaning here: The first-order language L fixed by the surrounding construction.

31 occurrences

Expression 249

C'

Conventional reading: C prime

Meaning here: A formula metavariable distinguished from C by a prime mark.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 176, column 17

Expression 250

(B [t / x] \land C [t / x])

Conventional reading: open parenthesis B with t substituted for x, and C with t substituted for x, close parenthesis

Meaning here: Substitution distributed through a conjunction of formulas B and C.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/substitution.tex, line 67, column 38

Expression 251

(B \land C)

Conventional reading: open parenthesis B and C close parenthesis

Meaning here: The fully parenthesized conjunction of formulas B and C.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 162, column 38

Expression 252

A \equiv \neg B

Conventional reading: A is syntactically identical to not B

Meaning here: Formula string A is exactly the negation of formula string B.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 123, column 23

Expression 253

A \equiv \forall x A_{j}

Conventional reading: A is syntactically identical to: for every x, A sub j

Meaning here: Formula string A is obtained by universally quantifying earlier formula A sub j with x.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 195, column 22

Expression 254

\exists

Conventional reading: there exists sign

Meaning here: The existential quantifier operator.

2 occurrences

Expression 255

l (A) = 1 + l (B) + l (C) = 1 + r (B) + r (C) = r (A)

Conventional reading: left parentheses in the current binary formula equals one plus left parentheses in B plus left parentheses in C, equals one plus right parentheses in B plus right parentheses in C, equals right parentheses in the current binary formula

Meaning here: The parenthesis-count chain for a binary formula built from B and C, including its outer parenthesis pair.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/unique-readability.tex, line 96, column 37

Expression 256

Frm (L)

Conventional reading: formula set of L

Meaning here: The inductively defined set of well-formed formulas of first-order language L.

5 occurrences

Expression 257

F

Conventional reading: set F

Meaning here: The set F of language strings that possess formation sequences.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 177, column 5

Expression 258

{A^{2}}_{0}

Conventional reading: A superscript two sub zero

Meaning here: The first indexed binary predicate symbol, aliased by less than, membership, or less than or equal to in the named example languages.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/first-order-languages.tex, line 87, column 45

Expression 259

A \equiv (B \to C)

Conventional reading: A is syntactically identical to open parenthesis if B then C close parenthesis

Meaning here: Formula string A is exactly the conditional from B to C.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 132, column 22

Expression 260

D

Conventional reading: D

Meaning here: The metavariable D denotes an arbitrary formula used in the unique-readability and main-operator examples.

9 occurrences

Expression 261

{f^{2}}_{0} (t_{1}, t_{2})

Conventional reading: function f superscript two sub zero of t sub one and t sub two

Meaning here: The binary addition-function term with arguments t sub one and t sub two.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/terms-formulas.tex, line 167, column 1

Expression 262

B \equiv B'

Conventional reading: B is syntactically identical to B prime

Meaning here: Formula strings B and B prime contain exactly the same symbols in the same positions.

2 occurrences

Expression 263

t_{i} \equiv f (t_{m_{0}}, \dots, t_{m_{k}})

Conventional reading: term t sub i is syntactically identical to f of terms t sub m sub zero through t sub m sub k

Meaning here: The displayed source clause forms term t sub i by applying f to earlier terms indexed m sub zero through m sub k. The surrounding source calls f k-ary, producing an explicit arity-versus-indexing mismatch that the reader preserves and discloses.

1 occurrence

Occurrence 1: content/first-order-logic/syntax-and-semantics/formation-sequences.tex, line 46, column 32

Expression 264

(A \land B)

Conventional reading: open parenthesis A and B close parenthesis

Meaning here: The fully parenthesized conjunction of formulas A and B.

2 occurrences

Reading preferences

Equation and object guide

264 expression records

Expression 1

Expression 2

Expression 3

Expression 4

Expression 5

Expression 6

Expression 7

Expression 8

Expression 9

Expression 10

Expression 11

Expression 12

Expression 13

Expression 14

Expression 15

Expression 16

Expression 17

Expression 18

Expression 19

Expression 20

Expression 21

Expression 22

Expression 23

Expression 24

Expression 25

Expression 26

Expression 27

Expression 28

Expression 29

Expression 30

Expression 31

Expression 32

Expression 33

Expression 34

Expression 35

Expression 36

Expression 37

Expression 38

Expression 39

Expression 40

Expression 41

Expression 42

Expression 43

Expression 44

Expression 45

Expression 46

Expression 47

Expression 48

Expression 49

Expression 50

Expression 51

Expression 52

Expression 53

Expression 54

Expression 55

Expression 56

Expression 57

Expression 58

Expression 59

Expression 60

Expression 61

Expression 62

Expression 63

Expression 64

Expression 65

Expression 66

Expression 67

Expression 68

Expression 69

Expression 70

Expression 71

Expression 72

Expression 73

Expression 74

Expression 75

Expression 76

Expression 77