Axiomatic Deduction — Read

Proof

Suppose $\Gamma \Proves !A \lif !B$source 107 and $\Gamma \Proves !B \lif !C$source 107. Then there is a derivation of $!A \lif !B$source 108 from $\Gamma$source 108; and a derivation of $!B \lif !C$source 109 from $\Gamma$source 109 as well. Combine these into a single derivation by concatenating them. Now add lines 3–7 of the derivation in the preceding example. This is a derivation of $!A \lif !C$source 112—which is the last line of the new derivation—from $\Gamma$source 113. Note that the justifications of lines 4 and 7 remain valid if the reference to line number 1 is replaced by reference to the last line of the derivation of $!A \lif !B$source 115, and reference to line number 2 by reference to the last line of the derivation of $!B \lif !C$source 117.

End of proof.

Proof

The formula $!A$source 49 by itself is a derivation of $!A$source 49 from $\Gamma$source 49.

End of proof.

Proof

Any derivation of $!A$source 59 from $\Gamma$source 59 is also a derivation of $!A$source 60 from $\Delta$source 60.

End of proof.

Proof

Suppose $\{!A\} \cup \Delta \Proves !B$source 70. Then there is a derivation $!B_1$source 71, …, $!B_l = !B$source 71 from $\{!A\} \cup \Delta$source 71. Some of the steps in that derivation will be correct because of a rule which refers to a prior line $!B_i = !A$source 73. By hypothesis, there is a derivation of $!A$source 74 from $\Gamma$source 74, i.e., a derivation $!A_1$source 75, …, $!A_k = !A$source 75 where every $!A_i$source 75 is an axiom, a element of $\Gamma$source 76, or correct by a rule of inference. Now consider the sequence $$!A_1, \dots, !A_k = !A, !B_1, \dots, !B_l = !B.$$source 78 This is a correct derivation of $!B$source 81 from $\Gamma \cup \Delta$source 81 since every $B_i = !A$source 82 is now justified by the same rule which justifies $!A_k = !A$source 83.

End of proof.

Proof

Exercise.

End of proof.

Proof

1. If $\Gamma \Proves !A$source 124, then there is a finite sequence of formulas $!A_1$source 125, …, $!A_n$source 125 so that $!A \ident !A_n$source 125 and each $!A_i$source 126 is either a logical axiom, a element of $\Gamma$source 126 or follows from previous formulas by modus ponens. Take $\Gamma_0$source 128 to be those $!A_i$source 128 which are in $\Gamma$source 128. Then the derivation is likewise a derivation from $\Gamma_0$source 129, and so $\Gamma_0 \Proves !A$source 130.

2. This is the contrapositive of (1) for the special case $!A \ident \lfalse$source 131.

End of proof.

Proof

We have that $\{!A, !A \lif !B\} \Proves !B$source 37:

By Reference to the transitivity proposition for derivability, $\Gamma \Proves !B$source 43.

End of proof.

Proof

The “if” direction is immediate. If $\Gamma \Proves !A \lif !B$source 55 then also $\Gamma \cup \{!A\} \Proves !A \lif !B$source 56 by Reference to the monotonicity proposition for derivability. Also, $\Gamma \cup \{!A\} \Proves !A$source 57 by Reference to the reflexivity proposition for derivability. So, by Reference to the meta-level modus ponens proposition, $\Gamma \cup \{!A\} \Proves !B$source 58.

For the “only if” direction, we proceed by induction on the length of the derivation of $!B$source 62 from $\Gamma \cup \{!A\}$source 62.

For the induction basis, we prove the claim for every derivation of length $1$source 65. A derivation of $!B$source 65 from $\Gamma \cup \{!A\}$source 65 of length $1$source 66 consists of $!B$source 66 by itself; and if it is correct $!B$source 66 is either $\in \Gamma \cup \{!A\}$source 67 or is an axiom. If $!B \in \Gamma$source 67 or is an axiom, then $\Gamma \Proves !B$source 68. We also have that $\Gamma \Proves !B \lif (!A \lif !B)$source 68 by Reference to the first conditional axiom scheme, and Reference to the meta-level modus ponens proposition gives $\Gamma \Proves !A \lif !B$source 70. If $!B \in \{ !A\}$source 70 then $\Gamma \Proves !A \lif !B$source 71 because the last sentence $!A \lif !B$source 71 is the same as $!A \lif !A$source 72, and we have derived that in Reference to the example deriving the identity conditional.

