The Open Logic Text — accessible offline edition

Natural Deduction — Explore equations

Natural Deduction

Reading preferences

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

Equation, formal-object, proof, and reference guide

This index exposes 279 expressions, 558 native MathML variants, 140 formal objects, 545 exact proof-command bindings, 10 references, and all ten unsolved exercises without adding solutions.

279 expression records

Expression 1

Inline MathML variant

Γ1⊨A\Gamma_1 \Entails !A

Block MathML variant

Γ1⊨A\Gamma_1 \Entails !A

Conventional reading: Gamma one semantically entails A

Meaning here: Every structure satisfying Gamma one satisfies A.

1 occurrence
  1. Occurrence 1: soundness.tex, line 237, column 43

Expression 3

Inline MathML variant

⊥C\FalseCl

Block MathML variant

⊥C\FalseCl

Conventional reading: classical absurdity rule

Meaning here: The classical natural-deduction rule that infers A from a contradiction derived under assumption not A, permitting that assumption to be discharged.

5 occurrences
  1. Occurrence 1: propositional-rules.tex, line 111, column 31
  2. Occurrence 2: propositional-rules.tex, line 113, column 29
  3. Occurrence 3: proving-things.tex, line 307, column 24
  4. Occurrence 4: proving-things-quant.tex, line 252, column 24
  5. Occurrence 5: provability-consistency.tex, line 66, column 54

Expression 4

Inline MathML variant

∃x(A(x)∧B(x))\lexists[x][(!A(x) \land !B(x))]

Block MathML variant

∃x(A(x)∧B(x))\lexists[x][(!A(x) \land !B(x))]

Conventional reading: there exists an x such that both A of x and B of x

Meaning here: The existential formula asserting that at least one object satisfies both A and B.

5 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 103, column 45
  2. Occurrence 2: proving-things-quant.tex, line 113, column 49
  3. Occurrence 3: proving-things-quant.tex, line 118, column 9
  4. Occurrence 4: proving-things-quant.tex, line 144, column 9
  5. Occurrence 5: proving-things-quant.tex, line 162, column 9

Expression 5

Inline MathML variant

⊢¬∃xA(x)→∀x¬A(x)\Proves \lnot\lexists[x][!A(x)] \lif \lforall[x][\lnot !A(x)]

Block MathML variant

⊢¬∃xA(x)→∀x¬A(x)\Proves \lnot\lexists[x][!A(x)] \lif \lforall[x][\lnot !A(x)]

Conventional reading: without undischarged assumptions, derive: if no x is A, then every x is not A

Meaning here: The negation of an existential A claim implies the universal negation of A, with the conditional derivable from no undischarged assumptions.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 239, column 7

Expression 9

Inline MathML variant

M,s⊨A(t2)\Sat{M}{!A(t_2)}[s]

Block MathML variant

M,s⊨A(t2)\Sat{M}{!A(t_2)}[s]

Conventional reading: structure M satisfies A of t two under assignment s

Meaning here: Formula A of the closed term t two is satisfied in structure M under variable assignment s.

1 occurrence
  1. Occurrence 1: soundness-identity.tex, line 43, column 39

Expression 10

Inline MathML variant

¬∀xA(x)\lnot \lforall[x][!A(x)]

Block MathML variant

¬∀xA(x)\lnot \lforall[x][!A(x)]

Conventional reading: it is not the case that, for every x, A of x

Meaning here: The negation of the universal statement that every object satisfies A.

9 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 31, column 10
  2. Occurrence 2: proving-things-quant.tex, line 35, column 44
  3. Occurrence 3: proving-things-quant.tex, line 44, column 10
  4. Occurrence 4: proving-things-quant.tex, line 46, column 13
  5. Occurrence 5: proving-things-quant.tex, line 50, column 20
  6. Occurrence 6: proving-things-quant.tex, line 61, column 12
  7. Occurrence 7: proving-things-quant.tex, line 63, column 13
  8. Occurrence 8: proving-things-quant.tex, line 81, column 12
  9. Occurrence 9: proving-things-quant.tex, line 83, column 13

Expression 11

Inline MathML variant

m=ValM(t1)=ValM(t2)m = \Value{t_1}{M} = \Value{t_2}{M}

Block MathML variant

m=ValM(t1)=ValM(t2)m = \Value{t_1}{M} = \Value{t_2}{M}

Conventional reading: m equals the value of t one in structure M, which also equals the value of t two in structure M

Meaning here: The object m is defined as the common denotation of the two identical closed terms in structure M.

1 occurrence
  1. Occurrence 1: soundness-identity.tex, line 41, column 37

Expression 12

Inline MathML variant

C→(C∧D)!C \lif (!C \land !D)

Block MathML variant

C→(C∧D)!C \lif (!C \land !D)

Conventional reading: if C, then C and D

Meaning here: The conditional with antecedent C and consequent the conjunction of C and D.

1 occurrence
  1. Occurrence 1: derivations.tex, line 86, column 12

Expression 14

Inline MathML variant

Γ⊢A(c)\Gamma \Proves !A(c)

Block MathML variant

Γ⊢A(c)\Gamma \Proves !A(c)

Conventional reading: Gamma syntactically derives A of c

Meaning here: There is a natural-deduction derivation of A of c whose undischarged assumptions all belong to Gamma.

1 occurrence
  1. Occurrence 1: provability-quantifiers.tex, line 23, column 28

Expression 17

Inline MathML variant

⊢(¬A∧¬B)→¬(A∨B)\Proves (\lnot !A \land \lnot !B) \lif\lnot(!A \lor !B)

Block MathML variant

⊢(¬A∧¬B)→¬(A∨B)\Proves (\lnot !A \land \lnot !B) \lif\lnot(!A \lor !B)

Conventional reading: without undischarged assumptions, derive: if both not A and not B, then it is not the case that A or B

Meaning here: One direction of De Morgan's law has a derivation without undischarged assumptions: not A and not B implies the negation of A or B.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 290, column 7

Expression 19

Inline MathML variant

∀x¬A(x)⊢¬∃xA(x)\lforall[x][\lnot !A(x)] \Proves \lnot\lexists[x][!A(x)]

Block MathML variant

∀x¬A(x)⊢¬∃xA(x)\lforall[x][\lnot !A(x)] \Proves \lnot\lexists[x][!A(x)]

Conventional reading: from: for every x, not A of x; derive: it is not the case that there exists an x such that A of x

Meaning here: Universal failure of A derives the negation of the existential claim that any object satisfies A.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 238, column 7

Expression 20

Inline MathML variant

⊢(∀xA(x)∧∀yB(y))→∀z(A(z)∧B(z))\Proves (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) \lif \lforall[z][(!A(z) \land !B(z))]

Block MathML variant

⊢(∀xA(x)∧∀yB(y))→∀z(A(z)∧B(z))\Proves (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) \lif \lforall[z][(!A(z) \land !B(z))]

Conventional reading: without undischarged assumptions, derive: if every x is A and every y is B, then every z is both A and B

Meaning here: The conjunction of the two universal claims implies that every object satisfies both predicates, and the conditional is derivable with no undischarged assumptions.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 233, column 7

Expression 25

Inline MathML variant

(∀xA(x)→B)⊢∃y(A(y)→B)(\lforall[x][!A(x)] \lif !B) \Proves \lexists[y][(!A(y) \lif !B)]

Block MathML variant

(∀xA(x)→B)⊢∃y(A(y)→B)(\lforall[x][!A(x)] \lif !B) \Proves \lexists[y][(!A(y) \lif !B)]

Conventional reading: from: if every x is A, then B; derive that there exists a y such that, if A of y, then B

Meaning here: The displayed premise derives an existentially quantified conditional with a witness y; the source marks the exercise as classical.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 249, column 7

Expression 27

Inline MathML variant

⊢(A→¬A)→¬A\Proves (!A \lif \lnot !A) \lif \lnot !A

Block MathML variant

⊢(A→¬A)→¬A\Proves (!A \lif \lnot !A) \lif \lnot !A

Conventional reading: without undischarged assumptions, derive: if the conditional from A to not A holds, then not A

Meaning here: The displayed conditional has a natural-deduction derivation with no undischarged assumptions.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 284, column 7

Expression 29

Inline MathML variant

M\Struct M

Block MathML variant

M\Struct M

Conventional reading: structure M

Meaning here: An arbitrary first-order structure M used in the soundness argument for identity.

1 occurrence
  1. Occurrence 1: soundness-identity.tex, line 19, column 25

Expression 31

Inline MathML variant

(A∨B)→C⊢A→C(!A \lor !B) \lif !C \Proves !A \lif !C

Block MathML variant

(A∨B)→C⊢A→C(!A \lor !B) \lif !C \Proves !A \lif !C

Conventional reading: from if A or B then C, derive: if A then C

Meaning here: The sequent asserting that the conditional from A or B to C yields a conditional from A to C.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 280, column 7

Expression 32

Inline MathML variant

(A→C)∧(B→C)⊢(A∨B)→C(!A \lif !C) \land (!B \lif !C) \Proves (!A \lor !B) \lif !C

Block MathML variant

(A→C)∧(B→C)⊢(A∨B)→C(!A \lif !C) \land (!B \lif !C) \Proves (!A \lor !B) \lif !C

Conventional reading: from the conjunction of the conditional from A to C with the conditional from B to C, derive the conditional from the disjunction A or B to C

Meaning here: From the single conjunctive assumption consisting of if A then C and if B then C, natural deduction derives the conditional from A or B to C.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 281, column 7

Expression 33

Inline MathML variant

[¬A]2,[A]3\Discharge{\lnot !A}{2}, \Discharge{!A}{3}

Block MathML variant

[¬A]2,[A]3\Discharge{\lnot !A}{2}, \Discharge{!A}{3}

Conventional reading: assumptions not A labeled two, and A labeled three, for discharge

Meaning here: Two active assumptions: not A carries discharge label two, while A carries discharge label three.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 102, column 9

Expression 34

Inline MathML variant

⊢¬¬A→A\Proves \lnot \lnot !A \lif !A

Block MathML variant

⊢¬¬A→A\Proves \lnot \lnot !A \lif !A

Conventional reading: without undischarged assumptions, derive: if not not A, then A

Meaning here: Double-negation elimination has a classical natural-deduction derivation with no undischarged assumptions.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 301, column 7

Expression 36

Inline MathML variant

A∧(B∧C)⊢(A∧B)∧C!A \land (!B \land !C) \Proves (!A \land !B) \land !C

Block MathML variant

A∧(B∧C)⊢(A∧B)∧C!A \land (!B \land !C) \Proves (!A \land !B) \land !C

Conventional reading: from the single conjunctive premise whose left conjunct is A and whose right conjunct is the conjunction of B and C, derive the conjunction of A and B, conjoined with C

Meaning here: There is a derivation of the conjunction of A and B, conjoined with C, from the single assumption A conjoined with the conjunction of B and C.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 270, column 7

Expression 37

Inline MathML variant

A→B!A \lif !B

Block MathML variant

A→B!A \lif !B

Conventional reading: if A, then B

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

27 occurrences
  1. Occurrence 1: propositional-rules.tex, line 69, column 12
  2. Occurrence 2: propositional-rules.tex, line 72, column 9
  3. Occurrence 3: derivations.tex, line 106, column 14
  4. Occurrence 4: proving-things.tex, line 73, column 10
  5. Occurrence 5: proving-things.tex, line 83, column 19
  6. Occurrence 6: proving-things.tex, line 89, column 10
  7. Occurrence 7: proving-things.tex, line 91, column 10
  8. Occurrence 8: proving-things.tex, line 93, column 14
  9. Occurrence 9: proving-things.tex, line 98, column 65
  10. Occurrence 10: proving-things.tex, line 105, column 12
  11. Occurrence 11: proving-things.tex, line 109, column 12
  12. Occurrence 12: proving-things.tex, line 111, column 14
  13. Occurrence 13: proving-things.tex, line 138, column 12
  14. Occurrence 14: proving-things.tex, line 142, column 12
  15. Occurrence 15: proving-things.tex, line 144, column 14
  16. Occurrence 16: proving-things.tex, line 165, column 12
  17. Occurrence 17: proving-things.tex, line 168, column 12
  18. Occurrence 18: proving-things.tex, line 170, column 14
  19. Occurrence 19: proof-theoretic-notions.tex, line 92, column 14
  20. Occurrence 20: provability-propositional.tex, line 107, column 15
  21. Occurrence 21: provability-propositional.tex, line 122, column 18
  22. Occurrence 22: provability-propositional.tex, line 126, column 18
  23. Occurrence 23: soundness.tex, line 130, column 43
  24. Occurrence 24: soundness.tex, line 137, column 16
  25. Occurrence 25: soundness.tex, line 245, column 12
  26. Occurrence 26: soundness.tex, line 249, column 14
  27. Occurrence 27: soundness.tex, line 256, column 28

Expression 38

Inline MathML variant

∃xC(x,b)\lexists[x][!C(x, b)]

Block MathML variant

∃xC(x,b)\lexists[x][!C(x, b)]

Conventional reading: there exists an x such that C of x and b

Meaning here: The existential formula asserting that some object stands in relation C to b.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 113, column 20

Expression 39

Inline MathML variant

[C]1\Discharge{!C}{1}

Block MathML variant

[C]1\Discharge{!C}{1}

Conventional reading: assumption C, labeled one for discharge

Meaning here: An occurrence of assumption C marked with discharge label one.

1 occurrence
  1. Occurrence 1: derivations.tex, line 81, column 9

Expression 41

Inline MathML variant

Γ∪{A}⊨B\Gamma \cup \{!A\} \Entails !B

Block MathML variant

Γ∪{A}⊨B\Gamma \cup \{!A\} \Entails !B

Conventional reading: Gamma together with assumption A semantically entails B

Meaning here: Every structure satisfying Gamma and A also satisfies B.

1 occurrence
  1. Occurrence 1: soundness.tex, line 140, column 36

Expression 44

Inline MathML variant

⊢¬(A→B)→¬B\Proves \lnot(!A \lif !B) \lif \lnot !B

Block MathML variant

⊢¬(A→B)→¬B\Proves \lnot(!A \lif !B) \lif \lnot !B

Conventional reading: without undischarged assumptions, derive: if it is not the case that A implies B, then not B

Meaning here: The displayed conditional from the negation of A implies B to not B has a derivation with no undischarged assumptions.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 285, column 7

Expression 48

Inline MathML variant

[∀xA(x)]1\Discharge{\lforall[x][!A(x)]}{1}

Block MathML variant

[∀xA(x)]1\Discharge{\lforall[x][!A(x)]}{1}

Conventional reading: assumption: for every x, A of x; labeled one for discharge

Meaning here: The universal assumption that every object satisfies A, marked with discharge label one.

3 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 196, column 9
  2. Occurrence 2: proving-things-quant.tex, line 207, column 9
  3. Occurrence 3: proving-things-quant.tex, line 220, column 9

Expression 50

Inline MathML variant

A≡⊥!A \ident \lfalse

Block MathML variant

A≡⊥!A \ident \lfalse

Conventional reading: formula A is syntactically identical to falsum

Meaning here: The formula denoted by A is the falsum formula; this is the special case used in the compactness argument.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 154, column 66

Expression 51

Inline MathML variant

M⊭¬A\Sat/{M}{\lnot !A}

Block MathML variant

M⊭¬A\Sat/{M}{\lnot !A}

Conventional reading: it is not the case that structure M satisfies not A

Meaning here: The outer negation applies to the entire satisfaction claim: structure M fails to satisfy the negated formula, not A.

1 occurrence
  1. Occurrence 1: soundness.tex, line 80, column 3

Expression 53

Inline MathML variant

B∈Γ!B \in \Gamma

Block MathML variant

B∈Γ!B \in \Gamma

Conventional reading: B is a member of Gamma

Meaning here: Sentence B belongs to the assumption set Gamma.

1 occurrence
  1. Occurrence 1: soundness.tex, line 190, column 42

Expression 54

Inline MathML variant

∃x(A(x)∧B(x))\lexists[x][(!A(x) \land !B(x)])

Block MathML variant

∃x(A(x)∧B(x))\lexists[x][(!A(x) \land !B(x)])

Conventional reading: there exists an x such that both A of x and B of x

Meaning here: The existential formula asserting that at least one object satisfies both A and B.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 127, column 9

Expression 55

Inline MathML variant

∃x¬A(x)→¬∀xA(x)\lexists[x][\lnot !A(x)] \lif \lnot \lforall[x][!A(x)]

Block MathML variant

∃x¬A(x)→¬∀xA(x)\lexists[x][\lnot !A(x)] \lif \lnot \lforall[x][!A(x)]

Conventional reading: if there exists an x such that not A of x, then it is not the case that, for every x, A of x

Meaning here: A conditional from the existence of a counterexample to A to the denial that every object satisfies A.

2 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 21, column 1
  2. Occurrence 2: proving-things-quant.tex, line 48, column 12

Expression 56

Inline MathML variant

∀x(B(x)→C(x,b))\lforall[x][(!B(x) \lif !C(x,b))]

Block MathML variant

∀x(B(x)→C(x,b))\lforall[x][(!B(x) \lif !C(x,b))]

Conventional reading: for every x, if B of x, then C of x and b

Meaning here: The universal conditional saying that every object satisfying B stands in relation C to b.

4 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 104, column 20
  2. Occurrence 2: proving-things-quant.tex, line 137, column 47
  3. Occurrence 3: proving-things-quant.tex, line 145, column 9
  4. Occurrence 4: proving-things-quant.tex, line 163, column 9

Expression 59

Inline MathML variant

¬A∨¬B⊢¬(A∧B)\lnot !A \lor \lnot !B \Proves \lnot(!A \land !B)

Block MathML variant

¬A∨¬B⊢¬(A∧B)\lnot !A \lor \lnot !B \Proves \lnot(!A \land !B)

Conventional reading: from the disjunction of not A with not B, derive not both A and B

Meaning here: The sequent asserts that the disjunction of not A and not B derives the negation of A and B.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 289, column 7

Expression 61

Inline MathML variant

[B]1\Discharge{!B}{1}

Block MathML variant

[B]1\Discharge{!B}{1}

Conventional reading: assumption B labeled one for discharge

Meaning here: An occurrence of assumption B marked with discharge label one.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 74, column 15

Expression 62

Inline MathML variant

[¬A]n\Discharge{\lnot !A}{n}

Block MathML variant

[¬A]n\Discharge{\lnot !A}{n}

Conventional reading: assumption not A, labeled n for discharge

Meaning here: An occurrence of the negated assumption not A marked with discharge label n.

1 occurrence
  1. Occurrence 1: propositional-rules.tex, line 104, column 9

Expression 64

Inline MathML variant

A→(B→C)⊢B→(A→C)!A \lif (!B \lif !C) \Proves !B \lif (!A \lif !C)

Block MathML variant

A→(B→C)⊢B→(A→C)!A \lif (!B \lif !C) \Proves !B \lif (!A \lif !C)

Conventional reading: from if A then if B then C, derive: if B then if A then C

Meaning here: The sequent asserting that the two antecedents of a nested conditional may be exchanged by natural deduction.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 272, column 7

Expression 65

Inline MathML variant

∃x¬A(x)→¬∀xA(x)\lexists[x][\lnot !A(x)]\lif \lnot \lforall[x][!A(x)]

Block MathML variant

∃x¬A(x)→¬∀xA(x)\lexists[x][\lnot !A(x)]\lif \lnot \lforall[x][!A(x)]

Conventional reading: if there exists an x such that not A of x, then it is not the case that, for every x, A of x

Meaning here: A conditional from the existence of a counterexample to A to the denial that every object satisfies A.

4 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 25, column 12
  2. Occurrence 2: proving-things-quant.tex, line 33, column 12
  3. Occurrence 3: proving-things-quant.tex, line 65, column 12
  4. Occurrence 4: proving-things-quant.tex, line 85, column 12

Expression 66

Inline MathML variant

A(t)⊢∃xA(x)!A(t) \Proves \lexists[x][!A(x)]

Block MathML variant

A(t)⊢∃xA(x)!A(t) \Proves \lexists[x][!A(x)]

Conventional reading: from A of t, derive that there exists an x such that A of x

Meaning here: Existential introduction yields the existential A statement from the instance A of the closed term t.

1 occurrence
  1. Occurrence 1: provability-quantifiers.tex, line 37, column 17

Expression 67

Inline MathML variant

==

Block MathML variant

==

Conventional reading: identity relation

Meaning here: The binary identity relation, used here when asking for symmetry and transitivity.

1 occurrence
  1. Occurrence 1: identity.tex, line 53, column 12

Expression 68

Inline MathML variant

∀xA(x)→∃yB(y)\lforall[x][!A(x)] \lif \lexists[y][!B(y)]

Block MathML variant

∀xA(x)→∃yB(y)\lforall[x][!A(x)] \lif \lexists[y][!B(y)]

Conventional reading: if, for every x, A of x, then there exists a y such that B of y

Meaning here: A conditional from the universal A statement to the existence of an object satisfying B.

4 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 185, column 48
  2. Occurrence 2: proving-things-quant.tex, line 203, column 14
  3. Occurrence 3: proving-things-quant.tex, line 206, column 9
  4. Occurrence 4: proving-things-quant.tex, line 219, column 9

Expression 69

Inline MathML variant

∃x∀y(A(y)→y=x),[A(a)∧A(b)]1\lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]] \quad \Discharge{!A(a) \land !A(b)}{1}

Block MathML variant

∃x∀y(A(y)→y=x),[A(a)∧A(b)]1\lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]] \quad \Discharge{!A(a) \land !A(b)}{1}

Conventional reading: the existential statement that there exists an x such that every A object equals x, together with the single conjunctive assumption that A holds of both a and b, carrying label one for discharge

Meaning here: A proof-tree line combines the existential uniqueness premise with a conjunctive assumption about a and b carrying discharge label one.

1 occurrence
  1. Occurrence 1: identity.tex, line 68, column 9

Expression 70

Inline MathML variant

[A(a)∧A(b)]1\Discharge{!A(a) \land !A(b)}{1}

Block MathML variant

[A(a)∧A(b)]1\Discharge{!A(a) \land !A(b)}{1}

Conventional reading: the single assumption that is the conjunction of A of a with A of b, labeled one for discharge

Meaning here: The conjunctive assumption that both a and b satisfy A, marked with discharge label one.

2 occurrences
  1. Occurrence 1: identity.tex, line 85, column 12
  2. Occurrence 2: identity.tex, line 104, column 9

Expression 71

Inline MathML variant

D→(C∧D)!D \lif (!C \land !D)

Block MathML variant

D→(C∧D)!D \lif (!C \land !D)

Conventional reading: if D, then C and D

Meaning here: The conditional with antecedent D and consequent the conjunction of C and D.

1 occurrence
  1. Occurrence 1: derivations.tex, line 93, column 12

Expression 72

Inline MathML variant

P(t,x)\Atom{\Obj P}{t,x}

Block MathML variant

P(t,x)\Atom{\Obj P}{t,x}

Conventional reading: P of t and x

Meaning here: The atomic formula with predicate P and ordered arguments t and x.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 74, column 4

Expression 73

Inline MathML variant

[¬(A∨¬A)]1\Discharge{\lnot(!A \lor \lnot !A)}{1}

Block MathML variant

[¬(A∨¬A)]1\Discharge{\lnot(!A \lor \lnot !A)}{1}

Conventional reading: assumption denying the whole disjunction A or not A, labeled one for discharge

Meaning here: An occurrence of the assumption denying the entire excluded-middle formula A or not A, marked with discharge label one.

8 occurrences
  1. Occurrence 1: proving-things.tex, line 191, column 11
  2. Occurrence 2: proving-things.tex, line 200, column 11
  3. Occurrence 3: proving-things.tex, line 202, column 11
  4. Occurrence 4: proving-things.tex, line 216, column 11
  5. Occurrence 5: proving-things.tex, line 227, column 11
  6. Occurrence 6: proving-things.tex, line 235, column 11
  7. Occurrence 7: proving-things.tex, line 244, column 11
  8. Occurrence 8: proving-things.tex, line 252, column 11

Expression 74

Inline MathML variant

Γ⊬⊥\Gamma \Proves/ \lfalse

Block MathML variant

Γ⊬⊥\Gamma \Proves/ \lfalse

Conventional reading: Gamma does not syntactically derive a contradiction

Meaning here: There is no natural-deduction derivation of falsum from undischarged assumptions in Gamma; this expresses consistency of Gamma.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 50, column 1

Expression 77

Inline MathML variant

A⊢¬¬A!A \Proves \lnot\lnot !A

Block MathML variant

A⊢¬¬A!A \Proves \lnot\lnot !A

Conventional reading: from A, derive not not A

Meaning here: The sequent asserting double-negation introduction: A has a derivation of not not A.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 273, column 7

Expression 78

Inline MathML variant

Γ={A1,A2,…,Ak}\Gamma = \{!A_1, !A_2, \ldots, !A_k\}

Block MathML variant

Γ={A1,A2,…,Ak}\Gamma = \{!A_1, !A_2, \ldots, !A_k\}

Conventional reading: Gamma equals the finite set containing A sub one, A sub two, through A sub k

Meaning here: Gamma is being presented as the finite set of formulas A sub one through A sub k.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 103, column 6

Expression 79

Inline MathML variant

M\Struct{M}

Block MathML variant

M\Struct{M}

Conventional reading: structure M

Meaning here: The first-order structure M.

15 occurrences
  1. Occurrence 1: soundness.tex, line 48, column 27
  2. Occurrence 2: soundness.tex, line 76, column 30
  3. Occurrence 3: soundness.tex, line 98, column 30
  4. Occurrence 4: soundness.tex, line 121, column 30
  5. Occurrence 5: soundness.tex, line 142, column 30
  6. Occurrence 6: soundness.tex, line 146, column 29
  7. Occurrence 7: soundness.tex, line 165, column 8
  8. Occurrence 8: soundness.tex, line 185, column 14
  9. Occurrence 9: soundness.tex, line 192, column 3
  10. Occurrence 10: soundness.tex, line 234, column 30
  11. Occurrence 11: soundness.tex, line 260, column 30
  12. Occurrence 12: soundness.tex, line 306, column 27
  13. Occurrence 13: soundness.tex, line 309, column 27
  14. Occurrence 14: soundness.tex, line 310, column 16
  15. Occurrence 15: soundness-identity.tex, line 38, column 25

Expression 81

Inline MathML variant

M⊭A\Sat/{M}{!A}

Block MathML variant

M⊭A\Sat/{M}{!A}

Conventional reading: structure M does not satisfy A

Meaning here: Structure M fails to satisfy formula A.

1 occurrence
  1. Occurrence 1: soundness.tex, line 167, column 5

Expression 83

Inline MathML variant

n^n

Block MathML variant

n^n

Conventional reading: discharge label n

Meaning here: The superscript n labels the adjacent bracketed assumption A of a for discharge by existential elimination.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 45, column 25

Expression 85

Inline MathML variant

[∀xA(x)]3\Discharge{\lforall[x][!A(x)]}{3}

Block MathML variant

[∀xA(x)]3\Discharge{\lforall[x][!A(x)]}{3}

Conventional reading: assumption: for every x, A of x; labeled three for discharge

Meaning here: The universal assumption that every object satisfies A, marked with discharge label three.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 75, column 9

Expression 87

Inline MathML variant

[¬A(a)]2,[∀xA(x)]3\Discharge{\lnot !A(a)}{2}, \Discharge{\lforall[x][!A(x)]}{3}

Block MathML variant

[¬A(a)]2,[∀xA(x)]3\Discharge{\lnot !A(a)}{2}, \Discharge{\lforall[x][!A(x)]}{3}

Conventional reading: assumptions not A of a labeled two, and for every x, A of x labeled three, for discharge

Meaning here: Two active assumptions: not A of a carries discharge label two, while the universal A statement carries label three.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 58, column 9

Expression 88

Inline MathML variant

∀x(A(x)→B)⊢∃yA(y)→B\lforall[x][(!A(x) \lif !B)] \Proves \lexists[y][!A(y)] \lif !B

Block MathML variant

∀x(A(x)→B)⊢∃yA(y)→B\lforall[x][(!A(x) \lif !B)] \Proves \lexists[y][!A(y)] \lif !B

Conventional reading: from: for every x, if A of x then B; derive: if there exists a y such that A of y, then B

Meaning here: The universal family of conditionals from A to B derives a conditional from the existence of an A-object to B.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 237, column 7

Expression 89

Inline MathML variant

A(s),s=t⊢A(t)!A(s), \eq[s][t] \Proves !A(t)

Block MathML variant

A(s),s=t⊢A(t)!A(s), \eq[s][t] \Proves !A(t)

Conventional reading: from A of s, together with s equals t, derive A of t

Meaning here: Leibniz's law in sequent form: an identical term may be substituted within formula A.

1 occurrence
  1. Occurrence 1: identity.tex, line 41, column 39

