The Open Logic Text — accessible offline edition

Theories and Their Models — Explore equations

Theories and Their Models

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Equation and object guide

All 163 stable expression records, 28 formal objects, and 310 occurrence backlinks are indexed here.

163 expression records

Expression 6

Inline MathML variant

∀X∀Y(℘(X)=Y→¬∃finj(f,Y,X))

Block MathML variant

∀X∀Y(℘(X)=Y→¬∃finj(f,Y,X))

Conventional reading: for every X and Y, if Y is the power set of X, then there is no injection from Y into X

Meaning here: This is Cantor's theorem in the membership-only language: no set receives an injection from its power set.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/set-theory.tex, line 144, column 1

Expression 8

Inline MathML variant

|M|

Block MathML variant

|M|

Conventional reading: the domain of structure M

Meaning here: This is the collection of objects over which variables range in structure M.

7 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/expressing-relations.tex, line 20, column 17
  2. Occurrence 2: content/first-order-logic/models-theories/expressing-relations.tex, line 20, column 43
  3. Occurrence 3: content/first-order-logic/models-theories/expressing-relations.tex, line 21, column 4
  4. Occurrence 4: content/first-order-logic/models-theories/size-of-structures.tex, line 33, column 43
  5. Occurrence 5: content/first-order-logic/models-theories/size-of-structures.tex, line 35, column 1
  6. Occurrence 6: content/first-order-logic/models-theories/size-of-structures.tex, line 52, column 43
  7. Occurrence 7: content/first-order-logic/models-theories/size-of-structures.tex, line 64, column 8

Expression 12

Inline MathML variant

∀u(u∈z↔(∀v(v∈u↔v=x)∨∀v(v∈u↔(v=x∨v=y))))

Block MathML variant

∀u(u∈z↔(∀v(v∈u↔v=x)∨∀v(v∈u↔(v=x∨v=y))))

Conventional reading: for every u, u belongs to z if and only if u is the singleton of x or the pair set of x and y

Meaning here: This formula defines z as the Kuratowski ordered-pair code containing the singleton of x and the pair set of x and y.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/set-theory.tex, line 98, column 1

Expression 18

Inline MathML variant

Y

Block MathML variant

Y

Conventional reading: set Y

Meaning here: The uppercase letter Y names a set, codomain, or comparison domain in the current set-theoretic context.

6 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 86, column 33
  2. Occurrence 2: content/first-order-logic/models-theories/set-theory.tex, line 36, column 66
  3. Occurrence 3: content/first-order-logic/models-theories/set-theory.tex, line 37, column 63
  4. Occurrence 4: content/first-order-logic/models-theories/set-theory.tex, line 82, column 47
  5. Occurrence 5: content/first-order-logic/models-theories/set-theory.tex, line 114, column 55
  6. Occurrence 6: content/first-order-logic/models-theories/set-theory.tex, line 119, column 22

Expression 19

Inline MathML variant

n

Block MathML variant

n

Conventional reading: n

Meaning here: The letter n is the current natural-number index, relation arity, or finite size bound, as fixed by the occurrence context.

11 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/expressing-relations.tex, line 60, column 54
  2. Occurrence 2: content/first-order-logic/models-theories/expressing-relations.tex, line 83, column 7
  3. Occurrence 3: content/first-order-logic/models-theories/expressing-relations.tex, line 84, column 7
  4. Occurrence 4: content/first-order-logic/models-theories/expressing-relations.tex, line 84, column 58
  5. Occurrence 5: content/first-order-logic/models-theories/expressing-relations.tex, line 85, column 7
  6. Occurrence 6: content/first-order-logic/models-theories/expressing-relations.tex, line 85, column 65
  7. Occurrence 7: content/first-order-logic/models-theories/expressing-relations.tex, line 86, column 11
  8. Occurrence 8: content/first-order-logic/models-theories/size-of-structures.tex, line 18, column 8
  9. Occurrence 9: content/first-order-logic/models-theories/size-of-structures.tex, line 34, column 7
  10. Occurrence 10: content/first-order-logic/models-theories/size-of-structures.tex, line 35, column 30
  11. Occurrence 11: content/first-order-logic/models-theories/size-of-structures.tex, line 53, column 9