For the inductive step, suppose a derivation of $!B$source 75 from $\Gamma \cup \{!A\}$source 76 ends with a step $!B$source 76 which is justified by modus ponens. (If it is not justified by modus ponens, $!B \in \Gamma$source 77, $!B \ident !A$source 77, or $!B$source 78 is an axiom, and the same reasoning as in the induction basis applies.) Then some previous steps in the derivation are $!C \lif !B$source 80 and $!C$source 80, for some formula $!C$source 80, i.e., $\Gamma \cup \{!A\} \Proves !C \lif !B$source 81 and $\Gamma \cup \{!A\} \Proves !C$source 81, and the respective derivations are shorter, so the inductive hypothesis applies to them. We thus have both:

But also $$\Gamma \Proves (!A \lif (!C \lif !B)) \lif ((!A\lif !C) \lif (!A \lif !B)),$$source 89 by Reference to the second conditional axiom scheme, and two applications of Reference to the meta-level modus ponens proposition give $\Gamma \Proves !A \lif !B$source 94, as required.

End of proof.

Proof

We again proceed by induction on the length of the derivation of $!B$source 20 from $\Gamma \cup \{!A\}$source 20.

The proof of the induction basis is identical to that in the proof of Reference to the Deduction Theorem.

For the inductive step, suppose again that the derivation of $!B$source 25 from $\Gamma \cup \{!A\}$source 26 ends with a step $!B$source 26 which is justified by an inference rule. If the inference rule is modus ponens, we proceed as in the proof of Reference to the Deduction Theorem. If the inference rule is quantifier rule, we know that $!B \ident !C \lif \lforall[x][!D(x)]$source 29 and a formula of the form $!C \lif !D(a)$source 30 appears earlier in the derivation, where $a$source 31 does not occur in $!C$source 31, $!A$source 31, or $\Gamma$source 31. We thus have that

i.e., $\Gamma \Proves !B$source 48.

We leave the case where $!B$source 50 is justified by the rule quantifier rule, but is of the form $\lexists[x][!D(x)] \lif !C$source 51, as an exercise.

End of proof.

Proof

If $\Gamma \cup \{!A\}$source 25 is inconsistent, then $\Gamma \cup \{!A\} \Proves \lfalse$source 25. By Reference to the reflexivity proposition for derivability, $\Gamma \Proves !B$source 26 for every $!B \in \Gamma$source 27. Since also $\Gamma \Proves !A$source 27 by hypothesis, $\Gamma \Proves !B$source 28 for every $!B \in \Gamma \cup \{!A\}$source 28. By Reference to the transitivity proposition for derivability, $\Gamma \Proves \lfalse$source 29, i.e., $\Gamma$source 30 is inconsistent.

End of proof.

Proof

First suppose $\Gamma \Proves !A$source 39. Then $\Gamma \cup \{\lnot !A\} \Proves !A$source 39 by Reference to the monotonicity proposition for derivability. $\Gamma \cup \{\lnot !A\} \Proves \lnot !A$source 40 by Reference to the reflexivity proposition for derivability. We also have $\Proves \lnot !A \lif (!A \lif \lfalse)$source 42 by Reference to the second negation axiom scheme. So by two applications of Reference to the meta-level modus ponens proposition, we have $\Gamma \cup \{\lnot !A\} \Proves \lfalse$source 43.

Now assume $\Gamma \cup \{\lnot !A\}$source 46 is inconsistent, i.e., $\Gamma \cup \{\lnot !A\} \Proves \lfalse$source 46. By the deduction theorem, $\Gamma \Proves \lnot !A \lif \lfalse$source 47. $\Gamma \Proves (\lnot !A \lif \lfalse) \lif \lnot\lnot !A$source 48 by Reference to the second falsity axiom scheme, so $\Gamma \Proves \lnot\lnot !A$source 49 by Reference to the meta-level modus ponens proposition. Since $\Gamma \Proves \lnot\lnot !A \lif !A$source 50 (Reference to the double-negation-elimination axiom scheme), we have $\Gamma \Proves !A$source 51 by Reference to the meta-level modus ponens proposition again.

