<< Chapter < Page | Chapter >> Page > |
For proofs on this homework, remember that each step must be justified by one of the following:
Fill in the blank reasons in the following proof that ∨ commutes, that is, .
1 | Premise | ||
2 | subproof: | ||
2.a | Premise for subproof | ||
2.b | ∨Intro, line 2.a | ||
3 | subproof: | ||
3.a | Premise for subproof | ||
3.b | ____________________ | ||
4 | ____________________ |
Show that .
Show what is often called the implication chain rule: .
[Practice problem solution provided.]
Show what is often called negated-or-elimination (left): .
1 | Premise | ||
2 | subproof: | ||
2.a | Premise for subproof | ||
2.b | ∨Intro, line 2a | ||
2.c | Intro, lines 1,2b | ||
3 | RAA, line 2 |
Using the inference rule RAA, prove .
Show that .
In our inference rules, unlike our equivalences, we chose to not include any corresponding to distributivity.
Prove a left-hand version of one direction of distributivity: .
Use the previous part's result, plus ∧'s commutativity to prove the corresponding right-hand version: .
In our inference rules, unlike our equivalences, we chose to not include any corresponding to DeMorgan's Law.Show that each of the following versions is still provable.
The above exercise suggests that it would be useful to have an inference rule or theorem that says given , then . Or, equivalently, because of ⇒Intro and ⇒Elim, . Why don't we?
In our inference rules, unlike our equivalences, we have nothing that directly equates and . Prove each of the following.
Prove the following:
Prove what is commonly called the Law of Excluded Middle : .
Give a short proof citing our previous proof of and the relevant version of DeMorgan's Law from above .
Give a direct version without using previous theorems.
Prove the missing steps and reasons in the following WaterWorld proof of .
1 | ____________________ | ||
2 | ____________________ | WaterWorld axiom | |
3 | ____________________ | ⇒Elim, lines 1,2 | |
4 | subproof: | ||
4.a | Premise for subproof | ||
4.b | ____________________ | ||
4.c | ____________________ | ||
5 | subproof: | ||
5.a | Premise for subproof | ||
5.b | CaseElim (left), lines ____________________ where , and | ||
5.c | ____________________ | ____________________ | |
5.d | ____________________ | ||
6 | Theorem: Excluded Middle, where | ||
7 | ____________________ |
[Practice problem solution provided.]
Given the above figure , and using any of the immediately obvious facts as premises, prove that location is safe by using our proof system and the WaterWorld axioms.
While this proof is longer (over two dozen steps), it's not too bad when sub-proofs are used appropriately.To make life easier, you may use the following theorem: , along with any proven previously. When looking at the given board, you can use premises like as well as .
1 | Premise | ||
2 | Premise | ||
3 | Premise | ||
4 | Theorem: above problem , line 2 | ||
5 | Theorem: ∨ commutes, line 4 | ||
6 | CaseElim, lines 3,5 | ||
7 | subproof: | ||
7.a | Premise for subproof | ||
7.b | ¬Elim, line 7.a | ||
7.c | ∧Elim, line 7.b | ||
7.d | WaterWorld axiom | ||
7.e | ⇒Elim, lines 7.c,7.d | ||
7.f | Intro, lines 6,7.e | ||
8 | RAA, line 7 | ||
9 | subproof: | ||
9.a | Premise for subproof | ||
9.b | ¬Elim, line 9.a | ||
9.c | ∧Elim, line 9.b | ||
9.d | WaterWorld axiom | ||
9.e | ⇒Elim, lines 9.c,9.d | ||
9.f | Intro, lines 6,9.e | ||
10 | RAA, line 9 | ||
11 | Theorem: Allowed by problem statement | ||
12 | ⇒Elim, lines 1,11 | ||
13 | Theorem: ∨ commutes, line 12 | ||
14 | CaseElim, lines 8,13 | ||
15 | Theorem: ∨ commutes, line 14 | ||
16 | CaseElim, lines 10,15 | ||
17 | ∧Elim, line 16 |
Alternatively, the subproofs could easily have been pulled out into lemmas. Just like using subroutines in a program, that wouldmake the proof somewhat clearer, even though in this case each lemma would be used only once.
Observe how the two subproofs have some identical lines (7.c-7.f and 9.c-9.f).It would be incorrect to replace those lines in the second subproof with a citation of the results of the first subproof.First, because the previous subproof had been completed, and moreover, the two subproofs have different premises.This is analogous to two subroutines that happen to have some identical code lines, even through they are called separately and havedifferent parameters.
Starting from the WaterWorld axiom , we could prove the following theorem cited in the previous problem : .
Prove the following theorem which is slightly simpler: .
[Practice problem solution provided.]
Show that the ¬Elim inference rule is redundant in our system. In other words, without using ¬Elim, prove that .
1 | Premise | ||
2 | subproof: | ||
2.a | Premise for subproof | ||
2.b | Intro, lines 1,2.a | ||
3 | RAA, line 2 |
Show that the ¬Intro inference rule is redundant in our system. In other words, without using ¬Intro, prove that . To make sure that you're not hiding any uses of ¬Intro,also do not use any previous theorems.
Show that the CaseElim inference rule is redundant in our system. For brevity, we'll just consider the left-hand version.In other words, without using CaseElim, prove that . To make sure that you're not hiding any uses of CaseElim,also do not use any previous theorems.
Lemma A line 1or
main proof line 2.)
Lemma A line 1or
main proof line 2.)
Which is worse, having an unsound (but complete) inference system or an incomplete (but sound) one? Why?
Notification Switch
Would you like to follow the 'Intro to logic' conversation and receive update notifications?