Expression 20

Inline MathML variant

M

Block MathML variant

M

Conventional reading: structure M

Meaning here: The fraktur M names the first-order structure currently being described or tested as a model.

23 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/introduction.tex, line 57, column 9
  2. Occurrence 2: content/first-order-logic/models-theories/introduction.tex, line 58, column 53
  3. Occurrence 3: content/first-order-logic/models-theories/introduction.tex, line 59, column 31
  4. Occurrence 4: content/first-order-logic/models-theories/introduction.tex, line 61, column 15
  5. Occurrence 5: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 26, column 16
  6. Occurrence 6: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 27, column 44
  7. Occurrence 7: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 30, column 15
  8. Occurrence 8: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 41, column 25
  9. Occurrence 9: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 46, column 48
  10. Occurrence 10: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 49, column 9
  11. Occurrence 11: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 51, column 36
  12. Occurrence 12: content/first-order-logic/models-theories/theories.tex, line 25, column 52
  13. Occurrence 13: content/first-order-logic/models-theories/expressing-relations.tex, line 16, column 29
  14. Occurrence 14: content/first-order-logic/models-theories/expressing-relations.tex, line 17, column 27
  15. Occurrence 15: content/first-order-logic/models-theories/expressing-relations.tex, line 18, column 19
  16. Occurrence 16: content/first-order-logic/models-theories/expressing-relations.tex, line 19, column 54
  17. Occurrence 17: content/first-order-logic/models-theories/expressing-relations.tex, line 22, column 1
  18. Occurrence 18: content/first-order-logic/models-theories/expressing-relations.tex, line 38, column 6
  19. Occurrence 19: content/first-order-logic/models-theories/expressing-relations.tex, line 44, column 61
  20. Occurrence 20: content/first-order-logic/models-theories/expressing-relations.tex, line 92, column 42
  21. Occurrence 21: content/first-order-logic/models-theories/size-of-structures.tex, line 33, column 27
  22. Occurrence 22: content/first-order-logic/models-theories/size-of-structures.tex, line 52, column 27
  23. Occurrence 23: content/first-order-logic/models-theories/size-of-structures.tex, line 63, column 61

Expression 28

Inline MathML variant

x

Block MathML variant

x

Conventional reading: x

Meaning here: The variable x denotes the current object, set, or first argument selected by the surrounding formula.

11 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 109, column 59
  2. Occurrence 2: content/first-order-logic/models-theories/theories.tex, line 138, column 8
  3. Occurrence 3: content/first-order-logic/models-theories/theories.tex, line 140, column 1
  4. Occurrence 4: content/first-order-logic/models-theories/set-theory.tex, line 43, column 38
  5. Occurrence 5: content/first-order-logic/models-theories/set-theory.tex, line 45, column 47
  6. Occurrence 6: content/first-order-logic/models-theories/set-theory.tex, line 46, column 31
  7. Occurrence 7: content/first-order-logic/models-theories/set-theory.tex, line 57, column 64
  8. Occurrence 8: content/first-order-logic/models-theories/set-theory.tex, line 103, column 13
  9. Occurrence 9: content/first-order-logic/models-theories/set-theory.tex, line 103, column 49
  10. Occurrence 10: content/first-order-logic/models-theories/set-theory.tex, line 151, column 41
  11. Occurrence 11: content/first-order-logic/models-theories/set-theory.tex, line 157, column 24

Expression 38

Inline MathML variant

∃v3(v1+v3′)=v2

Block MathML variant

∃v3(v1+v3′)=v2