End of proof.

Proof

$\Gamma \Proves \lnot !A \lif (!A \lif \lfalse)$source 66 by Reference to the second negation axiom scheme. $\Gamma \Proves \lfalse$source 67 by two applications of Reference to the meta-level modus ponens proposition.

End of proof.

Proof

Exercise.

End of proof.

Proof

1. From Reference to the first conjunction axiom scheme and Reference to the second conjunction axiom scheme by modus ponens.

2. From Reference to the third conjunction axiom scheme by two applications of modus ponens.

End of proof.

Proof

1. From Reference to the first negation axiom scheme we get $\Proves \lnot !A \lif (!A \lif \lfalse)$source 50 and $\Proves \lnot !B \lif (!B \lif \lfalse)$source 51. So by the deduction theorem, we have $\{\lnot !A\} \Proves !A \lif \lfalse$source 52 and $\{\lnot !B\} \Proves !B \lif \lfalse$source 53. From Reference to the third disjunction axiom scheme we get $\{\lnot !A, \lnot !B\} \Proves (!A \lor !B) \lif \lfalse$source 54. By the deduction theorem, $\{!A \lor !B, \lnot !A, \lnot !B\} \Proves \lfalse$source 55.

2. From Reference to the first disjunction axiom scheme and Reference to the second disjunction axiom scheme by modus ponens .

End of proof.

Proof

1. We can derive:

   Three-line conditional-elimination derivation

   The derivation takes A and the conditional from A to B as hypotheses and obtains B by modus ponens.

   1. Printed line 1. Justification: hypothesis.

      1. $!A$source 74

   2. Printed line 2. Justification: hypothesis.

      1. $!A \lif !B$source 75

   3. Printed line 3. Justification: modus ponens from lines one and two.

      1. $!B$source 76

   source 73

2. By Reference to the second negation axiom scheme and Reference to the first conditional axiom scheme and the deduction theorem, respectively.

End of proof.

Proof

By the deduction theorem, $\Gamma \Proves \ltrue \lif !A(c)$source 28. Since $c$source 29 does not occur in $\Gamma$source 29 or $\top$source 29, we get $\Gamma \Proves \ltrue \lif \lforall[x][!A(x)]$source 29. By the deduction theorem again, $\Gamma \Proves \lforall[x][!A(x)]$source 30.

End of proof.

Proof

By Reference to the existential-introduction axiom scheme and the deduction theorem. By Reference to the universal-instantiation axiom scheme and the deduction theorem.

End of proof.

Proof

We have to verify that all the axioms are valid. For instance, here is the case for Reference to the universal-instantiation axiom scheme: suppose $t$source 43 is free for $x$source 44 in $!A$source 44, and assume $\Sat{M}{\lforall[x][!A]}[s]$source 45. Then by definition of satisfaction, for each $\varAssign{s'}{s}{x}$source 46, also $\Sat{M}{!A}[s']$source 46, and in particular this holds when $s'(x) = \Value{t}{M}[s]$source 47. By Reference to the substitution and assignment extension proposition, $\Sat{M}{\Subst{!A}{t}{x}}[s]$source 49. This shows that $\Sat{M}{(\lforall[x][!A] \lif \Subst{!A}{t}{x})}[s]$source 50.

End of proof.

Proof

By induction on the length of the derivation of $!A$source 60 from $\Gamma$source 61. If there are no steps justified by inferences, then all formulas in the derivation are either instances of axioms or are in $\Gamma$source 63. By the previous proposition, all the axioms are valid, and hence if $!A$source 64 is an axiom then $\Gamma \Entails !A$source 65. If $!A \in \Gamma$source 65, then trivially $\Gamma \Entails !A$source 65.

