File tree Expand file tree Collapse file tree
content/first-order-logic/axiomatic-deduction Expand file tree Collapse file tree Original file line number Diff line number Diff line change 3232 1. & $ \lnot !D \lif (!D \lif !E)$ & \olref [prp]{ax:lnot2} \\
3333 2. & $ (\lnot !D \lif (!D \lif !E)) \lif {}$ \\
3434 &\qquad $ ((!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E)))$ & \olref [prp]{ax:lor3}\\
35- 3. & $ (( !E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E))$ & 1, 2, \MP \\
35+ 3. & $ (!E \lif (!D \lif !E)) \lif ((\lnot !D \lor !E) \lif (!D \lif !E))$ & 1, 2, \MP \\
3636 4. & $ !E \lif (!D \lif !E)$ & \olref [prp]{ax:lif1}\\
3737 5. & $ (\lnot !D \lor !E) \lif (!D \lif !E)$ & 3, 4, \MP
3838\end {derivation }
111111 lines 3--7 of the !!{derivation} in the preceding example. This is
112112 !!a{derivation} of $ !A \lif !C$ ---which is the last line of the new
113113 !!{derivation}---from~$ \Gamma $ . Note that the justifications of
114- lines 4 and~7 remain valid if the reference to line number~2 is
114+ lines 4 and~7 remain valid if the reference to line number~1 is
115115 replaced by reference to the last line of the !!{derivation} of~$ !A
116- \lif !B$ , and reference to line number~1 by reference to the last
117- line of the !!{derivation} of~$ B \lif !C$ .
116+ \lif !B$ , and reference to line number~2 by reference to the last
117+ line of the !!{derivation} of~$ ! B \lif !C$ .
118118\end {proof }
119119
120120\begin {prob }
You can’t perform that action at this time.
0 commit comments