Conventional reading: there exists object language v sub three such that v sub one plus the successor of v sub three equals v sub two

Meaning here: This arithmetic formula defines strict less-than by a positive additive difference. The reader supplies the source's omitted object-language marker on the final variable.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/expressing-relations.tex, line 63, column 47

Expression 46

Inline MathML variant

X

Block MathML variant

X

Conventional reading: set X

Meaning here: The uppercase letter X names a set, domain, or source of a displayed function.

11 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 25, column 28
  2. Occurrence 2: content/first-order-logic/models-theories/theories.tex, line 86, column 25
  3. Occurrence 3: content/first-order-logic/models-theories/theories.tex, line 87, column 25
  4. Occurrence 4: content/first-order-logic/models-theories/theories.tex, line 88, column 30
  5. Occurrence 5: content/first-order-logic/models-theories/set-theory.tex, line 36, column 47
  6. Occurrence 6: content/first-order-logic/models-theories/set-theory.tex, line 37, column 34
  7. Occurrence 7: content/first-order-logic/models-theories/set-theory.tex, line 82, column 24
  8. Occurrence 8: content/first-order-logic/models-theories/set-theory.tex, line 83, column 54
  9. Occurrence 9: content/first-order-logic/models-theories/set-theory.tex, line 114, column 48
  10. Occurrence 10: content/first-order-logic/models-theories/set-theory.tex, line 119, column 15
  11. Occurrence 11: content/first-order-logic/models-theories/set-theory.tex, line 143, column 54

Expression 55

Inline MathML variant

Γ

Block MathML variant

Γ

Conventional reading: Gamma

Meaning here: Gamma denotes the current theory, axiom set, or set of premise sentences.

11 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/introduction.tex, line 29, column 24
  2. Occurrence 2: content/first-order-logic/models-theories/introduction.tex, line 31, column 18
  3. Occurrence 3: content/first-order-logic/models-theories/introduction.tex, line 33, column 13
  4. Occurrence 4: content/first-order-logic/models-theories/introduction.tex, line 34, column 23
  5. Occurrence 5: content/first-order-logic/models-theories/introduction.tex, line 50, column 59
  6. Occurrence 6: content/first-order-logic/models-theories/introduction.tex, line 56, column 19
  7. Occurrence 7: content/first-order-logic/models-theories/introduction.tex, line 62, column 57
  8. Occurrence 8: content/first-order-logic/models-theories/introduction.tex, line 75, column 6
  9. Occurrence 9: content/first-order-logic/models-theories/introduction.tex, line 81, column 20
  10. Occurrence 10: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 40, column 5
  11. Occurrence 11: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 41, column 58

Expression 56

Inline MathML variant

z

Block MathML variant

z

Conventional reading: z

Meaning here: The variable z denotes a candidate set, ordered-pair code, product member, or third relation argument.

4 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 138, column 54
  2. Occurrence 2: content/first-order-logic/models-theories/theories.tex, line 139, column 61
  3. Occurrence 3: content/first-order-logic/models-theories/set-theory.tex, line 44, column 24
  4. Occurrence 4: content/first-order-logic/models-theories/set-theory.tex, line 102, column 40

Expression 59

Inline MathML variant

N

Block MathML variant

N

Conventional reading: structure N

Meaning here: This is the standard structure with natural-number domain and ordinary less-than relation.

7 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/expressing-relations.tex, line 104, column 30
  2. Occurrence 2: content/first-order-logic/models-theories/expressing-relations.tex, line 108, column 33
  3. Occurrence 3: content/first-order-logic/models-theories/expressing-relations.tex, line 109, column 33
  4. Occurrence 4: content/first-order-logic/models-theories/expressing-relations.tex, line 110, column 33
  5. Occurrence 5: content/first-order-logic/models-theories/expressing-relations.tex, line 112, column 3
  6. Occurrence 6: content/first-order-logic/models-theories/expressing-relations.tex, line 114, column 3
  7. Occurrence 7: content/first-order-logic/models-theories/expressing-relations.tex, line 116, column 3