Expression 91

Inline MathML variant

aM′=s(x)\Assign{a}{M'} = s(x)

Block MathML variant

aM′=s(x)\Assign{a}{M'} = s(x)

Conventional reading: the interpretation of a in structure M prime equals the object assigned to x by s

Meaning here: In M prime, the name a denotes the same object that assignment s assigns to variable x.

1 occurrence
  1. Occurrence 1: soundness.tex, line 192, column 28

Expression 92

Inline MathML variant

Γ\Gamma

Block MathML variant

Γ\Gamma

Conventional reading: Gamma

Meaning here: Gamma is the set of undischarged assumptions.

52 occurrences
  1. Occurrence 1: derivations.tex, line 25, column 13
  2. Occurrence 2: derivations.tex, line 28, column 59
  3. Occurrence 3: derivations.tex, line 37, column 5
  4. Occurrence 4: derivations.tex, line 39, column 33
  5. Occurrence 5: derivations.tex, line 40, column 27
  6. Occurrence 6: proof-theoretic-notions.tex, line 41, column 15
  7. Occurrence 7: proof-theoretic-notions.tex, line 43, column 35
  8. Occurrence 8: proof-theoretic-notions.tex, line 44, column 20
  9. Occurrence 9: proof-theoretic-notions.tex, line 48, column 24
  10. Occurrence 10: proof-theoretic-notions.tex, line 49, column 23
  11. Occurrence 11: proof-theoretic-notions.tex, line 60, column 48
  12. Occurrence 12: proof-theoretic-notions.tex, line 71, column 33
  13. Occurrence 13: proof-theoretic-notions.tex, line 83, column 42
  14. Occurrence 14: proof-theoretic-notions.tex, line 93, column 11
  15. Occurrence 15: proof-theoretic-notions.tex, line 114, column 13
  16. Occurrence 16: proof-theoretic-notions.tex, line 141, column 35
  17. Occurrence 17: proof-theoretic-notions.tex, line 142, column 22
  18. Occurrence 18: proof-theoretic-notions.tex, line 149, column 45
  19. Occurrence 19: provability-consistency.tex, line 21, column 8
  20. Occurrence 20: provability-consistency.tex, line 25, column 37
  21. Occurrence 21: provability-consistency.tex, line 34, column 9
  22. Occurrence 22: provability-consistency.tex, line 41, column 22
  23. Occurrence 23: provability-consistency.tex, line 52, column 13
  24. Occurrence 24: provability-consistency.tex, line 56, column 11
  25. Occurrence 25: provability-consistency.tex, line 66, column 30
  26. Occurrence 26: provability-consistency.tex, line 83, column 58
  27. Occurrence 27: provability-consistency.tex, line 89, column 44
  28. Occurrence 28: provability-consistency.tex, line 93, column 13
  29. Occurrence 29: provability-consistency.tex, line 100, column 6
  30. Occurrence 30: provability-consistency.tex, line 105, column 22
  31. Occurrence 31: provability-consistency.tex, line 127, column 35
  32. Occurrence 32: provability-consistency.tex, line 127, column 57
  33. Occurrence 33: provability-quantifiers.tex, line 23, column 4
  34. Occurrence 34: provability-quantifiers.tex, line 28, column 49
  35. Occurrence 35: provability-quantifiers.tex, line 30, column 51
  36. Occurrence 36: soundness.tex, line 36, column 1
  37. Occurrence 37: soundness.tex, line 90, column 13
  38. Occurrence 38: soundness.tex, line 97, column 32
  39. Occurrence 39: soundness.tex, line 113, column 13
  40. Occurrence 40: soundness.tex, line 120, column 15
  41. Occurrence 41: soundness.tex, line 143, column 53
  42. Occurrence 42: soundness.tex, line 157, column 13
  43. Occurrence 43: soundness.tex, line 177, column 13
  44. Occurrence 44: soundness.tex, line 184, column 15
  45. Occurrence 45: soundness.tex, line 189, column 45
  46. Occurrence 46: soundness.tex, line 193, column 16
  47. Occurrence 47: soundness.tex, line 298, column 4
  48. Occurrence 48: soundness.tex, line 302, column 44
  49. Occurrence 49: soundness.tex, line 304, column 48
  50. Occurrence 50: soundness.tex, line 307, column 16
  51. Occurrence 51: soundness.tex, line 310, column 57
  52. Occurrence 52: soundness.tex, line 311, column 7

Expression 94

Inline MathML variant

C⊢D→(C∧D)!C \Proves !D \lif (!C \land !D)

Block MathML variant

C⊢D→(C∧D)!C \Proves !D \lif (!C \land !D)

Conventional reading: from C, one can derive: if D, then C and D

Meaning here: There is a natural-deduction derivation of the conditional from D to C and D using C as its only possible undischarged assumption.

1 occurrence
  1. Occurrence 1: derivations.tex, line 96, column 1

Expression 95

Inline MathML variant

⊢(A→B)∨(B→C)\Proves (!A \lif !B) \lor (!B \lif !C)

Block MathML variant

⊢(A→B)∨(B→C)\Proves (!A \lif !B) \lor (!B \lif !C)

Conventional reading: without undischarged assumptions, derive either if A then B or if B then C

Meaning here: The displayed disjunction of conditionals has a classical natural-deduction derivation with no undischarged assumptions.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 305, column 7

Expression 96

Inline MathML variant

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

Block MathML variant

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

Conventional reading: for every x, every y, and every z, if x equals y and y equals z, then x equals z

Meaning here: The universally quantified transitivity principle for identity.

1 occurrence
  1. Occurrence 1: identity.tex, line 55, column 23

Expression 97

Inline MathML variant

Γ1∪Γ2⊨A∧B\Gamma_1 \cup \Gamma_2 \Entails !A \land !B

Block MathML variant

Γ1∪Γ2⊨A∧B\Gamma_1 \cup \Gamma_2 \Entails !A \land !B

Conventional reading: the combined assumptions Gamma one and Gamma two semantically entail A and B

Meaning here: Every structure satisfying both assumption sets satisfies the conjunction of A and B.

1 occurrence
  1. Occurrence 1: soundness.tex, line 232, column 38

Expression 98

Inline MathML variant

t2t_2

Block MathML variant

t2t_2

Conventional reading: term t two

Meaning here: The second of two closed terms used in the identity-elimination rule.

1 occurrence
  1. Occurrence 1: identity.tex, line 36, column 37

Expression 99

Inline MathML variant

[B]n\Discharge{!B}{n}

Block MathML variant

[B]n\Discharge{!B}{n}

Conventional reading: assumption B, labeled n for discharge

Meaning here: An occurrence of assumption B marked with discharge label n; an inference bearing n may discharge it.

1 occurrence
  1. Occurrence 1: propositional-rules.tex, line 56, column 9

Expression 100

Inline MathML variant

Γ⊆Δ\Gamma \subseteq \Delta

Block MathML variant

Γ⊆Δ\Gamma \subseteq \Delta

Conventional reading: Gamma is a subset of capital Delta

Meaning here: Every formula in assumption set Gamma also belongs to assumption set Delta.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 66, column 4

Expression 101

Inline MathML variant

P(t,t)\Atom{\Obj P}{t,t}

Block MathML variant

P(t,t)\Atom{\Obj P}{t,t}

Conventional reading: P of t and t

Meaning here: The atomic formula with term t in both argument positions.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 75, column 16

Expression 102

Inline MathML variant

M′,s⊨A(a)\Sat{M'}{!A(a)}[s]

Block MathML variant

M′,s⊨A(a)\Sat{M'}{!A(a)}[s]

Conventional reading: structure M prime satisfies A of a under assignment s

Meaning here: Formula A of a is satisfied in structure M prime under assignment s.

1 occurrence
  1. Occurrence 1: soundness.tex, line 196, column 3

Expression 106

Inline MathML variant

Δ,[A]1\Delta, \Discharge{!A}{1}

Block MathML variant

Δ,[A]1\Delta, \Discharge{!A}{1}

Conventional reading: capital Delta together with assumption A, labeled one for discharge

Meaning here: The open assumptions in Delta together with an occurrence of assumption A carrying discharge label one.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 88, column 11

Expression 107

Inline MathML variant

Γ⊢¬A\Gamma \Proves \lnot {!A}

Block MathML variant

Γ⊢¬A\Gamma \Proves \lnot {!A}

Conventional reading: Gamma syntactically derives not A

Meaning here: The negation of A is derivable from the assumption set Gamma.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 116, column 43

Expression 109

Inline MathML variant

A(a)→a=c!A(a) \lif \eq[a][c]

Block MathML variant

A(a)→a=c!A(a) \lif \eq[a][c]

Conventional reading: if A of a, then a equals c

Meaning here: A conditional instance of the assumption that every A-object is identical to c.

1 occurrence
  1. Occurrence 1: identity.tex, line 103, column 12

Expression 111

Inline MathML variant

Γ⊢¬A\Gamma \Proves \lnot !A

Block MathML variant

Γ⊢¬A\Gamma \Proves \lnot !A

Conventional reading: Gamma syntactically derives not A

Meaning here: The negation of A is derivable from the assumption set Gamma.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 78, column 12

Expression 113

Inline MathML variant

Γ⊨⊥\Gamma \Entails \lfalse

Block MathML variant

Γ⊨⊥\Gamma \Entails \lfalse

Conventional reading: Gamma semantically entails a contradiction

Meaning here: Every structure satisfying Gamma would have to satisfy falsum.

1 occurrence
  1. Occurrence 1: soundness.tex, line 163, column 28

Expression 116

Inline MathML variant

∀xA(x)\lforall[x][!A(x)]

Block MathML variant

∀xA(x)\lforall[x][!A(x)]

Conventional reading: for every x, A of x

Meaning here: For every object x, formula A holds of x.

10 occurrences
  1. Occurrence 1: quantifier-rules.tex, line 29, column 25
  2. Occurrence 2: quantifier-rules.tex, line 99, column 14
  3. Occurrence 3: quantifier-rules.tex, line 101, column 15
  4. Occurrence 4: proving-things-quant.tex, line 52, column 16
  5. Occurrence 5: proving-things-quant.tex, line 204, column 6
  6. Occurrence 6: provability-quantifiers.tex, line 30, column 1
  7. Occurrence 7: provability-quantifiers.tex, line 54, column 8
  8. Occurrence 8: provability-quantifiers.tex, line 56, column 9
  9. Occurrence 9: soundness.tex, line 181, column 16
  10. Occurrence 10: soundness.tex, line 186, column 50

Expression 117

Inline MathML variant

(A∧B)→C⊢(A→C)∨(B→C)(!A \land !B) \lif !C \Proves (!A \lif !C) \lor (!B \lif !C)

Block MathML variant

(A∧B)→C⊢(A→C)∨(B→C)(!A \land !B) \lif !C \Proves (!A \lif !C) \lor (!B \lif !C)

Conventional reading: from if A and B then C, derive either if A then C or if B then C

Meaning here: The classical sequent derives a disjunction of two conditionals from the conditional whose antecedent is A and B.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 303, column 7

Expression 119

Inline MathML variant

A→C⊢¬(A∧¬C)!A \lif !C \Proves \lnot (!A \land \lnot !C)

Block MathML variant

A→C⊢¬(A∧¬C)!A \lif !C \Proves \lnot (!A \land \lnot !C)

Conventional reading: from if A then C, derive not both A and not C

Meaning here: The sequent asserts that the conditional from A to C derives the negation of the conjunction A and not C.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 286, column 7

Expression 120

Inline MathML variant

A1,…,An⊢B!A_1, \dots, !A_n \Proves !B

Block MathML variant

A1,…,An⊢B!A_1, \dots, !A_n \Proves !B

Conventional reading: from A sub one through A sub n, derive B

Meaning here: B is derivable in natural deduction from the finite list of formulas A sub one through A sub n.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 106, column 64

Expression 122

Inline MathML variant

∀y((A(a)∧A(y))→a=y)\lforall[y][((!A(a) \land !A(y)) \lif \eq[a][y])]

Block MathML variant

∀y((A(a)∧A(y))→a=y)\lforall[y][((!A(a) \land !A(y)) \lif \eq[a][y])]

Conventional reading: for every y, if both A of a and A of y, then a equals y

Meaning here: A universally quantified uniqueness statement relative to the fixed constant a.

2 occurrences
  1. Occurrence 1: identity.tex, line 74, column 12
  2. Occurrence 2: identity.tex, line 92, column 12

Expression 123

Inline MathML variant

¬(A→B)⊢A\lnot(!A \lif !B) \Proves !A

Block MathML variant

¬(A→B)⊢A\lnot(!A \lif !B) \Proves !A

Conventional reading: from the negation of if A then B, derive A

Meaning here: The sequent asserts that denying the conditional from A to B yields a natural-deduction derivation of A.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 298, column 7

Expression 124

Inline MathML variant

B⊢A→B!B \Proves !A \lif !B

Block MathML variant

B⊢A→B!B \Proves !A \lif !B

Conventional reading: from B, derive: if A then B

Meaning here: B derives the conditional from A to B; conditional introduction need not discharge an occurrence of A.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 99, column 44

Expression 125

Inline MathML variant

D∧C!D \land !C

Block MathML variant

D∧C!D \land !C

Conventional reading: D and C

Meaning here: The conjunction of formulas D and C, in that order.

1 occurrence
  1. Occurrence 1: derivations.tex, line 72, column 13

Expression 126

Inline MathML variant

∀x∀y((x=y∧A(x))→A(y))\lforall[x][\lforall[y][((\eq[x][y] \land !A(x)) \lif !A(y))]]

Block MathML variant

∀x∀y((x=y∧A(x))→A(y))\lforall[x][\lforall[y][((\eq[x][y] \land !A(x)) \lif !A(y))]]

Conventional reading: for every x and every y, if x equals y and A of x, then A of y

Meaning here: The universal substitutability principle saying that identity preserves satisfaction of A.

1 occurrence
  1. Occurrence 1: identity.tex, line 117, column 7

Expression 127

Inline MathML variant

A∨B,¬A,¬B!A \lor !B, \lnot !A, \lnot !B

Block MathML variant

A∨B,¬A,¬B!A \lor !B, \lnot !A, \lnot !B

Conventional reading: the set of three assumptions: first, the disjunction A or B; second, not A; and third, not B

Meaning here: The three-formula assumption set consisting of A or B, not A, and not B; the surrounding proposition states that it is inconsistent.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 59, column 9

Expression 128

Inline MathML variant

[¬A]3\Discharge{\lnot !A}{3}

Block MathML variant

[¬A]3\Discharge{\lnot !A}{3}

Conventional reading: assumption not A, labeled three for discharge

Meaning here: An occurrence of assumption not A marked with discharge label three.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 253, column 11

Expression 129

Inline MathML variant

[∀y(A(y)→y=c)]2\Discharge{\lforall[y][(!A(y) \lif \eq[y][c]])}{2}

Block MathML variant

[∀y(A(y)→y=c)]2\Discharge{\lforall[y][(!A(y) \lif \eq[y][c]])}{2}

Conventional reading: assumption: for every y, if A of y then y equals c; labeled two for discharge

Meaning here: The universal assumption that every A-object is identical to c, marked with discharge label two.

2 occurrences
  1. Occurrence 1: identity.tex, line 83, column 9
  2. Occurrence 2: identity.tex, line 101, column 9

Expression 133

Inline MathML variant

A!A

Block MathML variant

A!A

Conventional reading: formula A

Meaning here: The metavariable A denotes an arbitrary formula.

90 occurrences
  1. Occurrence 1: propositional-rules.tex, line 19, column 9
  2. Occurrence 2: propositional-rules.tex, line 28, column 12
  3. Occurrence 3: propositional-rules.tex, line 42, column 9
  4. Occurrence 4: propositional-rules.tex, line 73, column 9
  5. Occurrence 5: propositional-rules.tex, line 90, column 9
  6. Occurrence 6: propositional-rules.tex, line 101, column 12
  7. Occurrence 7: propositional-rules.tex, line 107, column 12
  8. Occurrence 8: propositional-rules.tex, line 113, column 64
  9. Occurrence 9: propositional-rules.tex, line 118, column 6
  10. Occurrence 10: quantifier-rules.tex, line 64, column 33
  11. Occurrence 11: quantifier-rules.tex, line 73, column 36
  12. Occurrence 12: quantifier-rules.tex, line 73, column 48
  13. Occurrence 13: quantifier-rules.tex, line 80, column 19
  14. Occurrence 14: derivations.tex, line 24, column 61
  15. Occurrence 15: derivations.tex, line 30, column 50
  16. Occurrence 16: derivations.tex, line 31, column 58
  17. Occurrence 17: derivations.tex, line 36, column 18
  18. Occurrence 18: derivations.tex, line 39, column 23
  19. Occurrence 19: derivations.tex, line 39, column 62
  20. Occurrence 20: derivations.tex, line 41, column 37
  21. Occurrence 21: derivations.tex, line 46, column 59
  22. Occurrence 22: derivations.tex, line 51, column 9
  23. Occurrence 23: derivations.tex, line 56, column 57
  24. Occurrence 24: derivations.tex, line 66, column 45
  25. Occurrence 25: derivations.tex, line 102, column 31
  26. Occurrence 26: proving-things.tex, line 34, column 10
  27. Occurrence 27: proving-things.tex, line 39, column 71
  28. Occurrence 28: proving-things.tex, line 45, column 12
  29. Occurrence 29: proving-things.tex, line 117, column 45
  30. Occurrence 30: proving-things.tex, line 118, column 6
  31. Occurrence 31: proving-things.tex, line 119, column 9
  32. Occurrence 32: proving-things.tex, line 152, column 58
  33. Occurrence 33: proving-things.tex, line 155, column 53
  34. Occurrence 34: proving-things.tex, line 188, column 33
  35. Occurrence 35: proving-things.tex, line 203, column 12
  36. Occurrence 36: proving-things.tex, line 217, column 12
  37. Occurrence 37: proving-things.tex, line 225, column 33
  38. Occurrence 38: proving-things.tex, line 236, column 12
  39. Occurrence 39: proving-things.tex, line 242, column 59
  40. Occurrence 40: proving-things.tex, line 259, column 14
  41. Occurrence 41: proof-theoretic-notions.tex, line 33, column 16
  42. Occurrence 42: proof-theoretic-notions.tex, line 34, column 4
  43. Occurrence 43: proof-theoretic-notions.tex, line 35, column 43
  44. Occurrence 44: proof-theoretic-notions.tex, line 40, column 16
  45. Occurrence 45: proof-theoretic-notions.tex, line 42, column 32
  46. Occurrence 46: proof-theoretic-notions.tex, line 43, column 48
  47. Occurrence 47: proof-theoretic-notions.tex, line 59, column 16
  48. Occurrence 48: proof-theoretic-notions.tex, line 59, column 53
  49. Occurrence 49: proof-theoretic-notions.tex, line 60, column 36
  50. Occurrence 50: proof-theoretic-notions.tex, line 71, column 23
  51. Occurrence 51: proof-theoretic-notions.tex, line 72, column 1
  52. Occurrence 52: proof-theoretic-notions.tex, line 82, column 64
  53. Occurrence 53: proof-theoretic-notions.tex, line 95, column 12
  54. Occurrence 54: proof-theoretic-notions.tex, line 149, column 35
  55. Occurrence 55: proof-theoretic-notions.tex, line 153, column 10
  56. Occurrence 56: provability-consistency.tex, line 25, column 27
  57. Occurrence 57: provability-consistency.tex, line 36, column 10
  58. Occurrence 58: provability-consistency.tex, line 40, column 43
  59. Occurrence 59: provability-consistency.tex, line 51, column 31
  60. Occurrence 60: provability-consistency.tex, line 58, column 12
  61. Occurrence 61: provability-consistency.tex, line 66, column 20
  62. Occurrence 62: provability-consistency.tex, line 73, column 14
  63. Occurrence 63: provability-consistency.tex, line 89, column 34
  64. Occurrence 64: provability-consistency.tex, line 95, column 14
  65. Occurrence 65: provability-consistency.tex, line 126, column 23
  66. Occurrence 66: provability-propositional.tex, line 40, column 18
  67. Occurrence 67: provability-propositional.tex, line 48, column 15
  68. Occurrence 68: provability-propositional.tex, line 84, column 15
  69. Occurrence 69: provability-propositional.tex, line 108, column 15
  70. Occurrence 70: provability-propositional.tex, line 129, column 16
  71. Occurrence 71: soundness.tex, line 35, column 4
  72. Occurrence 72: soundness.tex, line 40, column 36
  73. Occurrence 73: soundness.tex, line 45, column 14
  74. Occurrence 74: soundness.tex, line 50, column 16
  75. Occurrence 75: soundness.tex, line 58, column 21
  76. Occurrence 76: soundness.tex, line 86, column 67
  77. Occurrence 77: soundness.tex, line 94, column 16
  78. Occurrence 78: soundness.tex, line 110, column 45
  79. Occurrence 79: soundness.tex, line 115, column 14
  80. Occurrence 80: soundness.tex, line 119, column 28
  81. Occurrence 81: soundness.tex, line 131, column 35
  82. Occurrence 82: soundness.tex, line 144, column 3
  83. Occurrence 83: soundness.tex, line 161, column 16
  84. Occurrence 84: soundness.tex, line 217, column 21
  85. Occurrence 85: soundness.tex, line 221, column 14
  86. Occurrence 86: soundness.tex, line 228, column 28
  87. Occurrence 87: soundness.tex, line 245, column 29
  88. Occurrence 88: soundness.tex, line 252, column 14
  89. Occurrence 89: soundness.tex, line 257, column 61
  90. Occurrence 90: soundness.tex, line 293, column 23

Expression 134

Inline MathML variant

[A]n\Discharge{!A}{n}

Block MathML variant

[A]n\Discharge{!A}{n}

Conventional reading: assumption A, labeled n for discharge

Meaning here: An occurrence of assumption A marked with discharge label n; an inference bearing n may discharge it.

4 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 43, column 42
  2. Occurrence 2: propositional-rules.tex, line 54, column 9
  3. Occurrence 3: propositional-rules.tex, line 66, column 9
  4. Occurrence 4: propositional-rules.tex, line 82, column 9

Expression 135

Inline MathML variant

B⊢A∨B!B \Proves !A \lor !B

Block MathML variant

B⊢A∨B!B \Proves !A \lor !B

Conventional reading: from B, derive A or B

Meaning here: B derives the disjunction A or B by disjunction introduction.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 60, column 42

Expression 136

Inline MathML variant

M⊨A(t2)\Sat{M}{!A(t_2)}

Block MathML variant

M⊨A(t2)\Sat{M}{!A(t_2)}

Conventional reading: structure M satisfies A of t two

Meaning here: Structure M satisfies formula A applied to closed term t two.

1 occurrence
  1. Occurrence 1: soundness-identity.tex, line 44, column 29

Expression 137

Inline MathML variant

s=t\eq[s][t]

Block MathML variant

s=t\eq[s][t]

Conventional reading: s equals t

Meaning here: An identity statement asserting that the closed terms s and t have the same denotation.

1 occurrence
  1. Occurrence 1: identity.tex, line 43, column 9

Expression 138

Inline MathML variant

M,s[m/x]⊨A(x)\Sat{M}{!A(x)}[\Subst{s}{m}{x}]

Block MathML variant

M,s[m/x]⊨A(x)\Sat{M}{!A(x)}[\Subst{s}{m}{x}]

Conventional reading: structure M satisfies A of x under the assignment obtained from s by assigning m to x

Meaning here: Formula A of x is satisfied in structure M under the assignment that agrees with s except that x receives object m.

1 occurrence
  1. Occurrence 1: soundness-identity.tex, line 43, column 1

Expression 139

Inline MathML variant

Γ,[¬A]2\Gamma, \Discharge{\lnot !A}{2}

Block MathML variant

Γ,[¬A]2\Gamma, \Discharge{\lnot !A}{2}

Conventional reading: the assumptions in Gamma, together with assumption not A labeled two for discharge

Meaning here: A proof context containing Gamma and an occurrence of assumption not A marked with discharge label two.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 113, column 9

Expression 140

Inline MathML variant

{A}∪Δ\{!A\} \cup \Delta

Block MathML variant

{A}∪Δ\{!A\} \cup \Delta

Conventional reading: assumption A together with capital Delta

Meaning here: The union of the singleton set containing formula A with the assumption set Delta.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 85, column 42

Expression 141

Inline MathML variant

B(a)→C(a,b)!B(a) \lif !C(a, b)

Block MathML variant

B(a)→C(a,b)!B(a) \lif !C(a, b)

Conventional reading: if B of a, then C of a and b

Meaning here: A conditional from B of a to the relational formula C of a and b.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 140, column 1

Expression 142

Inline MathML variant

(A→B)→A⊢A(!A \lif !B) \lif !A \Proves !A

Block MathML variant

(A→B)→A⊢A(!A \lif !B) \lif !A \Proves !A

Conventional reading: from the conditional whose antecedent is the conditional from A to B and whose consequent is A, derive A

Meaning here: The sequent is the natural-deduction form of Peirce-style classical reasoning: the displayed premise derives A.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 304, column 7

Expression 143

Inline MathML variant

Γ⊢Ai\Gamma \Proves !A_i

Block MathML variant

Γ⊢Ai\Gamma \Proves !A_i

Conventional reading: Gamma syntactically derives A sub i

Meaning here: The indexed formula A sub i is derivable from the assumption set Gamma.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 107, column 29

Expression 147

Inline MathML variant

⊢¬∃x∀y(A(x,y)→¬A(y,y)∧¬A(y,y)→A(x,y))\Proves \lnot\lexists[x][\lforall[y][((!A(x,y) \lif \lnot !A(y,y)) \land (\lnot !A(y,y) \lif !A(x,y)))]]

Block MathML variant

⊢¬∃x∀y(A(x,y)→¬A(y,y)∧¬A(y,y)→A(x,y))\Proves \lnot\lexists[x][\lforall[y][((!A(x,y) \lif \lnot !A(y,y)) \land (\lnot !A(y,y) \lif !A(x,y)))]]

Conventional reading: without undischarged assumptions, derive that there is no x such that, for every y, both conditional directions hold: first, if A holds with x as its first argument and y as its second argument, then A does not hold with y as its first argument and y as its second argument; second, if A does not hold with y as its first argument and y as its second argument, then A holds with x as its first argument and y as its second argument

Meaning here: The derivable negation rules out an object x whose A-relation to every y is equivalent, in both conditional directions, to y not bearing relation A to itself.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 240, column 7

Expression 148

Inline MathML variant

⊢∃x(A(x)→∀yA(y))\Proves \lexists[x][(!A(x) \lif \lforall[y][!A(y)])]

Block MathML variant

⊢∃x(A(x)→∀yA(y))\Proves \lexists[x][(!A(x) \lif \lforall[y][!A(y)])]

Conventional reading: without undischarged assumptions, derive that there exists an x such that, if A of x, then every y is A

Meaning here: A classical theorem asserting the existence of an object whose satisfying A would imply that every object satisfies A.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 250, column 7

Expression 149

Inline MathML variant

M⊨Γ∪{A}\Sat{M}{\Gamma \cup \{!A\}}

Block MathML variant

M⊨Γ∪{A}\Sat{M}{\Gamma \cup \{!A\}}

Conventional reading: structure M satisfies Gamma together with assumption A

Meaning here: Structure M satisfies every member of Gamma and also formula A.

1 occurrence
  1. Occurrence 1: soundness.tex, line 82, column 3

Expression 150

Inline MathML variant

C!C

Block MathML variant

C!C

Conventional reading: formula C

Meaning here: The metavariable C denotes an arbitrary formula.

11 occurrences
  1. Occurrence 1: propositional-rules.tex, line 55, column 10
  2. Occurrence 2: propositional-rules.tex, line 57, column 10
  3. Occurrence 3: propositional-rules.tex, line 59, column 14
  4. Occurrence 4: quantifier-rules.tex, line 46, column 10
  5. Occurrence 5: quantifier-rules.tex, line 48, column 13
  6. Occurrence 6: quantifier-rules.tex, line 53, column 62
  7. Occurrence 7: derivations.tex, line 57, column 40
  8. Occurrence 8: derivations.tex, line 60, column 9
  9. Occurrence 9: derivations.tex, line 66, column 54
  10. Occurrence 10: derivations.tex, line 70, column 9
  11. Occurrence 11: derivations.tex, line 88, column 9

Expression 151

Inline MathML variant

Γ∪{¬A}\Gamma \cup \{ \lnot !A \}

Block MathML variant

Γ∪{¬A}\Gamma \cup \{ \lnot !A \}

Conventional reading: Gamma union the singleton set containing not A

Meaning here: The assumption set obtained by adding the negated formula not A to Gamma.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 110, column 45

Expression 152

Inline MathML variant

δ1\delta_1

Block MathML variant

δ1\delta_1

Conventional reading: delta one

Meaning here: The first subderivation, named delta one.

23 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 84, column 51
  2. Occurrence 2: proof-theoretic-notions.tex, line 89, column 15
  3. Occurrence 3: provability-consistency.tex, line 25, column 49
  4. Occurrence 4: provability-consistency.tex, line 35, column 13
  5. Occurrence 5: provability-consistency.tex, line 64, column 1
  6. Occurrence 6: provability-consistency.tex, line 69, column 15
  7. Occurrence 7: provability-consistency.tex, line 109, column 27
  8. Occurrence 8: provability-consistency.tex, line 119, column 13
  9. Occurrence 9: soundness.tex, line 69, column 17
  10. Occurrence 10: soundness.tex, line 75, column 39
  11. Occurrence 11: soundness.tex, line 91, column 17
  12. Occurrence 12: soundness.tex, line 97, column 44
  13. Occurrence 13: soundness.tex, line 114, column 17
  14. Occurrence 14: soundness.tex, line 120, column 27
  15. Occurrence 15: soundness.tex, line 134, column 17
  16. Occurrence 16: soundness.tex, line 140, column 18
  17. Occurrence 17: soundness.tex, line 158, column 17
  18. Occurrence 18: soundness.tex, line 178, column 17
  19. Occurrence 19: soundness.tex, line 220, column 17
  20. Occurrence 20: soundness.tex, line 229, column 29
  21. Occurrence 21: soundness.tex, line 248, column 17
  22. Occurrence 22: soundness.tex, line 257, column 46
  23. Occurrence 23: soundness-identity.tex, line 27, column 15

Expression 155

Inline MathML variant

M⊨Γ1∪Γ2\Sat{M}{\Gamma_1 \cup \Gamma_2}

Block MathML variant

M⊨Γ1∪Γ2\Sat{M}{\Gamma_1 \cup \Gamma_2}

Conventional reading: structure M satisfies every assumption in Gamma one and Gamma two

Meaning here: Structure M satisfies every member of both assumption sets.

4 occurrences
  1. Occurrence 1: soundness.tex, line 235, column 8
  2. Occurrence 2: soundness.tex, line 261, column 25
  3. Occurrence 3: soundness.tex, line 263, column 3
  4. Occurrence 4: soundness-identity.tex, line 38, column 43

Expression 156

Inline MathML variant

∃xA(x)⊭∀xA(x)\lexists[x][!A(x)] \Entails/ \lforall[x][!A(x)]

Block MathML variant

∃xA(x)⊭∀xA(x)\lexists[x][!A(x)] \Entails/ \lforall[x][!A(x)]

Conventional reading: the complete existential claim on the left, there exists an x such that A of x, does not semantically entail the complete universal claim on the right, for every x, A of x

Meaning here: The existential sentence does not semantically entail the corresponding universal sentence; a structure may contain an A without making every object an A.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 103, column 10

Expression 157

Inline MathML variant

Γ∪{¬A}\Gamma \cup \{\lnot !A\}

Block MathML variant

Γ∪{¬A}\Gamma \cup \{\lnot !A\}

Conventional reading: Gamma union the singleton set containing not A

Meaning here: The assumption set obtained by adding the negated formula not A to Gamma.

5 occurrences
  1. Occurrence 1: provability-consistency.tex, line 46, column 25
  2. Occurrence 2: provability-consistency.tex, line 53, column 1
  3. Occurrence 3: provability-consistency.tex, line 63, column 12
  4. Occurrence 4: provability-consistency.tex, line 65, column 33
  5. Occurrence 5: provability-consistency.tex, line 104, column 31

Expression 160

Inline MathML variant

B→A⊢¬A→¬B!B \lif !A \Proves \lnot !A \lif \lnot !B

Block MathML variant

B→A⊢¬A→¬B!B \lif !A \Proves \lnot !A \lif \lnot !B

Conventional reading: from if B then A, derive: if not A then not B

Meaning here: The sequent expresses contraposition from the conditional B to A to the conditional not A to not B.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 283, column 7

Expression 161

Inline MathML variant

Γ2⊨B\Gamma_2 \Entails !B

Block MathML variant

Γ2⊨B\Gamma_2 \Entails !B

Conventional reading: Gamma two semantically entails B

Meaning here: Every structure satisfying Gamma two satisfies B.

1 occurrence
  1. Occurrence 1: soundness.tex, line 239, column 46

Expression 162

Inline MathML variant

M⊨Γ1\Sat{M}{\Gamma_1}

Block MathML variant

M⊨Γ1\Sat{M}{\Gamma_1}

Conventional reading: structure M satisfies every assumption in Gamma one

Meaning here: Structure M satisfies the first assumption set.

1 occurrence
  1. Occurrence 1: soundness.tex, line 236, column 3

Expression 164

Inline MathML variant

∀xA(x)⊢A(t)\lforall[x][!A(x)] \Proves !A(t)

Block MathML variant

∀xA(x)⊢A(t)\lforall[x][!A(x)] \Proves !A(t)

Conventional reading: from: for every x, A of x; derive A of t

Meaning here: Universal elimination yields the instance A of the closed term t from the universal A statement.

1 occurrence
  1. Occurrence 1: provability-quantifiers.tex, line 39, column 18

Expression 166

Inline MathML variant

∃xA\lexists[x][!A]

Block MathML variant

∃xA\lexists[x][!A]

Conventional reading: there exists an x such that A

Meaning here: The formula formed by existentially quantifying variable x in A.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 71, column 12

Expression 167

Inline MathML variant

Γ⊨A(a)\Gamma \Entails !A(a)

Block MathML variant

Γ⊨A(a)\Gamma \Entails !A(a)

Conventional reading: Gamma semantically entails A of a

Meaning here: Every structure that satisfies Gamma also satisfies A of a.

1 occurrence
  1. Occurrence 1: soundness.tex, line 194, column 52

Expression 171

Inline MathML variant

D⊢C→(C∧D)!D \Proves !C \lif (!C \land !D)

Block MathML variant

D⊢C→(C∧D)!D \Proves !C \lif (!C \land !D)

Conventional reading: from D, one can derive: if C, then C and D

Meaning here: There is a natural-deduction derivation of the conditional from C to C and D using D as its only possible undischarged assumption.

1 occurrence
  1. Occurrence 1: derivations.tex, line 95, column 31

Expression 173

Inline MathML variant

[¬A∨B]1\Discharge{\lnot !A \lor !B}{1}

Block MathML variant

[¬A∨B]1\Discharge{\lnot !A \lor !B}{1}

Conventional reading: the single assumption that is the disjunction of not A with B, labeled one for discharge

Meaning here: An occurrence of the disjunctive assumption not A or B marked with discharge label one.

5 occurrences
  1. Occurrence 1: proving-things.tex, line 72, column 9
  2. Occurrence 2: proving-things.tex, line 87, column 9
  3. Occurrence 3: proving-things.tex, line 101, column 9
  4. Occurrence 4: proving-things.tex, line 130, column 9
  5. Occurrence 5: proving-things.tex, line 157, column 9

Expression 175

Inline MathML variant

Γ⊭⊥\Gamma \Entails/ \lfalse

Block MathML variant

Γ⊭⊥\Gamma \Entails/ \lfalse

Conventional reading: Gamma does not semantically entail a contradiction

Meaning here: It is not the case that every structure satisfying Gamma satisfies falsum.

1 occurrence
  1. Occurrence 1: soundness.tex, line 169, column 10

Expression 176

Inline MathML variant

M,s⊨A(t1)\Sat{M}{!A(t_1)}[s]

Block MathML variant

M,s⊨A(t1)\Sat{M}{!A(t_1)}[s]

Conventional reading: structure M satisfies A of t one under assignment s

Meaning here: Formula A of the closed term t one is satisfied in structure M under variable assignment s.

1 occurrence
  1. Occurrence 1: soundness-identity.tex, line 42, column 43

Expression 177

Inline MathML variant

¬∀xA(x)\lnot\lforall[x][!A(x)]

Block MathML variant

¬∀xA(x)\lnot\lforall[x][!A(x)]

Conventional reading: it is not the case that, for every x, A of x

Meaning here: The negation of the universal statement that every object satisfies A.

5 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 185, column 1
  2. Occurrence 2: proving-things-quant.tex, line 190, column 12
  3. Occurrence 3: proving-things-quant.tex, line 199, column 12
  4. Occurrence 4: proving-things-quant.tex, line 212, column 12
  5. Occurrence 5: proving-things-quant.tex, line 226, column 12

Expression 178

Inline MathML variant

M⊨Γ\Sat{M}{\Gamma}

Block MathML variant

M⊨Γ\Sat{M}{\Gamma}

Conventional reading: structure M satisfies every assumption in Gamma

Meaning here: Structure M satisfies every member of the assumption set Gamma.

9 occurrences
  1. Occurrence 1: soundness.tex, line 77, column 25
  2. Occurrence 2: soundness.tex, line 79, column 8
  3. Occurrence 3: soundness.tex, line 99, column 17
  4. Occurrence 4: soundness.tex, line 101, column 3
  5. Occurrence 5: soundness.tex, line 122, column 25
  6. Occurrence 6: soundness.tex, line 124, column 3
  7. Occurrence 7: soundness.tex, line 147, column 3
  8. Occurrence 8: soundness.tex, line 166, column 5
  9. Occurrence 9: soundness.tex, line 185, column 38

Expression 179

Inline MathML variant

⊢¬(A∨B)→(¬A∧¬B)\Proves \lnot(!A \lor !B) \lif (\lnot !A \land \lnot !B)

Block MathML variant

⊢¬(A∨B)→(¬A∧¬B)\Proves \lnot(!A \lor !B) \lif (\lnot !A \land \lnot !B)

Conventional reading: without undischarged assumptions, derive: if it is not the case that A or B, then both not A and not B

Meaning here: The converse De Morgan direction has a derivation without undischarged assumptions: the negation of A or B implies not A and not B.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 291, column 7

Expression 180

Inline MathML variant

A,B⊢A∧B!A, !B \Proves !A \land !B

Block MathML variant

A,B⊢A∧B!A, !B \Proves !A \land !B

Conventional reading: from A and B as separate assumptions, derive the conjunction A and B

Meaning here: The separate assumptions A and B jointly derive their conjunction.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 30, column 47

Expression 181

Inline MathML variant

A∨B!A \lor !B

Block MathML variant

A∨B!A \lor !B

Conventional reading: A or B

Meaning here: The disjunction of formulas A and B.

10 occurrences
  1. Occurrence 1: propositional-rules.tex, line 44, column 12
  2. Occurrence 2: propositional-rules.tex, line 49, column 12
  3. Occurrence 3: propositional-rules.tex, line 53, column 9
  4. Occurrence 4: provability-propositional.tex, line 68, column 15
  5. Occurrence 5: provability-propositional.tex, line 81, column 17
  6. Occurrence 6: provability-propositional.tex, line 86, column 18
  7. Occurrence 7: provability-propositional.tex, line 90, column 18
  8. Occurrence 8: soundness.tex, line 109, column 67
  9. Occurrence 9: soundness.tex, line 117, column 16
  10. Occurrence 10: soundness.tex, line 127, column 66

Expression 183

Inline MathML variant

[A(a)]1\Discharge{!A(a)}{1}

Block MathML variant

[A(a)]1\Discharge{!A(a)}{1}

Conventional reading: assumption A of a labeled one for discharge

Meaning here: An occurrence of assumption A of a marked with discharge label one in the invalid quantifier derivation.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 97, column 11

Expression 184

Inline MathML variant

[A(a)∧B(a)]1\Discharge{!A(a) \land !B(a)}{1}

Block MathML variant

[A(a)∧B(a)]1\Discharge{!A(a) \land !B(a)}{1}

Conventional reading: the single assumption that is the conjunction of A of a and B of a, labeled one for discharge

Meaning here: The conjunctive assumption that a satisfies both A and B, marked with discharge label one.

4 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 119, column 9
  2. Occurrence 2: proving-things-quant.tex, line 128, column 9
  3. Occurrence 3: proving-things-quant.tex, line 148, column 9
  4. Occurrence 4: proving-things-quant.tex, line 166, column 9

Expression 185

Inline MathML variant

Γ,[A]n\Gamma, \Discharge{!A}{n}

Block MathML variant

Γ,[A]n\Gamma, \Discharge{!A}{n}

Conventional reading: Gamma together with assumption A, labeled n for discharge

Meaning here: The open assumptions Gamma together with an occurrence of assumption A labeled n; the final negation-introduction inference discharges the assumption carrying that label.

2 occurrences
  1. Occurrence 1: soundness.tex, line 68, column 13
  2. Occurrence 2: soundness.tex, line 133, column 13

Expression 187

Inline MathML variant

∃Elim\Elim\lexists

Block MathML variant

∃Elim\Elim\lexists

Conventional reading: existential elimination rule

Meaning here: The natural-deduction rule that reasons from an existential premise through a subderivation using a fresh eigenconstant.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 79, column 22

Expression 189

Inline MathML variant

M′⊨Γ\Sat{M'}{\Gamma}

Block MathML variant

M′⊨Γ\Sat{M'}{\Gamma}

Conventional reading: structure M prime satisfies every assumption in Gamma

Meaning here: Structure M prime satisfies the assumption set Gamma.

1 occurrence
  1. Occurrence 1: soundness.tex, line 193, column 26

Expression 190

Inline MathML variant

A∨B,¬B⊢A!A \lor !B, \lnot !B \Proves !A

Block MathML variant

A∨B,¬B⊢A!A \lor !B, \lnot !B \Proves !A

Conventional reading: from A or B, together with not B, derive A

Meaning here: The sequent is disjunctive syllogism: A or B and not B derive A.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 288, column 7

Expression 192

Inline MathML variant

⊢¬(A∧¬A)\Proves \lnot(!A \land \lnot !A)

Block MathML variant

⊢¬(A∧¬A)\Proves \lnot(!A \land \lnot !A)

Conventional reading: without undischarged assumptions, derive not both A and not A

Meaning here: The law of noncontradiction has a natural-deduction derivation with no undischarged assumptions.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 282, column 7

Expression 195

Inline MathML variant

t1t_1

Block MathML variant

t1t_1

Conventional reading: term t one

Meaning here: The first of two closed terms used in the identity-elimination rule.

1 occurrence
  1. Occurrence 1: identity.tex, line 36, column 26

Expression 196

Inline MathML variant

A∧B!A \land !B

Block MathML variant

A∧B!A \land !B

Conventional reading: A and B

Meaning here: The conjunction of formulas A and B.

14 occurrences
  1. Occurrence 1: propositional-rules.tex, line 22, column 13
  2. Occurrence 2: propositional-rules.tex, line 26, column 9
  3. Occurrence 3: propositional-rules.tex, line 31, column 9
  4. Occurrence 4: derivations.tex, line 54, column 13
  5. Occurrence 5: proving-things.tex, line 39, column 54
  6. Occurrence 6: provability-propositional.tex, line 38, column 15
  7. Occurrence 7: provability-propositional.tex, line 42, column 15
  8. Occurrence 8: provability-propositional.tex, line 51, column 19
  9. Occurrence 9: soundness.tex, line 87, column 44
  10. Occurrence 10: soundness.tex, line 92, column 14
  11. Occurrence 11: soundness.tex, line 96, column 28
  12. Occurrence 12: soundness.tex, line 107, column 17
  13. Occurrence 13: soundness.tex, line 216, column 44
  14. Occurrence 14: soundness.tex, line 226, column 17

Expression 197

Inline MathML variant

M,s⊨B\Sat{M}{!B}[s]

Block MathML variant

M,s⊨B\Sat{M}{!B}[s]

Conventional reading: structure M satisfies B under assignment s

Meaning here: Sentence B is satisfied in structure M under assignment s.

1 occurrence
  1. Occurrence 1: soundness.tex, line 190, column 17

Expression 198

Inline MathML variant

⊢¬∀xA(x)→∃x¬A(x)\Proves \lnot\lforall[x][!A(x)] \lif \lexists[x][\lnot!A(x)]

Block MathML variant

⊢¬∀xA(x)→∃x¬A(x)\Proves \lnot\lforall[x][!A(x)] \lif \lexists[x][\lnot!A(x)]

Conventional reading: without undischarged assumptions, derive: if not every x is A, then there exists an x such that not A of x

Meaning here: The classical quantifier-negation conditional from denial of a universal claim to existence of a counterexample.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 248, column 7

Expression 199

Inline MathML variant

∀x∀y(x=y→y=x)\lforall[x][\lforall[y][(\eq[x][y] \lif \eq[y][x])]]

Block MathML variant

∀x∀y(x=y→y=x)\lforall[x][\lforall[y][(\eq[x][y] \lif \eq[y][x])]]

Conventional reading: for every x and every y, if x equals y, then y equals x

Meaning here: The universally quantified symmetry principle for identity.

1 occurrence
  1. Occurrence 1: identity.tex, line 54, column 20

Expression 202

Inline MathML variant

¬(A∧B)⊢¬A∨¬B\lnot(!A \land !B) \Proves \lnot !A \lor \lnot !B

Block MathML variant

¬(A∧B)⊢¬A∨¬B\lnot(!A \land !B) \Proves \lnot !A \lor \lnot !B

Conventional reading: from not both A and B, derive the disjunction of not A with not B

Meaning here: The classical De Morgan sequent asserts that the negation of A and B derives the disjunction not A or not B.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 299, column 7

Expression 203

Inline MathML variant

M⊨t1=t2\Sat{M}{\eq[t_1][t_2]}

Block MathML variant

M⊨t1=t2\Sat{M}{\eq[t_1][t_2]}

Conventional reading: structure M satisfies that t one equals t two

Meaning here: The closed terms t one and t two have the same value in structure M.

1 occurrence
  1. Occurrence 1: soundness-identity.tex, line 40, column 1

Expression 205

Inline MathML variant

A∨(B∨C)⊢(A∨B)∨C!A \lor (!B \lor !C) \Proves (!A \lor !B) \lor !C

Block MathML variant

A∨(B∨C)⊢(A∨B)∨C!A \lor (!B \lor !C) \Proves (!A \lor !B) \lor !C

Conventional reading: from the disjunction whose left disjunct is A and whose right disjunct is the disjunction B or C, derive the disjunction whose left disjunct is A or B and whose right disjunct is C

Meaning here: There is a derivation of the disjunction of A and B, disjoined with C, from the single assumption A disjoined with the disjunction of B and C.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 271, column 7

Expression 206

Inline MathML variant

⊬A\Proves/ !A

Block MathML variant

⊬A\Proves/ !A

Conventional reading: A is not derivable without undischarged assumptions

Meaning here: There is no natural-deduction derivation of A with all assumptions discharged.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 36, column 1

Expression 207

Inline MathML variant

¬A\lnot !A

Block MathML variant

¬A\lnot !A

Conventional reading: not A

Meaning here: The negation of formula A.

20 occurrences
  1. Occurrence 1: propositional-rules.tex, line 86, column 12
  2. Occurrence 2: propositional-rules.tex, line 89, column 9
  3. Occurrence 3: propositional-rules.tex, line 113, column 14
  4. Occurrence 4: proving-things.tex, line 117, column 30
  5. Occurrence 5: proving-things.tex, line 118, column 63
  6. Occurrence 6: proving-things.tex, line 188, column 41
  7. Occurrence 7: proving-things.tex, line 201, column 12
  8. Occurrence 8: proving-things.tex, line 209, column 45
  9. Occurrence 9: proving-things.tex, line 215, column 14
  10. Occurrence 10: proving-things.tex, line 234, column 14
  11. Occurrence 11: proving-things.tex, line 251, column 14
  12. Occurrence 12: provability-consistency.tex, line 33, column 12
  13. Occurrence 13: provability-consistency.tex, line 55, column 11
  14. Occurrence 14: provability-consistency.tex, line 92, column 13
  15. Occurrence 15: provability-consistency.tex, line 122, column 12
  16. Occurrence 16: provability-consistency.tex, line 126, column 32
  17. Occurrence 17: provability-propositional.tex, line 69, column 15
  18. Occurrence 18: provability-propositional.tex, line 81, column 31
  19. Occurrence 19: provability-propositional.tex, line 115, column 15
  20. Occurrence 20: soundness.tex, line 72, column 16

Expression 208

Inline MathML variant

⊢(∃xA(x)∨∃yB(y))→∃z(A(z)∨B(z))\Proves (\lexists[x][!A(x)] \lor \lexists[y][!B(y)]) \lif \lexists[z][(!A(z) \lor !B(z))]

Block MathML variant

⊢(∃xA(x)∨∃yB(y))→∃z(A(z)∨B(z))\Proves (\lexists[x][!A(x)] \lor \lexists[y][!B(y)]) \lif \lexists[z][(!A(z) \lor !B(z))]

Conventional reading: without undischarged assumptions, derive: if either some x is A or some y is B, then there exists a z that is A or B

Meaning here: A disjunction of existential claims implies an existential disjunction, and the conditional is derivable with no undischarged assumptions.

1 occurrence
  1. Occurrence 1: proving-things-quant.tex, line 235, column 7

Expression 209

Inline MathML variant

∧Intro\Intro{\land}

Block MathML variant

∧Intro\Intro{\land}

Conventional reading: conjunction introduction rule

Meaning here: The natural-deduction rule that infers A and B from separate derivations of A and B.

1 occurrence
  1. Occurrence 1: derivations.tex, line 48, column 53

Expression 210

Inline MathML variant

∀x∀y((A(x)∧A(y))→x=y)\lforall[x][\lforall[y][((!A(x) \land !A(y)) \lif \eq[x][y])]]

Block MathML variant

∀x∀y((A(x)∧A(y))→x=y)\lforall[x][\lforall[y][((!A(x) \land !A(y)) \lif \eq[x][y])]]

Conventional reading: for every x and every y, if both A of x and A of y, then x equals y

Meaning here: The universal statement that at most one object satisfies A.

2 occurrences
  1. Occurrence 1: identity.tex, line 76, column 12
  2. Occurrence 2: identity.tex, line 94, column 12

Expression 212

Inline MathML variant

{A}⊢B\{!A\} \Proves !B

Block MathML variant

{A}⊢B\{!A\} \Proves !B

Conventional reading: from the singleton set containing A, derive B

Meaning here: B is derivable from the assumption set whose sole member is A.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 103, column 198

Expression 213

Inline MathML variant

A→B⊢¬A∨B!A \lif !B \Proves \lnot !A \lor !B

Block MathML variant

A→B⊢¬A∨B!A \lif !B \Proves \lnot !A \lor !B

Conventional reading: from the conditional if A then B, derive the disjunction of not A with B

Meaning here: The sequent asserts the classical equivalence direction from a conditional to its material disjunction.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 300, column 7

Expression 214

Inline MathML variant

¬A⊢A→B\lnot !A \Proves !A \lif !B

Block MathML variant

¬A⊢A→B\lnot !A \Proves !A \lif !B

Conventional reading: from not A, derive: if A then B

Meaning here: The negation of A derives the conditional from A to B by assuming A, deriving a contradiction, and then deriving B.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 99, column 10

Expression 215

Inline MathML variant

[∃x¬A(x)]1\Discharge{\lexists[x][\lnot !A(x)]}{1}

Block MathML variant

[∃x¬A(x)]1\Discharge{\lexists[x][\lnot !A(x)]}{1}

Conventional reading: assumption: there exists an x such that not A of x; labeled one for discharge

Meaning here: The existential assumption that some object fails to satisfy A, marked with discharge label one.

4 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 30, column 9
  2. Occurrence 2: proving-things-quant.tex, line 42, column 9
  3. Occurrence 3: proving-things-quant.tex, line 57, column 9
  4. Occurrence 4: proving-things-quant.tex, line 73, column 9

Expression 217

Inline MathML variant

aa

Block MathML variant

aa

Conventional reading: the name a

Meaning here: The name a used as a fresh parameter.

12 occurrences
  1. Occurrence 1: quantifier-rules.tex, line 28, column 33
  2. Occurrence 2: quantifier-rules.tex, line 31, column 26
  3. Occurrence 3: quantifier-rules.tex, line 33, column 13
  4. Occurrence 4: quantifier-rules.tex, line 52, column 34
  5. Occurrence 5: quantifier-rules.tex, line 56, column 1
  6. Occurrence 6: quantifier-rules.tex, line 79, column 68
  7. Occurrence 7: quantifier-rules.tex, line 90, column 14
  8. Occurrence 8: proving-things-quant.tex, line 71, column 7
  9. Occurrence 9: proving-things-quant.tex, line 91, column 67
  10. Occurrence 10: proving-things-quant.tex, line 139, column 39
  11. Occurrence 11: soundness.tex, line 192, column 60
  12. Occurrence 12: soundness.tex, line 200, column 31

Expression 218

Inline MathML variant

Γ,[¬A]1\Gamma, \Discharge{\lnot !A}{1}

Block MathML variant

Γ,[¬A]1\Gamma, \Discharge{\lnot !A}{1}

Conventional reading: the assumptions in Gamma, together with assumption not A labeled one for discharge

Meaning here: A proof context containing Gamma and an occurrence of the assumption not A marked with discharge label one.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 68, column 11

Expression 219

Inline MathML variant

Γ⊢A\Gamma \Proves !A

Block MathML variant

Γ⊢A\Gamma \Proves !A

Conventional reading: Gamma syntactically derives A

Meaning here: There is a natural-deduction derivation of A whose undischarged assumptions all belong to Gamma.

14 occurrences
  1. Occurrence 1: derivations.tex, line 40, column 52
  2. Occurrence 2: proof-theoretic-notions.tex, line 41, column 25
  3. Occurrence 3: proof-theoretic-notions.tex, line 55, column 26
  4. Occurrence 4: proof-theoretic-notions.tex, line 66, column 34
  5. Occurrence 5: proof-theoretic-notions.tex, line 77, column 4
  6. Occurrence 6: proof-theoretic-notions.tex, line 82, column 4
  7. Occurrence 7: proof-theoretic-notions.tex, line 105, column 14
  8. Occurrence 8: proof-theoretic-notions.tex, line 139, column 12
  9. Occurrence 9: proof-theoretic-notions.tex, line 148, column 14
  10. Occurrence 10: provability-consistency.tex, line 20, column 6
  11. Occurrence 11: provability-consistency.tex, line 46, column 1
  12. Occurrence 12: provability-consistency.tex, line 50, column 15
  13. Occurrence 13: provability-consistency.tex, line 83, column 6
  14. Occurrence 14: provability-consistency.tex, line 88, column 11

Expression 222

Inline MathML variant

Γ0⊢A\Gamma_0 \Proves !A

Block MathML variant

Γ0⊢A\Gamma_0 \Proves !A

Conventional reading: Gamma sub zero syntactically derives A

Meaning here: A is derivable from the finite assumption set Gamma sub zero.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 140, column 33

Expression 223

Inline MathML variant

A∨¬A!A \lor \lnot !A

Block MathML variant

A∨¬A!A \lor \lnot !A

Conventional reading: A or not A

Meaning here: The instance of excluded middle asserting the disjunction of A with its negation.

11 occurrences
  1. Occurrence 1: proving-things.tex, line 186, column 12
  2. Occurrence 2: proving-things.tex, line 187, column 15
  3. Occurrence 3: proving-things.tex, line 194, column 14
  4. Occurrence 4: proving-things.tex, line 207, column 14
  5. Occurrence 5: proving-things.tex, line 221, column 14
  6. Occurrence 6: proving-things.tex, line 224, column 42
  7. Occurrence 7: proving-things.tex, line 230, column 14
  8. Occurrence 8: proving-things.tex, line 240, column 14
  9. Occurrence 9: proving-things.tex, line 247, column 14
  10. Occurrence 10: proving-things.tex, line 255, column 14
  11. Occurrence 11: proving-things.tex, line 263, column 14

Expression 224

Inline MathML variant

⊥\lfalse

Block MathML variant

⊥\lfalse

Conventional reading: a contradiction

Meaning here: The falsum symbol, meaning contradiction.

50 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 48, column 101
  2. Occurrence 2: propositional-rules.tex, line 84, column 10
  3. Occurrence 3: propositional-rules.tex, line 92, column 13
  4. Occurrence 4: propositional-rules.tex, line 96, column 23
  5. Occurrence 5: propositional-rules.tex, line 99, column 9
  6. Occurrence 6: propositional-rules.tex, line 105, column 10
  7. Occurrence 7: proving-things.tex, line 124, column 13
  8. Occurrence 8: proving-things.tex, line 134, column 13
  9. Occurrence 9: proving-things.tex, line 161, column 13
  10. Occurrence 10: proving-things.tex, line 192, column 12
  11. Occurrence 11: proving-things.tex, line 196, column 42
  12. Occurrence 12: proving-things.tex, line 197, column 19
  13. Occurrence 13: proving-things.tex, line 205, column 15
  14. Occurrence 14: proving-things.tex, line 213, column 12
  15. Occurrence 15: proving-things.tex, line 219, column 15
  16. Occurrence 16: proving-things.tex, line 223, column 18
  17. Occurrence 17: proving-things.tex, line 232, column 15
  18. Occurrence 18: proving-things.tex, line 238, column 15
  19. Occurrence 19: proving-things.tex, line 249, column 15
  20. Occurrence 20: proving-things.tex, line 257, column 15
  21. Occurrence 21: proving-things.tex, line 261, column 15
  22. Occurrence 22: proving-things-quant.tex, line 59, column 10
  23. Occurrence 23: proving-things-quant.tex, line 79, column 13
  24. Occurrence 24: proving-things-quant.tex, line 197, column 10
  25. Occurrence 25: proving-things-quant.tex, line 210, column 10
  26. Occurrence 26: proving-things-quant.tex, line 224, column 13
  27. Occurrence 27: provability-consistency.tex, line 26, column 19
  28. Occurrence 28: provability-consistency.tex, line 31, column 10
  29. Occurrence 29: provability-consistency.tex, line 38, column 13
  30. Occurrence 30: provability-consistency.tex, line 52, column 52
  31. Occurrence 31: provability-consistency.tex, line 60, column 15
  32. Occurrence 32: provability-consistency.tex, line 64, column 51
  33. Occurrence 33: provability-consistency.tex, line 70, column 12
  34. Occurrence 34: provability-consistency.tex, line 97, column 17
  35. Occurrence 35: provability-consistency.tex, line 109, column 56
  36. Occurrence 36: provability-consistency.tex, line 110, column 30
  37. Occurrence 37: provability-consistency.tex, line 115, column 10
  38. Occurrence 38: provability-consistency.tex, line 120, column 10
  39. Occurrence 39: provability-consistency.tex, line 124, column 13
  40. Occurrence 40: provability-consistency.tex, line 127, column 20
  41. Occurrence 41: provability-propositional.tex, line 72, column 19
  42. Occurrence 42: provability-propositional.tex, line 76, column 19
  43. Occurrence 43: provability-propositional.tex, line 78, column 20
  44. Occurrence 44: provability-propositional.tex, line 80, column 32
  45. Occurrence 45: provability-propositional.tex, line 118, column 19
  46. Occurrence 46: soundness.tex, line 70, column 14
  47. Occurrence 47: soundness.tex, line 74, column 28
  48. Occurrence 48: soundness.tex, line 159, column 14
  49. Occurrence 49: soundness.tex, line 304, column 1
  50. Occurrence 50: soundness.tex, line 307, column 38

Expression 225

Inline MathML variant

M⊨t=t\Sat{M}{\eq[t][t]}

Block MathML variant

M⊨t=t\Sat{M}{\eq[t][t]}

Conventional reading: structure M satisfies that t equals t

Meaning here: Structure M satisfies the reflexive identity statement for the closed term t.

1 occurrence
  1. Occurrence 1: soundness-identity.tex, line 19, column 38

Expression 227

Inline MathML variant

M′\Struct{M'}

Block MathML variant

M′\Struct{M'}

Conventional reading: structure M prime

Meaning here: A structure M prime that differs from M only in its interpretation of the name a.

1 occurrence
  1. Occurrence 1: soundness.tex, line 191, column 45

Expression 228

Inline MathML variant

[¬(A∨¬A)]1,[A]2\Discharge{\lnot(!A \lor \lnot !A)}{1}, \Discharge{!A}{2}

Block MathML variant

[¬(A∨¬A)]1,[A]2\Discharge{\lnot(!A \lor \lnot !A)}{1}, \Discharge{!A}{2}

Conventional reading: two assumptions for discharge: the first denies the entire disjunction A or not A and is labeled one; the second is A and is labeled two

Meaning here: Two active assumptions: the negation of the complete disjunction A or not A carries label one, and A carries label two.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 212, column 11

Expression 229

Inline MathML variant

[D]1\Discharge{!D}{1}

Block MathML variant

[D]1\Discharge{!D}{1}

Conventional reading: assumption D, labeled one for discharge

Meaning here: An occurrence of assumption D marked with discharge label one.

1 occurrence
  1. Occurrence 1: derivations.tex, line 89, column 9

Expression 231

Inline MathML variant

→\lif

Block MathML variant

→\lif

Conventional reading: conditional

Meaning here: The binary conditional connective, read as if the antecedent then the consequent.

6 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 48, column 80
  2. Occurrence 2: propositional-rules.tex, line 63, column 23
  3. Occurrence 3: proving-things.tex, line 27, column 15
  4. Occurrence 4: proving-things.tex, line 65, column 13
  5. Occurrence 5: proving-things.tex, line 66, column 15
  6. Occurrence 6: proving-things.tex, line 68, column 15

Expression 232

Inline MathML variant

B!B

Block MathML variant

B!B

Conventional reading: formula B

Meaning here: The metavariable B denotes an arbitrary formula.

48 occurrences
  1. Occurrence 1: propositional-rules.tex, line 20, column 9
  2. Occurrence 2: propositional-rules.tex, line 33, column 12
  3. Occurrence 3: propositional-rules.tex, line 47, column 9
  4. Occurrence 4: propositional-rules.tex, line 67, column 10
  5. Occurrence 5: propositional-rules.tex, line 75, column 13
  6. Occurrence 6: propositional-rules.tex, line 118, column 48
  7. Occurrence 7: derivations.tex, line 47, column 38
  8. Occurrence 8: derivations.tex, line 52, column 9
  9. Occurrence 9: derivations.tex, line 56, column 66
  10. Occurrence 10: derivations.tex, line 67, column 4
  11. Occurrence 11: derivations.tex, line 104, column 11
  12. Occurrence 12: proving-things.tex, line 103, column 10
  13. Occurrence 13: proving-things.tex, line 107, column 10
  14. Occurrence 14: proving-things.tex, line 117, column 20
  15. Occurrence 15: proving-things.tex, line 118, column 15
  16. Occurrence 16: proving-things.tex, line 125, column 10
  17. Occurrence 17: proving-things.tex, line 127, column 35
  18. Occurrence 18: proving-things.tex, line 136, column 12
  19. Occurrence 19: proving-things.tex, line 140, column 10
  20. Occurrence 20: proving-things.tex, line 152, column 25
  21. Occurrence 21: proving-things.tex, line 152, column 67
  22. Occurrence 22: proving-things.tex, line 153, column 56
  23. Occurrence 23: proving-things.tex, line 153, column 66
  24. Occurrence 24: proving-things.tex, line 154, column 13
  25. Occurrence 25: proving-things.tex, line 163, column 12
  26. Occurrence 26: proving-things-quant.tex, line 124, column 47
  27. Occurrence 27: proof-theoretic-notions.tex, line 84, column 65
  28. Occurrence 28: proof-theoretic-notions.tex, line 90, column 12
  29. Occurrence 29: proof-theoretic-notions.tex, line 97, column 15
  30. Occurrence 30: provability-propositional.tex, line 44, column 18
  31. Occurrence 31: provability-propositional.tex, line 49, column 15
  32. Occurrence 32: provability-propositional.tex, line 88, column 15
  33. Occurrence 33: provability-propositional.tex, line 110, column 19
  34. Occurrence 34: provability-propositional.tex, line 120, column 18
  35. Occurrence 35: provability-propositional.tex, line 124, column 15
  36. Occurrence 36: soundness.tex, line 87, column 6
  37. Occurrence 37: soundness.tex, line 106, column 58
  38. Occurrence 38: soundness.tex, line 111, column 11
  39. Occurrence 39: soundness.tex, line 128, column 29
  40. Occurrence 40: soundness.tex, line 131, column 55
  41. Occurrence 41: soundness.tex, line 135, column 14
  42. Occurrence 42: soundness.tex, line 139, column 28
  43. Occurrence 43: soundness.tex, line 150, column 62
  44. Occurrence 44: soundness.tex, line 217, column 30
  45. Occurrence 45: soundness.tex, line 224, column 14
  46. Occurrence 46: soundness.tex, line 229, column 44
  47. Occurrence 47: soundness.tex, line 244, column 42
  48. Occurrence 48: soundness.tex, line 254, column 17

Expression 233

Inline MathML variant

A→B,¬A→B⊢B!A \lif !B, \lnot !A \lif !B \Proves !B

Block MathML variant

A→B,¬A→B⊢B!A \lif !B, \lnot !A \lif !B \Proves !B

Conventional reading: from two separate premises, the conditional from A to B and the conditional from not A to B, derive B

Meaning here: The two conditionals to B, covering A and not A, jointly derive B by classical reasoning.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 302, column 7

Expression 234

Inline MathML variant

Γ2⊨A\Gamma_2 \Entails !A

Block MathML variant

Γ2⊨A\Gamma_2 \Entails !A

Conventional reading: Gamma two semantically entails A

Meaning here: Every structure satisfying Gamma two satisfies A.

1 occurrence
  1. Occurrence 1: soundness.tex, line 265, column 22

Expression 235

Inline MathML variant

(∃xA(x)∧∀y∀z((A(y)∧A(z))→y=z))→∃x(A(x)∧∀y(A(y)→y=x))\lexists[x][!A(x)] \land \lforall[y][\lforall[z][((!A(y) \land !A(z)) \lif \eq[y][z])]] \lif \lexists[x][(!A(x) \land \lforall[y][(!A(y) \lif \eq[y][x])])]

Block MathML variant

(∃xA(x)∧∀y∀z((A(y)∧A(z))→y=z))→∃x(A(x)∧∀y(A(y)→y=x))\lexists[x][!A(x)] \land \lforall[y][\lforall[z][((!A(y) \land !A(z)) \lif \eq[y][z])]] \lif \lexists[x][(!A(x) \land \lforall[y][(!A(y) \lif \eq[y][x])])]

Conventional reading: if there exists an A object and every two A objects are equal, then there exists an x that is A and to which every A object is equal

Meaning here: A conditional deriving an explicit unique A-witness from existence together with the at-most-one condition.

1 occurrence
  1. Occurrence 1: identity.tex, line 118, column 7

Expression 236

Inline MathML variant

δ\delta

Block MathML variant

δ\delta

Conventional reading: delta

Meaning here: Delta names the derivation under discussion.

17 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 149, column 23
  2. Occurrence 2: proof-theoretic-notions.tex, line 150, column 53
  3. Occurrence 3: proof-theoretic-notions.tex, line 152, column 41
  4. Occurrence 4: provability-consistency.tex, line 89, column 22
  5. Occurrence 5: provability-consistency.tex, line 94, column 17
  6. Occurrence 6: provability-quantifiers.tex, line 28, column 5
  7. Occurrence 7: soundness.tex, line 40, column 5
  8. Occurrence 8: soundness.tex, line 41, column 42
  9. Occurrence 9: soundness.tex, line 44, column 23
  10. Occurrence 10: soundness.tex, line 52, column 42
  11. Occurrence 11: soundness.tex, line 88, column 34
  12. Occurrence 12: soundness.tex, line 143, column 35
  13. Occurrence 13: soundness.tex, line 155, column 46
  14. Occurrence 14: soundness.tex, line 175, column 52
  15. Occurrence 15: soundness.tex, line 217, column 39
  16. Occurrence 16: soundness.tex, line 231, column 35
  17. Occurrence 17: soundness.tex, line 245, column 54

Expression 237

Inline MathML variant

ValM(t1)=ValM(t2)\Value{t_1}{M} = \Value{t_2}{M}

Block MathML variant

ValM(t1)=ValM(t2)\Value{t_1}{M} = \Value{t_2}{M}

Conventional reading: the value of t one in structure M equals the value of t two in structure M

Meaning here: The two closed terms receive the same denotation in structure M.

1 occurrence
  1. Occurrence 1: soundness-identity.tex, line 40, column 38

Expression 238

Inline MathML variant

Γ∪{A}\Gamma \cup \{ !A \}

Block MathML variant

Γ∪{A}\Gamma \cup \{ !A \}

Conventional reading: Gamma union the singleton set containing A

Meaning here: The assumption set obtained by adding formula A to Gamma.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 110, column 3

Expression 239

Inline MathML variant

∃x∀y(A(y)→y=x)\lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]]

Block MathML variant

∃x∀y(A(y)→y=x)\lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]]

Conventional reading: there exists an x such that, for every y, if A of y, then y equals x

Meaning here: There is an object to which every object satisfying A is identical; the witness need not itself satisfy A in this formula alone.

1 occurrence
  1. Occurrence 1: identity.tex, line 82, column 9

Expression 240

Inline MathML variant

Δ⊢A\Delta \Proves !A

Block MathML variant

Δ⊢A\Delta \Proves !A

Conventional reading: capital Delta syntactically derives A

Meaning here: There is a natural-deduction derivation of A whose undischarged assumptions all belong to the set Delta.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 66, column 60

Expression 241

Inline MathML variant

A⊢A∨B!A \Proves !A \lor !B

Block MathML variant

A⊢A∨B!A \Proves !A \lor !B

Conventional reading: from A, derive A or B

Meaning here: A derives the disjunction A or B by disjunction introduction.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 60, column 14

Expression 242

Inline MathML variant

∃xA(x)\lexists[x][!A(x)]

Block MathML variant

∃xA(x)\lexists[x][!A(x)]

Conventional reading: there exists an x such that A of x

Meaning here: The existentially quantified formula asserting that A holds of at least one object.

5 occurrences
  1. Occurrence 1: quantifier-rules.tex, line 53, column 22
  2. Occurrence 2: quantifier-rules.tex, line 96, column 11
  3. Occurrence 3: proving-things-quant.tex, line 39, column 1
  4. Occurrence 4: provability-quantifiers.tex, line 46, column 6
  5. Occurrence 5: provability-quantifiers.tex, line 50, column 12

Expression 243

Inline MathML variant

∀x∀y((A(x)∧A(y))→x=y)from the sentence∃x∀y(A(y)→y=x)& \lforall[x][\lforall[y][((!A(x) \land !A(y)) \lif \eq[x][y])]] \intertext{from the !!{sentence}} & \lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]]

Block MathML variant

∀x∀y((A(x)∧A(y))→x=y)from the sentence∃x∀y(A(y)→y=x)& \lforall[x][\lforall[y][((!A(x) \land !A(y)) \lif \eq[x][y])]] \intertext{from the !!{sentence}} & \lexists[x][\lforall[y][(!A(y) \lif \eq[y][x])]]

Conventional reading: derive: for every x and every y, if both A of x and A of y, then x equals y; from the sentence: there exists an x such that, for every y, if A of y then y equals x

Meaning here: An aligned source display states the universal uniqueness conclusion first and then identifies the existential sentence from which it is to be derived.

1 occurrence
  1. Occurrence 1: identity.tex, line 61, column 1

Expression 244

Inline MathML variant

Γ⊨A∧B\Gamma \Entails !A \land !B

Block MathML variant

Γ⊨A∧B\Gamma \Entails !A \land !B

Conventional reading: Gamma semantically entails A and B

Meaning here: Every structure satisfying Gamma satisfies the conjunction of A and B.

1 occurrence
  1. Occurrence 1: soundness.tex, line 102, column 15

Expression 245

Inline MathML variant

P(a,a)\Atom{\Obj P}{a,a}

Block MathML variant

P(a,a)\Atom{\Obj P}{a,a}

Conventional reading: P of a and a

Meaning here: The atomic formula with constant a in both argument positions.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 81, column 40

Expression 246

Inline MathML variant

Γ,[A]1\Gamma, \Discharge{!A}{1}

Block MathML variant

Γ,[A]1\Gamma, \Discharge{!A}{1}

Conventional reading: the assumptions in Gamma, together with assumption A labeled one for discharge

Meaning here: A proof context containing the undischarged assumptions in Gamma and an occurrence of assumption A marked for discharge by a later discharging inference carrying label one.

2 occurrences
  1. Occurrence 1: provability-consistency.tex, line 29, column 9
  2. Occurrence 2: provability-consistency.tex, line 118, column 9

Expression 247

Inline MathML variant

∃xP(t,x)\lexists[x][\Atom{\Obj P}{t,x}]

Block MathML variant

∃xP(t,x)\lexists[x][\Atom{\Obj P}{t,x}]

Conventional reading: there exists an x such that P of t and x

Meaning here: The existential closure in x of the atomic formula P of t and x.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 74, column 43

Expression 248

Inline MathML variant

=Elim\Elim{\eq}

Block MathML variant

=Elim\Elim{\eq}

Conventional reading: identity elimination rule

Meaning here: The natural-deduction rule permitting substitution of identical closed terms within a formula.

1 occurrence
  1. Occurrence 1: identity.tex, line 45, column 13

Expression 249

Inline MathML variant

δ2\delta_2

Block MathML variant

δ2\delta_2

Conventional reading: delta two

Meaning here: The second subderivation, named delta two.

9 occurrences
  1. Occurrence 1: provability-consistency.tex, line 27, column 4
  2. Occurrence 2: provability-consistency.tex, line 30, column 13
  3. Occurrence 3: provability-consistency.tex, line 109, column 42
  4. Occurrence 4: provability-consistency.tex, line 114, column 13
  5. Occurrence 5: soundness.tex, line 223, column 17
  6. Occurrence 6: soundness.tex, line 230, column 46
  7. Occurrence 7: soundness.tex, line 251, column 17
  8. Occurrence 8: soundness.tex, line 259, column 6
  9. Occurrence 9: soundness-identity.tex, line 30, column 15

Expression 250

Inline MathML variant

M⊨A\Sat{M}{!A}

Block MathML variant

M⊨A\Sat{M}{!A}

Conventional reading: structure M satisfies A

Meaning here: Structure M satisfies formula A.

8 occurrences
  1. Occurrence 1: soundness.tex, line 81, column 3
  2. Occurrence 2: soundness.tex, line 100, column 3
  3. Occurrence 3: soundness.tex, line 105, column 3
  4. Occurrence 4: soundness.tex, line 125, column 3
  5. Occurrence 5: soundness.tex, line 149, column 3
  6. Occurrence 6: soundness.tex, line 237, column 3
  7. Occurrence 7: soundness.tex, line 266, column 3
  8. Occurrence 8: soundness.tex, line 269, column 3

Expression 256

Inline MathML variant

tt

Block MathML variant

tt

Conventional reading: closed term t

Meaning here: The metavariable t denotes a closed term in the stated quantifier and identity rules.

8 occurrences
  1. Occurrence 1: quantifier-rules.tex, line 27, column 30
  2. Occurrence 2: quantifier-rules.tex, line 52, column 8
  3. Occurrence 3: quantifier-rules.tex, line 73, column 11
  4. Occurrence 4: quantifier-rules.tex, line 77, column 33
  5. Occurrence 5: quantifier-rules.tex, line 87, column 10
  6. Occurrence 6: identity.tex, line 36, column 21
  7. Occurrence 7: identity.tex, line 41, column 12
  8. Occurrence 8: soundness-identity.tex, line 20, column 20

Expression 257

Inline MathML variant

Γ⊢∀xA(x)\Gamma \Proves \lforall[x][!A(x)]

Block MathML variant

Γ⊢∀xA(x)\Gamma \Proves \lforall[x][!A(x)]

Conventional reading: Gamma syntactically derives that, for every x, A of x

Meaning here: There is a natural-deduction derivation of the universal A statement from undischarged assumptions in Gamma.

1 occurrence
  1. Occurrence 1: provability-quantifiers.tex, line 23, column 57

Expression 258

Inline MathML variant

A(t)!A(t)

Block MathML variant

A(t)!A(t)

Conventional reading: A of t

Meaning here: The result of instantiating the indicated free argument place of formula A with the closed term t.

7 occurrences
  1. Occurrence 1: quantifier-rules.tex, line 23, column 12
  2. Occurrence 2: quantifier-rules.tex, line 66, column 15
  3. Occurrence 3: provability-quantifiers.tex, line 46, column 32
  4. Occurrence 4: provability-quantifiers.tex, line 48, column 9
  5. Occurrence 5: provability-quantifiers.tex, line 53, column 54
  6. Occurrence 6: provability-quantifiers.tex, line 58, column 12
  7. Occurrence 7: identity.tex, line 46, column 13

Expression 259

Inline MathML variant

Γ1⊨A→B\Gamma_1 \Entails !A \lif !B

Block MathML variant

Γ1⊨A→B\Gamma_1 \Entails !A \lif !B

Conventional reading: Gamma one semantically entails: if A, then B

Meaning here: Every structure satisfying Gamma one satisfies the conditional from A to B.

1 occurrence
  1. Occurrence 1: soundness.tex, line 264, column 3

Expression 260

Inline MathML variant

Γ∪{A}\Gamma \cup \{!A\}

Block MathML variant

Γ∪{A}\Gamma \cup \{!A\}

Conventional reading: Gamma together with assumption A

Meaning here: The union of Gamma with the singleton set containing formula A.

6 occurrences
  1. Occurrence 1: provability-consistency.tex, line 20, column 30
  2. Occurrence 2: provability-consistency.tex, line 26, column 34
  3. Occurrence 3: provability-consistency.tex, line 78, column 42
  4. Occurrence 4: provability-consistency.tex, line 104, column 6
  5. Occurrence 5: soundness.tex, line 75, column 15
  6. Occurrence 6: soundness.tex, line 151, column 18

Expression 262

Inline MathML variant

∃xC(x,b)\lexists[x][!C(x,b)]

Block MathML variant

∃xC(x,b)\lexists[x][!C(x,b)]

Conventional reading: there exists an x such that C of x and b

Meaning here: The existential formula asserting that some object stands in relation C to b.

10 occurrences
  1. Occurrence 1: proving-things-quant.tex, line 103, column 1
  2. Occurrence 2: proving-things-quant.tex, line 109, column 12
  3. Occurrence 3: proving-things-quant.tex, line 120, column 10
  4. Occurrence 4: proving-things-quant.tex, line 122, column 13
  5. Occurrence 5: proving-things-quant.tex, line 132, column 10
  6. Occurrence 6: proving-things-quant.tex, line 134, column 13
  7. Occurrence 7: proving-things-quant.tex, line 154, column 10
  8. Occurrence 8: proving-things-quant.tex, line 157, column 13
  9. Occurrence 9: proving-things-quant.tex, line 173, column 12
  10. Occurrence 10: proving-things-quant.tex, line 176, column 13

Expression 263

Inline MathML variant

(¬A∨B)→(A→B)(\lnot !A \lor !B) \lif (!A \lif !B)

Block MathML variant

(¬A∨B)→(A→B)(\lnot !A \lor !B) \lif (!A \lif !B)

Conventional reading: if either not A or B, then if A, then B

Meaning here: A conditional from the disjunction not A or B to the conditional from A to B.

7 occurrences
  1. Occurrence 1: proving-things.tex, line 54, column 35
  2. Occurrence 2: proving-things.tex, line 61, column 12
  3. Occurrence 3: proving-things.tex, line 75, column 12
  4. Occurrence 4: proving-things.tex, line 95, column 12
  5. Occurrence 5: proving-things.tex, line 113, column 12
  6. Occurrence 6: proving-things.tex, line 146, column 12
  7. Occurrence 7: proving-things.tex, line 172, column 12

Expression 265

Inline MathML variant

∀xP(a,x)\lforall[x][\Atom{\Obj P}{a,x}]

Block MathML variant

∀xP(a,x)\lforall[x][\Atom{\Obj P}{a,x}]

Conventional reading: for every x, P of a and x

Meaning here: The universally quantified formula whose matrix is P of a and x.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 81, column 1

Expression 266

Inline MathML variant

M⊨Γ2\Sat{M}{\Gamma_2}

Block MathML variant

M⊨Γ2\Sat{M}{\Gamma_2}

Conventional reading: structure M satisfies every assumption in Gamma two

Meaning here: Structure M satisfies the second assumption set.

1 occurrence
  1. Occurrence 1: soundness.tex, line 238, column 9

Expression 267

Inline MathML variant

A1,A2,…,Ak⊢B!A_1,!A_2,\ldots,!A_k \Proves !B

Block MathML variant

A1,A2,…,Ak⊢B!A_1,!A_2,\ldots,!A_k \Proves !B

Conventional reading: from A sub one, A sub two, through A sub k, derive B

Meaning here: B is derivable in natural deduction from the listed formulas A sub one through A sub k.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 103, column 97

Expression 270

Inline MathML variant

∃\lexists

Block MathML variant

∃\lexists

Conventional reading: existential quantifier

Meaning here: The existential quantifier forms a statement that holds for at least one object in the domain.

1 occurrence
  1. Occurrence 1: quantifier-rules.tex, line 36, column 23

Expression 271

Inline MathML variant

A(a)!A(a)

Block MathML variant

A(a)!A(a)

Conventional reading: A of a

Meaning here: Formula A with the name a in the indicated argument place.

9 occurrences
  1. Occurrence 1: quantifier-rules.tex, line 16, column 9
  2. Occurrence 2: quantifier-rules.tex, line 31, column 9
  3. Occurrence 3: quantifier-rules.tex, line 55, column 51
  4. Occurrence 4: proving-things-quant.tex, line 77, column 12
  5. Occurrence 5: soundness.tex, line 179, column 14
  6. Occurrence 6: soundness.tex, line 183, column 15
  7. Occurrence 7: soundness.tex, line 195, column 37
  8. Occurrence 8: soundness.tex, line 199, column 8
  9. Occurrence 9: identity.tex, line 106, column 12

Expression 272

Inline MathML variant

A∧B⊢B!A \land !B \Proves !B

Block MathML variant

A∧B⊢B!A \land !B \Proves !B

Conventional reading: from the conjunction A and B, derive B

Meaning here: The conjunction A and B derives its right conjunct B.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 29, column 13

Expression 273

Inline MathML variant

Γ⊬A\Gamma \Proves/ !A

Block MathML variant

Γ⊬A\Gamma \Proves/ !A

Conventional reading: Gamma does not syntactically derive A

Meaning here: There is no natural-deduction derivation of A whose undischarged assumptions all belong to Gamma.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 44, column 38

Expression 277

Inline MathML variant

A(x)[a/x]\Subst{!A(x)}{a}{x}

Block MathML variant

A(x)[a/x]\Subst{!A(x)}{a}{x}

Conventional reading: A of x with a substituted for x

Meaning here: The result of substituting the name a for free occurrences of x in formula A of x.

1 occurrence
  1. Occurrence 1: soundness.tex, line 199, column 24

Expression 278

Inline MathML variant

A∧¬C⊢¬(A→C)!A \land \lnot !C \Proves \lnot (!A \lif !C)

Block MathML variant

A∧¬C⊢¬(A→C)!A \land \lnot !C \Proves \lnot (!A \lif !C)

Conventional reading: from the conjunction of A with not C, derive that it is not the case that if A then C

Meaning here: The sequent asserts that A together with not C derives the negation of the conditional from A to C.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 287, column 7

Expression 279

Inline MathML variant

Γ∪Δ\Gamma \cup \Delta

Block MathML variant

Γ∪Δ\Gamma \cup \Delta

Conventional reading: the union of Gamma and capital Delta

Meaning here: The set containing every assumption that belongs to Gamma or to Delta.

1 occurrence
  1. Occurrence 1: proof-theoretic-notions.tex, line 99, column 52

140 formal objects

Inference rules 2

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Inference rules 2
  2. Derivation diagram 1
  3. Step 1 states formula A as a premise. Step 2 states formula B as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes A and B. The final conclusion is A and B.
  4. Derivation diagram 2
  5. Step 1 states A and B as a premise. Step 2 applies the conjunction elimination rule to 1 and concludes formula A. The final conclusion is formula A.
  6. Derivation diagram 3
  7. Step 1 states A and B as a premise. Step 2 applies the conjunction elimination rule to 1 and concludes formula B. The final conclusion is formula B.

Source: content/first-order-logic/natural-deduction/propositional-rules.tex, line 18.

Inference rules 3

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Inference rules 3
  2. Derivation diagram 4
  3. Step 1 states formula A as a premise. Step 2 applies the disjunction introduction rule to 1 and concludes A or B. The final conclusion is A or B.
  4. Derivation diagram 5
  5. Step 1 states formula B as a premise. Step 2 applies the disjunction introduction rule to 1 and concludes A or B. The final conclusion is A or B.
  6. Derivation diagram 6
  7. Step 1 states A or B as a premise. Step 2 states assumption A, labeled n for discharge as a premise. Step 3 applies the subderivation to 2 and concludes formula C. Step 4 states assumption B, labeled n for discharge as a premise. Step 5 applies the subderivation to 4 and concludes formula C. Step 6 applies the disjunction elimination rule to 1, 3, 5 and concludes formula C. The final conclusion is formula C.

Source: content/first-order-logic/natural-deduction/propositional-rules.tex, line 40.

Natural-deduction proof tree at propositional-rules.tex, line 60

Step 1 states A or B as a premise. Step 2 states assumption A, labeled n for discharge as a premise. Step 3 applies the subderivation to 2 and concludes formula C. Step 4 states assumption B, labeled n for discharge as a premise. Step 5 applies the subderivation to 4 and concludes formula C. Step 6 applies the disjunction elimination rule to 1, 3, 5 and concludes formula C. The final conclusion is formula C.

  1. Premise: projected-formula-0009197
  2. Premise: projected-formula-0009198
  3. Subderivation conclusion: projected-formula-0009199
  4. Premise: projected-formula-0009200
  5. Subderivation conclusion: projected-formula-0009201
  6. disjunction elimination rule: projected-formula-0009202

Source: content/first-order-logic/natural-deduction/propositional-rules.tex, line 60.

Inference rules 4

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Inference rules 4
  2. Derivation diagram 7
  3. Step 1 states assumption A, labeled n for discharge as a premise. Step 2 applies the subderivation to 1 and concludes formula B. Step 3 applies the conditional introduction rule to 2 and concludes if A, then B. The final conclusion is if A, then B.
  4. Derivation diagram 8
  5. Step 1 states if A, then B as a premise. Step 2 states formula A as a premise. Step 3 applies the conditional elimination rule to 1, 2 and concludes formula B. The final conclusion is formula B.

Source: content/first-order-logic/natural-deduction/propositional-rules.tex, line 65.

Natural-deduction proof tree at propositional-rules.tex, line 70

Step 1 states assumption A, labeled n for discharge as a premise. Step 2 applies the subderivation to 1 and concludes formula B. Step 3 applies the conditional introduction rule to 2 and concludes if A, then B. The final conclusion is if A, then B.

  1. Premise: projected-formula-0009204
  2. Subderivation conclusion: projected-formula-0009205
  3. conditional introduction rule: projected-formula-0009206

Source: content/first-order-logic/natural-deduction/propositional-rules.tex, line 70.

Inference rules 5

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Inference rules 5
  2. Derivation diagram 9
  3. Step 1 states assumption A, labeled n for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the negation introduction rule to 2 and concludes not A. The final conclusion is not A.
  4. Derivation diagram 10
  5. Step 1 states not A as a premise. Step 2 states formula A as a premise. Step 3 applies the negation elimination rule to 1, 2 and concludes a contradiction. The final conclusion is a contradiction.

Source: content/first-order-logic/natural-deduction/propositional-rules.tex, line 81.

Natural-deduction proof tree at propositional-rules.tex, line 87

Step 1 states assumption A, labeled n for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the negation introduction rule to 2 and concludes not A. The final conclusion is not A.

  1. Premise: projected-formula-0009211
  2. Subderivation conclusion: projected-formula-0009212
  3. negation introduction rule: projected-formula-0009213

Source: content/first-order-logic/natural-deduction/propositional-rules.tex, line 87.

Inference rules 6

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Inference rules 6
  2. Derivation diagram 11
  3. Step 1 states a contradiction as a premise. Step 2 applies the falsehood elimination rule to 1 and concludes formula A. The final conclusion is formula A.
  4. Derivation diagram 12
  5. Step 1 states assumption not A, labeled n for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the classical contradiction rule to 2 and concludes formula A. The final conclusion is formula A.

Source: content/first-order-logic/natural-deduction/propositional-rules.tex, line 98.

Natural-deduction proof tree at propositional-rules.tex, line 108

Step 1 states assumption not A, labeled n for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the classical contradiction rule to 2 and concludes formula A. The final conclusion is formula A.

  1. Premise: projected-formula-0009220
  2. Subderivation conclusion: projected-formula-0009221
  3. classical contradiction rule: projected-formula-0009222

Source: content/first-order-logic/natural-deduction/propositional-rules.tex, line 108.

Inference rules 7

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Inference rules 7
  2. Derivation diagram 13
  3. Step 1 states A of a as a premise. Step 2 applies the universal quantifier introduction rule to 1 and concludes for every x, A of x. The final conclusion is for every x, A of x.
  4. Derivation diagram 14
  5. Step 1 states for every x, A of x as a premise. Step 2 applies the universal quantifier elimination rule to 1 and concludes A of t. The final conclusion is A of t.

Source: content/first-order-logic/natural-deduction/quantifier-rules.tex, line 15.

Inference rules 8

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Inference rules 8
  2. Derivation diagram 15
  3. Step 1 states A of t as a premise. Step 2 applies the existential quantifier introduction rule to 1 and concludes there exists an x such that A of x. The final conclusion is there exists an x such that A of x.
  4. Derivation diagram 16
  5. Step 1 states there exists an x such that A of x as a premise. Step 2 states A of a as a premise marked discharge label n. Step 3 applies the subderivation to 2 and concludes formula C. Step 4 applies the existential quantifier elimination rule to 1, 3 and concludes formula C. The final conclusion is formula C.

Source: content/first-order-logic/natural-deduction/quantifier-rules.tex, line 38.

Natural-deduction proof tree at quantifier-rules.tex, line 49

Step 1 states there exists an x such that A of x as a premise. Step 2 states A of a as a premise marked discharge label n. Step 3 applies the subderivation to 2 and concludes formula C. Step 4 applies the existential quantifier elimination rule to 1, 3 and concludes formula C. The final conclusion is formula C.

  1. Premise: projected-formula-0009247
  2. Marked premise: projected-formula-0009248; projected-formula-0009249
  3. Subderivation conclusion: projected-formula-0009250
  4. existential quantifier elimination rule: projected-formula-0009251

Source: content/first-order-logic/natural-deduction/quantifier-rules.tex, line 49.

Natural-deduction proof tree at quantifier-rules.tex, line 95

Step 1 states there exists an x such that A of x as a premise. Step 2 states assumption A of a labeled one for discharge as a premise. Step 3 applies the invalid (starred) universal quantifier introduction rule to 2 and concludes for every x, A of x. Step 4 applies the existential quantifier elimination rule to 1, 3 and concludes for every x, A of x. The final conclusion is for every x, A of x.

  1. Premise: projected-formula-0009284
  2. Premise: projected-formula-0009285
  3. invalid (starred) universal quantifier introduction rule: projected-formula-0009286
  4. existential quantifier elimination rule: projected-formula-0009287

Source: content/first-order-logic/natural-deduction/quantifier-rules.tex, line 95.

Definition 9: Derivation

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Definition 9: Derivation
  2. A derivation of a sentence formula A from assumptions Gamma is a finite tree of sentences satisfying the following conditions:
  3. Item 1.
  4. The topmost sentences of the tree are either in Gamma or are discharged by an inference in the tree.
  5. Item 2.
  6. The bottommost sentence of the tree is formula A.
  7. Item 3.
  8. Every sentence in the tree except the sentence formula A at the bottom is a premise of a correct application of an inference rule whose conclusion stands directly below that sentence in the tree.
  9. We then say that formula A is the conclusion of the derivation and Gamma its undischarged assumptions.
  10. If a derivation of formula A from Gamma exists, we say that formula A is derivable from Gamma, or in symbols: Gamma syntactically derives A. If there is a derivation of formula A in which every assumption is discharged, we write A is derivable without undischarged assumptions.

Source: content/first-order-logic/natural-deduction/derivations.tex, line 23.

Example 1

Complete source-order listener rendering of this example; no claim or solution is added.

  1. Example 1
  2. Every assumption on its own is a derivation. So, e.g., formula A by itself is a derivation, and so is formula B by itself. We can obtain a new derivation from these by applying, say, the conjunction introduction rule,
  3. Derivation diagram 19
  4. Step 1 states formula A as a premise. Step 2 states formula B as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes A and B. The final conclusion is A and B.
  5. These rules are meant to be general: we can replace the formula A and formula B in it with any sentences, e.g., by formula C and formula D. Then the conclusion would be C and D, and so
  6. Derivation diagram 20
  7. Step 1 states formula C as a premise. Step 2 states formula D as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes C and D. The final conclusion is C and D.
  8. is a correct derivation. Of course, we can also switch the assumptions, so that formula D plays the role of formula A and formula C that of formula B. Thus,
  9. Derivation diagram 21
  10. Step 1 states formula D as a premise. Step 2 states formula C as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes D and C. The final conclusion is D and C.
  11. is also a correct derivation.
  12. We can now apply another rule, say, conditional introduction rule, which allows us to conclude a conditional and allows us to discharge any assumption that is identical to the antecedent of that conditional. So both of the following would be correct derivations:
  13. Derivation diagram 22
  14. Step 1 states assumption C, labeled one for discharge as a premise. Step 2 states formula D as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes C and D. Step 4 applies the conditional introduction rule to 3 and concludes if C, then C and D. The final conclusion is if C, then C and D.
  15. Derivation diagram 23
  16. Step 1 states formula C as a premise. Step 2 states assumption D, labeled one for discharge as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes C and D. Step 4 applies the conditional introduction rule to 3 and concludes if D, then C and D. The final conclusion is if D, then C and D.
  17. They show, respectively, that from D, one can derive: if C, then C and D and from C, one can derive: if D, then C and D.
  18. Remember that discharging of assumptions is a permission, not a requirement: we don't have to discharge the assumptions. In particular, we can apply a rule even if the assumptions are not present in the derivation. For instance, the following is legal, even though there is no assumption formula A to be discharged:
  19. Derivation diagram 24
  20. Step 1 states formula B as a premise. Step 2 applies the conditional introduction rule to 1 and concludes if A, then B. The final conclusion is if A, then B.

Source: content/first-order-logic/natural-deduction/derivations.tex, line 45.

Natural-deduction proof tree at derivations.tex, line 80

Step 1 states assumption C, labeled one for discharge as a premise. Step 2 states formula D as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes C and D. Step 4 applies the conditional introduction rule to 3 and concludes if C, then C and D. The final conclusion is if C, then C and D.

  1. Premise: projected-formula-0009325
  2. Premise: projected-formula-0009326
  3. conjunction introduction rule: projected-formula-0009327
  4. conditional introduction rule: projected-formula-0009328

Source: content/first-order-logic/natural-deduction/derivations.tex, line 80.

Natural-deduction proof tree at derivations.tex, line 87

Step 1 states formula C as a premise. Step 2 states assumption D, labeled one for discharge as a premise. Step 3 applies the conjunction introduction rule to 1, 2 and concludes C and D. Step 4 applies the conditional introduction rule to 3 and concludes if D, then C and D. The final conclusion is if D, then C and D.

  1. Premise: projected-formula-0009329
  2. Premise: projected-formula-0009330
  3. conjunction introduction rule: projected-formula-0009331
  4. conditional introduction rule: projected-formula-0009332

Source: content/first-order-logic/natural-deduction/derivations.tex, line 87.

Example 2

Complete source-order listener rendering of this example; no claim or solution is added.

  1. Example 2
  2. Let's give a derivation of the sentence if A and B, then A.
  3. We begin by writing the desired conclusion at the bottom of the derivation.
  4. Derivation diagram 25
  5. Step 1 has no printed premise. Step 2 applies the inference rule to 1 and concludes if A and B, then A. The final conclusion is if A and B, then A.
  6. Next, we need to figure out what kind of inference could result in a sentence of this form. The main operator of the conclusion is conditional, so we'll try to arrive at the conclusion using the conditional introduction rule. It is best to write down the assumptions involved and label the inference rules as you progress, so it is easy to see whether all assumptions have been discharged at the end of the proof.
  7. Derivation diagram 26
  8. Step 1 states the single assumption that is the conjunction of A and B, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes formula A. Step 3 applies the conditional introduction rule to 2 and concludes if A and B, then A. The final conclusion is if A and B, then A.
  9. We now need to fill in the steps from the assumption A and B to formula A. Since we only have one connective to deal with, conjunction, we must use the conjunction elimination rule. This gives us the following proof:
  10. Derivation diagram 27
  11. Step 1 states the single assumption that is the conjunction of A and B, labeled one for discharge as a premise. Step 2 applies the conjunction elimination rule to 1 and concludes formula A. Step 3 applies the conditional introduction rule to 2 and concludes if A and B, then A. The final conclusion is if A and B, then A.
  12. We now have a correct derivation of if A and B, then A.

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 15.

Natural-deduction proof tree at proving-things.tex, line 32

Step 1 states the single assumption that is the conjunction of A and B, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes formula A. Step 3 applies the conditional introduction rule to 2 and concludes if A and B, then A. The final conclusion is if A and B, then A.

  1. Premise: projected-formula-0009341
  2. Subderivation conclusion: projected-formula-0009342
  3. conditional introduction rule: projected-formula-0009343

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 32.

Natural-deduction proof tree at proving-things.tex, line 42

Step 1 states the single assumption that is the conjunction of A and B, labeled one for discharge as a premise. Step 2 applies the conjunction elimination rule to 1 and concludes formula A. Step 3 applies the conditional introduction rule to 2 and concludes if A and B, then A. The final conclusion is if A and B, then A.

  1. Premise: projected-formula-0009348
  2. conjunction elimination rule: projected-formula-0009349
  3. conditional introduction rule: projected-formula-0009350

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 42.

Example 3

Complete source-order listener rendering of this example; no claim or solution is added.

  1. Example 3
  2. Now let's give a derivation of if either not A or B, then if A, then B.
  3. We begin by writing the desired conclusion at the bottom of the derivation.
  4. Derivation diagram 28
  5. Step 1 has no printed premise. Step 2 applies the inference rule to 1 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.
  6. To find a logical rule that could give us this conclusion, we look at the logical connectives in the conclusion: negation, disjunction, and conditional. We only care at the moment about the first occurrence of conditional because it is the main operator of the sentence in the end-sequent, while negation, disjunction and the second occurrence of conditional are inside the scope of another connective, so we will take care of those later. We therefore start with the conditional introduction rule. A correct application must look like this:
  7. Derivation diagram 29
  8. Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes if A, then B. Step 3 applies the conditional introduction rule to 2 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.
  9. This leaves us with two possibilities to continue. Either we can keep working from the bottom up and look for another application of the conditional introduction rule, or we can work from the top down and apply a disjunction elimination rule. Let us apply the latter. We will use the assumption the disjunction of not A with B as the leftmost premise of disjunction elimination. For a valid application of disjunction elimination, the other two premises must be identical to the conclusion if A, then B, but each may be derived in turn from another assumption, namely one of the two disjuncts of the disjunction of not A with B. So our derivation will look like this:
  10. Derivation diagram 30
  11. Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumption not A, labeled two for discharge as a premise. Step 3 applies the subderivation to 2 and concludes if A, then B. Step 4 states assumption B, labeled two for discharge as a premise. Step 5 applies the subderivation to 4 and concludes if A, then B. Step 6 applies the disjunction elimination rule to 1, 3, 5 and concludes if A, then B. Step 7 applies the conditional introduction rule to 6 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.
  12. In each of the two branches on the right, we want to derive if A, then B, which is best done using conditional introduction.
  13. Derivation diagram 31
  14. Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumptions not A labeled two, and A labeled three, for discharge as a premise. Step 3 applies the subderivation to 2 and concludes formula B. Step 4 applies the conditional introduction rule to 3 and concludes if A, then B. Step 5 states assumptions B labeled two, and A labeled four, for discharge as a premise. Step 6 applies the subderivation to 5 and concludes formula B. Step 7 applies the conditional introduction rule to 6 and concludes if A, then B. Step 8 applies the disjunction elimination rule to 1, 4, 7 and concludes if A, then B. Step 9 applies the conditional introduction rule to 8 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.
  15. For the two missing parts of the derivation, we need derivations of formula B from not A and formula A in the middle, and from formula A and formula B on the left. Let's take the former first. not A and formula A are the two premises of negation elimination:
  16. Derivation diagram 32
  17. Step 1 states assumption not A, labeled two for discharge as a premise. Step 2 states assumption A, labeled three for discharge as a premise. Step 3 applies the negation elimination rule to 1, 2 and concludes a contradiction. Step 4 applies the subderivation to 3 and concludes formula B. The final conclusion is formula B.
  18. By using falsehood elimination, we can obtain formula B as a conclusion and complete the branch.
  19. Derivation diagram 33
  20. Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumption not A, labeled two for discharge as a premise. Step 3 states assumption A, labeled three for discharge as a premise. Step 4 applies the falsehood introduction rule to 2, 3 and concludes a contradiction. Step 5 applies the falsehood elimination rule to 4 and concludes formula B. Step 6 applies the conditional introduction rule to 5 and concludes if A, then B. Step 7 states assumptions B labeled two, and A labeled four, for discharge as a premise. Step 8 applies the subderivation to 7 and concludes formula B. Step 9 applies the conditional introduction rule to 8 and concludes if A, then B. Step 10 applies the disjunction elimination rule to 1, 6, 9 and concludes if A, then B. Step 11 applies the conditional introduction rule to 10 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.
  21. Let's now look at the rightmost branch. Here it's important to realize that the definition of derivation allows assumptions to be discharged but does not require them to be. In other words, if we can derive formula B from one of the assumptions formula A and formula B without using the other, that's ok. And to derive formula B from formula B is trivial: formula B by itself is such a derivation, and no inferences are needed. So we can simply delete the assumption formula A.
  22. Derivation diagram 34
  23. Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumption not A, labeled two for discharge as a premise. Step 3 states assumption A, labeled three for discharge as a premise. Step 4 applies the negation elimination rule to 2, 3 and concludes a contradiction. Step 5 applies the falsehood elimination rule to 4 and concludes formula B. Step 6 applies the conditional introduction rule to 5 and concludes if A, then B. Step 7 states assumption B, labeled two for discharge as a premise. Step 8 applies the conditional introduction rule to 7 and concludes if A, then B. Step 9 applies the disjunction elimination rule to 1, 6, 8 and concludes if A, then B. Step 10 applies the conditional introduction rule to 9 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.
  24. Note that in the finished derivation, the rightmost conditional introduction inference does not actually discharge any assumptions.

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 53.

Natural-deduction proof tree at proving-things.tex, line 71

Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes if A, then B. Step 3 applies the conditional introduction rule to 2 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

  1. Premise: projected-formula-0009361
  2. Subderivation conclusion: projected-formula-0009362
  3. conditional introduction rule: projected-formula-0009363

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 71.

Natural-deduction proof tree at proving-things.tex, line 86

Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumption not A, labeled two for discharge as a premise. Step 3 applies the subderivation to 2 and concludes if A, then B. Step 4 states assumption B, labeled two for discharge as a premise. Step 5 applies the subderivation to 4 and concludes if A, then B. Step 6 applies the disjunction elimination rule to 1, 3, 5 and concludes if A, then B. Step 7 applies the conditional introduction rule to 6 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

  1. Premise: projected-formula-0009367
  2. Premise: projected-formula-0009368
  3. Subderivation conclusion: projected-formula-0009369
  4. Premise: projected-formula-0009370
  5. Subderivation conclusion: projected-formula-0009371
  6. disjunction elimination rule: projected-formula-0009372
  7. conditional introduction rule: projected-formula-0009373

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 86.

Natural-deduction proof tree at proving-things.tex, line 100

Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumptions not A labeled two, and A labeled three, for discharge as a premise. Step 3 applies the subderivation to 2 and concludes formula B. Step 4 applies the conditional introduction rule to 3 and concludes if A, then B. Step 5 states assumptions B labeled two, and A labeled four, for discharge as a premise. Step 6 applies the subderivation to 5 and concludes formula B. Step 7 applies the conditional introduction rule to 6 and concludes if A, then B. Step 8 applies the disjunction elimination rule to 1, 4, 7 and concludes if A, then B. Step 9 applies the conditional introduction rule to 8 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

  1. Premise: projected-formula-0009375
  2. Premise: projected-formula-0009376
  3. Subderivation conclusion: projected-formula-0009377
  4. conditional introduction rule: projected-formula-0009378
  5. Premise: projected-formula-0009379
  6. Subderivation conclusion: projected-formula-0009380
  7. conditional introduction rule: projected-formula-0009381
  8. disjunction elimination rule: projected-formula-0009382
  9. conditional introduction rule: projected-formula-0009383

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 100.

Natural-deduction proof tree at proving-things.tex, line 120

Step 1 states assumption not A, labeled two for discharge as a premise. Step 2 states assumption A, labeled three for discharge as a premise. Step 3 applies the negation elimination rule to 1, 2 and concludes a contradiction. Step 4 applies the subderivation to 3 and concludes formula B. The final conclusion is formula B.

  1. Premise: projected-formula-0009391
  2. Premise: projected-formula-0009392
  3. negation elimination rule: projected-formula-0009393
  4. Subderivation conclusion: projected-formula-0009394

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 120.

Natural-deduction proof tree at proving-things.tex, line 129

Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumption not A, labeled two for discharge as a premise. Step 3 states assumption A, labeled three for discharge as a premise. Step 4 applies the falsehood introduction rule to 2, 3 and concludes a contradiction. Step 5 applies the falsehood elimination rule to 4 and concludes formula B. Step 6 applies the conditional introduction rule to 5 and concludes if A, then B. Step 7 states assumptions B labeled two, and A labeled four, for discharge as a premise. Step 8 applies the subderivation to 7 and concludes formula B. Step 9 applies the conditional introduction rule to 8 and concludes if A, then B. Step 10 applies the disjunction elimination rule to 1, 6, 9 and concludes if A, then B. Step 11 applies the conditional introduction rule to 10 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

  1. Premise: projected-formula-0009396
  2. Premise: projected-formula-0009397
  3. Premise: projected-formula-0009398
  4. falsehood introduction rule: projected-formula-0009399
  5. falsehood elimination rule: projected-formula-0009400
  6. conditional introduction rule: projected-formula-0009401
  7. Premise: projected-formula-0009402
  8. Subderivation conclusion: projected-formula-0009403
  9. conditional introduction rule: projected-formula-0009404
  10. disjunction elimination rule: projected-formula-0009405
  11. conditional introduction rule: projected-formula-0009406

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 129.

Natural-deduction proof tree at proving-things.tex, line 156

Step 1 states the single assumption that is the disjunction of not A with B, labeled one for discharge as a premise. Step 2 states assumption not A, labeled two for discharge as a premise. Step 3 states assumption A, labeled three for discharge as a premise. Step 4 applies the negation elimination rule to 2, 3 and concludes a contradiction. Step 5 applies the falsehood elimination rule to 4 and concludes formula B. Step 6 applies the conditional introduction rule to 5 and concludes if A, then B. Step 7 states assumption B, labeled two for discharge as a premise. Step 8 applies the conditional introduction rule to 7 and concludes if A, then B. Step 9 applies the disjunction elimination rule to 1, 6, 8 and concludes if A, then B. Step 10 applies the conditional introduction rule to 9 and concludes if either not A or B, then if A, then B. The final conclusion is if either not A or B, then if A, then B.

  1. Premise: projected-formula-0009414
  2. Premise: projected-formula-0009415
  3. Premise: projected-formula-0009416
  4. negation elimination rule: projected-formula-0009417
  5. falsehood elimination rule: projected-formula-0009418
  6. conditional introduction rule: projected-formula-0009419
  7. Premise: projected-formula-0009420
  8. conditional introduction rule: projected-formula-0009421
  9. disjunction elimination rule: projected-formula-0009422
  10. conditional introduction rule: projected-formula-0009423

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 156.

Example 4

Complete source-order listener rendering of this example; no claim or solution is added.

  1. Example 4
  2. So far we have not needed the classical contradiction rule. It is special in that it allows us to discharge an assumption that isn't a sub-formula of the conclusion of the rule. It is closely related to the falsehood elimination rule. In fact, the falsehood elimination rule is a special case of the classical contradiction rule—there is a logic called “intuitionistic logic” in which only falsehood elimination is allowed. The classical contradiction rule is a last resort when nothing else works. For instance, suppose we want to derive A or not A. Our usual strategy would be to attempt to derive A or not A using disjunction introduction rule. But this would require us to derive either formula A or not A from no assumptions, and this can't be done. classical contradiction to the rescue!
  3. Derivation diagram 35
  4. Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the classical contradiction rule to 2 and concludes A or not A. The final conclusion is A or not A.
  5. Now we're looking for a derivation of a contradiction from not the whole disjunction A or not A. Since a contradiction is the conclusion of negation elimination rule we might try that:
  6. Derivation diagram 36
  7. Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes not A. Step 3 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 4 applies the subderivation to 3 and concludes formula A. Step 5 applies the negation elimination rule to 2, 4 and concludes a contradiction. Step 6 applies the classical contradiction rule to 5 and concludes A or not A. The final conclusion is A or not A.
  8. Our strategy for finding a derivation of not A calls for an application of negation introduction rule:
  9. Derivation diagram 37
  10. Step 1 states two assumptions for discharge: the first denies the entire disjunction A or not A and is labeled one; the second is A and is labeled two as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the negation introduction rule to 2 and concludes not A. Step 4 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 5 applies the subderivation to 4 and concludes formula A. Step 6 applies the negation elimination rule to 3, 5 and concludes a contradiction. Step 7 applies the classical contradiction rule to 6 and concludes A or not A. The final conclusion is A or not A.
  11. Here, we can get a contradiction easily by applying negation elimination rule to the assumption not the whole disjunction A or not A and A or not A which follows from our new assumption formula A by disjunction introduction rule:
  12. Derivation diagram 38
  13. Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 states assumption A, labeled two for discharge as a premise. Step 3 applies the disjunction introduction rule to 2 and concludes A or not A. Step 4 applies the negation elimination rule to 1, 3 and concludes a contradiction. Step 5 applies the negation introduction rule to 4 and concludes not A. Step 6 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 7 applies the subderivation to 6 and concludes formula A. Step 8 applies the negation elimination rule to 5, 7 and concludes a contradiction. Step 9 applies the classical contradiction rule to 8 and concludes A or not A. The final conclusion is A or not A.
  14. On the right side we use the same strategy, except we get formula A by classical contradiction:
  15. Derivation diagram 39
  16. Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 states assumption A, labeled two for discharge as a premise. Step 3 applies the disjunction introduction rule to 2 and concludes A or not A. Step 4 applies the negation elimination rule to 1, 3 and concludes a contradiction. Step 5 applies the negation introduction rule to 4 and concludes not A. Step 6 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 7 states assumption not A, labeled three for discharge as a premise. Step 8 applies the disjunction introduction rule to 7 and concludes A or not A. Step 9 applies the negation elimination rule to 6, 8 and concludes a contradiction. Step 10 applies the classical contradiction rule to 9 and concludes formula A. Step 11 applies the negation elimination rule to 5, 10 and concludes a contradiction. Step 12 applies the classical contradiction rule to 11 and concludes A or not A. The final conclusion is A or not A.

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 178.

Natural-deduction proof tree at proving-things.tex, line 190

Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the classical contradiction rule to 2 and concludes A or not A. The final conclusion is A or not A.

  1. Premise: projected-formula-0009429
  2. Subderivation conclusion: projected-formula-0009430
  3. classical contradiction rule: projected-formula-0009431

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 190.

Natural-deduction proof tree at proving-things.tex, line 199

Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes not A. Step 3 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 4 applies the subderivation to 3 and concludes formula A. Step 5 applies the negation elimination rule to 2, 4 and concludes a contradiction. Step 6 applies the classical contradiction rule to 5 and concludes A or not A. The final conclusion is A or not A.

  1. Premise: projected-formula-0009436
  2. Subderivation conclusion: projected-formula-0009437
  3. Premise: projected-formula-0009438
  4. Subderivation conclusion: projected-formula-0009439
  5. negation elimination rule: projected-formula-0009440
  6. classical contradiction rule: projected-formula-0009441

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 199.

Natural-deduction proof tree at proving-things.tex, line 211

Step 1 states two assumptions for discharge: the first denies the entire disjunction A or not A and is labeled one; the second is A and is labeled two as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the negation introduction rule to 2 and concludes not A. Step 4 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 5 applies the subderivation to 4 and concludes formula A. Step 6 applies the negation elimination rule to 3, 5 and concludes a contradiction. Step 7 applies the classical contradiction rule to 6 and concludes A or not A. The final conclusion is A or not A.

  1. Premise: projected-formula-0009444
  2. Subderivation conclusion: projected-formula-0009445
  3. negation introduction rule: projected-formula-0009446
  4. Premise: projected-formula-0009447
  5. Subderivation conclusion: projected-formula-0009448
  6. negation elimination rule: projected-formula-0009449
  7. classical contradiction rule: projected-formula-0009450

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 211.

Natural-deduction proof tree at proving-things.tex, line 226

Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 states assumption A, labeled two for discharge as a premise. Step 3 applies the disjunction introduction rule to 2 and concludes A or not A. Step 4 applies the negation elimination rule to 1, 3 and concludes a contradiction. Step 5 applies the negation introduction rule to 4 and concludes not A. Step 6 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 7 applies the subderivation to 6 and concludes formula A. Step 8 applies the negation elimination rule to 5, 7 and concludes a contradiction. Step 9 applies the classical contradiction rule to 8 and concludes A or not A. The final conclusion is A or not A.

  1. Premise: projected-formula-0009457
  2. Premise: projected-formula-0009458
  3. disjunction introduction rule: projected-formula-0009459
  4. negation elimination rule: projected-formula-0009460
  5. negation introduction rule: projected-formula-0009461
  6. Premise: projected-formula-0009462
  7. Subderivation conclusion: projected-formula-0009463
  8. negation elimination rule: projected-formula-0009464
  9. classical contradiction rule: projected-formula-0009465

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 226.

Natural-deduction proof tree at proving-things.tex, line 243

Step 1 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 2 states assumption A, labeled two for discharge as a premise. Step 3 applies the disjunction introduction rule to 2 and concludes A or not A. Step 4 applies the negation elimination rule to 1, 3 and concludes a contradiction. Step 5 applies the negation introduction rule to 4 and concludes not A. Step 6 states assumption denying the whole disjunction A or not A, labeled one for discharge as a premise. Step 7 states assumption not A, labeled three for discharge as a premise. Step 8 applies the disjunction introduction rule to 7 and concludes A or not A. Step 9 applies the negation elimination rule to 6, 8 and concludes a contradiction. Step 10 applies the classical contradiction rule to 9 and concludes formula A. Step 11 applies the negation elimination rule to 5, 10 and concludes a contradiction. Step 12 applies the classical contradiction rule to 11 and concludes A or not A. The final conclusion is A or not A.

  1. Premise: projected-formula-0009467
  2. Premise: projected-formula-0009468
  3. disjunction introduction rule: projected-formula-0009469
  4. negation elimination rule: projected-formula-0009470
  5. negation introduction rule: projected-formula-0009471
  6. Premise: projected-formula-0009472
  7. Premise: projected-formula-0009473
  8. disjunction introduction rule: projected-formula-0009474
  9. negation elimination rule: projected-formula-0009475
  10. classical contradiction rule: projected-formula-0009476
  11. negation elimination rule: projected-formula-0009477
  12. classical contradiction rule: projected-formula-0009478

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 243.

Problem 1

Complete source-order listener rendering of this exercise; no claim or solution is added.

Unsolved source exercise; no solution added.

  1. Problem 1
  2. Give derivations that show the following:
  3. Item 1.
  4. from the single conjunctive premise whose left conjunct is A and whose right conjunct is the conjunction of B and C, derive the conjunction of A and B, conjoined with C.
  5. Item 2.
  6. from the disjunction whose left disjunct is A and whose right disjunct is the disjunction B or C, derive the disjunction whose left disjunct is A or B and whose right disjunct is C.
  7. Item 3.
  8. from if A then if B then C, derive: if B then if A then C.
  9. Item 4.
  10. from A, derive not not A.

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 267.

Problem 2

Complete source-order listener rendering of this exercise; no claim or solution is added.

Unsolved source exercise; no solution added.

  1. Problem 2
  2. Give derivations that show the following:
  3. Item 1.
  4. from if A or B then C, derive: if A then C.
  5. Item 2.
  6. from the conjunction of the conditional from A to C with the conditional from B to C, derive the conditional from the disjunction A or B to C.
  7. Item 3.
  8. without undischarged assumptions, derive not both A and not A.
  9. Item 4.
  10. from if B then A, derive: if not A then not B.
  11. Item 5.
  12. without undischarged assumptions, derive: if the conditional from A to not A holds, then not A.
  13. Item 6.
  14. without undischarged assumptions, derive: if it is not the case that A implies B, then not B.
  15. Item 7.
  16. from if A then C, derive not both A and not C.
  17. Item 8.
  18. from the conjunction of A with not C, derive that it is not the case that if A then C.
  19. Item 9.
  20. from A or B, together with not B, derive A.
  21. Item 10.
  22. from the disjunction of not A with not B, derive not both A and B.
  23. Item 11.
  24. without undischarged assumptions, derive: if both not A and not B, then it is not the case that A or B.
  25. Item 12.
  26. without undischarged assumptions, derive: if it is not the case that A or B, then both not A and not B.

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 277.

Problem 3

Complete source-order listener rendering of this exercise; no claim or solution is added.

Unsolved source exercise; no solution added.

  1. Problem 3
  2. Give derivations that show the following:
  3. Item 1.
  4. from the negation of if A then B, derive A.
  5. Item 2.
  6. from not both A and B, derive the disjunction of not A with not B.
  7. Item 3.
  8. from the conditional if A then B, derive the disjunction of not A with B.
  9. Item 4.
  10. without undischarged assumptions, derive: if not not A, then A.
  11. Item 5.
  12. from two separate premises, the conditional from A to B and the conditional from not A to B, derive B.
  13. Item 6.
  14. from if A and B then C, derive either if A then C or if B then C.
  15. Item 7.
  16. from the conditional whose antecedent is the conditional from A to B and whose consequent is A, derive A.
  17. Item 8.
  18. without undischarged assumptions, derive either if A then B or if B then C.
  19. (These all require the classical absurdity rule.)

Source: content/first-order-logic/natural-deduction/proving-things.tex, line 295.

Example 5

Complete source-order listener rendering of this example; no claim or solution is added.

  1. Example 5
  2. When dealing with quantifiers, we have to make sure not to violate the eigenvariable condition, and sometimes this requires us to play around with the order of carrying out certain inferences. In general, it helps to try and take care of rules subject to the eigenvariable condition first (they will be lower down in the finished proof).
  3. Let's see how we'd give a derivation of the formula if there exists an x such that not A of x, then it is not the case that, for every x, A of x. Starting as usual, we write
  4. Derivation diagram 40
  5. Step 1 has no printed premise. Step 2 applies the inference rule to 1 and concludes if there exists an x such that not A of x, then it is not the case that, for every x, A of x. The final conclusion is if there exists an x such that not A of x, then it is not the case that, for every x, A of x.
  6. We start by writing down what it would take to justify that last step using the conditional introduction rule.
  7. Derivation diagram 41
  8. Step 1 states assumption: there exists an x such that not A of x; labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes it is not the case that, for every x, A of x. Step 3 applies the conditional introduction rule to 2 and concludes if there exists an x such that not A of x, then it is not the case that, for every x, A of x. The final conclusion is if there exists an x such that not A of x, then it is not the case that, for every x, A of x.
  9. Since there is no obvious rule to apply to it is not the case that, for every x, A of x, we will proceed by setting up the derivation so we can use the existential quantifier elimination rule. Here we must pay attention to the eigenvariable condition, and choose a constant that does not appear in there exists an x such that A of x or any assumptions that it depends on. (Since no constant symbols appear, however, any choice will do fine.)
  10. Derivation diagram 42
  11. Step 1 states assumption: there exists an x such that not A of x; labeled one for discharge as a premise. Step 2 states assumption not A of a, labeled two for discharge as a premise. Step 3 applies the subderivation to 2 and concludes it is not the case that, for every x, A of x. Step 4 applies the existential quantifier elimination rule to 1, 3 and concludes it is not the case that, for every x, A of x. Step 5 applies the conditional introduction rule to 4 and concludes if there exists an x such that not A of x, then it is not the case that, for every x, A of x. The final conclusion is if there exists an x such that not A of x, then it is not the case that, for every x, A of x.
  12. In order to derive it is not the case that, for every x, A of x, we will attempt to use the negation introduction rule: this requires that we derive a contradiction, possibly using for every x, A of x as an additional assumption. Of course, this contradiction may involve the assumption not A of a which will be discharged by the existential quantifier elimination inference. We can set it up as follows:
  13. Derivation diagram 43
  14. Step 1 states assumption: there exists an x such that not A of x; labeled one for discharge as a premise. Step 2 states assumptions not A of a labeled two, and for every x, A of x labeled three, for discharge as a premise. Step 3 applies the subderivation to 2 and concludes a contradiction. Step 4 applies the negation introduction rule to 3 and concludes it is not the case that, for every x, A of x. Step 5 applies the existential quantifier elimination rule to 1, 4 and concludes it is not the case that, for every x, A of x. Step 6 applies the conditional introduction rule to 5 and concludes if there exists an x such that not A of x, then it is not the case that, for every x, A of x. The final conclusion is if there exists an x such that not A of x, then it is not the case that, for every x, A of x.
  15. It looks like we are close to getting a contradiction. The easiest rule to apply is the universal quantifier elimination, which has no eigenvariable conditions. Since we can use any term we want to replace the universally quantified x, it makes the most sense to continue using the name a so we can reach a contradiction.
  16. Derivation diagram 44
  17. Step 1 states assumption: there exists an x such that not A of x; labeled one for discharge as a premise. Step 2 states assumption not A of a, labeled two for discharge as a premise. Step 3 states assumption: for every x, A of x; labeled three for discharge as a premise. Step 4 applies the universal quantifier elimination rule to 3 and concludes A of a. Step 5 applies the negation elimination rule to 2, 4 and concludes a contradiction. Step 6 applies the negation introduction rule to 5 and concludes it is not the case that, for every x, A of x. Step 7 applies the existential quantifier elimination rule to 1, 6 and concludes it is not the case that, for every x, A of x. Step 8 applies the conditional introduction rule to 7 and concludes if there exists an x such that not A of x, then it is not the case that, for every x, A of x. The final conclusion is if there exists an x such that not A of x, then it is not the case that, for every x, A of x.
  18. It is important, especially when dealing with quantifiers, to double check at this point that the eigenvariable condition has not been violated. Since the only rule we applied that is subject to the eigenvariable condition was existential quantifier elimination rule, and the eigenvariable the name a does not occur in any assumptions it depends on, this is a correct derivation.

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 13.

Natural-deduction proof tree at proving-things-quant.tex, line 29

Step 1 states assumption: there exists an x such that not A of x; labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes it is not the case that, for every x, A of x. Step 3 applies the conditional introduction rule to 2 and concludes if there exists an x such that not A of x, then it is not the case that, for every x, A of x. The final conclusion is if there exists an x such that not A of x, then it is not the case that, for every x, A of x.

  1. Premise: projected-formula-0009506
  2. Subderivation conclusion: projected-formula-0009507
  3. conditional introduction rule: projected-formula-0009508

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 29.

Natural-deduction proof tree at proving-things-quant.tex, line 41

Step 1 states assumption: there exists an x such that not A of x; labeled one for discharge as a premise. Step 2 states assumption not A of a, labeled two for discharge as a premise. Step 3 applies the subderivation to 2 and concludes it is not the case that, for every x, A of x. Step 4 applies the existential quantifier elimination rule to 1, 3 and concludes it is not the case that, for every x, A of x. Step 5 applies the conditional introduction rule to 4 and concludes if there exists an x such that not A of x, then it is not the case that, for every x, A of x. The final conclusion is if there exists an x such that not A of x, then it is not the case that, for every x, A of x.

  1. Premise: projected-formula-0009511
  2. Premise: projected-formula-0009512
  3. Subderivation conclusion: projected-formula-0009513
  4. existential quantifier elimination rule: projected-formula-0009514
  5. conditional introduction rule: projected-formula-0009515

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 41.

Natural-deduction proof tree at proving-things-quant.tex, line 56

Step 1 states assumption: there exists an x such that not A of x; labeled one for discharge as a premise. Step 2 states assumptions not A of a labeled two, and for every x, A of x labeled three, for discharge as a premise. Step 3 applies the subderivation to 2 and concludes a contradiction. Step 4 applies the negation introduction rule to 3 and concludes it is not the case that, for every x, A of x. Step 5 applies the existential quantifier elimination rule to 1, 4 and concludes it is not the case that, for every x, A of x. Step 6 applies the conditional introduction rule to 5 and concludes if there exists an x such that not A of x, then it is not the case that, for every x, A of x. The final conclusion is if there exists an x such that not A of x, then it is not the case that, for every x, A of x.

  1. Premise: projected-formula-0009519
  2. Premise: projected-formula-0009520
  3. Subderivation conclusion: projected-formula-0009521
  4. negation introduction rule: projected-formula-0009522
  5. existential quantifier elimination rule: projected-formula-0009523
  6. conditional introduction rule: projected-formula-0009524

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 56.

Natural-deduction proof tree at proving-things-quant.tex, line 72

Step 1 states assumption: there exists an x such that not A of x; labeled one for discharge as a premise. Step 2 states assumption not A of a, labeled two for discharge as a premise. Step 3 states assumption: for every x, A of x; labeled three for discharge as a premise. Step 4 applies the universal quantifier elimination rule to 3 and concludes A of a. Step 5 applies the negation elimination rule to 2, 4 and concludes a contradiction. Step 6 applies the negation introduction rule to 5 and concludes it is not the case that, for every x, A of x. Step 7 applies the existential quantifier elimination rule to 1, 6 and concludes it is not the case that, for every x, A of x. Step 8 applies the conditional introduction rule to 7 and concludes if there exists an x such that not A of x, then it is not the case that, for every x, A of x. The final conclusion is if there exists an x such that not A of x, then it is not the case that, for every x, A of x.

  1. Premise: projected-formula-0009527
  2. Premise: projected-formula-0009528
  3. Premise: projected-formula-0009529
  4. universal quantifier elimination rule: projected-formula-0009530
  5. negation elimination rule: projected-formula-0009531
  6. negation introduction rule: projected-formula-0009532
  7. existential quantifier elimination rule: projected-formula-0009533
  8. conditional introduction rule: projected-formula-0009534

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 72.

Example 6

Complete source-order listener rendering of this example; no claim or solution is added.

  1. Example 6
  2. Sometimes we may derive a formula from other formulas. In these cases, we may have undischarged assumptions. It is important to keep track of our assumptions as well as the end goal.
  3. Let's see how we'd give a derivation of the formula there exists an x such that C of x and b from the assumptions there exists an x such that both A of x and B of x and for every x, if B of x, then C of x and b. Starting as usual, we write the conclusion at the bottom.
  4. Derivation diagram 45
  5. Step 1 has no printed premise. Step 2 applies the inference rule to 1 and concludes there exists an x such that C of x and b. The final conclusion is there exists an x such that C of x and b.
  6. We have two premises to work with. To use the first, i.e., try to find a derivation of there exists an x such that C of x and b from there exists an x such that both A of x and B of x we would use the existential quantifier elimination rule. Since it has an eigenvariable condition, we will apply that rule first. We get the following:
  7. Derivation diagram 46
  8. Step 1 states there exists an x such that both A of x and B of x as a premise. Step 2 states the single assumption that is the conjunction of A of a and B of a, labeled one for discharge as a premise. Step 3 applies the subderivation to 2 and concludes there exists an x such that C of x and b. Step 4 applies the existential quantifier elimination rule to 1, 3 and concludes there exists an x such that C of x and b. The final conclusion is there exists an x such that C of x and b.
  9. The two assumptions we are working with share formula B. It may be useful at this point to apply conjunction elimination to separate out B of a.
  10. Derivation diagram 47
  11. Step 1 states there exists an x such that both A of x and B of x as a premise. Step 2 states the single assumption that is the conjunction of A of a and B of a, labeled one for discharge as a premise. Step 3 applies the conjunction elimination rule to 2 and concludes B of a. Step 4 applies the subderivation to 3 and concludes there exists an x such that C of x and b. Step 5 applies the existential quantifier elimination rule to 1, 4 and concludes there exists an x such that C of x and b. The final conclusion is there exists an x such that C of x and b.
  12. The second assumption we have to work with is for every x, if B of x, then C of x and b. Since there is no eigenvariable condition we can instantiate x with the constant symbol the name a using universal quantifier elimination to get if B of a, then C of a and b. We now have both if B of a, then C of a and b and B of a. Our next move should be a straightforward application of the conditional elimination rule.
  13. Derivation diagram 48
  14. Step 1 states there exists an x such that both A of x and B of x as a premise. Step 2 states for every x, if B of x, then C of x and b as a premise. Step 3 applies the universal quantifier elimination rule to 2 and concludes if B of a, then C of a and b. Step 4 states the single assumption that is the conjunction of A of a and B of a, labeled one for discharge as a premise. Step 5 applies the conjunction elimination rule to 4 and concludes B of a. Step 6 applies the conditional elimination rule to 3, 5 and concludes C of a and b. Step 7 applies the subderivation to 6 and concludes there exists an x such that C of x and b. Step 8 applies the existential quantifier elimination rule to 1, 7 and concludes there exists an x such that C of x and b. The final conclusion is there exists an x such that C of x and b.
  15. We are so close! One application of existential quantifier introduction and we have reached our goal.
  16. Derivation diagram 49
  17. Step 1 states there exists an x such that both A of x and B of x as a premise. Step 2 states for every x, if B of x, then C of x and b as a premise. Step 3 applies the universal quantifier elimination rule to 2 and concludes if B of a, then C of a and b. Step 4 states the single assumption that is the conjunction of A of a and B of a, labeled one for discharge as a premise. Step 5 applies the conjunction elimination rule to 4 and concludes B of a. Step 6 applies the conditional elimination rule to 3, 5 and concludes C of a and b. Step 7 applies the existential quantifier introduction rule to 6 and concludes there exists an x such that C of x and b. Step 8 applies the existential quantifier elimination rule to 1, 7 and concludes there exists an x such that C of x and b. The final conclusion is there exists an x such that C of x and b.
  18. Since we ensured at each step that the eigenvariable conditions were not violated, we can be confident that this is a correct derivation.

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 96.

Natural-deduction proof tree at proving-things-quant.tex, line 117

Step 1 states there exists an x such that both A of x and B of x as a premise. Step 2 states the single assumption that is the conjunction of A of a and B of a, labeled one for discharge as a premise. Step 3 applies the subderivation to 2 and concludes there exists an x such that C of x and b. Step 4 applies the existential quantifier elimination rule to 1, 3 and concludes there exists an x such that C of x and b. The final conclusion is there exists an x such that C of x and b.

  1. Premise: projected-formula-0009542
  2. Premise: projected-formula-0009543
  3. Subderivation conclusion: projected-formula-0009544
  4. existential quantifier elimination rule: projected-formula-0009545

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 117.

Natural-deduction proof tree at proving-things-quant.tex, line 126

Step 1 states there exists an x such that both A of x and B of x as a premise. Step 2 states the single assumption that is the conjunction of A of a and B of a, labeled one for discharge as a premise. Step 3 applies the conjunction elimination rule to 2 and concludes B of a. Step 4 applies the subderivation to 3 and concludes there exists an x such that C of x and b. Step 5 applies the existential quantifier elimination rule to 1, 4 and concludes there exists an x such that C of x and b. The final conclusion is there exists an x such that C of x and b.

  1. Premise: projected-formula-0009548
  2. Premise: projected-formula-0009549
  3. conjunction elimination rule: projected-formula-0009550
  4. Subderivation conclusion: projected-formula-0009551
  5. existential quantifier elimination rule: projected-formula-0009552

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 126.

Natural-deduction proof tree at proving-things-quant.tex, line 143

Step 1 states there exists an x such that both A of x and B of x as a premise. Step 2 states for every x, if B of x, then C of x and b as a premise. Step 3 applies the universal quantifier elimination rule to 2 and concludes if B of a, then C of a and b. Step 4 states the single assumption that is the conjunction of A of a and B of a, labeled one for discharge as a premise. Step 5 applies the conjunction elimination rule to 4 and concludes B of a. Step 6 applies the conditional elimination rule to 3, 5 and concludes C of a and b. Step 7 applies the subderivation to 6 and concludes there exists an x such that C of x and b. Step 8 applies the existential quantifier elimination rule to 1, 7 and concludes there exists an x such that C of x and b. The final conclusion is there exists an x such that C of x and b.

  1. Premise: projected-formula-0009559
  2. Premise: projected-formula-0009560
  3. universal quantifier elimination rule: projected-formula-0009561
  4. Premise: projected-formula-0009562
  5. conjunction elimination rule: projected-formula-0009563
  6. conditional elimination rule: projected-formula-0009564
  7. Subderivation conclusion: projected-formula-0009565
  8. existential quantifier elimination rule: projected-formula-0009566

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 143.

Natural-deduction proof tree at proving-things-quant.tex, line 161

Step 1 states there exists an x such that both A of x and B of x as a premise. Step 2 states for every x, if B of x, then C of x and b as a premise. Step 3 applies the universal quantifier elimination rule to 2 and concludes if B of a, then C of a and b. Step 4 states the single assumption that is the conjunction of A of a and B of a, labeled one for discharge as a premise. Step 5 applies the conjunction elimination rule to 4 and concludes B of a. Step 6 applies the conditional elimination rule to 3, 5 and concludes C of a and b. Step 7 applies the existential quantifier introduction rule to 6 and concludes there exists an x such that C of x and b. Step 8 applies the existential quantifier elimination rule to 1, 7 and concludes there exists an x such that C of x and b. The final conclusion is there exists an x such that C of x and b.

  1. Premise: projected-formula-0009567
  2. Premise: projected-formula-0009568
  3. universal quantifier elimination rule: projected-formula-0009569
  4. Premise: projected-formula-0009570
  5. conjunction elimination rule: projected-formula-0009571
  6. conditional elimination rule: projected-formula-0009572
  7. existential quantifier introduction rule: projected-formula-0009573
  8. existential quantifier elimination rule: projected-formula-0009574

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 161.

Example 7

Complete source-order listener rendering of this example; no claim or solution is added.

  1. Example 7
  2. Give a derivation of the formula it is not the case that, for every x, A of x from the assumptions if, for every x, A of x, then there exists a y such that B of y and it is not the case that there exists a y such that B of y. Starting as usual, we write the target formula at the bottom.
  3. Derivation diagram 50
  4. Step 1 has no printed premise. Step 2 applies the inference rule to 1 and concludes it is not the case that, for every x, A of x. The final conclusion is it is not the case that, for every x, A of x.
  5. The last line of the derivation is a negation, so let's try using negation introduction. This will require that we figure out how to derive a contradiction.
  6. Derivation diagram 51
  7. Step 1 states assumption: for every x, A of x; labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the negation introduction rule to 2 and concludes it is not the case that, for every x, A of x. The final conclusion is it is not the case that, for every x, A of x.
  8. So far so good. We can use universal quantifier elimination but it's not obvious if that will help us get to our goal. Instead, let's use one of our assumptions. if, for every x, A of x, then there exists a y such that B of y together with for every x, A of x will allow us to use the conditional elimination rule.
  9. Derivation diagram 52
  10. Step 1 states if, for every x, A of x, then there exists a y such that B of y as a premise. Step 2 states assumption: for every x, A of x; labeled one for discharge as a premise. Step 3 applies the conditional elimination rule to 1, 2 and concludes there exists a y such that B of y. Step 4 applies the subderivation to 3 and concludes a contradiction. Step 5 applies the negation introduction rule to 4 and concludes it is not the case that, for every x, A of x. The final conclusion is it is not the case that, for every x, A of x.
  11. We now have one final assumption to work with, and it looks like this will help us reach a contradiction by using negation elimination.
  12. Derivation diagram 53
  13. Step 1 states it is not the case that there exists a y such that B of y as a premise. Step 2 states if, for every x, A of x, then there exists a y such that B of y as a premise. Step 3 states assumption: for every x, A of x; labeled one for discharge as a premise. Step 4 applies the conditional elimination rule to 2, 3 and concludes there exists a y such that B of y. Step 5 applies the negation elimination rule to 1, 4 and concludes a contradiction. Step 6 applies the negation introduction rule to 5 and concludes it is not the case that, for every x, A of x. The final conclusion is it is not the case that, for every x, A of x.

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 183.

Natural-deduction proof tree at proving-things-quant.tex, line 195

Step 1 states assumption: for every x, A of x; labeled one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a contradiction. Step 3 applies the negation introduction rule to 2 and concludes it is not the case that, for every x, A of x. The final conclusion is it is not the case that, for every x, A of x.

  1. Premise: projected-formula-0009579
  2. Subderivation conclusion: projected-formula-0009580
  3. negation introduction rule: projected-formula-0009581

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 195.

Natural-deduction proof tree at proving-things-quant.tex, line 205

Step 1 states if, for every x, A of x, then there exists a y such that B of y as a premise. Step 2 states assumption: for every x, A of x; labeled one for discharge as a premise. Step 3 applies the conditional elimination rule to 1, 2 and concludes there exists a y such that B of y. Step 4 applies the subderivation to 3 and concludes a contradiction. Step 5 applies the negation introduction rule to 4 and concludes it is not the case that, for every x, A of x. The final conclusion is it is not the case that, for every x, A of x.

  1. Premise: projected-formula-0009584
  2. Premise: projected-formula-0009585
  3. conditional elimination rule: projected-formula-0009586
  4. Subderivation conclusion: projected-formula-0009587
  5. negation introduction rule: projected-formula-0009588

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 205.

Natural-deduction proof tree at proving-things-quant.tex, line 217

Step 1 states it is not the case that there exists a y such that B of y as a premise. Step 2 states if, for every x, A of x, then there exists a y such that B of y as a premise. Step 3 states assumption: for every x, A of x; labeled one for discharge as a premise. Step 4 applies the conditional elimination rule to 2, 3 and concludes there exists a y such that B of y. Step 5 applies the negation elimination rule to 1, 4 and concludes a contradiction. Step 6 applies the negation introduction rule to 5 and concludes it is not the case that, for every x, A of x. The final conclusion is it is not the case that, for every x, A of x.

  1. Premise: projected-formula-0009589
  2. Premise: projected-formula-0009590
  3. Premise: projected-formula-0009591
  4. conditional elimination rule: projected-formula-0009592
  5. negation elimination rule: projected-formula-0009593
  6. negation introduction rule: projected-formula-0009594

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 217.

Problem 4

Complete source-order listener rendering of this exercise; no claim or solution is added.

Unsolved source exercise; no solution added.

  1. Problem 4
  2. Give derivations that show the following:
  3. Item 1.
  4. without undischarged assumptions, derive: if every x is A and every y is B, then every z is both A and B.
  5. Item 2.
  6. without undischarged assumptions, derive: if either some x is A or some y is B, then there exists a z that is A or B.
  7. Item 3.
  8. from: for every x, if A of x then B; derive: if there exists a y such that A of y, then B.
  9. Item 4.
  10. from: for every x, not A of x; derive: it is not the case that there exists an x such that A of x.
  11. Item 5.
  12. without undischarged assumptions, derive: if no x is A, then every x is not A.
  13. Item 6.
  14. without undischarged assumptions, derive that there is no x such that, for every y, both conditional directions hold: first, if A holds with x as its first argument and y as its second argument, then A does not hold with y as its first argument and y as its second argument; second, if A does not hold with y as its first argument and y as its second argument, then A holds with x as its first argument and y as its second argument.

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 230.

Problem 5

Complete source-order listener rendering of this exercise; no claim or solution is added.

Unsolved source exercise; no solution added.

  1. Problem 5
  2. Give derivations that show the following:
  3. Item 1.
  4. without undischarged assumptions, derive: if not every x is A, then there exists an x such that not A of x.
  5. Item 2.
  6. from: if every x is A, then B; derive that there exists a y such that, if A of y, then B.
  7. Item 3.
  8. without undischarged assumptions, derive that there exists an x such that, if A of x, then every y is A.
  9. (These all require the classical absurdity rule.)

Source: content/first-order-logic/natural-deduction/proving-things-quant.tex, line 245.

Definition 10: Theorems

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Definition 10: Theorems
  2. A sentence formula A is a theorem if there is a derivation of formula A in natural deduction in which all assumptions are discharged. We write A is derivable without undischarged assumptions if formula A is a theorem and A is not derivable without undischarged assumptions if it is not.

Source: content/first-order-logic/natural-deduction/proof-theoretic-notions.tex, line 32.

Definition 11: Derivability

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Definition 11: Derivability
  2. A Sentence formula A is derivable from a set of sentences Gamma, Gamma syntactically derives A, if there is a derivation with conclusion formula A and in which every assumption is either discharged or is in Gamma. If formula A is not derivable from Gamma we write Gamma does not syntactically derive A.

Source: content/first-order-logic/natural-deduction/proof-theoretic-notions.tex, line 39.

Natural-deduction proof tree at proof-theoretic-notions.tex, line 87

Step 1 states capital Delta together with assumption A, labeled one for discharge as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes formula B. Step 4 applies the conditional introduction rule to 3 and concludes if A, then B. Step 5 states Gamma as a premise. Step 6 labels the subderivation derivation delta zero. Step 7 applies the subderivation to 5 and concludes formula A. Step 8 applies the conditional elimination rule to 4, 7 and concludes formula B. The final conclusion is formula B.

  1. Premise: projected-formula-0009646
  2. Subderivation label: projected-formula-0009647
  3. Subderivation conclusion: projected-formula-0009648
  4. conditional introduction rule: projected-formula-0009649
  5. Premise: projected-formula-0009650
  6. Subderivation label: projected-formula-0009651
  7. Subderivation conclusion: projected-formula-0009652
  8. conditional elimination rule: projected-formula-0009653

Source: content/first-order-logic/natural-deduction/proof-theoretic-notions.tex, line 87.

Natural-deduction proof tree at provability-consistency.tex, line 28

Step 1 states the assumptions in Gamma, together with assumption A labeled one for discharge as a premise. Step 2 labels the subderivation delta two. Step 3 applies the subderivation to 1 and concludes a contradiction. Step 4 applies the negation introduction rule to 3 and concludes not A. Step 5 states Gamma as a premise. Step 6 labels the subderivation delta one. Step 7 applies the subderivation to 5 and concludes formula A. Step 8 applies the negation elimination rule to 4, 7 and concludes a contradiction. The final conclusion is a contradiction.

  1. Premise: projected-formula-0009699
  2. Subderivation label: projected-formula-0009700
  3. Subderivation conclusion: projected-formula-0009701
  4. negation introduction rule: projected-formula-0009702
  5. Premise: projected-formula-0009703
  6. Subderivation label: projected-formula-0009704
  7. Subderivation conclusion: projected-formula-0009705
  8. negation elimination rule: projected-formula-0009706

Source: content/first-order-logic/natural-deduction/provability-consistency.tex, line 28.

Natural-deduction proof tree at provability-consistency.tex, line 54

Step 1 states not A as a premise. Step 2 states Gamma as a premise. Step 3 labels the subderivation derivation delta zero. Step 4 applies the subderivation to 2 and concludes formula A. Step 5 applies the negation elimination rule to 1, 4 and concludes a contradiction. The final conclusion is a contradiction.

  1. Premise: projected-formula-0009717
  2. Premise: projected-formula-0009718
  3. Subderivation label: projected-formula-0009719
  4. Subderivation conclusion: projected-formula-0009720
  5. negation elimination rule: projected-formula-0009721

Source: content/first-order-logic/natural-deduction/provability-consistency.tex, line 54.

Natural-deduction proof tree at provability-consistency.tex, line 67

Step 1 states the assumptions in Gamma, together with assumption not A labeled one for discharge as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes a contradiction. Step 4 applies the classical contradiction rule to 3 and concludes formula A. The final conclusion is formula A.

  1. Premise: projected-formula-0009729
  2. Subderivation label: projected-formula-0009730
  3. Subderivation conclusion: projected-formula-0009731
  4. classical contradiction rule: projected-formula-0009732

Source: content/first-order-logic/natural-deduction/provability-consistency.tex, line 67.

Natural-deduction proof tree at provability-consistency.tex, line 91

Step 1 states not A as a premise. Step 2 states Gamma as a premise. Step 3 labels the subderivation delta. Step 4 applies the subderivation to 2 and concludes formula A. Step 5 applies the negation elimination rule to 1, 4 and concludes a contradiction. The final conclusion is a contradiction.

  1. Premise: projected-formula-0009744
  2. Premise: projected-formula-0009745
  3. Subderivation label: projected-formula-0009746
  4. Subderivation conclusion: projected-formula-0009747
  5. negation elimination rule: projected-formula-0009748

Source: content/first-order-logic/natural-deduction/provability-consistency.tex, line 91.

Natural-deduction proof tree at provability-consistency.tex, line 112

Step 1 states the assumptions in Gamma, together with assumption not A labeled two for discharge as a premise. Step 2 labels the subderivation delta two. Step 3 applies the subderivation to 1 and concludes a contradiction. Step 4 applies the negation introduction rule to 3 and concludes not not A. Step 5 states the assumptions in Gamma, together with assumption A labeled one for discharge as a premise. Step 6 labels the subderivation delta one. Step 7 applies the subderivation to 5 and concludes a contradiction. Step 8 applies the negation introduction rule to 7 and concludes not A. Step 9 applies the negation elimination rule to 4, 8 and concludes a contradiction. The final conclusion is a contradiction.

  1. Premise: projected-formula-0009761
  2. Subderivation label: projected-formula-0009762
  3. Subderivation conclusion: projected-formula-0009763
  4. negation introduction rule: projected-formula-0009764
  5. Premise: projected-formula-0009765
  6. Subderivation label: projected-formula-0009766
  7. Subderivation conclusion: projected-formula-0009767
  8. negation introduction rule: projected-formula-0009768
  9. negation elimination rule: projected-formula-0009769

Source: content/first-order-logic/natural-deduction/provability-consistency.tex, line 112.

Natural-deduction proof tree at provability-propositional.tex, line 67

Step 1 states A or B as a premise. Step 2 states not A as a premise. Step 3 states assumption A labeled one for discharge as a premise. Step 4 applies the negation elimination rule to 2, 3 and concludes a contradiction. Step 5 states not B as a premise. Step 6 states assumption B labeled one for discharge as a premise. Step 7 applies the negation elimination rule to 5, 6 and concludes a contradiction. Step 8 applies the disjunction elimination rule to 1, 4, 7 and concludes a contradiction. The final conclusion is a contradiction.

  1. Premise: projected-formula-0009791
  2. Premise: projected-formula-0009792
  3. Premise: projected-formula-0009793
  4. negation elimination rule: projected-formula-0009794
  5. Premise: projected-formula-0009795
  6. Premise: projected-formula-0009796
  7. negation elimination rule: projected-formula-0009797
  8. disjunction elimination rule: projected-formula-0009798

Source: content/first-order-logic/natural-deduction/provability-propositional.tex, line 67.

Natural-deduction proof tree at provability-propositional.tex, line 114

Step 1 states not A as a premise. Step 2 states assumption A labeled one for discharge as a premise. Step 3 applies the negation elimination rule to 1, 2 and concludes a contradiction. Step 4 applies the falsehood elimination rule to 3 and concludes formula B. Step 5 applies the conditional introduction rule to 4 and concludes if A, then B. The final conclusion is if A, then B.

  1. Premise: projected-formula-0009813
  2. Premise: projected-formula-0009814
  3. negation elimination rule: projected-formula-0009815
  4. falsehood elimination rule: projected-formula-0009816
  5. conditional introduction rule: projected-formula-0009817

Source: content/first-order-logic/natural-deduction/provability-propositional.tex, line 114.

Natural-deduction proof tree at soundness.tex, line 67

Step 1 states Gamma together with assumption A, labeled n for discharge as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes a contradiction. Step 4 applies the negation introduction rule to 3 and concludes not A. The final conclusion is not A.

  1. Premise: projected-formula-0009860
  2. Subderivation label: projected-formula-0009861
  3. Subderivation conclusion: projected-formula-0009862
  4. negation introduction rule: projected-formula-0009863

Source: content/first-order-logic/natural-deduction/soundness.tex, line 67.

Natural-deduction proof tree at soundness.tex, line 89

Step 1 states Gamma as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes A and B. Step 4 applies the conjunction elimination rule to 3 and concludes formula A. The final conclusion is formula A.

  1. Premise: projected-formula-0009879
  2. Subderivation label: projected-formula-0009880
  3. Subderivation conclusion: projected-formula-0009881
  4. conjunction elimination rule: projected-formula-0009882

Source: content/first-order-logic/natural-deduction/soundness.tex, line 89.

Natural-deduction proof tree at soundness.tex, line 112

Step 1 states Gamma as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes formula A. Step 4 applies the disjunction introduction rule to 3 and concludes A or B. The final conclusion is A or B.

  1. Premise: projected-formula-0009900
  2. Subderivation label: projected-formula-0009901
  3. Subderivation conclusion: projected-formula-0009902
  4. disjunction introduction rule: projected-formula-0009903

Source: content/first-order-logic/natural-deduction/soundness.tex, line 112.

Natural-deduction proof tree at soundness.tex, line 132

Step 1 states Gamma together with assumption A, labeled n for discharge as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes formula B. Step 4 applies the conditional introduction rule to 3 and concludes if A, then B. The final conclusion is if A, then B.

  1. Premise: projected-formula-0009919
  2. Subderivation label: projected-formula-0009920
  3. Subderivation conclusion: projected-formula-0009921
  4. conditional introduction rule: projected-formula-0009922

Source: content/first-order-logic/natural-deduction/soundness.tex, line 132.

Natural-deduction proof tree at soundness.tex, line 156

Step 1 states Gamma as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes a contradiction. Step 4 applies the falsehood elimination rule to 3 and concludes formula A. The final conclusion is formula A.

  1. Premise: projected-formula-0009941
  2. Subderivation label: projected-formula-0009942
  3. Subderivation conclusion: projected-formula-0009943
  4. falsehood elimination rule: projected-formula-0009944

Source: content/first-order-logic/natural-deduction/soundness.tex, line 156.

Natural-deduction proof tree at soundness.tex, line 176

Step 1 states Gamma as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes A of a. Step 4 applies the universal quantifier introduction rule to 3 and concludes for every x, A of x. The final conclusion is for every x, A of x.

  1. Premise: projected-formula-0009953
  2. Subderivation label: projected-formula-0009954
  3. Subderivation conclusion: projected-formula-0009955
  4. universal quantifier introduction rule: projected-formula-0009956

Source: content/first-order-logic/natural-deduction/soundness.tex, line 176.

Natural-deduction proof tree at soundness.tex, line 218

Step 1 states Gamma one as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes formula A. Step 4 states Gamma two as a premise. Step 5 labels the subderivation delta two. Step 6 applies the subderivation to 4 and concludes formula B. Step 7 applies the conjunction introduction rule to 3, 6 and concludes A and B. The final conclusion is A and B.

  1. Premise: projected-formula-0009992
  2. Subderivation label: projected-formula-0009993
  3. Subderivation conclusion: projected-formula-0009994
  4. Premise: projected-formula-0009995
  5. Subderivation label: projected-formula-0009996
  6. Subderivation conclusion: projected-formula-0009997
  7. conjunction introduction rule: projected-formula-0009998

Source: content/first-order-logic/natural-deduction/soundness.tex, line 218.

Natural-deduction proof tree at soundness.tex, line 246

Step 1 states Gamma one as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes if A, then B. Step 4 states Gamma two as a premise. Step 5 labels the subderivation delta two. Step 6 applies the subderivation to 4 and concludes formula A. Step 7 applies the conditional elimination rule to 3, 6 and concludes formula B. The final conclusion is formula B.

  1. Premise: projected-formula-0010021
  2. Subderivation label: projected-formula-0010022
  3. Subderivation conclusion: projected-formula-0010023
  4. Premise: projected-formula-0010024
  5. Subderivation label: projected-formula-0010025
  6. Subderivation conclusion: projected-formula-0010026
  7. conditional elimination rule: projected-formula-0010027

Source: content/first-order-logic/natural-deduction/soundness.tex, line 246.

Inference rules 13

Complete source-order listener rendering of this definition; no claim or solution is added.

  1. Inference rules 13
  2. Derivation diagram 79
  3. Step 1 has no printed premise. Step 2 applies the identity introduction rule to 1 and concludes t equals t. The final conclusion is t equals t.
  4. Derivation diagram 80
  5. Step 1 states t one equals t two as a premise. Step 2 states A of t one as a premise. Step 3 applies the identity elimination rule to 1, 2 and concludes A of t two. The final conclusion is A of t two.
  6. Derivation diagram 81
  7. Step 1 states t one equals t two as a premise. Step 2 states A of t two as a premise. Step 3 applies the identity elimination rule to 1, 2 and concludes A of t one. The final conclusion is A of t one.

Source: content/first-order-logic/natural-deduction/identity.tex, line 15.

Example 8

Complete source-order listener rendering of this example; no claim or solution is added.

  1. Example 8
  2. If s and t are closed terms, then from A of s, together with s equals t, derive A of t:
  3. Derivation diagram 82
  4. Step 1 states s equals t as a premise. Step 2 states A of s as a premise. Step 3 applies the identity elimination rule to 1, 2 and concludes A of t. The final conclusion is A of t.
  5. This may be familiar as the “principle of substitutability of identicals,” or Leibniz' Law.

Source: content/first-order-logic/natural-deduction/identity.tex, line 40.

Problem 9

Complete source-order listener rendering of this exercise; no claim or solution is added.

Unsolved source exercise; no solution added.

  1. Problem 9
  2. Prove that identity relation is both symmetric and transitive, i.e., give derivations of for every x and every y, if x equals y, then y equals x and for every x, every y, and every z, if x equals y and y equals z, then x equals z

Source: content/first-order-logic/natural-deduction/identity.tex, line 52.

Example 9

Complete source-order listener rendering of this example; no claim or solution is added.

  1. Example 9
  2. We derive the sentence for every x and every y, if both A of x and A of y, then x equals y; from the sentence: there exists an x such that, for every y, if A of y then y equals x. We develop the derivation backwards:
  3. Derivation diagram 83
  4. Step 1 states the existential statement that there exists an x such that every A object equals x, together with the single conjunctive assumption that A holds of both a and b, carrying label one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a equals b. Step 3 applies the conditional introduction rule to 2 and concludes if both A of a and A of b, then a equals b. Step 4 applies the universal quantifier introduction rule to 3 and concludes for every y, if both A of a and A of y, then a equals y. Step 5 applies the universal quantifier introduction rule to 4 and concludes for every x and every y, if both A of x and A of y, then x equals y. The final conclusion is for every x and every y, if both A of x and A of y, then x equals y.
  5. We'll now have to use the main assumption: since it is an existential formula, we use existential quantifier elimination to derive the intermediary conclusion a equals b.
  6. Derivation diagram 84
  7. Step 1 states there exists an x such that, for every y, if A of y, then y equals x as a premise. Step 2 states assumption: for every y, if A of y then y equals c; labeled two for discharge as a premise. Step 3 states the single assumption that is the conjunction of A of a with A of b, labeled one for discharge as a premise. Step 4 applies the subderivation to 3 and concludes a equals b. Step 5 applies the existential quantifier elimination rule to 1, 4 and concludes a equals b. Step 6 applies the conditional introduction rule to 5 and concludes if both A of a and A of b, then a equals b. Step 7 applies the universal quantifier introduction rule to 6 and concludes for every y, if both A of a and A of y, then a equals y. Step 8 applies the universal quantifier introduction rule to 7 and concludes for every x and every y, if both A of x and A of y, then x equals y. The final conclusion is for every x and every y, if both A of x and A of y, then x equals y.
  8. The sub-derivation on the top right is completed by using its assumptions to show that a equals c and b equals c. This requires two separate derivations. The derivation for a equals c is as follows:
  9. Derivation diagram 85
  10. Step 1 states assumption: for every y, if A of y then y equals c; labeled two for discharge as a premise. Step 2 applies the universal quantifier elimination rule to 1 and concludes if A of a, then a equals c. Step 3 states the single assumption that is the conjunction of A of a with A of b, labeled one for discharge as a premise. Step 4 applies the conjunction elimination rule to 3 and concludes A of a. Step 5 applies the conditional elimination rule to 2, 4 and concludes a equals c. The final conclusion is a equals c.
  11. From a equals c and b equals c we derive a equals b by identity elimination.

Source: content/first-order-logic/natural-deduction/identity.tex, line 59.

Natural-deduction proof tree at identity.tex, line 67

Step 1 states the existential statement that there exists an x such that every A object equals x, together with the single conjunctive assumption that A holds of both a and b, carrying label one for discharge as a premise. Step 2 applies the subderivation to 1 and concludes a equals b. Step 3 applies the conditional introduction rule to 2 and concludes if both A of a and A of b, then a equals b. Step 4 applies the universal quantifier introduction rule to 3 and concludes for every y, if both A of a and A of y, then a equals y. Step 5 applies the universal quantifier introduction rule to 4 and concludes for every x and every y, if both A of x and A of y, then x equals y. The final conclusion is for every x and every y, if both A of x and A of y, then x equals y.

  1. Premise: projected-formula-0010084
  2. Subderivation conclusion: projected-formula-0010085
  3. conditional introduction rule: projected-formula-0010086
  4. universal quantifier introduction rule: projected-formula-0010087
  5. universal quantifier introduction rule: projected-formula-0010088

Source: content/first-order-logic/natural-deduction/identity.tex, line 67.

Natural-deduction proof tree at identity.tex, line 81

Step 1 states there exists an x such that, for every y, if A of y, then y equals x as a premise. Step 2 states assumption: for every y, if A of y then y equals c; labeled two for discharge as a premise. Step 3 states the single assumption that is the conjunction of A of a with A of b, labeled one for discharge as a premise. Step 4 applies the subderivation to 3 and concludes a equals b. Step 5 applies the existential quantifier elimination rule to 1, 4 and concludes a equals b. Step 6 applies the conditional introduction rule to 5 and concludes if both A of a and A of b, then a equals b. Step 7 applies the universal quantifier introduction rule to 6 and concludes for every y, if both A of a and A of y, then a equals y. Step 8 applies the universal quantifier introduction rule to 7 and concludes for every x and every y, if both A of x and A of y, then x equals y. The final conclusion is for every x and every y, if both A of x and A of y, then x equals y.

  1. Premise: projected-formula-0010090
  2. Premise: projected-formula-0010091
  3. Marked premise: projected-formula-0010092
  4. Subderivation conclusion: projected-formula-0010093
  5. existential quantifier elimination rule: projected-formula-0010094
  6. conditional introduction rule: projected-formula-0010095
  7. universal quantifier introduction rule: projected-formula-0010096
  8. universal quantifier introduction rule: projected-formula-0010097

Source: content/first-order-logic/natural-deduction/identity.tex, line 81.

Natural-deduction proof tree at identity.tex, line 100

Step 1 states assumption: for every y, if A of y then y equals c; labeled two for discharge as a premise. Step 2 applies the universal quantifier elimination rule to 1 and concludes if A of a, then a equals c. Step 3 states the single assumption that is the conjunction of A of a with A of b, labeled one for discharge as a premise. Step 4 applies the conjunction elimination rule to 3 and concludes A of a. Step 5 applies the conditional elimination rule to 2, 4 and concludes a equals c. The final conclusion is a equals c.

  1. Premise: projected-formula-0010101
  2. universal quantifier elimination rule: projected-formula-0010102
  3. Premise: projected-formula-0010103
  4. conjunction elimination rule: projected-formula-0010104
  5. conditional elimination rule: projected-formula-0010105

Source: content/first-order-logic/natural-deduction/identity.tex, line 100.

Problem 10

Complete source-order listener rendering of this exercise; no claim or solution is added.

Unsolved source exercise; no solution added.

  1. Problem 10
  2. Give derivations of the following formulas:
  3. Item 1.
  4. for every x and every y, if x equals y and A of x, then A of y
  5. Item 2.
  6. if there exists an A object and every two A objects are equal, then there exists an x that is A and to which every A object is equal

Source: content/first-order-logic/natural-deduction/identity.tex, line 114.

Natural-deduction proof tree at soundness-identity.tex, line 25

Step 1 states Gamma one as a premise. Step 2 labels the subderivation delta one. Step 3 applies the subderivation to 1 and concludes t one equals t two. Step 4 states Gamma two as a premise. Step 5 labels the subderivation delta two. Step 6 applies the subderivation to 4 and concludes A of t one. Step 7 applies the identity elimination rule to 3, 6 and concludes A of t two. The final conclusion is A of t two.

  1. Premise: projected-formula-0010116
  2. Subderivation label: projected-formula-0010117
  3. Subderivation conclusion: projected-formula-0010118
  4. Premise: projected-formula-0010119
  5. Subderivation label: projected-formula-0010120
  6. Subderivation conclusion: projected-formula-0010121
  7. identity elimination rule: projected-formula-0010122

Source: content/first-order-logic/natural-deduction/soundness-identity.tex, line 25.

10 source references

  1. the proposition characterizing inconsistency by derivability of every sentence — source line 126.
  2. the proposition giving the satisfaction clauses for quantifiers — source line 189.
  3. the definition of satisfaction for first-order formulas — source line 191.
  4. the corollary that sentence satisfaction is independent of assignments — source line 194.
  5. the proposition equating sentence satisfaction with truth in a structure — source line 197.
  6. the proposition on extensionality of formulas under agreeing assignments — source line 198.
  7. the extensionality proposition for term values and formula satisfaction — source line 201.
  8. the soundness theorem for natural deduction — source line 281.
  9. the soundness theorem for natural deduction — source line 305.
  10. the proposition on extensionality of formulas under agreeing assignments — source line 42.

545 exact ordered proof-command bindings

Open the complete command binding ledger
  1. Introduce proof leaf: formula A. source line 19.
  2. Introduce proof leaf: formula B. source line 20.
  3. Label the next inference: conjunction introduction rule. source line 21.
  4. Infer: A and B from two preceding branches. source line 22.
  5. End and display this proof diagram. source line 23.
  6. Introduce proof leaf: A and B. source line 26.
  7. Label the next inference: conjunction elimination rule. source line 27.
  8. Infer: formula A from one preceding branch. source line 28.
  9. End and display this proof diagram. source line 29.
  10. Introduce proof leaf: A and B. source line 31.
  11. Label the next inference: conjunction elimination rule. source line 32.
  12. Infer: formula B from one preceding branch. source line 33.
  13. End and display this proof diagram. source line 34.
  14. Introduce proof leaf: formula A. source line 42.
  15. Label the next inference: disjunction introduction rule. source line 43.
  16. Infer: A or B from one preceding branch. source line 44.
  17. End and display this proof diagram. source line 45.
  18. Introduce proof leaf: formula B. source line 47.
  19. Label the next inference: disjunction introduction rule. source line 48.
  20. Infer: A or B from one preceding branch. source line 49.
  21. End and display this proof diagram. source line 50.
  22. Introduce proof leaf: A or B. source line 53.
  23. Introduce proof leaf: assumption A, labeled n for discharge. source line 54.
  24. State the derived proof line: formula C. source line 55.
  25. Introduce proof leaf: assumption B, labeled n for discharge. source line 56.
  26. State the derived proof line: formula C. source line 57.
  27. Apply the disjunction elimination rule and discharge assumptions labeled n. source line 58.
  28. Infer: formula C from three preceding branches. source line 59.
  29. End and display this proof diagram. source line 60.
  30. Introduce proof leaf: assumption A, labeled n for discharge. source line 66.
  31. State the derived proof line: formula B. source line 67.
  32. Apply the conditional introduction rule and discharge assumptions labeled n. source line 68.
  33. Infer: if A, then B from one preceding branch. source line 69.
  34. End and display this proof diagram. source line 70.
  35. Introduce proof leaf: if A, then B. source line 72.
  36. Introduce proof leaf: formula A. source line 73.
  37. Label the next inference: conditional elimination rule. source line 74.
  38. Infer: formula B from two preceding branches. source line 75.
  39. End and display this proof diagram. source line 76.
  40. Introduce proof leaf: assumption A, labeled n for discharge. source line 82.
  41. Suppress the inference bar at this proof step. source line 83.
  42. State the derived proof line: a contradiction. source line 84.
  43. Apply the negation introduction rule and discharge assumptions labeled n. source line 85.
  44. Infer: not A from one preceding branch. source line 86.
  45. End and display this proof diagram. source line 87.
  46. Introduce proof leaf: not A. source line 89.
  47. Introduce proof leaf: formula A. source line 90.
  48. Label the next inference: negation elimination rule. source line 91.
  49. Infer: a contradiction from two preceding branches. source line 92.
  50. End and display this proof diagram. source line 93.
  51. Introduce proof leaf: a contradiction. source line 99.
  52. Label the next inference: intuitionistic absurdity rule. source line 100.
  53. Infer: formula A from one preceding branch. source line 101.
  54. End and display this proof diagram. source line 102.
  55. Introduce proof leaf: assumption not A, labeled n for discharge. source line 104.
  56. State the derived proof line: a contradiction. source line 105.
  57. Apply the classical absurdity rule and discharge assumptions labeled n. source line 106.
  58. Infer: formula A from one preceding branch. source line 107.
  59. End and display this proof diagram. source line 108.
  60. Introduce proof leaf: A of a. source line 16.
  61. Label the next inference: universal introduction rule. source line 17.
  62. Infer: for every x, A of x from one preceding branch. source line 18.
  63. End and display this proof diagram. source line 19.
  64. Introduce proof leaf: for every x, A of x. source line 21.
  65. Label the next inference: universal elimination rule. source line 22.
  66. Infer: A of t from one preceding branch. source line 23.
  67. End and display this proof diagram. source line 24.
  68. Introduce proof leaf: A of t. source line 39.
  69. Label the next inference: existential introduction rule. source line 40.
  70. Infer: there exists an x such that A of x from one preceding branch. source line 41.
  71. End and display this proof diagram. source line 42.
  72. Introduce proof leaf: there exists an x such that A of x. source line 44.
  73. Introduce proof leaf: A of a; then discharge label n. source line 45.
  74. State the derived proof line: formula C. source line 46.
  75. Apply the existential elimination rule and discharge assumptions labeled n. source line 47.
  76. Infer: formula C from two preceding branches. source line 48.
  77. End and display this proof diagram. source line 49.
  78. Introduce proof leaf: A with t substituted for free x. source line 69.
  79. Label the next inference: existential introduction rule. source line 70.
  80. Infer: there exists an x such that A from one preceding branch. source line 71.
  81. Introduce proof leaf: there exists an x such that A of x. source line 96.
  82. Introduce proof leaf: assumption A of a labeled one for discharge. source line 97.
  83. Label the next inference: starred universal introduction rule. source line 98.
  84. Infer: for every x, A of x from one preceding branch. source line 99.
  85. Label the next inference: existential elimination rule. source line 100.
  86. Infer: for every x, A of x from two preceding branches. source line 101.
  87. Introduce proof leaf: formula A. source line 51.
  88. Introduce proof leaf: formula B. source line 52.
  89. Label the next inference: conjunction introduction rule. source line 53.
  90. Infer: A and B from two preceding branches. source line 54.
  91. Introduce proof leaf: formula C. source line 60.
  92. Introduce proof leaf: formula D. source line 61.
  93. Label the next inference: conjunction introduction rule. source line 62.
  94. Infer: C and D from two preceding branches. source line 63.
  95. Introduce proof leaf: formula D. source line 69.
  96. Introduce proof leaf: formula C. source line 70.
  97. Label the next inference: conjunction introduction rule. source line 71.
  98. Infer: D and C from two preceding branches. source line 72.
  99. Introduce proof leaf: assumption C, labeled one for discharge. source line 81.
  100. Introduce proof leaf: formula D. source line 82.
  101. Label the next inference: conjunction introduction rule. source line 83.
  102. Infer: C and D from two preceding branches. source line 84.
  103. Apply the conditional introduction rule and discharge assumptions labeled one. source line 85.
  104. Infer: if C, then C and D from one preceding branch. source line 86.
  105. End and display this proof diagram. source line 87.
  106. Introduce proof leaf: formula C. source line 88.
  107. Introduce proof leaf: assumption D, labeled one for discharge. source line 89.
  108. Label the next inference: conjunction introduction rule. source line 90.
  109. Infer: C and D from two preceding branches. source line 91.
  110. Apply the conditional introduction rule and discharge assumptions labeled one. source line 92.
  111. Infer: if D, then C and D from one preceding branch. source line 93.
  112. Introduce proof leaf: formula B. source line 104.
  113. Apply the conditional introduction rule and discharge assumptions labeled one. source line 105.
  114. Infer: if A, then B from one preceding branch. source line 106.
  115. Introduce proof leaf with an empty premise. source line 21.
  116. Infer: if A and B, then A from one preceding branch. source line 22.
  117. Introduce proof leaf: the single assumption that is the conjunction of A and B, labeled one for discharge. source line 33.
  118. State the derived proof line: formula A. source line 34.
  119. Apply the conditional introduction rule and discharge assumptions labeled one. source line 35.
  120. Infer: if A and B, then A from one preceding branch. source line 36.
  121. Introduce proof leaf: the single assumption that is the conjunction of A and B, labeled one for discharge. source line 43.
  122. Label the next inference: conjunction elimination rule. source line 44.
  123. Infer: formula A from one preceding branch. source line 45.
  124. Apply the conditional introduction rule and discharge assumptions labeled one. source line 46.
  125. Infer: if A and B, then A from one preceding branch. source line 47.
  126. Introduce proof leaf with an empty premise. source line 60.
  127. Infer: if either not A or B, then if A, then B from one preceding branch. source line 61.
  128. Introduce proof leaf: the single assumption that is the disjunction of not A with B, labeled one for discharge. source line 72.
  129. State the derived proof line: if A, then B. source line 73.
  130. Apply the conditional introduction rule and discharge assumptions labeled one. source line 74.
  131. Infer: if either not A or B, then if A, then B from one preceding branch. source line 75.
  132. Introduce proof leaf: the single assumption that is the disjunction of not A with B, labeled one for discharge. source line 87.
  133. Introduce proof leaf: assumption not A, labeled two for discharge. source line 88.
  134. State the derived proof line: if A, then B. source line 89.
  135. Introduce proof leaf: assumption B, labeled two for discharge. source line 90.
  136. State the derived proof line: if A, then B. source line 91.
  137. Apply the disjunction elimination rule and discharge assumptions labeled two. source line 92.
  138. Infer: if A, then B from three preceding branches. source line 93.
  139. Apply the conditional introduction rule and discharge assumptions labeled one. source line 94.
  140. Infer: if either not A or B, then if A, then B from one preceding branch. source line 95.
  141. Introduce proof leaf: the single assumption that is the disjunction of not A with B, labeled one for discharge. source line 101.
  142. Introduce proof leaf: assumptions not A labeled two, and A labeled three, for discharge. source line 102.
  143. State the derived proof line: formula B. source line 103.
  144. Apply the conditional introduction rule and discharge assumptions labeled three. source line 104.
  145. Infer: if A, then B from one preceding branch. source line 105.
  146. Introduce proof leaf: assumptions B labeled two, and A labeled four, for discharge. source line 106.
  147. State the derived proof line: formula B. source line 107.
  148. Apply the conditional introduction rule and discharge assumptions labeled four. source line 108.
  149. Infer: if A, then B from one preceding branch. source line 109.
  150. Apply the disjunction elimination rule and discharge assumptions labeled two. source line 110.
  151. Infer: if A, then B from three preceding branches. source line 111.
  152. Apply the conditional introduction rule and discharge assumptions labeled one. source line 112.
  153. Infer: if either not A or B, then if A, then B from one preceding branch. source line 113.
  154. Introduce proof leaf: assumption not A, labeled two for discharge. source line 121.
  155. Introduce proof leaf: assumption A, labeled three for discharge. source line 122.
  156. Label the next inference: negation elimination rule. source line 123.
  157. Infer: a contradiction from two preceding branches. source line 124.
  158. State the derived proof line: formula B. source line 125.
  159. Introduce proof leaf: the single assumption that is the disjunction of not A with B, labeled one for discharge. source line 130.
  160. Introduce proof leaf: assumption not A, labeled two for discharge. source line 131.
  161. Introduce proof leaf: assumption A, labeled three for discharge. source line 132.
  162. Label the next inference: falsum introduction rule. source line 133.
  163. Infer: a contradiction from two preceding branches. source line 134.
  164. Label the next inference: intuitionistic absurdity rule. source line 135.
  165. Infer: formula B from one preceding branch. source line 136.
  166. Apply the conditional introduction rule and discharge assumptions labeled three. source line 137.
  167. Infer: if A, then B from one preceding branch. source line 138.
  168. Introduce proof leaf: assumptions B labeled two, and A labeled four, for discharge. source line 139.
  169. State the derived proof line: formula B. source line 140.
  170. Apply the conditional introduction rule and discharge assumptions labeled four. source line 141.
  171. Infer: if A, then B from one preceding branch. source line 142.
  172. Apply the disjunction elimination rule and discharge assumptions labeled two. source line 143.
  173. Infer: if A, then B from three preceding branches. source line 144.
  174. Apply the conditional introduction rule and discharge assumptions labeled one. source line 145.
  175. Infer: if either not A or B, then if A, then B from one preceding branch. source line 146.
  176. Introduce proof leaf: the single assumption that is the disjunction of not A with B, labeled one for discharge. source line 157.
  177. Introduce proof leaf: assumption not A, labeled two for discharge. source line 158.
  178. Introduce proof leaf: assumption A, labeled three for discharge. source line 159.
  179. Label the next inference: negation elimination rule. source line 160.
  180. Infer: a contradiction from two preceding branches. source line 161.
  181. Label the next inference: intuitionistic absurdity rule. source line 162.
  182. Infer: formula B from one preceding branch. source line 163.
  183. Apply the conditional introduction rule and discharge assumptions labeled three. source line 164.
  184. Infer: if A, then B from one preceding branch. source line 165.
  185. Introduce proof leaf: assumption B, labeled two for discharge. source line 166.
  186. Label the next inference: conditional introduction rule. source line 167.
  187. Infer: if A, then B from one preceding branch. source line 168.
  188. Apply the disjunction elimination rule and discharge assumptions labeled two. source line 169.
  189. Infer: if A, then B from three preceding branches. source line 170.
  190. Apply the conditional introduction rule and discharge assumptions labeled one. source line 171.
  191. Infer: if either not A or B, then if A, then B from one preceding branch. source line 172.
  192. Introduce proof leaf: assumption denying the whole disjunction A or not A, labeled one for discharge. source line 191.
  193. State the derived proof line: a contradiction. source line 192.
  194. Apply the classical absurdity rule and discharge assumptions labeled one. source line 193.
  195. Infer: A or not A from one preceding branch. source line 194.
  196. Introduce proof leaf: assumption denying the whole disjunction A or not A, labeled one for discharge. source line 200.
  197. State the derived proof line: not A. source line 201.
  198. Introduce proof leaf: assumption denying the whole disjunction A or not A, labeled one for discharge. source line 202.
  199. State the derived proof line: formula A. source line 203.
  200. Label the next inference: negation elimination rule. source line 204.
  201. Infer: a contradiction from two preceding branches. source line 205.
  202. Apply the classical absurdity rule and discharge assumptions labeled one. source line 206.
  203. Infer: A or not A from one preceding branch. source line 207.
  204. Introduce proof leaf: two assumptions for discharge: the first denies the entire disjunction A or not A and is labeled one; the second is A and is labeled two. source line 212.
  205. State the derived proof line: a contradiction. source line 213.
  206. Apply the negation introduction rule and discharge assumptions labeled two. source line 214.
  207. Infer: not A from one preceding branch. source line 215.
  208. Introduce proof leaf: assumption denying the whole disjunction A or not A, labeled one for discharge. source line 216.
  209. State the derived proof line: formula A. source line 217.
  210. Label the next inference: negation elimination rule. source line 218.
  211. Infer: a contradiction from two preceding branches. source line 219.
  212. Apply the classical absurdity rule and discharge assumptions labeled one. source line 220.
  213. Infer: A or not A from one preceding branch. source line 221.
  214. Introduce proof leaf: assumption denying the whole disjunction A or not A, labeled one for discharge. source line 227.
  215. Introduce proof leaf: assumption A, labeled two for discharge. source line 228.
  216. Label the next inference: disjunction introduction rule. source line 229.
  217. Infer: A or not A from one preceding branch. source line 230.
  218. Label the next inference: negation elimination rule. source line 231.
  219. Infer: a contradiction from two preceding branches. source line 232.
  220. Apply the negation introduction rule and discharge assumptions labeled two. source line 233.
  221. Infer: not A from one preceding branch. source line 234.
  222. Introduce proof leaf: assumption denying the whole disjunction A or not A, labeled one for discharge. source line 235.
  223. State the derived proof line: formula A. source line 236.
  224. Label the next inference: negation elimination rule. source line 237.
  225. Infer: a contradiction from two preceding branches. source line 238.
  226. Apply the classical absurdity rule and discharge assumptions labeled one. source line 239.
  227. Infer: A or not A from one preceding branch. source line 240.
  228. Introduce proof leaf: assumption denying the whole disjunction A or not A, labeled one for discharge. source line 244.
  229. Introduce proof leaf: assumption A, labeled two for discharge. source line 245.
  230. Label the next inference: disjunction introduction rule. source line 246.
  231. Infer: A or not A from one preceding branch. source line 247.
  232. Label the next inference: negation elimination rule. source line 248.
  233. Infer: a contradiction from two preceding branches. source line 249.
  234. Apply the negation introduction rule and discharge assumptions labeled two. source line 250.
  235. Infer: not A from one preceding branch. source line 251.
  236. Introduce proof leaf: assumption denying the whole disjunction A or not A, labeled one for discharge. source line 252.
  237. Introduce proof leaf: assumption not A, labeled three for discharge. source line 253.
  238. Label the next inference: disjunction introduction rule. source line 254.
  239. Infer: A or not A from one preceding branch. source line 255.
  240. Label the next inference: negation elimination rule. source line 256.
  241. Infer: a contradiction from two preceding branches. source line 257.
  242. Apply the classical absurdity rule and discharge assumptions labeled three. source line 258.
  243. Infer: formula A from one preceding branch. source line 259.
  244. Label the next inference: negation elimination rule. source line 260.
  245. Infer: a contradiction from two preceding branches. source line 261.
  246. Apply the classical absurdity rule and discharge assumptions labeled one. source line 262.
  247. Infer: A or not A from one preceding branch. source line 263.
  248. Introduce proof leaf with an empty premise. source line 24.
  249. Infer: if there exists an x such that not A of x, then it is not the case that, for every x, A of x from one preceding branch. source line 25.
  250. Introduce proof leaf: assumption: there exists an x such that not A of x; labeled one for discharge. source line 30.
  251. State the derived proof line: it is not the case that, for every x, A of x. source line 31.
  252. Apply the conditional introduction rule and discharge assumptions labeled one. source line 32.
  253. Infer: if there exists an x such that not A of x, then it is not the case that, for every x, A of x from one preceding branch. source line 33.
  254. Introduce proof leaf: assumption: there exists an x such that not A of x; labeled one for discharge. source line 42.
  255. Introduce proof leaf: assumption not A of a, labeled two for discharge. source line 43.
  256. State the derived proof line: it is not the case that, for every x, A of x. source line 44.
  257. Apply the existential elimination rule and discharge assumptions labeled two. source line 45.
  258. Infer: it is not the case that, for every x, A of x from two preceding branches. source line 46.
  259. Apply the conditional introduction rule and discharge assumptions labeled one. source line 47.
  260. Infer: if there exists an x such that not A of x, then it is not the case that, for every x, A of x from one preceding branch. source line 48.
  261. Introduce proof leaf: assumption: there exists an x such that not A of x; labeled one for discharge. source line 57.
  262. Introduce proof leaf: assumptions not A of a labeled two, and for every x, A of x labeled three, for discharge. source line 58.
  263. State the derived proof line: a contradiction. source line 59.
  264. Apply the negation introduction rule and discharge assumptions labeled three. source line 60.
  265. Infer: it is not the case that, for every x, A of x from one preceding branch. source line 61.
  266. Apply the existential elimination rule and discharge assumptions labeled two. source line 62.
  267. Infer: it is not the case that, for every x, A of x from two preceding branches. source line 63.
  268. Apply the conditional introduction rule and discharge assumptions labeled one. source line 64.
  269. Infer: if there exists an x such that not A of x, then it is not the case that, for every x, A of x from one preceding branch. source line 65.
  270. Introduce proof leaf: assumption: there exists an x such that not A of x; labeled one for discharge. source line 73.
  271. Introduce proof leaf: assumption not A of a, labeled two for discharge. source line 74.
  272. Introduce proof leaf: assumption: for every x, A of x; labeled three for discharge. source line 75.
  273. Label the next inference: universal elimination rule. source line 76.
  274. Infer: A of a from one preceding branch. source line 77.
  275. Label the next inference: negation elimination rule. source line 78.
  276. Infer: a contradiction from two preceding branches. source line 79.
  277. Apply the negation introduction rule and discharge assumptions labeled three. source line 80.
  278. Infer: it is not the case that, for every x, A of x from one preceding branch. source line 81.
  279. Apply the existential elimination rule and discharge assumptions labeled two. source line 82.
  280. Infer: it is not the case that, for every x, A of x from two preceding branches. source line 83.
  281. Apply the conditional introduction rule and discharge assumptions labeled one. source line 84.
  282. Infer: if there exists an x such that not A of x, then it is not the case that, for every x, A of x from one preceding branch. source line 85.
  283. Introduce proof leaf with an empty premise. source line 108.
  284. Infer: there exists an x such that C of x and b from one preceding branch. source line 109.
  285. Introduce proof leaf: there exists an x such that both A of x and B of x. source line 118.
  286. Introduce proof leaf: the single assumption that is the conjunction of A of a and B of a, labeled one for discharge. source line 119.
  287. State the derived proof line: there exists an x such that C of x and b. source line 120.
  288. Apply the existential elimination rule and discharge assumptions labeled one. source line 121.
  289. Infer: there exists an x such that C of x and b from two preceding branches. source line 122.
  290. Introduce proof leaf: there exists an x such that both A of x and B of x. source line 127.
  291. Introduce proof leaf: the single assumption that is the conjunction of A of a and B of a, labeled one for discharge. source line 128.
  292. Label the next inference: conjunction elimination rule. source line 130.
  293. Infer: B of a from one preceding branch. source line 131.
  294. State the derived proof line: there exists an x such that C of x and b. source line 132.
  295. Apply the existential elimination rule and discharge assumptions labeled one. source line 133.
  296. Infer: there exists an x such that C of x and b from two preceding branches. source line 134.
  297. Introduce proof leaf: there exists an x such that both A of x and B of x. source line 144.
  298. Introduce proof leaf: for every x, if B of x, then C of x and b. source line 145.
  299. Label the next inference: universal elimination rule. source line 146.
  300. Infer: if B of a, then C of a and b from one preceding branch. source line 147.
  301. Introduce proof leaf: the single assumption that is the conjunction of A of a and B of a, labeled one for discharge. source line 148.
  302. Label the next inference: conjunction elimination rule. source line 150.
  303. Infer: B of a from one preceding branch. source line 151.
  304. Label the next inference: conditional elimination rule. source line 152.
  305. Infer: C of a and b from two preceding branches. source line 153.
  306. State the derived proof line: there exists an x such that C of x and b. source line 154.
  307. Apply the existential elimination rule and discharge assumptions labeled one. source line 155.
  308. Infer: there exists an x such that C of x and b from two preceding branches. source line 157.
  309. Introduce proof leaf: there exists an x such that both A of x and B of x. source line 162.
  310. Introduce proof leaf: for every x, if B of x, then C of x and b. source line 163.
  311. Label the next inference: universal elimination rule. source line 164.
  312. Infer: if B of a, then C of a and b from one preceding branch. source line 165.
  313. Introduce proof leaf: the single assumption that is the conjunction of A of a and B of a, labeled one for discharge. source line 166.
  314. Label the next inference: conjunction elimination rule. source line 168.
  315. Infer: B of a from one preceding branch. source line 169.
  316. Label the next inference: conditional elimination rule. source line 170.
  317. Infer: C of a and b from two preceding branches. source line 171.
  318. Label the next inference: existential introduction rule. source line 172.
  319. Infer: there exists an x such that C of x and b from one preceding branch. source line 173.
  320. Apply the existential elimination rule and discharge assumptions labeled one. source line 174.
  321. Infer: there exists an x such that C of x and b from two preceding branches. source line 176.
  322. Introduce proof leaf with an empty premise. source line 189.
  323. Infer: it is not the case that, for every x, A of x from one preceding branch. source line 190.
  324. Introduce proof leaf: assumption: for every x, A of x; labeled one for discharge. source line 196.
  325. State the derived proof line: a contradiction. source line 197.
  326. Apply the negation introduction rule and discharge assumptions labeled one. source line 198.
  327. Infer: it is not the case that, for every x, A of x from one preceding branch. source line 199.
  328. Introduce proof leaf: if, for every x, A of x, then there exists a y such that B of y. source line 206.
  329. Introduce proof leaf: assumption: for every x, A of x; labeled one for discharge. source line 207.
  330. Label the next inference: conditional elimination rule. source line 208.
  331. Infer: there exists a y such that B of y from two preceding branches. source line 209.
  332. State the derived proof line: a contradiction. source line 210.
  333. Apply the negation introduction rule and discharge assumptions labeled one. source line 211.
  334. Infer: it is not the case that, for every x, A of x from one preceding branch. source line 212.
  335. Introduce proof leaf: it is not the case that there exists a y such that B of y. source line 218.
  336. Introduce proof leaf: if, for every x, A of x, then there exists a y such that B of y. source line 219.
  337. Introduce proof leaf: assumption: for every x, A of x; labeled one for discharge. source line 220.
  338. Label the next inference: conditional elimination rule. source line 221.
  339. Infer: there exists a y such that B of y from two preceding branches. source line 222.
  340. Label the next inference: negation elimination rule. source line 223.
  341. Infer: a contradiction from two preceding branches. source line 224.
  342. Apply the negation introduction rule and discharge assumptions labeled one. source line 225.
  343. Infer: it is not the case that, for every x, A of x from one preceding branch. source line 226.
  344. Introduce proof leaf: capital Delta together with assumption A, labeled one for discharge. source line 88.
  345. Label the next inference: delta one. source line 89.
  346. State the derived proof line: formula B. source line 90.
  347. Apply the conditional introduction rule and discharge assumptions labeled one. source line 91.
  348. Infer: if A, then B from one preceding branch. source line 92.
  349. Introduce proof leaf: Gamma. source line 93.
  350. Label the next inference: derivation delta zero. source line 94.
  351. State the derived proof line: formula A. source line 95.
  352. Label the next inference: conditional elimination rule. source line 96.
  353. Infer: formula B from two preceding branches. source line 97.
  354. Introduce proof leaf: the assumptions in Gamma, together with assumption A labeled one for discharge. source line 29.
  355. Label the next inference: delta two. source line 30.
  356. State the derived proof line: a contradiction. source line 31.
  357. Apply the negation introduction rule and discharge assumptions labeled one. source line 32.
  358. Infer: not A from one preceding branch. source line 33.
  359. Introduce proof leaf: Gamma. source line 34.
  360. Label the next inference: delta one. source line 35.
  361. State the derived proof line: formula A. source line 36.
  362. Label the next inference: negation elimination rule. source line 37.
  363. Infer: a contradiction from two preceding branches. source line 38.
  364. Introduce proof leaf: not A. source line 55.
  365. Introduce proof leaf: Gamma. source line 56.
  366. Label the next inference: derivation delta zero. source line 57.
  367. State the derived proof line: formula A. source line 58.
  368. Label the next inference: negation elimination rule. source line 59.
  369. Infer: a contradiction from two preceding branches. source line 60.
  370. Introduce proof leaf: the assumptions in Gamma, together with assumption not A labeled one for discharge. source line 68.
  371. Label the next inference: delta one. source line 69.
  372. State the derived proof line: a contradiction. source line 70.
  373. Label the next inference: classical absurdity rule. source line 71.
  374. Apply the classical absurdity rule and discharge assumptions labeled one. source line 72.
  375. Infer: formula A from one preceding branch. source line 73.
  376. Introduce proof leaf: not A. source line 92.
  377. Introduce proof leaf: Gamma. source line 93.
  378. Label the next inference: delta. source line 94.
  379. State the derived proof line: formula A. source line 95.
  380. Label the next inference: negation elimination rule. source line 96.
  381. Infer: a contradiction from two preceding branches. source line 97.
  382. Introduce proof leaf: the assumptions in Gamma, together with assumption not A labeled two for discharge. source line 113.
  383. Label the next inference: delta two. source line 114.
  384. State the derived proof line: a contradiction. source line 115.
  385. Apply the negation introduction rule and discharge assumptions labeled two. source line 116.
  386. Infer: not not A from one preceding branch. source line 117.
  387. Introduce proof leaf: the assumptions in Gamma, together with assumption A labeled one for discharge. source line 118.
  388. Label the next inference: delta one. source line 119.
  389. State the derived proof line: a contradiction. source line 120.
  390. Apply the negation introduction rule and discharge assumptions labeled one. source line 121.
  391. Infer: not A from one preceding branch. source line 122.
  392. Label the next inference: negation elimination rule. source line 123.
  393. Infer: a contradiction from two preceding branches. source line 124.
  394. Introduce proof leaf: A and B. source line 38.
  395. Label the next inference: conjunction elimination rule. source line 39.
  396. Infer: formula A from one preceding branch. source line 40.
  397. End and display this proof diagram. source line 41.
  398. Introduce proof leaf: A and B. source line 42.
  399. Label the next inference: conjunction elimination rule. source line 43.
  400. Infer: formula B from one preceding branch. source line 44.
  401. Introduce proof leaf: formula A. source line 48.
  402. Introduce proof leaf: formula B. source line 49.
  403. Label the next inference: conjunction introduction rule. source line 50.
  404. Infer: A and B from two preceding branches. source line 51.
  405. Introduce proof leaf: A or B. source line 68.
  406. Introduce proof leaf: not A. source line 69.
  407. Introduce proof leaf: assumption A labeled one for discharge. source line 70.
  408. Label the next inference: negation elimination rule. source line 71.
  409. Infer: a contradiction from two preceding branches. source line 72.
  410. Introduce proof leaf: not B. source line 73.
  411. Introduce proof leaf: assumption B labeled one for discharge. source line 74.
  412. Label the next inference: negation elimination rule. source line 75.
  413. Infer: a contradiction from two preceding branches. source line 76.
  414. Apply the disjunction elimination rule and discharge assumptions labeled one. source line 77.
  415. Infer: a contradiction from three preceding branches. source line 78.
  416. Introduce proof leaf: formula A. source line 84.
  417. Label the next inference: disjunction introduction rule. source line 85.
  418. Infer: A or B from one preceding branch. source line 86.
  419. End and display this proof diagram. source line 87.
  420. Introduce proof leaf: formula B. source line 88.
  421. Label the next inference: disjunction introduction rule. source line 89.
  422. Infer: A or B from one preceding branch. source line 90.
  423. Introduce proof leaf: if A, then B. source line 107.
  424. Introduce proof leaf: formula A. source line 108.
  425. Label the next inference: conditional elimination rule. source line 109.
  426. Infer: formula B from two preceding branches. source line 110.
  427. Introduce proof leaf: not A. source line 115.
  428. Introduce proof leaf: assumption A labeled one for discharge. source line 116.
  429. Label the next inference: negation elimination rule. source line 117.
  430. Infer: a contradiction from two preceding branches. source line 118.
  431. Label the next inference: intuitionistic absurdity rule. source line 119.
  432. Infer: formula B from one preceding branch. source line 120.
  433. Apply the conditional introduction rule and discharge assumptions labeled one. source line 121.
  434. Infer: if A, then B from one preceding branch. source line 122.
  435. End and display this proof diagram. source line 123.
  436. Introduce proof leaf: formula B. source line 124.
  437. Label the next inference: conditional introduction rule. source line 125.
  438. Infer: if A, then B from one preceding branch. source line 126.
  439. Introduce proof leaf: A of t. source line 48.
  440. Label the next inference: existential introduction rule. source line 49.
  441. Infer: there exists an x such that A of x from one preceding branch. source line 50.
  442. Introduce proof leaf: for every x, A of x. source line 56.
  443. Label the next inference: universal elimination rule. source line 57.
  444. Infer: A of t from one preceding branch. source line 58.
  445. Introduce proof leaf: Gamma together with assumption A, labeled n for discharge. source line 68.
  446. Label the next inference: delta one. source line 69.
  447. State the derived proof line: a contradiction. source line 70.
  448. Apply the negation introduction rule and discharge assumptions labeled n. source line 71.
  449. Infer: not A from one preceding branch. source line 72.
  450. Introduce proof leaf: Gamma. source line 90.
  451. Label the next inference: delta one. source line 91.
  452. State the derived proof line: A and B. source line 92.
  453. Label the next inference: conjunction elimination rule. source line 93.
  454. Infer: formula A from one preceding branch. source line 94.
  455. Introduce proof leaf: Gamma. source line 113.
  456. Label the next inference: delta one. source line 114.
  457. State the derived proof line: formula A. source line 115.
  458. Label the next inference: disjunction introduction rule. source line 116.
  459. Infer: A or B from one preceding branch. source line 117.
  460. Introduce proof leaf: Gamma together with assumption A, labeled n for discharge. source line 133.
  461. Label the next inference: delta one. source line 134.
  462. State the derived proof line: formula B. source line 135.
  463. Apply the conditional introduction rule and discharge assumptions labeled n. source line 136.
  464. Infer: if A, then B from one preceding branch. source line 137.
  465. Introduce proof leaf: Gamma. source line 157.
  466. Label the next inference: delta one. source line 158.
  467. State the derived proof line: a contradiction. source line 159.
  468. Label the next inference: intuitionistic absurdity rule. source line 160.
  469. Infer: formula A from one preceding branch. source line 161.
  470. Introduce proof leaf: Gamma. source line 177.
  471. Label the next inference: delta one. source line 178.
  472. State the derived proof line: A of a. source line 179.
  473. Label the next inference: universal introduction rule. source line 180.
  474. Infer: for every x, A of x from one preceding branch. source line 181.
  475. Introduce proof leaf: Gamma one. source line 219.
  476. Label the next inference: delta one. source line 220.
  477. State the derived proof line: formula A. source line 221.
  478. Introduce proof leaf: Gamma two. source line 222.
  479. Label the next inference: delta two. source line 223.
  480. State the derived proof line: formula B. source line 224.
  481. Label the next inference: conjunction introduction rule. source line 225.
  482. Infer: A and B from two preceding branches. source line 226.
  483. Introduce proof leaf: Gamma one. source line 247.
  484. Label the next inference: delta one. source line 248.
  485. State the derived proof line: if A, then B. source line 249.
  486. Introduce proof leaf: Gamma two. source line 250.
  487. Label the next inference: delta two. source line 251.
  488. State the derived proof line: formula A. source line 252.
  489. Label the next inference: conditional elimination rule. source line 253.
  490. Infer: formula B from two preceding branches. source line 254.
  491. Introduce proof leaf with an empty premise. source line 16.
  492. Label the next inference: identity introduction rule. source line 17.
  493. Infer: t equals t from one preceding branch. source line 18.
  494. End and display this proof diagram. source line 19.
  495. Introduce proof leaf: t one equals t two. source line 22.
  496. Introduce proof leaf: A of t one. source line 23.
  497. Label the next inference: identity elimination rule. source line 24.
  498. Infer: A of t two from two preceding branches. source line 25.
  499. End and display this proof diagram. source line 26.
  500. Introduce proof leaf: t one equals t two. source line 28.
  501. Introduce proof leaf: A of t two. source line 29.
  502. Label the next inference: identity elimination rule. source line 30.
  503. Infer: A of t one from two preceding branches. source line 31.
  504. End and display this proof diagram. source line 32.
  505. Introduce proof leaf: s equals t. source line 43.
  506. Introduce proof leaf: A of s. source line 44.
  507. Label the next inference: identity elimination rule. source line 45.
  508. Infer: A of t from two preceding branches. source line 46.
  509. Introduce proof leaf: the existential statement that there exists an x such that every A object equals x, together with the single conjunctive assumption that A holds of both a and b, carrying label one for discharge. source line 68.
  510. State the derived proof line: a equals b. source line 70.
  511. Apply the conditional introduction rule and discharge assumptions labeled one. source line 71.
  512. Infer: if both A of a and A of b, then a equals b from one preceding branch. source line 72.
  513. Label the next inference: universal introduction rule. source line 73.
  514. Infer: for every y, if both A of a and A of y, then a equals y from one preceding branch. source line 74.
  515. Label the next inference: universal introduction rule. source line 75.
  516. Infer: for every x and every y, if both A of x and A of y, then x equals y from one preceding branch. source line 76.
  517. Introduce proof leaf: there exists an x such that, for every y, if A of y, then y equals x. source line 82.
  518. Introduce proof leaf: assumption: for every y, if A of y then y equals c; labeled two for discharge. source line 83.
  519. Suppress the inference bar at this proof step. source line 84.
  520. Infer: the single assumption that is the conjunction of A of a with A of b, labeled one for discharge from one preceding branch. source line 85.
  521. State the derived proof line: a equals b. source line 86.
  522. Apply the existential elimination rule and discharge assumptions labeled two. source line 87.
  523. Infer: a equals b from two preceding branches. source line 88.
  524. Apply the conditional introduction rule and discharge assumptions labeled one. source line 89.
  525. Infer: if both A of a and A of b, then a equals b from one preceding branch. source line 90.
  526. Label the next inference: universal introduction rule. source line 91.
  527. Infer: for every y, if both A of a and A of y, then a equals y from one preceding branch. source line 92.
  528. Label the next inference: universal introduction rule. source line 93.
  529. Infer: for every x and every y, if both A of x and A of y, then x equals y from one preceding branch. source line 94.
  530. Introduce proof leaf: assumption: for every y, if A of y then y equals c; labeled two for discharge. source line 101.
  531. Label the next inference: universal elimination rule. source line 102.
  532. Infer: if A of a, then a equals c from one preceding branch. source line 103.
  533. Introduce proof leaf: the single assumption that is the conjunction of A of a with A of b, labeled one for discharge. source line 104.
  534. Label the next inference: conjunction elimination rule. source line 105.
  535. Infer: A of a from one preceding branch. source line 106.
  536. Label the next inference: conditional elimination rule. source line 107.
  537. Infer: a equals c from two preceding branches. source line 108.
  538. Introduce proof leaf: Gamma one. source line 26.
  539. Label the next inference: delta one. source line 27.
  540. State the derived proof line: t one equals t two. source line 28.
  541. Introduce proof leaf: Gamma two. source line 29.
  542. Label the next inference: delta two. source line 30.
  543. State the derived proof line: A of t one. source line 31.
  544. Label the next inference: identity elimination rule. source line 32.
  545. Infer: A of t two from two preceding branches. source line 33.