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 67Reader correction: The frozen source omits B before the membership sign in this induction-basis sentence. The reader supplies B, matching the same sentence and the immediately following case split. 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: The two induction-hypothesis consequences $$& \Gamma \Proves !A \lif (!C \lif !B); \\ & \Gamma \Proves !A \lif !C.$$source 84 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

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 schemeReader correction: The frozen proof cites the first conjunction-elimination axiom twice. The two conclusions require the first and second conjunction-elimination axioms, so the reader names axiom land two for the second citation. 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 Reader correction TR013-SOURCE-PROSE-004: The reader corrects the frozen source spelling 'modus ponsens' to '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

Do truth tables for each axiom to verify that they are tautologies.

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 tautologies, 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.

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 valuation $\pAssign{v}$source 133 that satisfies $\Gamma$source 134 must satisfy $\lfalse$source 134. Since $\pSat/{v}{\lfalse}$source 136 for every valuation $\pAssign{v}$source 137, no $\pAssign{v}$source 138 can satisfy $\Gamma$source 138, i.e., $\Gamma$source 139 is not satisfiable.

End of proof.