Expression 61

Inline MathML variant

m

Block MathML variant

m

Conventional reading: m

Meaning here: The letter m denotes a natural number, a relation argument, or an output in the current occurrence.

3 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/expressing-relations.tex, line 60, column 30
  2. Occurrence 2: content/first-order-logic/models-theories/expressing-relations.tex, line 84, column 26
  3. Occurrence 3: content/first-order-logic/models-theories/expressing-relations.tex, line 84, column 37

Expression 71

Inline MathML variant

≤

Block MathML variant

≤

Conventional reading: less than or equal to

Meaning here: This is the non-strict ordering relation discussed as a definable structural primitive.

3 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/introduction.tex, line 90, column 3
  2. Occurrence 2: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 21, column 37
  3. Occurrence 3: content/first-order-logic/models-theories/expressing-relations.tex, line 57, column 60

Expression 74

Inline MathML variant

M⊨A20(a,b)

Block MathML variant

M⊨A20(a,b)

Conventional reading: the deliberately invalid notation structure M satisfies predicate A superscript two sub zero applied to domain elements a and b

Meaning here: This is deliberately invalid notation rejected by the source. The letters a and b denote domain elements rather than object-language terms, so the displayed satisfaction expression is not well formed and no assignment-relative truth condition is asserted here.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/expressing-relations.tex, line 31, column 17

Expression 80

Inline MathML variant

∀x(x·1)=x∀x∀y∀z(x·(y·z))=((x·y)·z)∀x∃y(x·y)=1

Block MathML variant

∀x(x·1)=x∀x∀y∀z(x·(y·z))=((x·y)·z)∀x∃y(x·y)=1

Conventional reading: first, every x times one equals x; second, multiplication is associative; third, for every x there is a y such that x times y equals one

Meaning here: These three sentences axiomatize groups using an identity constant, associativity, and existence of inverses.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 32, column 1

Expression 82

Inline MathML variant

∅

Block MathML variant

∅

Conventional reading: the empty set

Meaning here: This is the unique set with no elements.

6 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 85, column 1
  2. Occurrence 2: content/first-order-logic/models-theories/set-theory.tex, line 26, column 15
  3. Occurrence 3: content/first-order-logic/models-theories/set-theory.tex, line 57, column 30
  4. Occurrence 4: content/first-order-logic/models-theories/set-theory.tex, line 58, column 50
  5. Occurrence 5: content/first-order-logic/models-theories/set-theory.tex, line 62, column 23
  6. Occurrence 6: content/first-order-logic/models-theories/set-theory.tex, line 64, column 35

Expression 84

Inline MathML variant

{∀xx≤x,∀x∀y((x≤y∧y≤x)→x=y),∀x∀y∀z((x≤y∧y≤z)→x≤z)}

Block MathML variant

{∀xx≤x,∀x∀y((x≤y∧y≤x)→x=y),∀x∀y∀z((x≤y∧y≤z)→x≤z)}

Conventional reading: the three axioms of reflexivity antisymmetry and transitivity for less than or equal to

Meaning here: This displayed axiom set characterizes partial orders.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 53, column 1

Expression 89

Inline MathML variant

℘(X)

Block MathML variant

℘(X)

Conventional reading: the power set of X

Meaning here: This is the set of all subsets of X.

4 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/set-theory.tex, line 27, column 30
  2. Occurrence 2: content/first-order-logic/models-theories/set-theory.tex, line 73, column 58
  3. Occurrence 3: content/first-order-logic/models-theories/set-theory.tex, line 83, column 17
  4. Occurrence 4: content/first-order-logic/models-theories/set-theory.tex, line 143, column 41

Expression 94

Inline MathML variant

y

Block MathML variant

y

Conventional reading: y

Meaning here: The variable y denotes the current set, output, witness, or second argument selected by the context.