If the last step of the derivation of $!A$source 68 is justified by modus ponens, then there are formulas $!B$source 69 and $!B \lif !A$source 69 in the derivation, and the induction hypothesis applies to the part of the derivation ending in those formulas (since they contain at least one fewer step justified by an inference). So, by induction hypothesis, $\Gamma \Entails !B$source 73 and $\Gamma \Entails !B \lif !A$source 73. Then $\Gamma \Entails !A$source 74 by Reference to the Semantic Deduction Theorem.

Now suppose the last step is justified by quantifier rule. Then that step has the form $!C \lif \lforall[x][B(x)]$source 80 and there is a preceding step $!C \lif !B(c)$source 81 with $c$source 81 not in $\Gamma$source 81, $!C$source 82, or $\lforall[x][B(x)]$source 82. By induction hypothesis, $\Gamma \Entails !C \lif !B(c)$source 82. By Reference to the Semantic Deduction Theorem, $\Gamma \cup \{!C\} \Entails !B(c)$source 84.

Consider some structure $\Struct{M}$source 87 such that $\Sat{M}{\Gamma \cup \{!C\}}$source 87. We need to show that $\Sat{M}{\lforall[x][!B(x)]}$source 88. Since $\lforall[x][!B(x)]$source 89 is a sentence, this means we have to show that for every variable assignment $s$source 90, $\Sat{M}{!B(x)}[s]$source 90 (Reference to the proposition characterizing satisfaction of quantified sentences). Since $\Gamma \cup \{!C\}$source 91 consists entirely of sentences, $\Sat{M}{!D}[s]$source 92 for all $!D \in \Gamma$source 92 by Reference to the definition of satisfaction. Let $\Struct{M'}$source 93 be like $\Struct{M}$source 94 except that $\Assign{c}{M'} = s(x)$source 94. Since $c$source 94 does not occur in $\Gamma$source 95 or $!C$source 95, $\Sat{M'}{\Gamma \cup \{!C\}}$source 95 by Reference to the sentence extensionality corollary. Since $\Gamma \cup \{!C\} \Entails !B(c)$source 96, $\Sat{M'}{B(c)}$source 97. Since $!B(c)$source 97 is a sentence, $\Sat{M'}{!B(c)}[s]$source 98 by Reference to the proposition relating sentence truth to satisfaction under assignments. $\Sat{M'}{!B(x)}[s]$source 99 iff $\Sat{M'}{!B(c)}[s]$source 100 by Reference to the substitution and assignment extension proposition (recall that $!B(c)$source 101 is just $\Subst{!B(x)}{c}{x}$source 101). So, $\Sat{M'}{!B(x)}[s]$source 102. Since $c$source 102 does not occur in $!B(x)$source 102, by Reference to the extensionality proposition, $\Sat{M}{!B(x)}[s]$source 103. But $s$source 103 was an arbitrary variable assignment, so $\Sat{M}{\lforall[x][!B(x)]}$source 105. Thus $\Gamma \cup \{!C\} \Entails \lforall[x][!B(x)]$source 105. By Reference to the Semantic Deduction Theorem, $\Gamma \Entails !C \lif \lforall[x][!B(x)]$source 106.

The case where $!A$source 109 is justified by quantifier rule but is of the form $\lexists[x][!B(x)] \lif !C$source 110 is left as an exercise.

End of proof.

Proof

We prove the contrapositive. Suppose that $\Gamma$source 130 is not consistent. Then $\Gamma \Proves \lfalse$source 131, i.e., there is a derivation of $\lfalse$source 132 from $\Gamma$source 132. By Reference to the soundness theorem for axiomatic deduction, any structure $\Struct{M}$source 133 that satisfies $\Gamma$source 134 must satisfy $\lfalse$source 134. Since $\Sat/{M}{\lfalse}$source 135 for every structure $\Struct{M}$source 136, no $\Struct{M}$source 138 can satisfy $\Gamma$source 138, i.e., $\Gamma$source 139 is not satisfiable.

End of proof.

Proof

Exercise.

End of proof.

Proof

The formula $$(\eq[t_1][t_2] \lif (!A(t_1) \lif !A(t_2)))$$source 49 is an instance of Reference to the substitution-of-identicals axiom scheme. The conclusion follows by two applications of modus ponens.

End of proof.