My idea is to use disjunction elimination on (¬ A v C)to obtain C, and then use disjunction introduction to obtain (¬ D v C), but I'm having a hard time obtaining C.
2 Answers
Yes, that's the way to go.
You have two disjunctions in the premise. Eliminate both of them. Eliminate the conditional premise too.
- When you assume A, you can derive C from ¬ A v C via disjunctive syllogism (or sub-prof)
- When you assume ¬ B, you derive C from ¬ C → B via modus tollens (or sub-prof).
- Whenever you can derive C you may derive ¬ D v C by disjunction introduction.
- Therefore deriving ¬ D v C from A v ¬ B by disjunction elimination.
| A v ¬ B Premise
| ¬ A v C Premise
|_ ¬ C → B Premise
| A v ¬ B Reiteration (first premise)
| |_ A Assumption
| | ¬ A v C Reiteration (second premise)
| | |_ ¬ A Assumption
| | | : :
| | | ¬ D v C Somehow
| | +
| | |_ C Assumptuon
| | | ¬ D v C v-Introduction
| | ¬ D v C v-Elimination
| +
| |_ ¬ B Assumption
| | ¬ C → B Reiteration (third premise)
| | : :
| | ¬ D v C Somehow
| ¬ D v C v-Elimination
First, draw a tree diagram of the formula:
When you draw trees by hand, it is faster (and equally correct) to only write down the root operator for each node.
A "node" is one of the circles/boxes in the tree
- "
therefore
" is the same as→
. - comma
,
has the same meaning asand
I can feel the hate coming, so I will warn you you that some philosophers have a bee in their bonnet about "meta" vs "non-meta" operators:
- "
therefore
" is technically meta-level logical implication →
is the non-meta implication operator ("implication" isif...then
)- comma
,
is meta-level conjunction (and
operator) - some symbol, like
^
, represents non-meta conjunction (and
operator)
"meta" versus "non-meta" only matters if you do things like define meta-implication differently from non-meta implication.
In your case, your meta-level operators and the non-meta operators are defined the same way. So, there is no difference. For all intents and purposes meta-level and
(the comma ,
) is the same thing as non-meta and
.
Basically, you are trying to prove:
For all
A
,B
,C
, andD
in the set{true, false}
[(A or [not B]) and ([not A] or C) and ([not C] → B)] → ([not D] or C)
Given that your teacher used separate "therefore
" and →
, I am a little bit worried for you.
The same people often also say you cannot prove new rules of inference using the letters ABC...Z
.
Instead you must use Greek letters for proving new rules of inference.
That is just wrong; factually incorrect.
If you have a bad professor, do what you need to do to pass the class, but take everything they say with a grain of salt.
Anyway... end of digression. Let us get back to proving things!
Do a proof by contradiction.
Begin by assuming that the theorem is false.
Finish by finding a contradiction (X and [not X] for some statement X).
Mark the root node as "false"
There is a rule of inference which says that if an implication node is false, then its left child is true.
For any
x
,y
in{true, false}
,[not (x -> y)] -> x
Using your teacher's notation, it probably looks something like this:
**RULE NAME: IMPLICATION -- PARENT TO LEFT-CHILD **
[¬ (α -> β)] therefore α
There is a different rule which says that if a ->
node is false, then its right child must also be false.
IMPLICATION -- PARENT TO RIGHT-CHILD
INPUT "α -> β
" isfalse
OUTPUT: "β
" isfalse
There is a rule of inference which says that if an or
node is false, then both of its children are false.
** DISJUNCTION -- PARENT TO LEFT-CHILD**
INPUT "α v β
" isfalse
OUTPUT: "α
" isfalse
** DISJUNCTION -- PARENT TO RIGHT-CHILD**
INPUT "α v β
" isfalse
OUTPUT: "β
" isfalse
Anyway, just keep going like that.
Our proof looks like this:
+---------+------------------------------------------------------------+--------------+----------------------------------+
| LINE NO | STATEMENT | SOURCE LINES | JUSTIFICATION |
+---------+------------------------------------------------------------+--------------+----------------------------------+
| 1 | NOT [[(A v ¬ B) and (¬ A v C) and (¬ C → B)] -> (¬ D v C)] | n/a | assumption |
| 2 | [A v (¬ B)] and [(¬ A) v C] and [ (¬C) → B] | 1 | [¬ (α -> β)] therefore α |
| 3 | ¬(¬ D v C) | 1 | [¬ (α -> β)] therefore ¬β |
| 4 | D | 3 | ¬(α v β) therefore ¬α |
| 5 | ¬C | 3 | ¬(α v β) therefore ¬β |
| 6 | (¬C) → B | 2 | AND(x1, x2, ... xn) therefore xn |
| 7 | B | 5, 6 | α and (α -> β) therefore β |
| 8 | A v (¬B) | 2 | AND(x1, x2, ... xn) therefore xn |
| 9 | A | 7,8 | (not β) and (α v β) therefore α |
| 10 | (¬ A) v C | 2 | AND(x1, x2, ... xn) therefore xn |
| 11 | C | 9, 10 | (not α) and (α v β) therefore β |
| 12 | C and (not C) | 5, 11 | conjunction |
| 13 | [(A v ¬ B) and (¬ A v C) and (¬ C → B)] -> (¬ D v C) | 1, 12 | proof by contradiction |
+---------+------------------------------------------------------------+--------------+----------------------------------+
Your professor might not allow the rules of inference that I used.
If that is the case, just prove each of my rules from your professor's rules.
Then the proof is complete.
All of my rules are very easy to prove.
(not α) and (α v β) therefore β
comes straight from the truth-table definition of the v
operator.
Mathematicians would just say, "by the definition of the or
operator"
Sometimes with the tree-approach, we can get stuck. Sometimes, we cannot propagate a value from parent to child or a child to parent.
Next time, if you ever get stuck using the "tree" diagram method, proceed by cases.
Choose a node to make true in one case and false in the other case.
Write truth values in two different color pens.
For example, the node (A v ¬ B)
might say true
in red ink, and false
in blue ink.