10 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 110, column 9
  2. Occurrence 2: content/first-order-logic/models-theories/theories.tex, line 138, column 30
  3. Occurrence 3: content/first-order-logic/models-theories/theories.tex, line 139, column 22
  4. Occurrence 4: content/first-order-logic/models-theories/theories.tex, line 139, column 53
  5. Occurrence 5: content/first-order-logic/models-theories/set-theory.tex, line 43, column 46
  6. Occurrence 6: content/first-order-logic/models-theories/set-theory.tex, line 45, column 55
  7. Occurrence 7: content/first-order-logic/models-theories/set-theory.tex, line 46, column 39
  8. Occurrence 8: content/first-order-logic/models-theories/set-theory.tex, line 103, column 57
  9. Occurrence 9: content/first-order-logic/models-theories/set-theory.tex, line 140, column 20
  10. Occurrence 10: content/first-order-logic/models-theories/set-theory.tex, line 156, column 46

Expression 99

Inline MathML variant

A=n≡∃x1∃x2…∃xn(x1≠x2∧x1≠x3∧x1≠x4∧…∧x1≠xn∧x2≠x3∧x2≠x4∧…∧x2≠xn∧⋮xn−1≠xn∧∀y(y=x1∨…∨y=xn))

Block MathML variant

A=n≡∃x1∃x2…∃xn(x1≠x2∧x1≠x3∧x1≠x4∧…∧x1≠xn∧x2≠x3∧x2≠x4∧…∧x2≠xn∧⋮xn−1≠xn∧∀y(y=x1∨…∨y=xn))

Conventional reading: A sub exactly n says that there exist n pairwise distinct objects and every object equals one of them

Meaning here: This sentence is true exactly in structures whose domains contain n elements.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/size-of-structures.tex, line 41, column 1

Expression 103

Inline MathML variant

f:X→Y∧∀x∀x′(((x∈X∧x′∈X)∧∃y(maps(f,x,y)∧maps(f,x′,y)))→x=x′)

Block MathML variant

f:X→Y∧∀x∀x′(((x∈X∧x′∈X)∧∃y(maps(f,x,y)∧maps(f,x′,y)))→x=x′)

Conventional reading: f is a function from X to Y and any two members of X mapped to one y are equal

Meaning here: This is the explicit injectivity condition. The reader regroups a scope split by the source alignment.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/set-theory.tex, line 133, column 1

Expression 104

Inline MathML variant

A≥n≡∃x1∃x2…∃xn(x1≠x2∧x1≠x3∧x1≠x4∧…∧x1≠xn∧x2≠x3∧x2≠x4∧…∧x2≠xn∧⋮xn−1≠xn)

Block MathML variant

A≥n≡∃x1∃x2…∃xn(x1≠x2∧x1≠x3∧x1≠x4∧…∧x1≠xn∧x2≠x3∧x2≠x4∧…∧x2≠xn∧⋮xn−1≠xn)

Conventional reading: A sub at least n says that there exist n pairwise distinct objects

Meaning here: This sentence is true exactly in structures whose domains contain at least n elements.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/size-of-structures.tex, line 23, column 1

Expression 110

Inline MathML variant

RabiffM,s⊨A20(v1,v2).

Block MathML variant

RabiffM,s⊨A20(v1,v2).

Conventional reading: R holds of a and b if and only if structure M under assignment s satisfies predicate A superscript two sub zero of v sub one and v sub two

Meaning here: This equivalence explains how an atomic formula expresses the relation assigned to its predicate symbol.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/expressing-relations.tex, line 27, column 1

Expression 123

Inline MathML variant

ZFC

Block MathML variant

ZFC

Conventional reading: Z F C

Meaning here: This abbreviation names Zermelo Fraenkel set theory with the axiom of choice.

