The Open Logic Text — accessible offline edition

Axiomatic Deduction — Explore equations

Axiomatic Deduction

Reading preferences

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

Equation, formal-object, and reference guide

This guide exposes 209 expression records, 424 native MathML roots including six source-fidelity comparison variants, 61 formal objects, 283 ordered components, 84 references, and all eight exercises without adding solutions.

209 expression records

Expression 3

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula A is axiomatically derivable from the premise set containing not not A

Means here: The statement is read 'the complete formula A is axiomatically derivable from the premise set containing not not A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 113, column 8

Expression 5

Inline MathML variant

(E→(D→E))→((¬D∨E)→(D→E))(!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E))

Block MathML variant

(E→(D→E))→((¬D∨E)→(D→E))(!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E))

Read as: open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 35, column 8

Expression 6

Inline MathML variant

C→B(c)!C \lif !B(c)

Block MathML variant

C→B(c)!C \lif !B(c)

Read as: the conditional whose antecedent is formula C; and whose consequent is formula B with argument constant c

Means here: The first-order formula read 'the conditional whose antecedent is formula C; and whose consequent is formula B with argument constant c' preserves its metavariables, connectives, term arguments, and written grouping.

1 occurrence
  1. Occurrence 1: soundness.tex, line 81, column 27

Expression 7

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula not A implies open parenthesis A implies falsum close parenthesis is derivable with no premises

Means here: The statement is read 'the complete formula not A implies open parenthesis A implies falsum close parenthesis is derivable with no premises'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

2 occurrences
  1. Occurrence 1: provability-consistency.tex, line 42, column 1
  2. Occurrence 2: provability-propositional.tex, line 50, column 43

Expression 8

Inline MathML variant

Γ⊢(¬A→⊥)→¬¬A\Gamma \Proves (\lnot !A \lif \lfalse) \lif \lnot\lnot !A

Block MathML variant

Γ⊢(¬A→⊥)→¬¬A\Gamma \Proves (\lnot !A \lif \lfalse) \lif \lnot\lnot !A

Read as: the complete formula open parenthesis not A implies falsum close parenthesis implies not not A is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula open parenthesis not A implies falsum close parenthesis implies not not A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 48, column 33

Expression 9

Inline MathML variant

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

Block MathML variant

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

Source-fidelity inline MathML

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

Source-fidelity block MathML

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

Read as: the complete formula open parenthesis A implies B close parenthesis implies open parenthesis open parenthesis B implies C close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis is derivable with no premises

Means here: The statement is read 'the complete formula open parenthesis A implies B close parenthesis implies open parenthesis open parenthesis B implies C close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis is derivable with no premises'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 106, column 7

Expression 10

Inline MathML variant

Bl=B!B_l = !B

Block MathML variant

Bl=B!B_l = !B

Read as: B sub l equals B

Means here: The equation is read 'B sub l equals B'. It identifies the indexed derivation formula with the named final formula.

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

Expression 11

Inline MathML variant

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

Block MathML variant

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

Read as: Gamma syntactically derives formula A with argument constant c

Means here: The expression read 'Gamma syntactically derives formula A with argument constant c' asserts existence of a finite first-order axiomatic derivation using the printed premises, axiom schemes, modus ponens, and quantifier rule.

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

Expression 13

Inline MathML variant

Γ⊢A(t2)\Gamma \Proves !A(t_2)

Block MathML variant

Γ⊢A(t2)\Gamma \Proves !A(t_2)

Read as: Gamma syntactically derives formula A with argument term t sub two

Means here: The expression read 'Gamma syntactically derives formula A with argument term t sub two' asserts existence of a finite first-order axiomatic derivation using the printed premises, axiom schemes, modus ponens, and quantifier rule.

1 occurrence
  1. Occurrence 1: identity.tex, line 44, column 24

Expression 14

Inline MathML variant

Γ={A→B,B→C}\Gamma = \{!A \lif !B, !B \lif !C\}

Block MathML variant

Γ={A→B,B→C}\Gamma = \{!A \lif !B, !B \lif !C\}

Read as: Gamma equals the set containing A implies B comma B implies C

Means here: Gamma is defined as the two-premise set containing the conditional from A to B and the conditional from B to C.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 85, column 47

Expression 15

Inline MathML variant

Γ∪{C}⊨∀x(B(x))\Gamma \cup \{!C\} \Entails \lforall[x][!B(x)]

Block MathML variant

Γ∪{C}⊨∀x(B(x))\Gamma \cup \{!C\} \Entails \lforall[x][!B(x)]

Read as: the union of Gamma, and the set containing formula C semantically entails for every variable x, formula B with argument variable x

Means here: The expression read 'the union of Gamma, and the set containing formula C semantically entails for every variable x, formula B with argument variable x' states first-order semantic consequence over the named structures and assignments.

1 occurrence
  1. Occurrence 1: soundness.tex, line 105, column 37

Expression 16

Inline MathML variant

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

Block MathML variant

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

Read as: the conditional whose antecedent is formula C; and whose consequent is for every variable x, B applied to variable x

Means here: The quantified first-order formula read 'the conditional whose antecedent is formula C; and whose consequent is for every variable x, B applied to variable x' preserves each bound variable, quantifier order, connective, and scope.

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

Expression 18

Inline MathML variant

Γ⊢⊥\Gamma \Proves \lfalse

Block MathML variant

Γ⊢⊥\Gamma \Proves \lfalse

Read as: the complete formula falsum is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula falsum is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

3 occurrences
  1. Occurrence 1: provability-consistency.tex, line 29, column 47
  2. Occurrence 2: provability-consistency.tex, line 67, column 3
  3. Occurrence 3: soundness.tex, line 131, column 6

Expression 19

Inline MathML variant

Γ⊢⊤→A(c)\Gamma \Proves \ltrue \lif !A(c)

Block MathML variant

Γ⊢⊤→A(c)\Gamma \Proves \ltrue \lif !A(c)

Read as: Gamma syntactically derives the conditional whose antecedent is the truth constant top; and whose consequent is formula A with argument constant c

Means here: The expression read 'Gamma syntactically derives the conditional whose antecedent is the truth constant top; and whose consequent is formula A with argument constant c' asserts existence of a finite first-order axiomatic derivation using the printed premises, axiom schemes, modus ponens, and quantifier rule.

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

Expression 21

Inline MathML variant

A⊢B!A \Proves !B

Block MathML variant

A⊢B!A \Proves !B

Read as: the complete formula B is axiomatically derivable from premise A

Means here: The statement is read 'the complete formula B is axiomatically derivable from premise A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

2 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 86, column 68
  2. Occurrence 2: deduction-theorem.tex, line 28, column 1

Expression 22

Inline MathML variant

A→B!A \lif !B

Block MathML variant

A→B!A \lif !B

Read as: A implies B

Means here: The complete first-order formula or truth-functional formula scheme is read 'A implies B'. Spoken parentheses and connective names preserve its printed logical scope.

9 occurrences
  1. Occurrence 1: proving-things.tex, line 20, column 16
  2. Occurrence 2: proving-things.tex, line 44, column 46
  3. Occurrence 3: proving-things.tex, line 66, column 61
  4. Occurrence 4: proving-things.tex, line 88, column 8
  5. Occurrence 5: proving-things.tex, line 108, column 41
  6. Occurrence 6: proving-things.tex, line 115, column 67
  7. Occurrence 7: deduction-theorem.tex, line 40, column 10
  8. Occurrence 8: deduction-theorem.tex, line 71, column 64
  9. Occurrence 9: provability-propositional.tex, line 75, column 12

Expression 23

Inline MathML variant

Bi=AB_i = !A

Block MathML variant

Bi=AB_i = !A

Read as: B sub i equals A

Means here: The equation is read 'B sub i equals A'. It identifies the indexed derivation formula with the named final formula.

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

Expression 24

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula not not A is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula not not A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 49, column 61

Expression 25

Inline MathML variant

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

Block MathML variant

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

Read as: structure M, under variable assignment lowercase s, satisfies formula A

Means here: The satisfaction claim read 'structure M, under variable assignment lowercase s, satisfies formula A' is evaluated in the named first-order structure and, when printed, the named variable assignment.

1 occurrence
  1. Occurrence 1: soundness.tex, line 37, column 6

Expression 26

Inline MathML variant

xx

Block MathML variant

xx

Read as: variable x

Means here: The symbol read 'variable x' receives its exact term, variable, constant, or assignment role from each bound source occurrence.

1 occurrence
  1. Occurrence 1: soundness.tex, line 44, column 16

Expression 28

Inline MathML variant

(D→(D→D))→(D→D)(!D \lif (!D \lif !D)) \lif (!D \lif !D)

Block MathML variant

(D→(D→D))→(D→D)(!D \lif (!D \lif !D)) \lif (!D \lif !D)

Read as: open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 76, column 8

Expression 29

Inline MathML variant

A≡⊥!A \ident \lfalse

Block MathML variant

A≡⊥!A \ident \lfalse

Read as: A is syntactically identical to falsum

Means here: The expression is read 'A is syntactically identical to falsum'. It states syntactic identity of the two complete formulas, not merely semantic equivalence.

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

Expression 31

Inline MathML variant

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

Block MathML variant

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

Read as: formula A with argument term t syntactically derives for some variable x, formula A with argument variable x

Means here: The expression read 'formula A with argument term t syntactically derives for some variable x, formula A with argument variable x' asserts existence of a finite first-order axiomatic derivation using the printed premises, axiom schemes, modus ponens, and quantifier rule.

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

Expression 32

Inline MathML variant

B∈Γ∪{A}!B \in \Gamma \cup \{!A\}

Block MathML variant

B∈Γ∪{A}!B \in \Gamma \cup \{!A\}

Read as: B belongs to Gamma union the set containing A

Means here: The expression is read 'B belongs to Gamma union the set containing A'. This states that the displayed formula belongs to the displayed premise set.

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

Expression 33

Inline MathML variant

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

Block MathML variant

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

Read as: not open parenthesis A or B close parenthesis implies not A

Means here: The complete first-order formula or truth-functional formula scheme is read 'not open parenthesis A or B close parenthesis implies not A'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 34

Inline MathML variant

A(a)→B!A(a) \lif !B

Block MathML variant

A(a)→B!A(a) \lif !B

Read as: the conditional whose antecedent is formula A with argument constant a; and whose consequent is formula B

Means here: The first-order formula read 'the conditional whose antecedent is formula A with argument constant a; and whose consequent is formula B' preserves its metavariables, connectives, term arguments, and written grouping.

1 occurrence
  1. Occurrence 1: axioms-rules-quantifiers.tex, line 27, column 10

Expression 35

Inline MathML variant

((A∧B)→C)→(A→(B→C))((!A \land !B) \lif !C) \lif (!A \lif (!B \lif !C))

Block MathML variant

((A∧B)→C)→(A→(B→C))((!A \land !B) \lif !C) \lif (!A \lif (!B \lif !C))

Read as: open parenthesis open parenthesis A and B close parenthesis implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis open parenthesis A and B close parenthesis implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 36

Inline MathML variant

Γ⊢A→C\Gamma \Proves !A \lif !C

Block MathML variant

Γ⊢A→C\Gamma \Proves !A \lif !C

Read as: the complete formula A implies C is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula A implies C is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 103, column 29

Expression 38

Inline MathML variant

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

Block MathML variant

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

Read as: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis

Means here: The quantified first-order formula read 'the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis' preserves each bound variable, quantifier order, connective, and scope.

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

Expression 39

Inline MathML variant

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

Block MathML variant

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

Read as: structure M, under variable assignment s prime, satisfies formula A

Means here: The satisfaction claim read 'structure M, under variable assignment s prime, satisfies formula A' is evaluated in the named first-order structure and, when printed, the named variable assignment.

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

Expression 40

Inline MathML variant

Γ∪{¬A}⊢¬B\Gamma \cup \{ \lnot !A\} \Proves \lnot !B

Block MathML variant

Γ∪{¬A}⊢¬B\Gamma \cup \{ \lnot !A\} \Proves \lnot !B

Read as: the complete formula not B is axiomatically derivable from the union of Gamma and the singleton set containing not A

Means here: The statement is read 'the complete formula not B is axiomatically derivable from the union of Gamma and the singleton set containing not A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 108, column 10

Expression 41

Inline MathML variant

{A,¬A}⊢B\{ !A, \lnot!A\} \Proves !B

Block MathML variant

{A,¬A}⊢B\{ !A, \lnot!A\} \Proves !B

Read as: the complete formula B is axiomatically derivable from the displayed premises the set containing A comma not A

Means here: The statement is read 'the complete formula B is axiomatically derivable from the displayed premises the set containing A comma not A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 111, column 8

Expression 42

Inline MathML variant

A1,…,Ak=A,B1,…,Bl=B.!A_1, \dots, !A_k = !A, !B_1, \dots, !B_l = !B.

Block MathML variant

A1,…,Ak=A,B1,…,Bl=B.!A_1, \dots, !A_k = !A, !B_1, \dots, !B_l = !B.

Read as: derivation A sub one through A sub k, whose last formula is A; followed by derivation B sub one through B sub l, whose last formula is B

Means here: The displayed text concatenates a derivation ending in A with a derivation ending in B, preserving both indexed endpoints.

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

Expression 43

Inline MathML variant