5 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/set-theory.tex, line 18, column 1
  2. Occurrence 2: content/first-order-logic/models-theories/set-theory.tex, line 54, column 38
  3. Occurrence 3: content/first-order-logic/models-theories/set-theory.tex, line 60, column 36
  4. Occurrence 4: content/first-order-logic/models-theories/set-theory.tex, line 90, column 4
  5. Occurrence 5: content/first-order-logic/models-theories/set-theory.tex, line 166, column 11

Expression 132

Inline MathML variant

<

Block MathML variant

<

Conventional reading: less than

Meaning here: This is the strict ordering predicate or relation in the current example.

4 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/introduction.tex, line 90, column 52
  2. Occurrence 2: content/first-order-logic/models-theories/theories.tex, line 59, column 52
  3. Occurrence 3: content/first-order-logic/models-theories/expressing-relations.tex, line 65, column 49
  4. Occurrence 4: content/first-order-logic/models-theories/expressing-relations.tex, line 103, column 1

Expression 134

Inline MathML variant

∀z∃y∀x(x∈y↔(x∈z∧A(x)).

Block MathML variant

∀z∃y∀x(x∈y↔(x∈z∧A(x)).

Conventional reading: for every z there exists a y containing exactly those x in z for which A of x holds

Meaning here: This is the separation schema, which forms a subset of an existing set rather than an unrestricted comprehension set.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/set-theory.tex, line 168, column 1

Expression 135

Inline MathML variant

≤M

Block MathML variant

≤M

Conventional reading: the interpretation of less than or equal to in structure M

Meaning here: This is the relation that M assigns to the non-strict ordering predicate.

4 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 47, column 1
  2. Occurrence 2: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 49, column 25
  3. Occurrence 3: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 51, column 52
  4. Occurrence 4: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 60, column 39

Expression 140

Inline MathML variant

∀u(u∈f→∃x∃y(x∈X∧y∈Y∧⟨x,y⟩=u))∧∀x(x∈X→(∃y(y∈Y∧maps(f,x,y))∧∀y∀y′((maps(f,x,y)∧maps(f,x,y′))→y=y′)))

Block MathML variant

∀u(u∈f→∃x∃y(x∈X∧y∈Y∧⟨x,y⟩=u))∧∀x(x∈X→(∃y(y∈Y∧maps(f,x,y))∧∀y∀y′((maps(f,x,y)∧maps(f,x,y′))→y=y′)))

Conventional reading: every member of f codes a pair from X and Y, every x in X has a mapped y in Y, and mapped values are unique

Meaning here: These clauses say exactly that the set f is the graph of a total single-valued function from X to Y. The reader regroups both implication scopes split by source alignment at lines one hundred twenty-one and one hundred twenty-three.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/set-theory.tex, line 120, column 1

Expression 143

Inline MathML variant

∀xP(x,x)∀x∀y((P(x,y)∧P(y,x))→x=y)∀x∀y∀z((P(x,y)∧P(y,z))→P(x,z))Moreover, any two objects have a mereological sum (an object that has these two objects as parts, and is minimal in this respect).∀x∀y∃z∀u(P(z,u)↔(P(x,u)∧P(y,u)))

Block MathML variant

∀xP(x,x)∀x∀y((P(x,y)∧P(y,x))→x=y)∀x∀y∀z((P(x,y)∧P(y,z))→P(x,z))Moreover, any two objects have a mereological sum (an object that has these two objects as parts, and is minimal in this respect).∀x∀y∃z∀u(P(z,u)↔(P(x,u)∧P(y,u)))

Conventional reading: parthood is reflexive antisymmetric and transitive, and every two objects have a least common whole

Meaning here: These displayed sentences give basic mereological axioms, with the final biconditional characterizing the mereological sum by its superobjects.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 122, column 1

Expression 144

Inline MathML variant

∀u((u∈x∨u∈y)↔u∈z)∀u(u⊆x↔u∈y)

Block MathML variant

∀u((u∈x∨u∈y)↔u∈z)∀u(u⊆x↔u∈y)

Conventional reading: u belongs to z exactly when it belongs to x or y, and u belongs to y exactly when it is a subset of x

Meaning here: The two rows define the binary union relation and the power-set relation in the membership language.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/set-theory.tex, line 77, column 1

Expression 145

Inline MathML variant

∃x¬∃yy∈x∀x∀y(∀z(z∈x↔z∈y)→x=y)∀x∀y∃z∀u(u∈z↔(u=x∨u=y))∀x∃y∀z(z∈y↔∃u(z∈u∧u∈x))plus all sentences of the form∃x∀y(y∈x↔A(y))

Block MathML variant

∃x¬∃yy∈x∀x∀y(∀z(z∈x↔z∈y)→x=y)∀x∀y∃z∀u(u∈z↔(u=x∨u=y))∀x∃y∀z(z∈y↔∃u(z∈u∧u∈x))plus all sentences of the form∃x∀y(y∈x↔A(y))

Conventional reading: there is an empty set; sets with the same elements are equal; pair sets and unions exist; and every property has a comprehension set

Meaning here: This displayed candidate theory combines empty set, extensionality, pairing, union, and unrestricted comprehension. The reader repairs the malformed z quantifier scope while preserving the source text.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 73, column 1

Expression 148

Inline MathML variant

∀z(z∈Z↔∃x∃y(x∈X∧y∈Y∧⟨x,y⟩=z))

Block MathML variant

∀z(z∈Z↔∃x∃y(x∈X∧y∈Y∧⟨x,y⟩=z))

Conventional reading: for every z, z belongs to Z exactly when it is an ordered pair of an x in X and a y in Y

Meaning here: This membership-only formula defines Z as the Cartesian product of X and Y.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/set-theory.tex, line 107, column 1

Expression 150

Inline MathML variant

L

Block MathML variant

L

Conventional reading: language L

Meaning here: The script L names the first-order language of the current structure or theory.

6 occurrences
  1. Occurrence 1: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 22, column 46
  2. Occurrence 2: content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 40, column 54
  3. Occurrence 3: content/first-order-logic/models-theories/expressing-relations.tex, line 17, column 14
  4. Occurrence 4: content/first-order-logic/models-theories/expressing-relations.tex, line 21, column 54
  5. Occurrence 5: content/first-order-logic/models-theories/expressing-relations.tex, line 43, column 55
  6. Occurrence 6: content/first-order-logic/models-theories/expressing-relations.tex, line 45, column 26

Expression 151

Inline MathML variant

∀x∀y((∀z(z∈x→z∈y)∧∀z(z∈y→z∈x))→x=y).

Block MathML variant

∀x∀y((∀z(z∈x→z∈y)∧∀z(z∈y→z∈x))→x=y).

Conventional reading: for every x and y, if every element of x is in y and every element of y is in x, then x equals y

Meaning here: This is the axiom of extensionality with both subset relations expanded into membership formulas.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/set-theory.tex, line 50, column 1

Expression 155

Inline MathML variant

∀x∀y(x′=y′→x=y)∀x0≠x′∀x(x+0)=x∀x∀y(x+y′)=(x+y)′∀x(x×0)=0∀x∀y(x×y′)=((x×y)+x)∀x∀y(x<y↔∃z(z′+x)=y)plus all sentences of the form(A(0)∧∀x(A(x)→A(x′)))→∀xA(x)

Block MathML variant

∀x∀y(x′=y′→x=y)∀x0≠x′∀x(x+0)=x∀x∀y(x+y′)=(x+y)′∀x(x×0)=0∀x∀y(x×y′)=((x×y)+x)∀x∀y(x<y↔∃z(z′+x)=y)plus all sentences of the form(A(0)∧∀x(A(x)→A(x′)))→∀xA(x)

Conventional reading: successor is injective and never zero; addition and multiplication obey their recursive equations; less than has a positive difference; and every formula has its induction instance

Meaning here: These rows present the displayed Peano-arithmetic axioms and the induction schema.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 43, column 1

Expression 163

Inline MathML variant

{∀x¬x<x,∀x∀y((x<y∨y<x)∨x=y),∀x∀y∀z((x<y∧y<z)→x<z)}

Block MathML variant

{∀x¬x<x,∀x∀y((x<y∨y<x)∨x=y),∀x∀y∀z((x<y∧y<z)→x<z)}

Conventional reading: the three axioms that less than is irreflexive total and transitive

Meaning here: This displayed axiom set characterizes strict linear orders.

1 occurrence
  1. Occurrence 1: content/first-order-logic/models-theories/theories.tex, line 16, column 1

28 formal objects

  1. Definition of a closed theory and its closure — content/first-order-logic/models-theories/introduction.tex, line 28.
  2. Definition of a model of a sentence set — content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 39.
  3. Example axiomatizing partial orders — content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 45.
  4. Displayed partial-order axioms — content/first-order-logic/models-theories/expressing-props-of-structures.tex, line 53.
  5. Example theory of strict linear orders — content/first-order-logic/models-theories/theories.tex, line 13.
  6. Displayed strict-linear-order axioms — content/first-order-logic/models-theories/theories.tex, line 16.
  7. Example theory of groups — content/first-order-logic/models-theories/theories.tex, line 29.
  8. Displayed group axioms — content/first-order-logic/models-theories/theories.tex, line 32.
  9. Example Peano arithmetic — content/first-order-logic/models-theories/theories.tex, line 40.
  10. Displayed Peano-arithmetic axioms — content/first-order-logic/models-theories/theories.tex, line 43.
  11. Example candidate theory of pure sets — content/first-order-logic/models-theories/theories.tex, line 62.
  12. Displayed pure-set axioms — content/first-order-logic/models-theories/theories.tex, line 73.
  13. Example theory of mereological parthood — content/first-order-logic/models-theories/theories.tex, line 102.
  14. Displayed mereology axioms — content/first-order-logic/models-theories/theories.tex, line 122.
  15. Definition of a formula expressing a relation — content/first-order-logic/models-theories/expressing-relations.tex, line 42.
  16. Example definable arithmetic relations — content/first-order-logic/models-theories/expressing-relations.tex, line 55.
  17. Exercise defining arithmetic relations — content/first-order-logic/models-theories/expressing-relations.tex, line 80; preserved unsolved prompt.
  18. Exercise transforming an expressed relation — content/first-order-logic/models-theories/expressing-relations.tex, line 90; preserved unsolved prompt.
  19. Exercise on definability in the natural-number order — content/first-order-logic/models-theories/expressing-relations.tex, line 101; preserved unsolved prompt.
  20. Displayed definitions of union and power set — content/first-order-logic/models-theories/set-theory.tex, line 77.
  21. Displayed definition of a function graph — content/first-order-logic/models-theories/set-theory.tex, line 120.
  22. Displayed definition of injectivity — content/first-order-logic/models-theories/set-theory.tex, line 133.
  23. Exercise deriving Russell's contradiction — content/first-order-logic/models-theories/set-theory.tex, line 173; preserved unsolved prompt.
  24. Proposition expressing at least and at most n elements — content/first-order-logic/models-theories/size-of-structures.tex, line 21.
  25. Displayed sentence for at least n elements — content/first-order-logic/models-theories/size-of-structures.tex, line 23.
  26. Proposition expressing exactly n elements — content/first-order-logic/models-theories/size-of-structures.tex, line 39.
  27. Displayed sentence for exactly n elements — content/first-order-logic/models-theories/size-of-structures.tex, line 41.
  28. Proposition characterizing infinite structures — content/first-order-logic/models-theories/size-of-structures.tex, line 56.

References and diagrams

No source references or proof diagrams occur in this chapter.