M′⊨Γ∪{C}\Sat{M'}{\Gamma \cup \{!C\}}

Block MathML variant

M′⊨Γ∪{C}\Sat{M'}{\Gamma \cup \{!C\}}

Read as: structure M prime satisfies the union of Gamma, and the set containing formula C

Means here: The satisfaction claim read 'structure M prime satisfies the union of Gamma, and the set containing formula C' is evaluated in the named first-order structure and, when printed, the named variable assignment.

1 occurrence
  1. Occurrence 1: soundness.tex, line 95, column 32

Expression 44

Inline MathML variant

D→D!D \lif !D

Block MathML variant

D→D!D \lif !D

Read as: D implies D

Means here: The complete first-order formula or truth-functional formula scheme is read 'D implies D'. Spoken parentheses and connective names preserve its printed logical scope.

4 occurrences
  1. Occurrence 1: proving-things.tex, line 42, column 38
  2. Occurrence 2: proving-things.tex, line 46, column 57
  3. Occurrence 3: proving-things.tex, line 64, column 44
  4. Occurrence 4: proving-things.tex, line 78, column 8

Expression 45

Inline MathML variant

∃x(D(x))→C\lexists[x][!D(x)] \lif !C

Block MathML variant

∃x(D(x))→C\lexists[x][!D(x)] \lif !C

Read as: the conditional whose antecedent is for some variable x, formula D with argument variable x; and whose consequent is formula C

Means here: The quantified first-order formula read 'the conditional whose antecedent is for some variable x, formula D with argument variable x; and whose consequent is formula C' preserves each bound variable, quantifier order, connective, and scope.

1 occurrence
  1. Occurrence 1: deduction-theorem-quantifiers.tex, line 51, column 10

Expression 46

Inline MathML variant

s′(x)=⟦t⟧M,ss'(x) = \Value{t}{M}[s]

Block MathML variant

s′(x)=⟦t⟧M,ss'(x) = \Value{t}{M}[s]

Read as: variable assignment s prime at variable x equals the value of term t in structure M under variable assignment lowercase s

Means here: The semantic term read 'variable assignment s prime at variable x equals the value of term t in structure M under variable assignment lowercase s' specifies an interpretation, term value, or assignment relation in a first-order structure.

1 occurrence
  1. Occurrence 1: soundness.tex, line 47, column 19

Expression 47

Inline MathML variant

B∈{A}!B \in \{ !A\}

Block MathML variant

B∈{A}!B \in \{ !A\}

Read as: B belongs to the set containing A

Means here: The expression is read 'B belongs to the set containing A'. This states that the displayed formula belongs to the displayed premise set.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 70, column 55

Expression 48

Inline MathML variant

Γ⊬⊥\Gamma\Proves/ \lfalse

Block MathML variant

Γ⊬⊥\Gamma\Proves/ \lfalse

Read as: the complete formula falsum is not axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula falsum is not axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 49

Inline MathML variant

{A}∪Δ⊢B\{!A\} \cup \Delta \Proves !B

Block MathML variant

{A}∪Δ⊢B\{!A\} \cup \Delta \Proves !B

Read as: the complete formula B is axiomatically derivable from the union of the singleton set containing A and Delta

Means here: The statement is read 'the complete formula B is axiomatically derivable from the union of the singleton set containing A and Delta'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

2 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 65, column 28
  2. Occurrence 2: proof-theoretic-notions.tex, line 70, column 11

Expression 50

Inline MathML variant

Γ∪{B}⊢A\Gamma \cup \{ !B\} \Proves !A

Block MathML variant

Γ∪{B}⊢A\Gamma \cup \{ !B\} \Proves !A

Read as: the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing B

Means here: The statement is read 'the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 109, column 26

Expression 51

Inline MathML variant

Γ⊢¬A→⊥\Gamma \Proves \lnot !A \lif \lfalse

Block MathML variant

Γ⊢¬A→⊥\Gamma \Proves \lnot !A \lif \lfalse

Read as: the complete formula not A implies falsum is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula not A implies falsum is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 47, column 63

Expression 53

Inline MathML variant

Γ\Gamma

Block MathML variant

Γ\Gamma

Read as: Gamma

Means here: Gamma is the set of premise formulas from which axiomatic derivability is considered.

46 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 25, column 4
  2. Occurrence 2: rules-and-proofs.tex, line 26, column 28
  3. Occurrence 3: rules-and-proofs.tex, line 45, column 60
  4. Occurrence 4: rules-and-proofs.tex, line 53, column 27
  5. Occurrence 5: rules-and-proofs.tex, line 78, column 57
  6. Occurrence 6: rules-and-proofs.tex, line 84, column 49
  7. Occurrence 7: rules-and-proofs.tex, line 85, column 55
  8. Occurrence 8: axioms-rules-quantifiers.tex, line 25, column 21
  9. Occurrence 9: axioms-rules-quantifiers.tex, line 28, column 21
  10. Occurrence 10: proving-things.tex, line 84, column 42
  11. Occurrence 11: proving-things.tex, line 98, column 45
  12. Occurrence 12: proving-things.tex, line 108, column 59
  13. Occurrence 13: proving-things.tex, line 109, column 44
  14. Occurrence 14: proving-things.tex, line 113, column 25
  15. Occurrence 15: proof-theoretic-notions.tex, line 27, column 49
  16. Occurrence 16: proof-theoretic-notions.tex, line 28, column 55
  17. Occurrence 17: proof-theoretic-notions.tex, line 39, column 7
  18. Occurrence 18: proof-theoretic-notions.tex, line 49, column 66
  19. Occurrence 19: proof-theoretic-notions.tex, line 59, column 33
  20. Occurrence 20: proof-theoretic-notions.tex, line 74, column 53
  21. Occurrence 21: proof-theoretic-notions.tex, line 76, column 26
  22. Occurrence 22: proof-theoretic-notions.tex, line 93, column 1
  23. Occurrence 23: proof-theoretic-notions.tex, line 117, column 35
  24. Occurrence 24: proof-theoretic-notions.tex, line 118, column 22
  25. Occurrence 25: proof-theoretic-notions.tex, line 126, column 62
  26. Occurrence 26: proof-theoretic-notions.tex, line 128, column 50
  27. Occurrence 27: deduction-theorem-quantifiers.tex, line 31, column 60
  28. Occurrence 28: provability-consistency.tex, line 21, column 8
  29. Occurrence 29: provability-consistency.tex, line 30, column 19
  30. Occurrence 30: provability-consistency.tex, line 61, column 58
  31. Occurrence 31: provability-consistency.tex, line 73, column 22
  32. Occurrence 32: provability-quantifiers.tex, line 23, column 4
  33. Occurrence 33: provability-quantifiers.tex, line 29, column 23
  34. Occurrence 34: soundness.tex, line 23, column 49
  35. Occurrence 35: soundness.tex, line 25, column 32
  36. Occurrence 36: soundness.tex, line 61, column 1
  37. Occurrence 37: soundness.tex, line 63, column 4
  38. Occurrence 38: soundness.tex, line 81, column 59
  39. Occurrence 39: soundness.tex, line 95, column 14
  40. Occurrence 40: soundness.tex, line 126, column 4
  41. Occurrence 41: soundness.tex, line 130, column 44
  42. Occurrence 42: soundness.tex, line 132, column 16
  43. Occurrence 43: soundness.tex, line 134, column 16
  44. Occurrence 44: soundness.tex, line 138, column 54
  45. Occurrence 45: soundness.tex, line 139, column 1
  46. Occurrence 46: identity.tex, line 39, column 55

Expression 54

Inline MathML variant

⊢\Proves

Block MathML variant

⊢\Proves

Read as: axiomatic derivability

Means here: The statement is read 'axiomatic derivability'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

3 occurrences
  1. Occurrence 1: provability-propositional.tex, line 16, column 51
  2. Occurrence 2: provability-quantifiers.tex, line 18, column 25
  3. Occurrence 3: identity.tex, line 14, column 53

Expression 55

Inline MathML variant

∃x(A(x))→B\lexists[x][!A(x)] \lif !B

Block MathML variant

∃x(A(x))→B\lexists[x][!A(x)] \lif !B

Read as: the conditional whose antecedent is for some variable x, formula A with argument variable x; and whose consequent is formula B

Means here: The quantified first-order formula read 'the conditional whose antecedent is for some variable x, formula A with argument variable x; and whose consequent is formula B' preserves each bound variable, quantifier order, connective, and scope.

1 occurrence
  1. Occurrence 1: axioms-rules-quantifiers.tex, line 28, column 44

Expression 56

Inline MathML variant

t2t_2

Block MathML variant

t2t_2

Read as: term t sub two

Means here: The symbol read 'term t sub two' receives its exact term, variable, constant, or assignment role from each bound source occurrence.

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

Expression 57

Inline MathML variant

Γ∪{A}⊢A→B\Gamma \cup \{!A\} \Proves !A \lif !B

Block MathML variant

Γ∪{A}⊢A→B\Gamma \cup \{!A\} \Proves !A \lif !B

Read as: the complete formula A implies B is axiomatically derivable from the union of Gamma and the singleton set containing A

Means here: The statement is read 'the complete formula A implies B is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 56, column 11

Expression 58

Inline MathML variant

cM′=s(x)\Assign{c}{M'} = s(x)

Block MathML variant

cM′=s(x)\Assign{c}{M'} = s(x)

Read as: the interpretation of constant c in structure M prime equals s applied to variable x

Means here: The semantic term read 'the interpretation of constant c in structure M prime equals s applied to variable x' specifies an interpretation, term value, or assignment relation in a first-order structure.

1 occurrence
  1. Occurrence 1: soundness.tex, line 94, column 31

Expression 59

Inline MathML variant

B(x)[c/x]\Subst{!B(x)}{c}{x}

Block MathML variant

B(x)[c/x]\Subst{!B(x)}{c}{x}

Read as: the result of substituting constant c for variable x in formula B with argument variable x

Means here: The substitution expression read 'the result of substituting constant c for variable x in formula B with argument variable x' replaces the stated free variable by the stated term, subject to the source convention.

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

Expression 60

Inline MathML variant

Γ⊆Δ\Gamma \subseteq \Delta

Block MathML variant

Γ⊆Δ\Gamma \subseteq \Delta

Read as: Gamma is a subset of Delta

Means here: The expression is read 'Gamma is a subset of Delta'. This states inclusion between the two displayed premise sets.

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

Expression 61

Inline MathML variant

D→(B→D)!D \lif (!B \lif !D)

Block MathML variant

D→(B→D)!D \lif (!B \lif !D)

Read as: D implies open parenthesis B implies D close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'D implies open parenthesis B implies D close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 67, column 24

Expression 62

Inline MathML variant

Γ⊢t1=t2\Gamma \Proves \eq[t_1][t_2]

Block MathML variant

Γ⊢t1=t2\Gamma \Proves \eq[t_1][t_2]

Read as: Gamma syntactically derives term t sub one is identical to term t sub two

Means here: The expression read 'Gamma syntactically derives term t sub one is identical to term t sub two' asserts existence of a finite first-order axiomatic derivation using the printed premises, axiom schemes, modus ponens, and quantifier rule.

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

Expression 63

Inline MathML variant

{¬A,¬B}⊢(A∨B)→⊥\{\lnot !A, \lnot !B\} \Proves (!A \lor !B) \lif \lfalse

Block MathML variant

{¬A,¬B}⊢(A∨B)→⊥\{\lnot !A, \lnot !B\} \Proves (!A \lor !B) \lif \lfalse

Read as: the complete formula open parenthesis A or B close parenthesis implies falsum is axiomatically derivable from the displayed premises the set containing not A comma not B

Means here: The statement is read 'the complete formula open parenthesis A or B close parenthesis implies falsum is axiomatically derivable from the displayed premises the set containing not A comma not B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 54, column 33

Expression 65

Inline MathML variant

Γ∪Δ⊢B\Gamma \cup \Delta \Proves !B

Block MathML variant

Γ∪Δ⊢B\Gamma \cup \Delta \Proves !B

Read as: the complete formula B is axiomatically derivable from the union of premise sets Gamma and Delta

Means here: The statement is read 'the complete formula B is axiomatically derivable from the union of premise sets Gamma and Delta'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 66

Inline MathML variant

(D→((D→D)→D))→continued on the next display line(!D \lif ((!D \lif !D) \lif !D)) \lif {}

Block MathML variant

(D→((D→D)→D))→continued on the next display line(!D \lif ((!D \lif !D) \lif !D)) \lif {}

Read as: open parenthesis D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis close parenthesis implies continued on the next display line

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis close parenthesis implies continued on the next display line'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 74, column 8

Expression 67

Inline MathML variant

formula row oneΓ∪{A}⊢C→D(a)and the induction hypothesis applies, that is, we have thatformula row twoΓ⊢A→(C→D(a))Byformula row three⊢(A→(C→D(a)))→((A∧C)→D(a))and modus ponens we getformula row fourΓ⊢(A∧C)→D(a)Since the eigenvariable condition still applies, we can add a step to this derivation justified by the quantifier rule, and getformula row fiveΓ⊢(A∧C)→∀x(D(x))We also haveformula row six⊢((A∧C)→∀x(D(x)))→(A→(C→∀x(D(x))))so by modus ponensformula row sevenΓ⊢A→(C→∀x(D(x)))\Gamma \cup \{!A\} & \Proves !C \lif !D(a),\\ \intertext{and the induction hypothesis applies, i.e., we have that} \Gamma & \Proves !A \lif (!C \lif !D(a)).\\ \intertext{By} & \Proves (!A \lif (!C \lif !D(a))) \lif ((!A \land !C) \lif !D(a))\\ \intertext{and modus ponens we get} \Gamma & \Proves (!A \land !C) \lif !D(a).\\ \intertext{Since the eigenvariable condition still applies, we can add a step to this !!{derivation} justified by \QR, and get} \Gamma & \Proves (!A \land !C) \lif \lforall[x][!D(x)].\\ \intertext{We also have} & \Proves ((!A \land !C) \lif \lforall[x][!D(x)]) \lif (!A \lif (!C \lif \lforall[x][!D(x)]),\\ \intertext{so by modus ponens,} \Gamma & \Proves !A \lif (!C \lif \lforall[x][!D(x)]),

Block MathML variant

formula row oneΓ∪{A}⊢C→D(a)and the induction hypothesis applies, that is, we have thatformula row twoΓ⊢A→(C→D(a))Byformula row three⊢(A→(C→D(a)))→((A∧C)→D(a))and modus ponens we getformula row fourΓ⊢(A∧C)→D(a)Since the eigenvariable condition still applies, we can add a step to this derivation justified by the quantifier rule, and getformula row fiveΓ⊢(A∧C)→∀x(D(x))We also haveformula row six⊢((A∧C)→∀x(D(x)))→(A→(C→∀x(D(x))))so by modus ponensformula row sevenΓ⊢A→(C→∀x(D(x)))\Gamma \cup \{!A\} & \Proves !C \lif !D(a),\\ \intertext{and the induction hypothesis applies, i.e., we have that} \Gamma & \Proves !A \lif (!C \lif !D(a)).\\ \intertext{By} & \Proves (!A \lif (!C \lif !D(a))) \lif ((!A \land !C) \lif !D(a))\\ \intertext{and modus ponens we get} \Gamma & \Proves (!A \land !C) \lif !D(a).\\ \intertext{Since the eigenvariable condition still applies, we can add a step to this !!{derivation} justified by \QR, and get} \Gamma & \Proves (!A \land !C) \lif \lforall[x][!D(x)].\\ \intertext{We also have} & \Proves ((!A \land !C) \lif \lforall[x][!D(x)]) \lif (!A \lif (!C \lif \lforall[x][!D(x)]),\\ \intertext{so by modus ponens,} \Gamma & \Proves !A \lif (!C \lif \lforall[x][!D(x)]),

Source-fidelity inline MathML

formula row oneΓ∪{A}⊢C→D(a)and the induction hypothesis applies, that is, we have thatformula row twoΓ⊢A→(C→D(a))Byformula row three⊢(A→(C→D(a)))→((A∧C)→D(a))and modus ponens we getformula row fourΓ⊢(A∧C)→D(a)Since the eigenvariable condition still applies, we can add a step to this derivation justified by the quantifier rule, and getformula row fiveΓ⊢(A∧C)→∀x(D(x))We also haveformula row six⊢((A∧C)→∀x(D(x)))→(A→(C→∀x(D(x)))so by modus ponensformula row sevenΓ⊢A→(C→∀x(D(x)))\Gamma \cup \{!A\} & \Proves !C \lif !D(a),\\ \intertext{and the induction hypothesis applies, i.e., we have that} \Gamma & \Proves !A \lif (!C \lif !D(a)).\\ \intertext{By} & \Proves (!A \lif (!C \lif !D(a))) \lif ((!A \land !C) \lif !D(a))\\ \intertext{and modus ponens we get} \Gamma & \Proves (!A \land !C) \lif !D(a).\\ \intertext{Since the eigenvariable condition still applies, we can add a step to this !!{derivation} justified by \QR, and get} \Gamma & \Proves (!A \land !C) \lif \lforall[x][!D(x)].\\ \intertext{We also have} & \Proves ((!A \land !C) \lif \lforall[x][!D(x)]) \lif (!A \lif (!C \lif \lforall[x][!D(x)]),\\ \intertext{so by modus ponens,} \Gamma & \Proves !A \lif (!C \lif \lforall[x][!D(x)]),

Source-fidelity block MathML

formula row oneΓ∪{A}⊢C→D(a)and the induction hypothesis applies, that is, we have thatformula row twoΓ⊢A→(C→D(a))Byformula row three⊢(A→(C→D(a)))→((A∧C)→D(a))and modus ponens we getformula row fourΓ⊢(A∧C)→D(a)Since the eigenvariable condition still applies, we can add a step to this derivation justified by the quantifier rule, and getformula row fiveΓ⊢(A∧C)→∀x(D(x))We also haveformula row six⊢((A∧C)→∀x(D(x)))→(A→(C→∀x(D(x)))so by modus ponensformula row sevenΓ⊢A→(C→∀x(D(x)))\Gamma \cup \{!A\} & \Proves !C \lif !D(a),\\ \intertext{and the induction hypothesis applies, i.e., we have that} \Gamma & \Proves !A \lif (!C \lif !D(a)).\\ \intertext{By} & \Proves (!A \lif (!C \lif !D(a))) \lif ((!A \land !C) \lif !D(a))\\ \intertext{and modus ponens we get} \Gamma & \Proves (!A \land !C) \lif !D(a).\\ \intertext{Since the eigenvariable condition still applies, we can add a step to this !!{derivation} justified by \QR, and get} \Gamma & \Proves (!A \land !C) \lif \lforall[x][!D(x)].\\ \intertext{We also have} & \Proves ((!A \land !C) \lif \lforall[x][!D(x)]) \lif (!A \lif (!C \lif \lforall[x][!D(x)]),\\ \intertext{so by modus ponens,} \Gamma & \Proves !A \lif (!C \lif \lforall[x][!D(x)]),

Read as: displayed formula: formula row one: the union of Gamma, and the set containing formula A syntactically derives the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a. The induction hypothesis therefore gives formula row two: Gamma syntactically derives the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a, close parenthesis. Next, formula row three: no premises syntactically derives the conditional whose antecedent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a, close parenthesis, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is formula D with argument constant a, close parenthesis. By this formula and modus ponens, we get formula row four: Gamma syntactically derives the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is formula D with argument constant a. Since the eigenvariable condition still applies, we can add a step to this derivation justified by the quantifier rule, and get formula row five: Gamma syntactically derives the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is for every variable x, formula D with argument variable x. We also have formula row six: no premises syntactically derives the conditional whose antecedent is open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is for every variable x, formula D with argument variable x, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is for every variable x, formula D with argument variable x, close parenthesis, close parenthesis. So, by modus ponens, formula row seven: Gamma syntactically derives the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is for every variable x, formula D with argument variable x, close parenthesis.

Means here: The expression read 'formula row one: the union of Gamma, and the set containing formula A syntactically derives the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a The source then says that the induction hypothesis applies, that is, we have that formula row two: Gamma syntactically derives the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a, close parenthesis The source then invokes formula row three: no premises syntactically derives the conditional whose antecedent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a, close parenthesis, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is formula D with argument constant a, close parenthesis By this result and modus ponens, the source obtains formula row four: Gamma syntactically derives the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is formula D with argument constant a The source next notes that the eigenvariable condition still applies, we can add a step to this derivation justified by the quantifier rule, and get formula row five: Gamma syntactically derives the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is for every variable x, formula D with argument variable x The source next gives formula row six: no premises syntactically derives the conditional whose antecedent is open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is for every variable x, formula D with argument variable x, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is for every variable x, formula D with argument variable x, close parenthesis, close parenthesis The source then applies modus ponens to obtain formula row seven: Gamma syntactically derives the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is for every variable x, formula D with argument variable x, close parenthesis' preserves every printed formula row and every intervening proof transition in source order.

1 occurrence
  1. Occurrence 1: deduction-theorem-quantifiers.tex, line 33, column 1

Expression 68

Inline MathML variant

Ai!A_i

Block MathML variant

Ai!A_i

Read as: A sub i

Means here: A sub i is the formula at derivation step i.

8 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 31, column 7
  2. Occurrence 2: rules-and-proofs.tex, line 32, column 7
  3. Occurrence 3: rules-and-proofs.tex, line 72, column 7
  4. Occurrence 4: rules-and-proofs.tex, line 76, column 27
  5. Occurrence 5: rules-and-proofs.tex, line 78, column 32
  6. Occurrence 6: proof-theoretic-notions.tex, line 75, column 58
  7. Occurrence 7: proof-theoretic-notions.tex, line 126, column 12
  8. Occurrence 8: proof-theoretic-notions.tex, line 128, column 30

Expression 69

Inline MathML variant

{A,A→B}⊢B\{!A, !A \lif !B\} \Proves !B

Block MathML variant

{A,A→B}⊢B\{!A, !A \lif !B\} \Proves !B

Read as: the complete formula B is axiomatically derivable from the displayed premises the set containing A comma A implies B

Means here: The statement is read 'the complete formula B is axiomatically derivable from the displayed premises the set containing A comma A implies B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 37, column 16

Expression 70

Inline MathML variant

((D→(D→D))→(D→D))((!D \lif (!D \lif !D)) \lif (!D \lif !D))

Block MathML variant

((D→(D→D))→(D→D))((!D \lif (!D \lif !D)) \lif (!D \lif !D))

Read as: open parenthesis open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 71

Inline MathML variant

E→(D→E)!E \lif (!D \lif !E)

Block MathML variant

E→(D→E)!E \lif (!D \lif !E)

Read as: E implies open parenthesis D implies E close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'E implies open parenthesis D implies E close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 29, column 40
  2. Occurrence 2: proving-things.tex, line 36, column 8

Expression 72

Inline MathML variant

Γ⊢⊤→∀x(A(x))\Gamma \Proves \ltrue \lif \lforall[x][!A(x)]

Block MathML variant

Γ⊢⊤→∀x(A(x))\Gamma \Proves \ltrue \lif \lforall[x][!A(x)]

Read as: Gamma syntactically derives the conditional whose antecedent is the truth constant top; and whose consequent is for every variable x, formula A with argument variable x

Means here: The expression read 'Gamma syntactically derives the conditional whose antecedent is the truth constant top; and whose consequent is for every variable x, formula A with argument variable x' asserts existence of a finite first-order axiomatic derivation using the printed premises, axiom schemes, modus ponens, and quantifier rule.

1 occurrence
  1. Occurrence 1: provability-quantifiers.tex, line 29, column 50

Expression 74

Inline MathML variant

Γ∪{C}⊨B(c)\Gamma \cup \{!C\} \Entails !B(c)

Block MathML variant

Γ∪{C}⊨B(c)\Gamma \cup \{!C\} \Entails !B(c)

Read as: the union of Gamma, and the set containing formula C semantically entails formula B with argument constant c

Means here: The expression read 'the union of Gamma, and the set containing formula C semantically entails formula B with argument constant c' states first-order semantic consequence over the named structures and assignments.

2 occurrences
  1. Occurrence 1: soundness.tex, line 84, column 38
  2. Occurrence 2: soundness.tex, line 96, column 50

Expression 75

Inline MathML variant

D→(D→D)!D \lif (!D \lif !D)

Block MathML variant

D→(D→D)!D \lif (!D \lif !D)

Read as: D implies open parenthesis D implies D close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'D implies open parenthesis D implies D close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 50, column 1
  2. Occurrence 2: proving-things.tex, line 77, column 8

Expression 76

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula not A is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula not A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 77

Inline MathML variant

s′=uivxs\varAssign{s'}{s}{x}

Block MathML variant

s′=uivxs\varAssign{s'}{s}{x}

Read as: variable assignment s prime agrees with variable assignment lowercase s except possibly at variable x

Means here: The semantic term read 'variable assignment s prime agrees with variable assignment lowercase s except possibly at variable x' specifies an interpretation, term value, or assignment relation in a first-order structure.

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

Expression 78

Inline MathML variant

Bi=A!B_i = !A

Block MathML variant

Bi=A!B_i = !A

Read as: B sub i equals A

Means here: The equation is read 'B sub i equals A'. It identifies the indexed derivation formula with the named final formula.

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

Expression 79

Inline MathML variant

=\eq

Block MathML variant

=\eq

Read as: identity sign

Means here: The logical notation read 'identity sign' names the exact connective, quantifier, identity sign, sequent arrow, or derivability relation printed by the source.

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

Expression 80

Inline MathML variant

(A∧B)→A(A∧B)→BA→(B→(A∧B))A→(A∨B)A→(B∨A)(A→C)→((B→C)→((A∨B)→C))A→(B→A)(A→(B→C))→((A→B)→(A→C))(A→B)→((A→¬B)→¬A)¬A→(A→B)⊤⊥→A(A→⊥)→¬A¬¬A→A& (!A \land !B) \lif !A \ollabel{ax:land1}\\ & (!A \land !B) \lif !B \ollabel{ax:land2}\\ & !A \lif (!B \lif (!A \land !B)) \ollabel{ax:land3}\\ & !A \lif (!A \lor !B) \ollabel{ax:lor1}\\ & !A \lif (!B \lor !A) \ollabel{ax:lor2}\\ & (!A \lif !C) \lif ((!B \lif !C) \lif ((!A \lor !B) \lif !C)) \ollabel{ax:lor3}\\ & !A \lif (!B \lif !A) \ollabel{ax:lif1}\\ & (!A \lif (!B \lif !C)) \lif ((!A \lif !B) \lif (!A \lif !C)) \ollabel{ax:lif2}\\ & (!A \lif !B) \lif ((!A \lif \lnot !B) \lif \lnot !A) \ollabel{ax:lnot1}\\ & \lnot !A \lif (!A \lif !B) \ollabel{ax:lnot2}\\ & \ltrue \ollabel{ax:ltrue}\\ & \lfalse \lif !A \ollabel{ax:lfalse1}\\ & (!A \lif \lfalse) \lif \lnot !A \ollabel{ax:lfalse2}\\ & \lnot\lnot !A \lif !A \ollabel{ax:dne}

Block MathML variant

(A∧B)→A(A∧B)→BA→(B→(A∧B))A→(A∨B)A→(B∨A)(A→C)→((B→C)→((A∨B)→C))A→(B→A)(A→(B→C))→((A→B)→(A→C))(A→B)→((A→¬B)→¬A)¬A→(A→B)⊤⊥→A(A→⊥)→¬A¬¬A→A& (!A \land !B) \lif !A \ollabel{ax:land1}\\ & (!A \land !B) \lif !B \ollabel{ax:land2}\\ & !A \lif (!B \lif (!A \land !B)) \ollabel{ax:land3}\\ & !A \lif (!A \lor !B) \ollabel{ax:lor1}\\ & !A \lif (!B \lor !A) \ollabel{ax:lor2}\\ & (!A \lif !C) \lif ((!B \lif !C) \lif ((!A \lor !B) \lif !C)) \ollabel{ax:lor3}\\ & !A \lif (!B \lif !A) \ollabel{ax:lif1}\\ & (!A \lif (!B \lif !C)) \lif ((!A \lif !B) \lif (!A \lif !C)) \ollabel{ax:lif2}\\ & (!A \lif !B) \lif ((!A \lif \lnot !B) \lif \lnot !A) \ollabel{ax:lnot1}\\ & \lnot !A \lif (!A \lif !B) \ollabel{ax:lnot2}\\ & \ltrue \ollabel{ax:ltrue}\\ & \lfalse \lif !A \ollabel{ax:lfalse1}\\ & (!A \lif \lfalse) \lif \lnot !A \ollabel{ax:lfalse2}\\ & \lnot\lnot !A \lif !A \ollabel{ax:dne}

Read as: fourteen axiom schemes in source order. Conjunction elimination left: open parenthesis A and B close parenthesis implies A. Conjunction elimination right: open parenthesis A and B close parenthesis implies B. Conjunction introduction: A implies open parenthesis B implies open parenthesis A and B close parenthesis close parenthesis. Disjunction introduction left: A implies open parenthesis A or B close parenthesis. Disjunction introduction right: A implies open parenthesis B or A close parenthesis. Disjunction elimination: open parenthesis A implies C close parenthesis implies open parenthesis open parenthesis B implies C close parenthesis implies open parenthesis open parenthesis A or B close parenthesis implies C close parenthesis close parenthesis. Conditional scheme one: A implies open parenthesis B implies A close parenthesis. Conditional scheme two: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis. Negation scheme one: open parenthesis A implies B close parenthesis implies open parenthesis open parenthesis A implies not B close parenthesis implies not A close parenthesis. Negation scheme two: not A implies open parenthesis A implies B close parenthesis. Truth scheme: verum. Falsity scheme one: falsum implies A. Falsity scheme two: open parenthesis A implies falsum close parenthesis implies not A. Double negation elimination: not not A implies A.

Means here: This is the complete ordered list of fourteen truth-functional axiom schemes used with first-order formulas; every connective scope and source label is preserved.

1 occurrence
  1. Occurrence 1: axioms-rules-propositional.tex, line 18, column 1

Expression 82

Inline MathML variant

Γ⊢(A→(C→B))→((A→C)→(A→B)),\Gamma \Proves (!A \lif (!C \lif !B)) \lif ((!A\lif !C) \lif (!A \lif !B)),

Block MathML variant

Γ⊢(A→(C→B))→((A→C)→(A→B)),\Gamma \Proves (!A \lif (!C \lif !B)) \lif ((!A\lif !C) \lif (!A \lif !B)),

Read as: from Gamma derive the conditional whose antecedent is the conditional from A to the conditional from C to B, and whose consequent is the conditional whose antecedent is the conditional from A to C and whose consequent is the conditional from A to B

Means here: The statement is read 'from Gamma derive the conditional whose antecedent is the conditional from A to the conditional from C to B, and whose consequent is the conditional whose antecedent is the conditional from A to C and whose consequent is the conditional from A to B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 89, column 1

Expression 83

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

Read as: the complete formula B is axiomatically derivable from the displayed premises A sub one comma through the omitted intermediate entries comma A sub n

Means here: The statement is read 'the complete formula B is axiomatically derivable from the displayed premises A sub one comma through the omitted intermediate entries comma A sub n'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 84

Inline MathML variant

Γ∪{A}⊢⊥\Gamma \cup \{!A\} \Proves \lfalse

Block MathML variant

Γ∪{A}⊢⊥\Gamma \cup \{!A\} \Proves \lfalse

Read as: the complete formula falsum is axiomatically derivable from the union of Gamma and the singleton set containing A

Means here: The statement is read 'the complete formula falsum is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 25, column 49

Expression 85

Inline MathML variant

M′,s⊨B(x)\Sat{M'}{!B(x)}[s]

Block MathML variant

M′,s⊨B(x)\Sat{M'}{!B(x)}[s]

Read as: structure M prime, under variable assignment lowercase s, satisfies formula B with argument variable x

Means here: The satisfaction claim read 'structure M prime, under variable assignment lowercase s, satisfies formula B with argument variable x' is evaluated in the named first-order structure and, when printed, the named variable assignment.

2 occurrences
  1. Occurrence 1: soundness.tex, line 99, column 43
  2. Occurrence 2: soundness.tex, line 102, column 1

Expression 86

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula A implies B is axiomatically derivable from premise B

Means here: The statement is read 'the complete formula A implies B is axiomatically derivable from premise B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 87

Inline MathML variant

∃x(B(x))→C\lexists[x][!B(x)] \lif !C

Block MathML variant

∃x(B(x))→C\lexists[x][!B(x)] \lif !C

Read as: the conditional whose antecedent is for some variable x, formula B with argument variable x; and whose consequent is formula C

Means here: The quantified first-order formula read 'the conditional whose antecedent is for some variable x, formula B with argument variable x; and whose consequent is formula C' preserves each bound variable, quantifier order, connective, and scope.

1 occurrence
  1. Occurrence 1: soundness.tex, line 110, column 1

Expression 88

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

Read as: the three formulas A or B, not A, and not B

Means here: The complete first-order formula or truth-functional formula scheme is read 'the three formulas A or B, not A, and not B'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 89

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula A implies B is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula A implies B is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

9 occurrences
  1. Occurrence 1: proving-things.tex, line 102, column 27
  2. Occurrence 2: proving-things.tex, line 107, column 11
  3. Occurrence 3: deduction-theorem.tex, line 32, column 48
  4. Occurrence 4: deduction-theorem.tex, line 51, column 9
  5. Occurrence 5: deduction-theorem.tex, line 55, column 40
  6. Occurrence 6: deduction-theorem.tex, line 70, column 23
  7. Occurrence 7: deduction-theorem.tex, line 71, column 6
  8. Occurrence 8: deduction-theorem.tex, line 94, column 1
  9. Occurrence 9: deduction-theorem-quantifiers.tex, line 15, column 6

Expression 90

Inline MathML variant

formula row one(∀x(A(x))∧∀y(B(y)))→∀x(A(x))is an instance of the first conjunction axiom, andformula row two∀x(A(x))→A(a)of the universal-instantiation axiom. So, by the chain proposition, we know thatformula row three(∀x(A(x))∧∀y(B(y)))→A(a)is derivable. Likewise, sinceformula row four(∀x(A(x))∧∀y(B(y)))→∀y(B(y))formula row five∀y(B(y))→B(a)are instances of the second conjunction axiom and the universal-instantiation axiom, respectivelyformula row six(∀x(A(x))∧∀y(B(y)))→B(a)is derivable by the chain proposition. Using an appropriate instance of the conjunction-introduction axiom and two applications of modus ponens, we see thatformula row seven(∀x(A(x))∧∀y(B(y)))→(A(a)∧B(a))is derivable. We can now apply the quantifier rule to obtainformula row eight(∀x(A(x))∧∀y(B(y)))→∀x((A(x)∧B(x)))(\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif \lforall[x][!A(x)]\\ \intertext{is an instance of \olref[prp]{ax:land1}, and} \lforall[x][!A(x)] & \lif !A(a) \\ \intertext{of \olref[qua]{ax:q1}. So, by \olref[pro]{prop:chain}, we know that} (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif !A(a) \\ \intertext{is !!{derivable}. Likewise, since} (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif \lforall[y][!B(y)] \qquad\text{and}\\ \lforall[y][!B(y)] & \lif !B(a)\\ \intertext{are instances of \olref[prp]{ax:land2} and \olref[qua]{ax:q1}, respectively,} (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif !B(a)\\ \intertext{is derivable by \olref[pro]{prop:chain}. Using an appropriate instance of \olref[prp]{ax:land3} and two applications of~\MP, we see that} (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif (!A(a) \land !B(a))\\ \intertext{is derivable. We can now apply \QR{} to obtain} (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif \lforall[x][(!A(x) \land !B(x))].

Block MathML variant

formula row one(∀x(A(x))∧∀y(B(y)))→∀x(A(x))is an instance of the first conjunction axiom, andformula row two∀x(A(x))→A(a)of the universal-instantiation axiom. So, by the chain proposition, we know thatformula row three(∀x(A(x))∧∀y(B(y)))→A(a)is derivable. Likewise, sinceformula row four(∀x(A(x))∧∀y(B(y)))→∀y(B(y))formula row five∀y(B(y))→B(a)are instances of the second conjunction axiom and the universal-instantiation axiom, respectivelyformula row six(∀x(A(x))∧∀y(B(y)))→B(a)is derivable by the chain proposition. Using an appropriate instance of the conjunction-introduction axiom and two applications of modus ponens, we see thatformula row seven(∀x(A(x))∧∀y(B(y)))→(A(a)∧B(a))is derivable. We can now apply the quantifier rule to obtainformula row eight(∀x(A(x))∧∀y(B(y)))→∀x((A(x)∧B(x)))(\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif \lforall[x][!A(x)]\\ \intertext{is an instance of \olref[prp]{ax:land1}, and} \lforall[x][!A(x)] & \lif !A(a) \\ \intertext{of \olref[qua]{ax:q1}. So, by \olref[pro]{prop:chain}, we know that} (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif !A(a) \\ \intertext{is !!{derivable}. Likewise, since} (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif \lforall[y][!B(y)] \qquad\text{and}\\ \lforall[y][!B(y)] & \lif !B(a)\\ \intertext{are instances of \olref[prp]{ax:land2} and \olref[qua]{ax:q1}, respectively,} (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif !B(a)\\ \intertext{is derivable by \olref[pro]{prop:chain}. Using an appropriate instance of \olref[prp]{ax:land3} and two applications of~\MP, we see that} (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif (!A(a) \land !B(a))\\ \intertext{is derivable. We can now apply \QR{} to obtain} (\lforall[x][!A(x)] \land \lforall[y][!B(y)]) & \lif \lforall[x][(!A(x) \land !B(x))].

Read as: displayed formula: formula row one: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, formula A with argument variable x. This is an instance of the first conjunction axiom. Formula row two: the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is formula A with argument constant a. This is an instance of the universal-instantiation axiom. So, by the chain proposition, we know that formula row three: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is formula A with argument constant a. This formula is derivable. Likewise, since formula row four: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable y, formula B with argument variable y. And formula row five: the conditional whose antecedent is for every variable y, formula B with argument variable y; and whose consequent is formula B with argument constant a. These two formulas are instances of the second conjunction axiom and the universal-instantiation axiom, respectively. Formula row six: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is formula B with argument constant a. This formula is derivable by the chain proposition. Using an appropriate instance of the conjunction-introduction axiom and two applications of modus ponens, we see that formula row seven: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is open parenthesis, the conjunction of formula A with argument constant a and formula B with argument constant a, close parenthesis. This formula is derivable. We can now apply the quantifier rule to obtain formula row eight: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis.

Means here: The expression read 'formula row one: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, formula A with argument variable x The source then says that this formula is an instance of the first conjunction axiom, and formula row two: the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is formula A with argument constant a The source then identifies this formula as an instance of the universal-instantiation axiom. So, by the chain proposition, we know that formula row three: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is formula A with argument constant a The source then says that this formula is derivable. Likewise, since formula row four: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable y, formula B with argument variable y formula row five: the conditional whose antecedent is for every variable y, formula B with argument variable y; and whose consequent is formula B with argument constant a The source then says that these formulas are instances of the second conjunction axiom and the universal-instantiation axiom, respectively formula row six: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is formula B with argument constant a The source then says that this formula is derivable by the chain proposition. Using an appropriate instance of the conjunction-introduction axiom and two applications of modus ponens, we see that formula row seven: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is open parenthesis, the conjunction of formula A with argument constant a and formula B with argument constant a, close parenthesis The source then says that this formula is derivable. We can now apply the quantifier rule to obtain formula row eight: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis' preserves every printed formula row and every intervening proof transition in source order.

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

Expression 91

Inline MathML variant

A(x)!A(x)

Block MathML variant

A(x)!A(x)

Read as: formula A with argument variable x

Means here: The first-order formula read 'formula A with argument variable x' preserves its metavariables, connectives, term arguments, and written grouping.

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

Expression 92

Inline MathML variant

A!A

Block MathML variant

A!A

Read as: A

Means here: A is the arbitrary complete first-order formula used in this exact source statement.

41 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 48, column 46
  2. Occurrence 2: rules-and-proofs.tex, line 52, column 28
  3. Occurrence 3: rules-and-proofs.tex, line 55, column 15
  4. Occurrence 4: rules-and-proofs.tex, line 55, column 47
  5. Occurrence 5: rules-and-proofs.tex, line 58, column 6
  6. Occurrence 6: rules-and-proofs.tex, line 58, column 29
  7. Occurrence 7: rules-and-proofs.tex, line 65, column 8
  8. Occurrence 8: rules-and-proofs.tex, line 84, column 15
  9. Occurrence 9: rules-and-proofs.tex, line 86, column 4
  10. Occurrence 10: rules-and-proofs.tex, line 90, column 15
  11. Occurrence 11: rules-and-proofs.tex, line 91, column 4
  12. Occurrence 12: rules-and-proofs.tex, line 91, column 55
  13. Occurrence 13: axioms-rules-propositional.tex, line 37, column 67
  14. Occurrence 14: proving-things.tex, line 20, column 7
  15. Occurrence 15: proving-things.tex, line 21, column 52
  16. Occurrence 16: proving-things.tex, line 47, column 54
  17. Occurrence 17: proving-things.tex, line 54, column 24
  18. Occurrence 18: proving-things.tex, line 65, column 33
  19. Occurrence 19: proof-theoretic-notions.tex, line 27, column 15
  20. Occurrence 20: proof-theoretic-notions.tex, line 29, column 4
  21. Occurrence 21: proof-theoretic-notions.tex, line 33, column 15
  22. Occurrence 22: proof-theoretic-notions.tex, line 34, column 1
  23. Occurrence 23: proof-theoretic-notions.tex, line 34, column 52
  24. Occurrence 24: proof-theoretic-notions.tex, line 49, column 19
  25. Occurrence 25: proof-theoretic-notions.tex, line 49, column 56
  26. Occurrence 26: proof-theoretic-notions.tex, line 59, column 23
  27. Occurrence 27: proof-theoretic-notions.tex, line 60, column 1
  28. Occurrence 28: proof-theoretic-notions.tex, line 74, column 43
  29. Occurrence 29: proof-theoretic-notions.tex, line 93, column 60
  30. Occurrence 30: deduction-theorem.tex, line 39, column 10
  31. Occurrence 31: deduction-theorem-quantifiers.tex, line 31, column 51
  32. Occurrence 32: provability-propositional.tex, line 74, column 12
  33. Occurrence 33: soundness.tex, line 22, column 27
  34. Occurrence 34: soundness.tex, line 23, column 10
  35. Occurrence 35: soundness.tex, line 35, column 6
  36. Occurrence 36: soundness.tex, line 44, column 23
  37. Occurrence 37: soundness.tex, line 60, column 53
  38. Occurrence 38: soundness.tex, line 64, column 47
  39. Occurrence 39: soundness.tex, line 68, column 43
  40. Occurrence 40: soundness.tex, line 109, column 16
  41. Occurrence 41: soundness.tex, line 121, column 23

Expression 93

Inline MathML variant

Γ∪{A}⊢B\Gamma \cup \{!A\} \Proves !B

Block MathML variant

Γ∪{A}⊢B\Gamma \cup \{!A\} \Proves !B

Read as: the complete formula B is axiomatically derivable from the union of Gamma and the singleton set containing A

Means here: The statement is read 'the complete formula B is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

3 occurrences
  1. Occurrence 1: deduction-theorem.tex, line 50, column 29
  2. Occurrence 2: deduction-theorem.tex, line 58, column 56
  3. Occurrence 3: deduction-theorem-quantifiers.tex, line 14, column 34

Expression 94

Inline MathML variant

(t1=t2→(A(t1)→A(t2)))(\eq[t_1][t_2] \lif (!A(t_1) \lif !A(t_2)))

Block MathML variant

(t1=t2→(A(t1)→A(t2)))(\eq[t_1][t_2] \lif (!A(t_1) \lif !A(t_2)))

Read as: open parenthesis, the conditional whose antecedent states that term t sub one is identical to term t sub two; and whose consequent is open parenthesis, the conditional whose antecedent is formula A with argument term t sub one; and whose consequent is formula A with argument term t sub two, close parenthesis, close parenthesis

Means here: The identity expression read 'open parenthesis, the conditional whose antecedent states that term t sub one is identical to term t sub two; and whose consequent is open parenthesis, the conditional whose antecedent is formula A with argument term t sub one; and whose consequent is formula A with argument term t sub two, close parenthesis, close parenthesis' states equality of the named first-order terms or semantic values.

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

Expression 95

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula A or B is axiomatically derivable from premise B

Means here: The statement is read 'the complete formula A or B is axiomatically derivable from premise B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 96

Inline MathML variant

A≡An!A \ident !A_n

Block MathML variant

A≡An!A \ident !A_n

Read as: A is syntactically identical to A sub n

Means here: The expression is read 'A is syntactically identical to A sub n'. It states syntactic identity of the two complete formulas, not merely semantic equivalence.

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

Expression 98

Inline MathML variant

⊢¬B→(B→⊥)\Proves \lnot !B \lif (!B \lif \lfalse)

Block MathML variant

⊢¬B→(B→⊥)\Proves \lnot !B \lif (!B \lif \lfalse)

Read as: the complete formula not B implies open parenthesis B implies falsum close parenthesis is derivable with no premises

Means here: The statement is read 'the complete formula not B implies open parenthesis B implies falsum close parenthesis is derivable with no premises'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 51, column 24

Expression 99

Inline MathML variant

(¬D→(D→E))→((E→(D→E))→((¬D∨E)→(D→E))).(\lnot !D \lif (!D \lif !E)) \lif ((!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E))).

Block MathML variant

(¬D→(D→E))→((E→(D→E))→((¬D∨E)→(D→E))).(\lnot !D \lif (!D \lif !E)) \lif ((!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E))).

Read as: open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 100

Inline MathML variant

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

Block MathML variant

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

Read as: the union of Gamma, and the set containing formula C

Means here: The relation read 'the union of Gamma, and the set containing formula C' concerns the exact premise sets or formula sequences named by the source.

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

Expression 101

Inline MathML variant

Γ∪{A}⊢C\Gamma \cup \{!A\} \Proves !C

Block MathML variant

Γ∪{A}⊢C\Gamma \cup \{!A\} \Proves !C

Read as: the complete formula C is axiomatically derivable from the union of Gamma and the singleton set containing A

Means here: The statement is read 'the complete formula C is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 81, column 51

Expression 102

Inline MathML variant

(D→D)(!D \lif !D)

Block MathML variant

(D→D)(!D \lif !D)

Read as: open parenthesis D implies D close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis D implies D close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 103

Inline MathML variant

{¬B}⊢B→⊥\{\lnot !B\} \Proves !B \lif \lfalse

Block MathML variant

{¬B}⊢B→⊥\{\lnot !B\} \Proves !B \lif \lfalse

Read as: the complete formula B implies falsum is axiomatically derivable from the premise set containing not B

Means here: The statement is read 'the complete formula B implies falsum is axiomatically derivable from the premise set containing not B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 53, column 18

Expression 104

Inline MathML variant

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

Block MathML variant

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

Read as: the set containing A union Delta

Means here: The expression is read 'the set containing A union Delta'. This forms the union of the displayed premise sets.

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

Expression 105

Inline MathML variant

Γ⊢Ai\Gamma \Proves !A_i

Block MathML variant

Γ⊢Ai\Gamma \Proves !A_i

Read as: the complete formula A sub i is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula A sub i is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 106

Inline MathML variant

(¬D→(D→E))→continued on the next display line(\lnot !D \lif (!D \lif !E)) \lif {}

Block MathML variant

(¬D→(D→E))→continued on the next display line(\lnot !D \lif (!D \lif !E)) \lif {}

Read as: open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies continued on the next display line

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies continued on the next display line'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 33, column 8

Expression 107

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula B is axiomatically derivable from the displayed premises A comma A implies B

Means here: The statement is read 'the complete formula B is axiomatically derivable from the displayed premises A comma A implies B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

2 occurrences
  1. Occurrence 1: provability-propositional.tex, line 19, column 19
  2. Occurrence 2: provability-propositional.tex, line 64, column 46

Expression 108

Inline MathML variant

M⊨∀x(B(x))\Sat{M}{\lforall[x][!B(x)]}

Block MathML variant

M⊨∀x(B(x))\Sat{M}{\lforall[x][!B(x)]}

Read as: structure M satisfies for every variable x, formula B with argument variable x

Means here: The satisfaction claim read 'structure M satisfies for every variable x, formula B with argument variable x' is evaluated in the named first-order structure and, when printed, the named variable assignment.

2 occurrences
  1. Occurrence 1: soundness.tex, line 88, column 35
  2. Occurrence 2: soundness.tex, line 105, column 1

Expression 109

Inline MathML variant

Γ⊨B\Gamma \Entails !B

Block MathML variant

Γ⊨B\Gamma \Entails !B

Read as: the complete formula B is semantically entailed by premise set Gamma

Means here: The statement is read 'the complete formula B is semantically entailed by premise set Gamma'. Every first-order structure and variable assignment satisfying every formula in the displayed premise set also satisfies the complete conclusion.

1 occurrence
  1. Occurrence 1: soundness.tex, line 73, column 13

Expression 110

Inline MathML variant

A→A!A \lif !A

Block MathML variant

A→A!A \lif !A

Read as: A implies A

Means here: The complete first-order formula or truth-functional formula scheme is read 'A implies A'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 72, column 25

Expression 111

Inline MathML variant

¬D\lnot !D

Block MathML variant

¬D\lnot !D

Read as: not D

Means here: The complete first-order formula or truth-functional formula scheme is read 'not D'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 21, column 63

Expression 112

Inline MathML variant

Γ⊢¬A→(A→⊥)\Gamma \Proves \lnot !A \lif (!A \lif \lfalse)

Block MathML variant

Γ⊢¬A→(A→⊥)\Gamma \Proves \lnot !A \lif (!A \lif \lfalse)

Read as: the complete formula not A implies open parenthesis A implies falsum close parenthesis is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula not A implies open parenthesis A implies falsum close parenthesis is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 113

Inline MathML variant

⊤\top

Block MathML variant

⊤\top

Read as: the truth constant top

Means here: The expression read 'the truth constant top' denotes the truth constant used as the premise discharged by the deduction theorem.

1 occurrence
  1. Occurrence 1: provability-quantifiers.tex, line 29, column 35

Expression 114

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula not A is axiomatically derivable from the union of Gamma and the singleton set containing not A

Means here: The statement is read 'the complete formula not A is axiomatically derivable from the union of Gamma and the singleton set containing not A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 40, column 48

Expression 115

Inline MathML variant

C!C

Block MathML variant

C!C

Read as: C

Means here: C is the arbitrary complete first-order formula used in this exact source statement.

7 occurrences
  1. Occurrence 1: proving-things.tex, line 22, column 27
  2. Occurrence 2: proving-things.tex, line 65, column 42
  3. Occurrence 3: deduction-theorem.tex, line 80, column 37
  4. Occurrence 4: deduction-theorem.tex, line 80, column 64
  5. Occurrence 5: deduction-theorem-quantifiers.tex, line 31, column 45
  6. Occurrence 6: soundness.tex, line 82, column 1
  7. Occurrence 7: soundness.tex, line 95, column 26

Expression 116

Inline MathML variant

¬A∈Γ\lnot !A \in \Gamma

Block MathML variant

¬A∈Γ\lnot !A \in \Gamma

Read as: not A belongs to Gamma

Means here: The expression is read 'not A belongs to Gamma'. This states that the displayed formula belongs to the displayed premise set.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 61, column 30

Expression 117

Inline MathML variant

B=uivC→∀x(D(x))!B \ident !C \lif \lforall[x][!D(x)]

Block MathML variant

B=uivC→∀x(D(x))!B \ident !C \lif \lforall[x][!D(x)]

Read as: formula B is syntactically identical to the conditional whose antecedent is formula C; and whose consequent is for every variable x, formula D with argument variable x

Means here: The expression read 'formula B is syntactically identical to the conditional whose antecedent is formula C; and whose consequent is for every variable x, formula D with argument variable x' states that the two displayed formula forms are syntactically identical, not merely logically equivalent.

1 occurrence
  1. Occurrence 1: deduction-theorem-quantifiers.tex, line 29, column 27

Expression 119

Inline MathML variant

Γ⊢A(t1)\Gamma \Proves !A(t_1)

Block MathML variant

Γ⊢A(t1)\Gamma \Proves !A(t_1)

Read as: Gamma syntactically derives formula A with argument term t sub one

Means here: The expression read 'Gamma syntactically derives formula A with argument term t sub one' asserts existence of a finite first-order axiomatic derivation using the printed premises, axiom schemes, modus ponens, and quantifier rule.

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

Expression 120

Inline MathML variant

D→E!D \lif !E

Block MathML variant

D→E!D \lif !E

Read as: D implies E

Means here: The complete first-order formula or truth-functional formula scheme is read 'D implies E'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 22, column 38

Expression 122

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula not not A implies A is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula not not A implies A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 50, column 55

Expression 123

Inline MathML variant

Γ0⊆Γ\Gamma_0 \subseteq \Gamma

Block MathML variant

Γ0⊆Γ\Gamma_0 \subseteq \Gamma

Read as: Gamma sub zero is a subset of Gamma

Means here: The expression is read 'Gamma sub zero is a subset of Gamma'. This states inclusion between the two displayed premise sets.

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

Expression 124

Inline MathML variant

A→C!A \lif !C

Block MathML variant

A→C!A \lif !C

Read as: A implies C

Means here: The complete first-order formula or truth-functional formula scheme is read 'A implies C'. Spoken parentheses and connective names preserve its printed logical scope.

4 occurrences
  1. Occurrence 1: proving-things.tex, line 64, column 28
  2. Occurrence 2: proving-things.tex, line 85, column 29
  3. Occurrence 3: proving-things.tex, line 95, column 8
  4. Occurrence 4: proving-things.tex, line 112, column 22

Expression 125

Inline MathML variant

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

Block MathML variant

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

Read as: for every variable x, formula A with argument variable x syntactically derives formula A with argument term t

Means here: The expression read 'for every variable x, formula A with argument variable x syntactically derives formula A with argument term t' asserts existence of a finite first-order axiomatic derivation using the printed premises, axiom schemes, modus ponens, and quantifier rule.

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

Expression 126

Inline MathML variant

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

Block MathML variant

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

Read as: open parenthesis B implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis B implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 90, column 8

Expression 127

Inline MathML variant

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

Block MathML variant

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

Read as: structure M, under variable assignment lowercase s, satisfies formula B with argument variable x

Means here: The satisfaction claim read 'structure M, under variable assignment lowercase s, satisfies formula B with argument variable x' is evaluated in the named first-order structure and, when printed, the named variable assignment.

2 occurrences
  1. Occurrence 1: soundness.tex, line 90, column 36
  2. Occurrence 2: soundness.tex, line 103, column 40

Expression 128

Inline MathML variant

Γ⊢B\Gamma \Proves !B

Block MathML variant

Γ⊢B\Gamma \Proves !B

Read as: the complete formula B is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula B is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

9 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 87, column 19
  2. Occurrence 2: proof-theoretic-notions.tex, line 89, column 1
  3. Occurrence 3: deduction-theorem.tex, line 28, column 23
  4. Occurrence 4: deduction-theorem.tex, line 33, column 13
  5. Occurrence 5: deduction-theorem.tex, line 43, column 38
  6. Occurrence 6: deduction-theorem.tex, line 68, column 19
  7. Occurrence 7: deduction-theorem-quantifiers.tex, line 48, column 7
  8. Occurrence 8: provability-consistency.tex, line 26, column 55
  9. Occurrence 9: provability-consistency.tex, line 28, column 15

Expression 129

Inline MathML variant

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

Block MathML variant

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

Read as: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 130

Inline MathML variant

C→D(a)!C \lif !D(a)

Block MathML variant

C→D(a)!C \lif !D(a)

Read as: the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a

Means here: The first-order formula read 'the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a' preserves its metavariables, connectives, term arguments, and written grouping.

1 occurrence
  1. Occurrence 1: deduction-theorem-quantifiers.tex, line 30, column 26

Expression 131

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing not A

Means here: The statement is read 'the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing not A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-consistency.tex, line 39, column 41

Expression 132

Inline MathML variant

Γ⊨A\Gamma \Entails !A

Block MathML variant

Γ⊨A\Gamma \Entails !A

Read as: the complete formula A is semantically entailed by premise set Gamma

Means here: The statement is read 'the complete formula A is semantically entailed by premise set Gamma'. Every first-order structure and variable assignment satisfying every formula in the displayed premise set also satisfies the complete conclusion.

4 occurrences
  1. Occurrence 1: soundness.tex, line 56, column 29
  2. Occurrence 2: soundness.tex, line 65, column 1
  3. Occurrence 3: soundness.tex, line 65, column 58
  4. Occurrence 4: soundness.tex, line 74, column 11

Expression 133

Inline MathML variant

identity axiom onet=tidentity axiom twot1=t2→(B(t1)→B(t2))\ollabel{ax:id1} & \eq[t][t], \\ \ollabel{ax:id2} & \eq[t_1][t_2] \lif (!B(t_1) \lif !B(t_2)),

Block MathML variant

identity axiom onet=tidentity axiom twot1=t2→(B(t1)→B(t2))\ollabel{ax:id1} & \eq[t][t], \\ \ollabel{ax:id2} & \eq[t_1][t_2] \lif (!B(t_1) \lif !B(t_2)),

Read as: identity axiom one: term t is identical to term t identity axiom two: the conditional whose antecedent states that term t sub one is identical to term t sub two; and whose consequent is open parenthesis, the conditional whose antecedent is formula B with argument term t sub one; and whose consequent is formula B with argument term t sub two, close parenthesis

Means here: The expression read 'identity axiom one: term t is identical to term t identity axiom two: the conditional whose antecedent states that term t sub one is identical to term t sub two; and whose consequent is open parenthesis, the conditional whose antecedent is formula B with argument term t sub one; and whose consequent is formula B with argument term t sub two, close parenthesis' preserves every printed formula row and every intervening proof transition in source order.

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

Expression 134

Inline MathML variant

D→((D→D)→D)!D \lif ((!D \lif !D) \lif !D)

Block MathML variant

D→((D→D)→D)!D \lif ((!D \lif !D) \lif !D)

Read as: D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 73, column 8

Expression 135

Inline MathML variant

M,s⊨A[t/x]\Sat{M}{\Subst{!A}{t}{x}}[s]

Block MathML variant

M,s⊨A[t/x]\Sat{M}{\Subst{!A}{t}{x}}[s]

Read as: structure M, under variable assignment lowercase s, satisfies the result of substituting term t for variable x in formula A

Means here: The satisfaction claim read 'structure M, under variable assignment lowercase s, satisfies the result of substituting term t for variable x in formula A' is evaluated in the named first-order structure and, when printed, the named variable assignment.

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

Expression 136

Inline MathML variant

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

Block MathML variant

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

Read as: structure M satisfies the union of Gamma, and the set containing formula C

Means here: The satisfaction claim read 'structure M satisfies the union of Gamma, and the set containing formula C' is evaluated in the named first-order structure and, when printed, the named variable assignment.

1 occurrence
  1. Occurrence 1: soundness.tex, line 87, column 48

Expression 138

Inline MathML variant

Γ⊨C→∀x(B(x))\Gamma \Entails !C \lif \lforall[x][!B(x)]

Block MathML variant

Γ⊨C→∀x(B(x))\Gamma \Entails !C \lif \lforall[x][!B(x)]

Read as: Gamma semantically entails the conditional whose antecedent is formula C; and whose consequent is for every variable x, formula B with argument variable x

Means here: The expression read 'Gamma semantically entails the conditional whose antecedent is formula C; and whose consequent is for every variable x, formula B with argument variable x' states first-order semantic consequence over the named structures and assignments.

1 occurrence
  1. Occurrence 1: soundness.tex, line 106, column 62

Expression 139

Inline MathML variant

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

Block MathML variant

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

Read as: open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 93, column 12
  2. Occurrence 2: proving-things.tex, line 94, column 8

Expression 140

Inline MathML variant

Γ⊨C→B(c)\Gamma \Entails !C \lif !B(c)

Block MathML variant

Γ⊨C→B(c)\Gamma \Entails !C \lif !B(c)

Read as: Gamma semantically entails the conditional whose antecedent is formula C; and whose consequent is formula B with argument constant c

Means here: The expression read 'Gamma semantically entails the conditional whose antecedent is formula C; and whose consequent is formula B with argument constant c' states first-order semantic consequence over the named structures and assignments.

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

Expression 142

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

Read as: the complete formula A and B is axiomatically derivable from the displayed premises A comma B

Means here: The statement is read 'the complete formula A and B is axiomatically derivable from the displayed premises A comma B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 143

Inline MathML variant

∀x(B(x))\lforall[x][B(x)]

Block MathML variant

∀x(B(x))\lforall[x][B(x)]

Read as: for every variable x, B applied to variable x

Means here: The quantified first-order formula read 'for every variable x, B applied to variable x' preserves each bound variable, quantifier order, connective, and scope.

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

Expression 144

Inline MathML variant

M′⊨B(c)\Sat{M'}{B(c)}

Block MathML variant

M′⊨B(c)\Sat{M'}{B(c)}

Read as: structure M prime satisfies B applied to constant c

Means here: The satisfaction claim read 'structure M prime satisfies B applied to constant c' is evaluated in the named first-order structure and, when printed, the named variable assignment.

1 occurrence
  1. Occurrence 1: soundness.tex, line 97, column 18

Expression 145

Inline MathML variant

{¬A}⊢A→⊥\{\lnot !A\} \Proves !A \lif \lfalse

Block MathML variant

{¬A}⊢A→⊥\{\lnot !A\} \Proves !A \lif \lfalse

Read as: the complete formula A implies falsum is axiomatically derivable from the premise set containing not A

Means here: The statement is read 'the complete formula A implies falsum is axiomatically derivable from the premise set containing not A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: provability-propositional.tex, line 52, column 39

Expression 146

Inline MathML variant

Γ∪{A}⊢C→B\Gamma \cup \{!A\} \Proves !C \lif !B

Block MathML variant

Γ∪{A}⊢C→B\Gamma \cup \{!A\} \Proves !C \lif !B

Read as: the complete formula C implies B is axiomatically derivable from the union of Gamma and the singleton set containing A

Means here: The statement is read 'the complete formula C implies B is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 81, column 7

Expression 147

Inline MathML variant

C→B!C \lif !B

Block MathML variant

C→B!C \lif !B

Read as: C implies B

Means here: The complete first-order formula or truth-functional formula scheme is read 'C implies B'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 80, column 20

Expression 148

Inline MathML variant

Γ∪{B}⊢A\Gamma \cup \{!B\} \Proves !A

Block MathML variant

Γ∪{B}⊢A\Gamma \cup \{!B\} \Proves !A

Read as: the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing B

Means here: The statement is read 'the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 26, column 11

Expression 149

Inline MathML variant

B∈Γ∪{A}\in \Gamma \cup \{!A\}

Block MathML variant

B∈Γ∪{A}\in \Gamma \cup \{!A\}

Source-fidelity inline MathML

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

Source-fidelity block MathML

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

Read as: B belongs to Gamma union the set containing A

Means here: The expression is read 'B belongs to Gamma union the set containing A'. This states that the displayed formula belongs to the displayed premise set.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 67, column 8

Expression 150

Inline MathML variant

A∈Γ!A \in \Gamma

Block MathML variant

A∈Γ!A \in \Gamma

Read as: A belongs to Gamma

Means here: The expression is read 'A belongs to Gamma'. This states that the displayed formula belongs to the displayed premise set.

5 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 48, column 56
  2. Occurrence 2: rules-and-proofs.tex, line 52, column 6
  3. Occurrence 3: proof-theoretic-notions.tex, line 45, column 4
  4. Occurrence 4: deduction-theorem.tex, line 24, column 31
  5. Occurrence 5: soundness.tex, line 65, column 26

Expression 151

Inline MathML variant

M,s⊨∀x(A)\Sat{M}{\lforall[x][!A]}[s]

Block MathML variant

M,s⊨∀x(A)\Sat{M}{\lforall[x][!A]}[s]

Read as: structure M, under variable assignment lowercase s, satisfies for every variable x, formula A

Means here: The satisfaction claim read 'structure M, under variable assignment lowercase s, satisfies for every variable x, formula A' is evaluated in the named first-order structure and, when printed, the named variable assignment.

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

Expression 152

Inline MathML variant

(A→(B→C))→continued on the next display line(!A \lif (!B \lif !C)) \lif {}

Block MathML variant

(A→(B→C))→continued on the next display line(!A \lif (!B \lif !C)) \lif {}

Read as: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies continued on the next display line

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies continued on the next display line'. Spoken parentheses and connective names preserve its printed logical scope.

1 occurrence
  1. Occurrence 1: proving-things.tex, line 92, column 8

Expression 153

Inline MathML variant

t1t_1

Block MathML variant

t1t_1

Read as: term t sub one

Means here: The symbol read 'term t sub one' receives its exact term, variable, constant, or assignment role from each bound source occurrence.

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

Expression 154

Inline MathML variant

B→∀x(A(x))!B \lif \lforall[x][!A(x)]

Block MathML variant

B→∀x(A(x))!B \lif \lforall[x][!A(x)]

Read as: the conditional whose antecedent is formula B; and whose consequent is for every variable x, formula A with argument variable x

Means here: The quantified first-order formula read 'the conditional whose antecedent is formula B; and whose consequent is for every variable x, formula A with argument variable x' preserves each bound variable, quantifier order, connective, and scope.

1 occurrence
  1. Occurrence 1: axioms-rules-quantifiers.tex, line 25, column 44

Expression 155

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula B implies open parenthesis A implies B close parenthesis is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula B implies open parenthesis A implies B close parenthesis is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 68, column 58

Expression 156

Inline MathML variant

Γ∪{¬A}⊢⊥\Gamma \cup \{\lnot !A\} \Proves \lfalse

Block MathML variant

Γ∪{¬A}⊢⊥\Gamma \cup \{\lnot !A\} \Proves \lfalse

Read as: the complete formula falsum is axiomatically derivable from the union of Gamma and the singleton set containing not A

Means here: The statement is read 'the complete formula falsum is axiomatically derivable from the union of Gamma and the singleton set containing not A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

2 occurrences
  1. Occurrence 1: provability-consistency.tex, line 43, column 54
  2. Occurrence 2: provability-consistency.tex, line 46, column 62

Expression 157

Inline MathML variant

⊬A\Proves/ !A

Block MathML variant

⊬A\Proves/ !A

Read as: the complete formula A is not derivable with no premises

Means here: The statement is read 'the complete formula A is not derivable with no premises'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

2 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 92, column 13
  2. Occurrence 2: proof-theoretic-notions.tex, line 35, column 5

Expression 158

Inline MathML variant

⊢A\Proves !A

Block MathML variant

⊢A\Proves !A

Read as: the complete formula A is derivable with no premises

Means here: The statement is read 'the complete formula A is derivable with no premises'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

3 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 91, column 39
  2. Occurrence 2: proof-theoretic-notions.tex, line 34, column 36
  3. Occurrence 3: soundness.tex, line 121, column 4

Expression 159

Inline MathML variant

B→A(a)!B \lif !A(a)

Block MathML variant

B→A(a)!B \lif !A(a)

Read as: the conditional whose antecedent is formula B; and whose consequent is formula A with argument constant a

Means here: The first-order formula read 'the conditional whose antecedent is formula B; and whose consequent is formula A with argument constant a' preserves its metavariables, connectives, term arguments, and written grouping.

1 occurrence
  1. Occurrence 1: axioms-rules-quantifiers.tex, line 24, column 10

Expression 160

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing A

Means here: The statement is read 'the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 57, column 40

Expression 161

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula A implies B is axiomatically derivable from premise not A

Means here: The statement is read 'the complete formula A implies B is axiomatically derivable from premise not A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 162

Inline MathML variant

M⊭⊥\Sat/{M}{\lfalse}

Block MathML variant

M⊭⊥\Sat/{M}{\lfalse}

Read as: structure M does not satisfy falsum

Means here: The satisfaction claim read 'structure M does not satisfy falsum' is evaluated in the named first-order structure and, when printed, the named variable assignment.

1 occurrence
  1. Occurrence 1: soundness.tex, line 135, column 13

Expression 164

Inline MathML variant

Γ⊢A\Gamma \Proves !A

Block MathML variant

Γ⊢A\Gamma \Proves !A

Read as: the complete formula A is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

21 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 85, column 1
  2. Occurrence 2: proof-theoretic-notions.tex, line 28, column 1
  3. Occurrence 3: proof-theoretic-notions.tex, line 45, column 26
  4. Occurrence 4: proof-theoretic-notions.tex, line 54, column 34
  5. Occurrence 5: proof-theoretic-notions.tex, line 65, column 4
  6. Occurrence 6: proof-theoretic-notions.tex, line 86, column 44
  7. Occurrence 7: proof-theoretic-notions.tex, line 93, column 30
  8. Occurrence 8: proof-theoretic-notions.tex, line 115, column 12
  9. Occurrence 9: proof-theoretic-notions.tex, line 124, column 14
  10. Occurrence 10: deduction-theorem.tex, line 23, column 62
  11. Occurrence 11: deduction-theorem.tex, line 25, column 54
  12. Occurrence 12: deduction-theorem.tex, line 27, column 48
  13. Occurrence 13: deduction-theorem.tex, line 32, column 24
  14. Occurrence 14: deduction-theorem.tex, line 115, column 45
  15. Occurrence 15: provability-consistency.tex, line 20, column 6
  16. Occurrence 16: provability-consistency.tex, line 27, column 45
  17. Occurrence 17: provability-consistency.tex, line 35, column 1
  18. Occurrence 18: provability-consistency.tex, line 39, column 15
  19. Occurrence 19: provability-consistency.tex, line 51, column 55
  20. Occurrence 20: provability-consistency.tex, line 61, column 6
  21. Occurrence 21: soundness.tex, line 56, column 4

Expression 165

Inline MathML variant

Γ0⊢A\Gamma_0 \Proves !A

Block MathML variant

Γ0⊢A\Gamma_0 \Proves !A

Read as: the complete formula A is axiomatically derivable from premise set Gamma sub zero

Means here: The statement is read 'the complete formula A is axiomatically derivable from premise set Gamma sub zero'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

2 occurrences
  1. Occurrence 1: proof-theoretic-notions.tex, line 116, column 33
  2. Occurrence 2: proof-theoretic-notions.tex, line 130, column 10

Expression 167

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula A is axiomatically derivable from premise A and B

Means here: The statement is read 'the complete formula A is axiomatically derivable from premise A and B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

2 occurrences
  1. Occurrence 1: provability-propositional.tex, line 18, column 57
  2. Occurrence 2: provability-propositional.tex, line 25, column 51

Expression 168

Inline MathML variant

M′\Struct{M'}

Block MathML variant

M′\Struct{M'}

Read as: structure M prime

Means here: The expression read 'structure M prime' denotes the named first-order structure.

1 occurrence
  1. Occurrence 1: soundness.tex, line 93, column 54

Expression 170

Inline MathML variant

→\lif

Block MathML variant

→\lif

Read as: conditional connective

Means here: The term 'conditional connective' names the displayed truth-functional connective.

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

Expression 171

Inline MathML variant

B!B

Block MathML variant

B!B

Read as: B

Means here: B is the arbitrary complete first-order formula used in this exact source statement.

27 occurrences
  1. Occurrence 1: rules-and-proofs.tex, line 64, column 23
  2. Occurrence 2: rules-and-proofs.tex, line 74, column 13
  3. Occurrence 3: rules-and-proofs.tex, line 77, column 2
  4. Occurrence 4: axioms-rules-propositional.tex, line 37, column 6
  5. Occurrence 5: axioms-rules-quantifiers.tex, line 25, column 33
  6. Occurrence 6: axioms-rules-quantifiers.tex, line 28, column 33
  7. Occurrence 7: proving-things.tex, line 20, column 50
  8. Occurrence 8: proving-things.tex, line 22, column 6
  9. Occurrence 9: proving-things.tex, line 45, column 47
  10. Occurrence 10: proving-things.tex, line 66, column 16
  11. Occurrence 11: proving-things.tex, line 69, column 42
  12. Occurrence 12: proving-things.tex, line 70, column 48
  13. Occurrence 13: proof-theoretic-notions.tex, line 81, column 39
  14. Occurrence 14: deduction-theorem.tex, line 41, column 10
  15. Occurrence 15: deduction-theorem.tex, line 62, column 26
  16. Occurrence 16: deduction-theorem.tex, line 65, column 36
  17. Occurrence 17: deduction-theorem.tex, line 66, column 24
  18. Occurrence 18: deduction-theorem.tex, line 66, column 61
  19. Occurrence 19: deduction-theorem.tex, line 75, column 52
  20. Occurrence 20: deduction-theorem.tex, line 76, column 39
  21. Occurrence 21: deduction-theorem.tex, line 78, column 16
  22. Occurrence 22: deduction-theorem-quantifiers.tex, line 20, column 26
  23. Occurrence 23: deduction-theorem-quantifiers.tex, line 25, column 66
  24. Occurrence 24: deduction-theorem-quantifiers.tex, line 26, column 44
  25. Occurrence 25: deduction-theorem-quantifiers.tex, line 50, column 25
  26. Occurrence 26: provability-propositional.tex, line 76, column 12
  27. Occurrence 27: soundness.tex, line 69, column 37

Expression 172

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula not not A is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula not not A is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 115, column 10

Expression 173

Inline MathML variant

Γ⊢t=t\Gamma \Proves \eq[t][t]

Block MathML variant

Γ⊢t=t\Gamma \Proves \eq[t][t]

Read as: Gamma syntactically derives term t is identical to term t

Means here: The expression read 'Gamma syntactically derives term t is identical to term t' asserts existence of a finite first-order axiomatic derivation using the printed premises, axiom schemes, modus ponens, and quantifier rule.

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

Expression 174

Inline MathML variant

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

Block MathML variant

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

Read as: A implies open parenthesis B implies C close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'A implies open parenthesis B implies C close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 66, column 34
  2. Occurrence 2: proving-things.tex, line 91, column 8

Expression 175

Inline MathML variant

Δ⊢A\Delta \Proves !A

Block MathML variant

Δ⊢A\Delta \Proves !A

Read as: the complete formula A is axiomatically derivable from premise set Delta

Means here: The statement is read 'the complete formula A is axiomatically derivable from premise set Delta'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 176

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula A or B is axiomatically derivable from premise A

Means here: The statement is read 'the complete formula A or B is axiomatically derivable from premise A'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 177

Inline MathML variant

Γ⊢B→C\Gamma \Proves !B \lif !C

Block MathML variant

Γ⊢B→C\Gamma \Proves !B \lif !C

Read as: the complete formula B implies C is axiomatically derivable from premise set Gamma

Means here: The statement is read 'the complete formula B implies C is axiomatically derivable from premise set Gamma'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 102, column 59
  2. Occurrence 2: proving-things.tex, line 107, column 43

Expression 179

Inline MathML variant

(¬D∨E)→(D→E)(\lnot !D \lor !E) \lif (!D \lif !E)

Block MathML variant

(¬D∨E)→(D→E)(\lnot !D \lor !E) \lif (!D \lif !E)

Read as: open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 17, column 26
  2. Occurrence 2: proving-things.tex, line 37, column 8

Expression 180

Inline MathML variant

¬D→(D→E)\lnot !D \lif (!D \lif !E)

Block MathML variant

¬D→(D→E)\lnot !D \lif (!D \lif !E)

Read as: not D implies open parenthesis D implies E close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'not D implies open parenthesis D implies E close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

2 occurrences
  1. Occurrence 1: proving-things.tex, line 28, column 31
  2. Occurrence 2: proving-things.tex, line 32, column 9

Expression 182

Inline MathML variant

M,s⊨(∀x(A)→A[t/x])\Sat{M}{(\lforall[x][!A] \lif \Subst{!A}{t}{x})}[s]

Block MathML variant

M,s⊨(∀x(A)→A[t/x])\Sat{M}{(\lforall[x][!A] \lif \Subst{!A}{t}{x})}[s]

Read as: structure M, under variable assignment lowercase s, satisfies open parenthesis, the conditional whose antecedent is for every variable x, formula A; and whose consequent is the result of substituting term t for variable x in formula A, close parenthesis

Means here: The satisfaction claim read 'structure M, under variable assignment lowercase s, satisfies open parenthesis, the conditional whose antecedent is for every variable x, formula A; and whose consequent is the result of substituting term t for variable x in formula A, close parenthesis' is evaluated in the named first-order structure and, when printed, the named variable assignment.

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

Expression 184

Inline MathML variant

D∈Γ!D \in \Gamma

Block MathML variant

D∈Γ!D \in \Gamma

Read as: formula D is a member of Gamma

Means here: The relation read 'formula D is a member of Gamma' concerns the exact premise sets or formula sequences named by the source.

1 occurrence
  1. Occurrence 1: soundness.tex, line 92, column 58

Expression 188

Inline MathML variant

((E→(D→E))→((¬D∨E)→(D→E)))((!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E)))

Block MathML variant

((E→(D→E))→((¬D∨E)→(D→E)))((!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E)))

Read as: open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 190

Inline MathML variant

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

Block MathML variant

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

Read as: Gamma syntactically derives for every variable x, formula A with argument variable x

Means here: The expression read 'Gamma syntactically derives for every variable x, formula A with argument variable x' asserts existence of a finite first-order axiomatic derivation using the printed premises, axiom schemes, modus ponens, and quantifier rule.

2 occurrences
  1. Occurrence 1: provability-quantifiers.tex, line 23, column 57
  2. Occurrence 2: provability-quantifiers.tex, line 30, column 66

Expression 191

Inline MathML variant

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

Block MathML variant

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

Read as: structure M, under variable assignment lowercase s, satisfies formula D

Means here: The satisfaction claim read 'structure M, under variable assignment lowercase s, satisfies formula D' is evaluated in the named first-order structure and, when printed, the named variable assignment.

1 occurrence
  1. Occurrence 1: soundness.tex, line 92, column 33

Expression 192

Inline MathML variant

B≡A!B \ident !A

Block MathML variant

B≡A!B \ident !A

Read as: B is syntactically identical to A

Means here: The expression is read 'B is syntactically identical to A'. It states syntactic identity of the two complete formulas, not merely semantic equivalence.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 77, column 67

Expression 193

Inline MathML variant

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

Block MathML variant

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

Read as: Gamma union the set containing A

Means here: The expression is read 'Gamma union the set containing A'. This forms the union of the displayed premise sets.

9 occurrences
  1. Occurrence 1: deduction-theorem.tex, line 62, column 36
  2. Occurrence 2: deduction-theorem.tex, line 65, column 46
  3. Occurrence 3: deduction-theorem.tex, line 76, column 1
  4. Occurrence 4: deduction-theorem-quantifiers.tex, line 20, column 36
  5. Occurrence 5: deduction-theorem-quantifiers.tex, line 26, column 6
  6. Occurrence 6: provability-consistency.tex, line 20, column 30
  7. Occurrence 7: provability-consistency.tex, line 25, column 6
  8. Occurrence 8: provability-consistency.tex, line 56, column 42
  9. Occurrence 9: provability-consistency.tex, line 72, column 6

Expression 194

Inline MathML variant

M′,s⊨B(c)\Sat{M'}{!B(c)}[s]

Block MathML variant

M′,s⊨B(c)\Sat{M'}{!B(c)}[s]

Read as: structure M prime, under variable assignment lowercase s, satisfies formula B with argument constant c

Means here: The satisfaction claim read 'structure M prime, under variable assignment lowercase s, satisfies formula B with argument constant c' is evaluated in the named first-order structure and, when printed, the named variable assignment.

2 occurrences
  1. Occurrence 1: soundness.tex, line 98, column 1
  2. Occurrence 2: soundness.tex, line 100, column 1

Expression 196

Inline MathML variant

∀x(B(x))\lforall[x][!B(x)]

Block MathML variant

∀x(B(x))\lforall[x][!B(x)]

Read as: for every variable x, formula B with argument variable x

Means here: The quantified first-order formula read 'for every variable x, formula B with argument variable x' preserves each bound variable, quantifier order, connective, and scope.

1 occurrence
  1. Occurrence 1: soundness.tex, line 89, column 1

Expression 200

Inline MathML variant

quantifier axiom one∀x(B)→B(t)quantifier axiom twoB(t)→∃x(B)\ollabel{ax:q1} & \lforall[x][!B] \lif !B(t), \\ \ollabel{ax:q2} & !B(t) \lif \lexists[x][!B].

Block MathML variant

quantifier axiom one∀x(B)→B(t)quantifier axiom twoB(t)→∃x(B)\ollabel{ax:q1} & \lforall[x][!B] \lif !B(t), \\ \ollabel{ax:q2} & !B(t) \lif \lexists[x][!B].

Read as: quantifier axiom one: the conditional whose antecedent is for every variable x, formula B; and whose consequent is formula B with argument term t quantifier axiom two: the conditional whose antecedent is formula B with argument term t; and whose consequent is for some variable x, formula B

Means here: The expression read 'quantifier axiom one: the conditional whose antecedent is for every variable x, formula B; and whose consequent is formula B with argument term t quantifier axiom two: the conditional whose antecedent is formula B with argument term t; and whose consequent is for some variable x, formula B' preserves every printed formula row and every intervening proof transition in source order.

1 occurrence
  1. Occurrence 1: axioms-rules-quantifiers.tex, line 16, column 1

Expression 201

Inline MathML variant

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

Block MathML variant

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

Read as: the complete formula B is axiomatically derivable from premise A and B

Means here: The statement is read 'the complete formula B is axiomatically derivable from premise A and B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 202

Inline MathML variant

(A∧B)→(B∧A)(!A \land !B) \lif (!B \land !A)

Block MathML variant

(A∧B)→(B∧A)(!A \land !B) \lif (!B \land !A)

Read as: open parenthesis A and B close parenthesis implies open parenthesis B and A close parenthesis

Means here: The complete first-order formula or truth-functional formula scheme is read 'open parenthesis A and B close parenthesis implies open parenthesis B and A close parenthesis'. Spoken parentheses and connective names preserve its printed logical scope.

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

Expression 204

Inline MathML variant

B(x)!B(x)

Block MathML variant

B(x)!B(x)

Read as: formula B with argument variable x

Means here: The first-order formula read 'formula B with argument variable x' preserves its metavariables, connectives, term arguments, and written grouping.

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

Expression 205

Inline MathML variant

Γ⊨B→A\Gamma \Entails !B \lif !A

Block MathML variant

Γ⊨B→A\Gamma \Entails !B \lif !A

Read as: the complete formula B implies A is semantically entailed by premise set Gamma

Means here: The statement is read 'the complete formula B implies A is semantically entailed by premise set Gamma'. Every first-order structure and variable assignment satisfying every formula in the displayed premise set also satisfies the complete conclusion.

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

Expression 206

Inline MathML variant

{A∨B,¬A,¬B}⊢⊥\{!A \lor !B, \lnot !A, \lnot !B\} \Proves \lfalse

Block MathML variant

{A∨B,¬A,¬B}⊢⊥\{!A \lor !B, \lnot !A, \lnot !B\} \Proves \lfalse

Read as: the complete formula falsum is axiomatically derivable from the displayed premises the set containing A or B comma not A comma not B

Means here: The statement is read 'the complete formula falsum is axiomatically derivable from the displayed premises the set containing A or B comma not A comma not B'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

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

Expression 207

Inline MathML variant

Γ∪Δ\Gamma \cup \Delta

Block MathML variant

Γ∪Δ\Gamma \cup \Delta

Read as: Gamma union Delta

Means here: The expression is read 'Gamma union Delta'. This forms the union of the displayed premise sets.

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

Expression 209

Inline MathML variant

Γ⊢A→(C→B);Γ⊢A→C.& \Gamma \Proves !A \lif (!C \lif !B); \\ & \Gamma \Proves !A \lif !C.

Block MathML variant

Γ⊢A→(C→B);Γ⊢A→C.& \Gamma \Proves !A \lif (!C \lif !B); \\ & \Gamma \Proves !A \lif !C.

Read as: two statements: from Gamma derive the conditional from A to the conditional from C to B; and from Gamma derive the conditional from A to C

Means here: The statement is read 'two statements: from Gamma derive the conditional from A to the conditional from C to B; and from Gamma derive the conditional from A to C'. It asserts or denies the existence of a finite first-order axiomatic derivation with the displayed premises and conclusion, using the allowed axiom schemes and inference rules.

1 occurrence
  1. Occurrence 1: deduction-theorem.tex, line 84, column 1

61 formal objects

Definition of an axiomatic derivation from Gamma

The source defines a derivation from Gamma as a finite sequence of formulas. Each position is a premise from Gamma, an axiom, or follows from earlier positions by an inference rule.

  1. Expression one, in source order: Gamma.
  2. Expression two, in source order: language L.
  3. Expression three, in source order: Gamma.
  4. Expression four, in source order: A sub one.
  5. Expression five, in source order: A sub n.
  6. Expression six, in source order: i is less than or equal to n.
  7. Expression seven, in source order: A sub i belongs to Gamma.
  8. Expression eight, in source order: A sub i.
  9. Expression nine, in source order: A sub i.
  10. Expression ten, in source order: A sub j.
  11. Expression eleven, in source order: A sub k.
  12. Expression twelve, in source order: j is less than i.
  13. Expression thirteen, in source order: k is less than i.

Source: content/first-order-logic/axiomatic-deduction/rules-and-proofs.tex, line 24.

Definition of theoremhood in Rules and derivations

The source defines A as a theorem when A has a derivation from the empty set, and also records the notation for theoremhood and non-theoremhood.

  1. Expression one, in source order: A.
  2. Expression two, in source order: A.
  3. Expression three, in source order: the complete formula A is derivable with no premises.
  4. Expression four, in source order: A.
  5. Expression five, in source order: the complete formula A is not derivable with no premises.

Source: content/first-order-logic/axiomatic-deduction/rules-and-proofs.tex, line 89.

Definition of the propositional axiom set

The source defines the propositional axiom set as all substitution instances of the fourteen schemes in its nested display.

  1. Expression one, in source order: Ax sub zero.
  2. Expression two, in source order: displayed formula: fourteen axiom schemes in source order. Conjunction elimination left: open parenthesis A and B close parenthesis implies A. Conjunction elimination right: open parenthesis A and B close parenthesis implies B. Conjunction introduction: A implies open parenthesis B implies open parenthesis A and B close parenthesis close parenthesis. Disjunction introduction left: A implies open parenthesis A or B close parenthesis. Disjunction introduction right: A implies open parenthesis B or A close parenthesis. Disjunction elimination: open parenthesis A implies C close parenthesis implies open parenthesis open parenthesis B implies C close parenthesis implies open parenthesis open parenthesis A or B close parenthesis implies C close parenthesis close parenthesis. Conditional scheme one: A implies open parenthesis B implies A close parenthesis. Conditional scheme two: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis. Negation scheme one: open parenthesis A implies B close parenthesis implies open parenthesis open parenthesis A implies not B close parenthesis implies not A close parenthesis. Negation scheme two: not A implies open parenthesis A implies B close parenthesis. Truth scheme: verum. Falsity scheme one: falsum implies A. Falsity scheme two: open parenthesis A implies falsum close parenthesis implies not A. Double negation elimination: not not A implies A.

Source: content/first-order-logic/axiomatic-deduction/axioms-rules-propositional.tex, line 15.

The fourteen propositional axiom schemes

The display lists fourteen schemes in source order: three for conjunction, three for disjunction, two for the conditional, two for negation, one for truth, two for falsity, and double-negation elimination.

  1. Expression one, in source order: displayed formula: fourteen axiom schemes in source order. Conjunction elimination left: open parenthesis A and B close parenthesis implies A. Conjunction elimination right: open parenthesis A and B close parenthesis implies B. Conjunction introduction: A implies open parenthesis B implies open parenthesis A and B close parenthesis close parenthesis. Disjunction introduction left: A implies open parenthesis A or B close parenthesis. Disjunction introduction right: A implies open parenthesis B or A close parenthesis. Disjunction elimination: open parenthesis A implies C close parenthesis implies open parenthesis open parenthesis B implies C close parenthesis implies open parenthesis open parenthesis A or B close parenthesis implies C close parenthesis close parenthesis. Conditional scheme one: A implies open parenthesis B implies A close parenthesis. Conditional scheme two: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis. Negation scheme one: open parenthesis A implies B close parenthesis implies open parenthesis open parenthesis A implies not B close parenthesis implies not A close parenthesis. Negation scheme two: not A implies open parenthesis A implies B close parenthesis. Truth scheme: verum. Falsity scheme one: falsum implies A. Falsity scheme two: open parenthesis A implies falsum close parenthesis implies not A. Double negation elimination: not not A implies A.

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

Definition of the two quantifier axiom schemes

The definition introduces universal instantiation, from universal B to B of a closed term, and existential introduction, from B of a closed term to existential B. The source restricts the substituting term to be closed.

  1. Expression one, in source order: displayed formula: quantifier axiom one: the conditional whose antecedent is for every variable x, formula B; and whose consequent is formula B with argument term t quantifier axiom two: the conditional whose antecedent is formula B with argument term t; and whose consequent is for some variable x, formula B.
  2. Expression two, in source order: term t.

Source: content/first-order-logic/axiomatic-deduction/axioms-rules-quantifiers.tex, line 13.

The universal and existential quantifier axiom display

The nested display gives the two quantifier schemes in source order: universal instantiation first and existential introduction second.

  1. Expression one, in source order: displayed formula: quantifier axiom one: the conditional whose antecedent is for every variable x, formula B; and whose consequent is formula B with argument term t quantifier axiom two: the conditional whose antecedent is formula B with argument term t; and whose consequent is for some variable x, formula B.

Source: content/first-order-logic/axiomatic-deduction/axioms-rules-quantifiers.tex, line 16.

Definition of the two quantifier inference rules

The definition gives the universal and existential quantifier rules. Each carries an eigenvariable condition excluding the chosen parameter from Gamma and the unaffected side formula.

  1. Expression one, in source order: the conditional whose antecedent is formula B; and whose consequent is formula A with argument constant a.
  2. Expression two, in source order: constant a.
  3. Expression three, in source order: Gamma.
  4. Expression four, in source order: B.
  5. Expression five, in source order: the conditional whose antecedent is formula B; and whose consequent is for every variable x, formula A with argument variable x.
  6. Expression six, in source order: the conditional whose antecedent is formula A with argument constant a; and whose consequent is formula B.
  7. Expression seven, in source order: constant a.
  8. Expression eight, in source order: Gamma.
  9. Expression nine, in source order: B.
  10. Expression ten, in source order: the conditional whose antecedent is for some variable x, formula A with argument variable x; and whose consequent is formula B.

Source: content/first-order-logic/axiomatic-deduction/axioms-rules-quantifiers.tex, line 23.

Example deriving the conditional from not D or E to the conditional from D to E

The example explains the axiom instances and two uses of modus ponens that produce its target conditional, then prints the complete five-line derivation.

  1. Expression one, in source order: open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis.
  2. Expression two, in source order: A.
  3. Expression three, in source order: A implies B.
  4. Expression four, in source order: B.
  5. Resolved reference one, in source order: Reference to the third disjunction axiom scheme.
  6. Expression five, in source order: A.
  7. Expression six, in source order: not D.
  8. Expression seven, in source order: B.
  9. Expression eight, in source order: E.
  10. Expression nine, in source order: C.
  11. Expression ten, in source order: D implies E.
  12. Expression eleven, in source order: displayed formula: open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis.
  13. Expression twelve, in source order: not D implies open parenthesis D implies E close parenthesis.
  14. Resolved reference two, in source order: Reference to the second negation axiom scheme.
  15. Expression thirteen, in source order: E implies open parenthesis D implies E close parenthesis.
  16. Resolved reference three, in source order: Reference to the first conditional axiom scheme.
  17. Expression fourteen, in source order: not D implies open parenthesis D implies E close parenthesis.
  18. Resolved reference four, in source order: Reference to the second negation axiom scheme.
  19. Expression fifteen, in source order: open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies continued on the next display line.
  20. Expression sixteen, in source order: open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis.
  21. Resolved reference five, in source order: Reference to the third disjunction axiom scheme.
  22. Expression seventeen, in source order: open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis.
  23. Expression eighteen, in source order: E implies open parenthesis D implies E close parenthesis.
  24. Resolved reference six, in source order: Reference to the first conditional axiom scheme.
  25. Expression nineteen, in source order: open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis.

Source: content/first-order-logic/axiomatic-deduction/proving-things.tex, line 16.

Five-line derivation from not D or E to D implies E

The derivation uses three named propositional axiom schemes and two applications of modus ponens. A long formula on line two is split across two printed rows and is preserved as two ordered source segments.

  1. Expression one, in source order: not D implies open parenthesis D implies E close parenthesis.
  2. Resolved reference one, in source order: Reference to the second negation axiom scheme.
  3. Expression two, in source order: open parenthesis not D implies open parenthesis D implies E close parenthesis close parenthesis implies continued on the next display line.
  4. Expression three, in source order: open parenthesis open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis close parenthesis.
  5. Resolved reference two, in source order: Reference to the third disjunction axiom scheme.
  6. Expression four, in source order: open parenthesis E implies open parenthesis D implies E close parenthesis close parenthesis implies open parenthesis open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis close parenthesis.
  7. Expression five, in source order: E implies open parenthesis D implies E close parenthesis.
  8. Resolved reference three, in source order: Reference to the first conditional axiom scheme.
  9. Expression six, in source order: open parenthesis not D or E close parenthesis implies open parenthesis D implies E close parenthesis.

Source: content/first-order-logic/axiomatic-deduction/proving-things.tex, line 31.

Example deriving the identity conditional

The example searches for a derivation of the identity conditional, rejects an insufficient first strategy, then combines the two conditional axiom schemes in a five-line derivation.

  1. Expression one, in source order: D implies D.
  2. Resolved reference one, in source order: Reference to the first conditional axiom scheme.
  3. Expression two, in source order: A implies B.
  4. Expression three, in source order: B.
  5. Expression four, in source order: D implies D.
  6. Expression five, in source order: A.
  7. Expression six, in source order: D.
  8. Resolved reference two, in source order: Reference to the first conditional axiom scheme.
  9. Expression seven, in source order: displayed formula: D implies open parenthesis D implies D close parenthesis.
  10. Expression eight, in source order: A.
  11. Expression nine, in source order: D.
  12. Expression ten, in source order: D.
  13. Expression eleven, in source order: conditional connective.
  14. Resolved reference three, in source order: Reference to the second conditional axiom scheme.
  15. Expression twelve, in source order: displayed formula: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis.
  16. Resolved reference four, in source order: Reference to the second conditional axiom scheme.
  17. Expression thirteen, in source order: A implies C.
  18. Expression fourteen, in source order: D implies D.
  19. Expression fifteen, in source order: A.
  20. Expression sixteen, in source order: C.
  21. Expression seventeen, in source order: D.
  22. Expression eighteen, in source order: B.
  23. Expression nineteen, in source order: A implies open parenthesis B implies C close parenthesis.
  24. Expression twenty, in source order: A implies B.
  25. Expression twenty one, in source order: D implies open parenthesis B implies D close parenthesis.
  26. Expression twenty two, in source order: D implies B.
  27. Resolved reference five, in source order: Reference to the first conditional axiom scheme.
  28. Expression twenty three, in source order: B.
  29. Expression twenty four, in source order: D implies B.
  30. Resolved reference six, in source order: Reference to the first conditional axiom scheme.
  31. Expression twenty five, in source order: B.
  32. Expression twenty six, in source order: open parenthesis D implies D close parenthesis.
  33. Expression twenty seven, in source order: D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis.
  34. Resolved reference seven, in source order: Reference to the first conditional axiom scheme.
  35. Expression twenty eight, in source order: open parenthesis D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis close parenthesis implies continued on the next display line.
  36. Expression twenty nine, in source order: open parenthesis open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis close parenthesis.
  37. Resolved reference eight, in source order: Reference to the second conditional axiom scheme.
  38. Expression thirty, in source order: open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis.
  39. Expression thirty one, in source order: D implies open parenthesis D implies D close parenthesis.
  40. Resolved reference nine, in source order: Reference to the first conditional axiom scheme.
  41. Expression thirty two, in source order: D implies D.

Source: content/first-order-logic/axiomatic-deduction/proving-things.tex, line 41.

Five-line derivation of D implies D

The derivation uses three conditional-axiom instances and two applications of modus ponens. Its second line is preserved as two ordered printed formula segments.

  1. Expression one, in source order: D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis.
  2. Resolved reference one, in source order: Reference to the first conditional axiom scheme.
  3. Expression two, in source order: open parenthesis D implies open parenthesis open parenthesis D implies D close parenthesis implies D close parenthesis close parenthesis implies continued on the next display line.
  4. Expression three, in source order: open parenthesis open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis close parenthesis.
  5. Resolved reference two, in source order: Reference to the second conditional axiom scheme.
  6. Expression four, in source order: open parenthesis D implies open parenthesis D implies D close parenthesis close parenthesis implies open parenthesis D implies D close parenthesis.
  7. Expression five, in source order: D implies open parenthesis D implies D close parenthesis.
  8. Resolved reference three, in source order: Reference to the first conditional axiom scheme.
  9. Expression six, in source order: D implies D.

Source: content/first-order-logic/axiomatic-deduction/proving-things.tex, line 72.

Example chaining two conditionals

The example derives the conditional from A to C from the two hypotheses A implies B and B implies C, and explains that lines marked as hypotheses belong to Gamma.

  1. Expression one, in source order: Gamma.
  2. Expression two, in source order: A implies C.
  3. Expression three, in source order: Gamma equals the set containing A implies B comma B implies C.
  4. Expression four, in source order: A implies B.
  5. Expression five, in source order: B implies C.
  6. Expression six, in source order: open parenthesis B implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis.
  7. Resolved reference one, in source order: Reference to the first conditional axiom scheme.
  8. Expression seven, in source order: A implies open parenthesis B implies C close parenthesis.
  9. Expression eight, in source order: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies continued on the next display line.
  10. Expression nine, in source order: open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis.
  11. Resolved reference two, in source order: Reference to the second conditional axiom scheme.
  12. Expression ten, in source order: open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis.
  13. Expression eleven, in source order: A implies C.
  14. Expression twelve, in source order: Gamma.

Source: content/first-order-logic/axiomatic-deduction/proving-things.tex, line 82.

Seven-line derivation chaining A implies B and B implies C

The seven-line derivation begins with two hypotheses, adds instances of the two conditional axiom schemes, and applies modus ponens three times. Its fifth line spans two printed formula segments.

  1. Expression one, in source order: A implies B.
  2. Expression two, in source order: B implies C.
  3. Expression three, in source order: open parenthesis B implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis.
  4. Resolved reference one, in source order: Reference to the first conditional axiom scheme.
  5. Expression four, in source order: A implies open parenthesis B implies C close parenthesis.
  6. Expression five, in source order: open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis implies continued on the next display line.
  7. Expression six, in source order: open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis.
  8. Resolved reference two, in source order: Reference to the second conditional axiom scheme.
  9. Expression seven, in source order: open parenthesis open parenthesis A implies B close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis.
  10. Expression eight, in source order: A implies C.

Source: content/first-order-logic/axiomatic-deduction/proving-things.tex, line 87.

Proposition: chaining derivable conditionals

The proposition states that if Gamma derives the conditional from A to B and the conditional from B to C, then Gamma derives the conditional from A to C.

  1. Expression one, in source order: the complete formula A implies B is axiomatically derivable from premise set Gamma.
  2. Expression two, in source order: the complete formula B implies C is axiomatically derivable from premise set Gamma.
  3. Expression three, in source order: the complete formula A implies C is axiomatically derivable from premise set Gamma.

Source: content/first-order-logic/axiomatic-deduction/proving-things.tex, line 101.

Exercise: three derivations from the propositional axioms

This unsolved exercise asks for three explicit derivations from the axioms: commutation of a conjunction, a curried consequence of a conjunction, and a negated consequence of a disjunction. No solution is supplied.

Unsolved source exercise; no solution added.

  1. Expression one, in source order: open parenthesis A and B close parenthesis implies open parenthesis B and A close parenthesis.
  2. Expression two, in source order: open parenthesis open parenthesis A and B close parenthesis implies C close parenthesis implies open parenthesis A implies open parenthesis B implies C close parenthesis close parenthesis.
  3. Expression three, in source order: not open parenthesis A or B close parenthesis implies not A.

Source: content/first-order-logic/axiomatic-deduction/proving-things.tex, line 120.

Example deriving a conjunction of universal formulas pointwise

The example derives that the conjunction of two universal premises implies the universal closure of their pointwise conjunction. It chains conjunction elimination, universal instantiation, conjunction introduction, modus ponens, and the quantifier rule.

  1. Expression one, in source order: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis.
  2. Expression two, in source order: displayed formula: formula row one: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, formula A with argument variable x The source then says that this formula is an instance of the first conjunction axiom, and formula row two: the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is formula A with argument constant a The source then identifies this formula as an instance of the universal-instantiation axiom. So, by the chain proposition, we know that formula row three: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is formula A with argument constant a The source then says that this formula is derivable. Likewise, since formula row four: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable y, formula B with argument variable y formula row five: the conditional whose antecedent is for every variable y, formula B with argument variable y; and whose consequent is formula B with argument constant a The source then says that these formulas are instances of the second conjunction axiom and the universal-instantiation axiom, respectively formula row six: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is formula B with argument constant a The source then says that this formula is derivable by the chain proposition. Using an appropriate instance of the conjunction-introduction axiom and two applications of modus ponens, we see that formula row seven: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is open parenthesis, the conjunction of formula A with argument constant a and formula B with argument constant a, close parenthesis The source then says that this formula is derivable. We can now apply the quantifier rule to obtain formula row eight: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis.
  3. Resolved reference one, in source order: Reference to the first conjunction axiom scheme.
  4. Resolved reference two, in source order: Reference to the universal-instantiation axiom scheme.
  5. Resolved reference three, in source order: Reference to the proposition chaining derivable conditionals.
  6. Resolved reference four, in source order: Reference to the second conjunction axiom scheme.
  7. Resolved reference five, in source order: Reference to the universal-instantiation axiom scheme.
  8. Resolved reference six, in source order: Reference to the proposition chaining derivable conditionals.
  9. Resolved reference seven, in source order: Reference to the third conjunction axiom scheme.

Source: content/first-order-logic/axiomatic-deduction/proving-things-quant.tex, line 13.

Source-ordered quantified derivation display

The display records the complete source-order argument from the conjunction of two universal formulas to the universal closure of their pointwise conjunction, including every intermediate conditional.

  1. Expression one, in source order: displayed formula: formula row one: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, formula A with argument variable x The source then says that this formula is an instance of the first conjunction axiom, and formula row two: the conditional whose antecedent is for every variable x, formula A with argument variable x; and whose consequent is formula A with argument constant a The source then identifies this formula as an instance of the universal-instantiation axiom. So, by the chain proposition, we know that formula row three: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is formula A with argument constant a The source then says that this formula is derivable. Likewise, since formula row four: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable y, formula B with argument variable y formula row five: the conditional whose antecedent is for every variable y, formula B with argument variable y; and whose consequent is formula B with argument constant a The source then says that these formulas are instances of the second conjunction axiom and the universal-instantiation axiom, respectively formula row six: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is formula B with argument constant a The source then says that this formula is derivable by the chain proposition. Using an appropriate instance of the conjunction-introduction axiom and two applications of modus ponens, we see that formula row seven: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is open parenthesis, the conjunction of formula A with argument constant a and formula B with argument constant a, close parenthesis The source then says that this formula is derivable. We can now apply the quantifier rule to obtain formula row eight: the conditional whose antecedent is open parenthesis, the conjunction of for every variable x, formula A with argument variable x and for every variable y, formula B with argument variable y, close parenthesis; and whose consequent is for every variable x, open parenthesis, the conjunction of formula A with argument variable x and formula B with argument variable x, close parenthesis.
  2. Resolved reference one, in source order: Reference to the first conjunction axiom scheme.
  3. Resolved reference two, in source order: Reference to the universal-instantiation axiom scheme.
  4. Resolved reference three, in source order: Reference to the proposition chaining derivable conditionals.
  5. Resolved reference four, in source order: Reference to the second conjunction axiom scheme.
  6. Resolved reference five, in source order: Reference to the universal-instantiation axiom scheme.
  7. Resolved reference six, in source order: Reference to the proposition chaining derivable conditionals.
  8. Resolved reference seven, in source order: Reference to the third conjunction axiom scheme.

Source: content/first-order-logic/axiomatic-deduction/proving-things-quant.tex, line 18.

Definition of derivability in Proof-Theoretic Notions

The source restates that A is derivable from Gamma exactly when a derivation from Gamma ends with A.

  1. Expression one, in source order: A.
  2. Expression two, in source order: Gamma.
  3. Expression three, in source order: the complete formula A is axiomatically derivable from premise set Gamma.
  4. Expression four, in source order: Gamma.
  5. Expression five, in source order: A.

Source: content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex, line 26.

Definition of theoremhood in Proof-Theoretic Notions

The source restates that A is a theorem exactly when A has a derivation from the empty set, including the positive and negative theoremhood notation.

  1. Expression one, in source order: A.
  2. Expression two, in source order: A.
  3. Expression three, in source order: the complete formula A is derivable with no premises.
  4. Expression four, in source order: A.
  5. Expression five, in source order: the complete formula A is not derivable with no premises.

Source: content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex, line 32.

Proposition: monotonicity of derivability

The proposition states that derivability is preserved when the premise set is enlarged from Gamma to Delta.

  1. Expression one, in source order: Gamma is a subset of Delta.
  2. Expression two, in source order: the complete formula A is axiomatically derivable from premise set Gamma.
  3. Expression three, in source order: the complete formula A is axiomatically derivable from premise set Delta.

Source: content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex, line 52.

Proposition: transitivity of derivability

The proposition combines a derivation of A from Gamma with a derivation of B from A together with Delta, yielding a derivation of B from Gamma together with Delta.

  1. Expression one, in source order: the complete formula A is axiomatically derivable from premise set Gamma.
  2. Expression two, in source order: the complete formula B is axiomatically derivable from the union of the singleton set containing A and Delta.
  3. Expression three, in source order: the complete formula B is axiomatically derivable from the union of premise sets Gamma and Delta.

Source: content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex, line 63.

Exercise: prove the first-order inconsistency characterization

This first-order exercise asks the reader to prove that Gamma is inconsistent exactly when Gamma derives every formula. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

  1. Resolved reference one, in source order: Reference to the proposition characterizing inconsistency by derivability.

Source: content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex, line 101.

Proposition: compactness of axiomatic derivability

The proposition gives two compactness claims: every derivation uses a finite subset of its premises, and a set whose every finite subset is consistent is itself consistent.

  1. Expression one, in source order: the complete formula A is axiomatically derivable from premise set Gamma.
  2. Expression two, in source order: Gamma sub zero is a subset of Gamma.
  3. Expression three, in source order: the complete formula A is axiomatically derivable from premise set Gamma sub zero.
  4. Expression four, in source order: Gamma.
  5. Expression five, in source order: Gamma.

Source: content/first-order-logic/axiomatic-deduction/proof-theoretic-notions.tex, line 112.

Proposition: meta-level modus ponens

The proposition states a meta-level form of modus ponens: if Gamma derives A and also derives the conditional from A to B, then Gamma derives B.

  1. Expression one, in source order: the complete formula A is axiomatically derivable from premise set Gamma.
  2. Expression two, in source order: the complete formula A implies B is axiomatically derivable from premise set Gamma.
  3. Expression three, in source order: the complete formula B is axiomatically derivable from premise set Gamma.

Source: content/first-order-logic/axiomatic-deduction/deduction-theorem.tex, line 31.

Proposition: five useful derivability facts

The proposition groups five source claims about implication chaining, contraposition, explosion, double-negation elimination, and eliminating a derived double negation.

  1. Expression one, in source order: the complete formula open parenthesis A implies B close parenthesis implies open parenthesis open parenthesis B implies C close parenthesis implies open parenthesis A implies C close parenthesis close parenthesis is derivable with no premises.
  2. Expression two, in source order: the complete formula not B is axiomatically derivable from the union of Gamma and the singleton set containing not A.
  3. Expression three, in source order: the complete formula A is axiomatically derivable from the union of Gamma and the singleton set containing B.
  4. Expression four, in source order: the complete formula B is axiomatically derivable from the displayed premises the set containing A comma not A.
  5. Expression five, in source order: the complete formula A is axiomatically derivable from the premise set containing not not A.
  6. Expression six, in source order: the complete formula not not A is axiomatically derivable from premise set Gamma.
  7. Expression seven, in source order: the complete formula A is axiomatically derivable from premise set Gamma.
  8. Source correction: The frozen source is missing the final closing parenthesis in this displayed conditional. The reader adds that delimiter while retaining source MathML for comparison.

Source: content/first-order-logic/axiomatic-deduction/deduction-theorem.tex, line 103.

Exercise: prove the five first-order derivability facts

This first-order exercise asks for proofs of all five preceding derivability facts, including implication chaining, contraposition, explosion, and double-negation principles. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

  1. Resolved reference one, in source order: Reference to the proposition listing five derivability facts.

Source: content/first-order-logic/axiomatic-deduction/deduction-theorem.tex, line 121.

The Deduction Theorem with quantifiers

The theorem states the forward quantified deduction result: if B is derivable from Gamma together with A, then the conditional from A to B is derivable from Gamma.

  1. Expression one, in source order: the complete formula B is axiomatically derivable from the union of Gamma and the singleton set containing A.
  2. Expression two, in source order: the complete formula A implies B is axiomatically derivable from premise set Gamma.

Source: content/first-order-logic/axiomatic-deduction/deduction-theorem-quantifiers.tex, line 13.

Quantifier-rule induction case for the Deduction Theorem

The display follows the universal-quantifier rule case of the induction. It moves from the shorter derivation through conjunction with the discharged assumption, applies the quantifier rule, and recovers the required nested conditional.

  1. Expression one, in source order: displayed formula: formula row one: the union of Gamma, and the set containing formula A syntactically derives the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a The source then says that the induction hypothesis applies, that is, we have that formula row two: Gamma syntactically derives the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a, close parenthesis The source then invokes formula row three: no premises syntactically derives the conditional whose antecedent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is formula D with argument constant a, close parenthesis, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is formula D with argument constant a, close parenthesis By this result and modus ponens, the source obtains formula row four: Gamma syntactically derives the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is formula D with argument constant a The source next notes that the eigenvariable condition still applies, we can add a step to this derivation justified by the quantifier rule, and get formula row five: Gamma syntactically derives the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is for every variable x, formula D with argument variable x The source next gives formula row six: no premises syntactically derives the conditional whose antecedent is open parenthesis, the conditional whose antecedent is open parenthesis, the conjunction of formula A and formula C, close parenthesis; and whose consequent is for every variable x, formula D with argument variable x, close parenthesis; and whose consequent is open parenthesis, the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is for every variable x, formula D with argument variable x, close parenthesis, close parenthesis The source then applies modus ponens to obtain formula row seven: Gamma syntactically derives the conditional whose antecedent is formula A; and whose consequent is open parenthesis, the conditional whose antecedent is formula C; and whose consequent is for every variable x, formula D with argument variable x, close parenthesis.
  2. Source correction: The frozen quantified deduction-theorem display is missing one final closing parenthesis in its sixth formula row. The reader adds that delimiter while retaining exact source MathML for comparison.

Source: content/first-order-logic/axiomatic-deduction/deduction-theorem-quantifiers.tex, line 33.

Exercise: characterize derivability of a negation by inconsistency

This unsolved exercise asks for the dual result: characterize derivability of not A by inconsistency after adding A to Gamma. No solution is supplied.

Unsolved source exercise; no solution added.

  1. Expression one, in source order: the complete formula not A is axiomatically derivable from premise set Gamma.
  2. Expression two, in source order: Gamma union the set containing A.

Source: content/first-order-logic/axiomatic-deduction/provability-consistency.tex, line 55.

Exercise: prove inconsistency from two opposite extensions

This first-order exercise asks for a proof that Gamma is inconsistent when both its extension by A and its extension by not A are inconsistent. It is explicitly preserved as unsolved; the source supplies no solution.

Unsolved source exercise; no solution added.

  1. Resolved reference one, in source order: Reference to the proposition about two inconsistent opposite extensions.

Source: content/first-order-logic/axiomatic-deduction/provability-consistency.tex, line 81.

Proposition: derivability principles for conjunction

The proposition states both projections from a conjunction and the derivability of a conjunction from its two conjuncts.

  1. Expression one, in source order: the complete formula A is axiomatically derivable from premise A and B.
  2. Expression two, in source order: the complete formula B is axiomatically derivable from premise A and B.
  3. Expression three, in source order: the complete formula A and B is axiomatically derivable from the displayed premises A comma B.

Source: content/first-order-logic/axiomatic-deduction/provability-propositional.tex, line 23.

Proposition: derivability principles for disjunction

The proposition states that a disjunction together with both negated disjuncts is inconsistent, and that either disjunct derives the disjunction.

  1. Expression one, in source order: the three formulas A or B, not A, and not B.
  2. Expression two, in source order: the complete formula A or B is axiomatically derivable from premise A.
  3. Expression three, in source order: the complete formula A or B is axiomatically derivable from premise B.

Source: content/first-order-logic/axiomatic-deduction/provability-propositional.tex, line 41.

Proposition: derivability principles for the conditional

The proposition states conditional elimination from A and A implies B, together with two ways to derive A implies B: from not A and from B.

  1. Expression one, in source order: the complete formula B is axiomatically derivable from the displayed premises A comma A implies B.
  2. Expression two, in source order: the complete formula A implies B is axiomatically derivable from premise not A.
  3. Expression three, in source order: the complete formula A implies B is axiomatically derivable from premise B.

Source: content/first-order-logic/axiomatic-deduction/provability-propositional.tex, line 62.

Strong Generalization Theorem

The theorem states that if a fresh constant c occurs neither in Gamma nor in A of x, and Gamma derives A of c, then Gamma derives the universal closure of A of x.

  1. Expression one, in source order: constant c.
  2. Expression two, in source order: Gamma.
  3. Expression three, in source order: formula A with argument variable x.
  4. Expression four, in source order: Gamma syntactically derives formula A with argument constant c.
  5. Expression five, in source order: Gamma syntactically derives for every variable x, formula A with argument variable x.

Source: content/first-order-logic/axiomatic-deduction/provability-quantifiers.tex, line 21.

Proposition: derivability principles for the quantifiers

The proposition records existential introduction from an instance and universal instantiation from a universal premise as two source-ordered derivability claims.

  1. Expression one, in source order: formula A with argument term t syntactically derives for some variable x, formula A with argument variable x.
  2. Expression two, in source order: for every variable x, formula A with argument variable x syntactically derives formula A with argument term t.

Source: content/first-order-logic/axiomatic-deduction/provability-quantifiers.tex, line 34.

Proposition: every first-order axiom is valid

The proposition states that every axiom is satisfied by every first-order structure under every variable assignment. The proof illustrates the universal-instantiation axiom.

  1. Expression one, in source order: A.
  2. Expression two, in source order: structure M, under variable assignment lowercase s, satisfies formula A.
  3. Expression three, in source order: structure M.
  4. Expression four, in source order: lowercase s.

Source: content/first-order-logic/axiomatic-deduction/soundness.tex, line 34.

Definition of the identity axiom schemes

The definition adds reflexivity of identity and substitution of identical closed terms as axiom schemes while leaving the definition of derivation unchanged.

  1. Expression one, in source order: displayed formula: identity axiom one: term t is identical to term t identity axiom two: the conditional whose antecedent states that term t sub one is identical to term t sub two; and whose consequent is open parenthesis, the conditional whose antecedent is formula B with argument term t sub one; and whose consequent is formula B with argument term t sub two, close parenthesis.
  2. Expression two, in source order: term t.
  3. Expression three, in source order: term t sub one.
  4. Expression four, in source order: term t sub two.

Source: content/first-order-logic/axiomatic-deduction/identity.tex, line 17.

The two identity axiom schemes

The display lists identity reflexivity first and the substitution-of-identicals conditional second, for closed terms.

  1. Expression one, in source order: displayed formula: identity axiom one: term t is identical to term t identity axiom two: the conditional whose antecedent states that term t sub one is identical to term t sub two; and whose consequent is open parenthesis, the conditional whose antecedent is formula B with argument term t sub one; and whose consequent is formula B with argument term t sub two, close parenthesis.

Source: content/first-order-logic/axiomatic-deduction/identity.tex, line 18.

Proposition: derivable substitution of identicals

The proposition states that if Gamma derives A of the first term and also derives that the first term equals the second, then Gamma derives A of the second term.

  1. Expression one, in source order: Gamma syntactically derives formula A with argument term t sub one.
  2. Expression two, in source order: Gamma syntactically derives term t sub one is identical to term t sub two.
  3. Expression three, in source order: Gamma syntactically derives formula A with argument term t sub two.

Source: content/first-order-logic/axiomatic-deduction/identity.tex, line 42.

84 resolved references

  1. Reference to the third disjunction axiom scheme — source line 21.
  2. Reference to the second negation axiom scheme — source line 29.
  3. Reference to the first conditional axiom scheme — source line 30.
  4. Reference to the second negation axiom scheme — source line 32.
  5. Reference to the third disjunction axiom scheme — source line 34.
  6. Reference to the first conditional axiom scheme — source line 36.
  7. Reference to the first conditional axiom scheme — source line 44.
  8. Reference to the first conditional axiom scheme — source line 49.
  9. Reference to the second conditional axiom scheme — source line 58.
  10. Reference to the second conditional axiom scheme — source line 64.
  11. Reference to the first conditional axiom scheme — source line 69.
  12. Reference to the first conditional axiom scheme — source line 70.
  13. Reference to the first conditional axiom scheme — source line 73.
  14. Reference to the second conditional axiom scheme — source line 75.
  15. Reference to the first conditional axiom scheme — source line 77.
  16. Reference to the first conditional axiom scheme — source line 90.
  17. Reference to the second conditional axiom scheme — source line 93.
  18. Reference to the first conjunction axiom scheme — source line 20.
  19. Reference to the universal-instantiation axiom scheme — source line 22.
  20. Reference to the proposition chaining derivable conditionals — source line 22.
  21. Reference to the second conjunction axiom scheme — source line 27.
  22. Reference to the universal-instantiation axiom scheme — source line 27.
  23. Reference to the proposition chaining derivable conditionals — source line 29.
  24. Reference to the third conjunction axiom scheme — source line 29.
  25. Reference to the proposition characterizing inconsistency by derivability — source line 102.
  26. Reference to the reflexivity proposition for derivability — source line 23.
  27. Reference to the monotonicity proposition for derivability — source line 25.
  28. Reference to the transitivity proposition for derivability — source line 27.
  29. Reference to the transitivity proposition for derivability — source line 43.
  30. Reference to the monotonicity proposition for derivability — source line 57.
  31. Reference to the reflexivity proposition for derivability — source line 58.
  32. Reference to the meta-level modus ponens proposition — source line 58.
  33. Reference to the first conditional axiom scheme — source line 69.
  34. Reference to the meta-level modus ponens proposition — source line 70.
  35. Reference to the example deriving the identity conditional — source line 73.
  36. Reference to the second conditional axiom scheme — source line 93.
  37. Reference to the meta-level modus ponens proposition — source line 93.
  38. Reference to the first conditional axiom scheme — source line 97.
  39. Reference to the second conditional axiom scheme — source line 97.
  40. Reference to the proposition listing five derivability facts — source line 122.
  41. Reference to the Deduction Theorem — source line 23.
  42. Reference to the Deduction Theorem — source line 28.
  43. Reference to the quantified Deduction Theorem — source line 55.
  44. Reference to the reflexivity proposition for derivability — source line 26.
  45. Reference to the transitivity proposition for derivability — source line 29.
  46. Reference to the monotonicity proposition for derivability — source line 40.
  47. Reference to the reflexivity proposition for derivability — source line 41.
  48. Reference to the second negation axiom scheme — source line 42.
  49. Reference to the meta-level modus ponens proposition — source line 43.
  50. Reference to the second falsity axiom scheme — source line 49.
  51. Reference to the meta-level modus ponens proposition — source line 50.
  52. Reference to the double-negation-elimination axiom scheme — source line 51.
  53. Reference to the meta-level modus ponens proposition — source line 52.
  54. Reference to the second negation axiom scheme — source line 66.
  55. Reference to the meta-level modus ponens proposition — source line 67.
  56. Reference to the proposition about two inconsistent opposite extensions — source line 82.
  57. Reference to the first conjunction axiom scheme — source line 33.
  58. Reference to the second conjunction axiom scheme — source line 33.
  59. Reference to the third conjunction axiom scheme — source line 35.
  60. Reference to the first negation axiom scheme — source line 50.
  61. Reference to the third disjunction axiom scheme — source line 54.
  62. Reference to the first disjunction axiom scheme — source line 57.
  63. Reference to the second disjunction axiom scheme — source line 57.
  64. Reference to the second negation axiom scheme — source line 79.
  65. Reference to the first conditional axiom scheme — source line 79.
  66. Reference to the existential-introduction axiom scheme — source line 45.
  67. Reference to the universal-instantiation axiom scheme — source line 46.
  68. Reference to the universal-instantiation axiom scheme — source line 43.
  69. Reference to the substitution and assignment extension proposition — source line 48.
  70. Reference to the Semantic Deduction Theorem — source line 76.
  71. Reference to the Semantic Deduction Theorem — source line 84.
  72. Reference to the proposition characterizing satisfaction of quantified sentences — source line 91.
  73. Reference to the definition of satisfaction — source line 93.
  74. Reference to the sentence extensionality corollary — source line 96.
  75. Reference to the proposition relating sentence truth to satisfaction under assignments — source line 99.
  76. Reference to the substitution and assignment extension proposition — source line 100.
  77. Reference to the extensionality proposition — source line 103.
  78. Reference to the Semantic Deduction Theorem — source line 106.
  79. Reference to the soundness theorem for axiomatic deduction — source line 115.
  80. Reference to the soundness theorem for axiomatic deduction — source line 132.
  81. Reference to the reflexive identity axiom scheme — source line 27.
  82. Reference to the substitution-of-identicals axiom scheme — source line 27.
  83. Reference to the proposition that the identity axioms are valid — source line 35.
  84. Reference to the substitution-of-identicals axiom scheme — source line 52.