I'm having trouble understanding quantifiers in proofs. The proof I'm working with is :
¬∀x Tet(x) -- Premise
¬∀x (Tet(x) ∧ Medium(x)) -- Goal
How do I reach this goal and also get to the goal Medium(x) if it's not listed as a premise?
-
Hint: remember the disjunction-introduction rule in propositional logic? You can infer P v Q from P alone, even though Q may not appear among any of the premises. The negation of universal statement (one that begins with a ∀) is logically equivalent to an existential statement (one that begins with an ∃). Try converting your premise to one that begins with an ∃, apply the ∃ instantiation/elimination rule, and see if you can use the above disjunction-introduction rule to introduce Medium(x). And welcome to Philosophy SE!!– Adam SharpeCommented May 28, 2019 at 20:15
Add a comment
|
2 Answers
How do I reach this goal and also get to the goal Medium(x) if it's not listed as a premise?
The key point is that you want to prove that not all things are Tet and Medium.
That is a job for Proof of Negation.
Assume the positive, ∀x (Tet(x) ∧ Medium(x)), aiming to derive a contradiction of the premises, ie derive ∀x Tet(x), thereby deducing the negative ¬∀x (Tet(x) ∧ Medium(x)) .
|_ ¬∀x Tet(x) -- Premise
| |_ ∀x (Tet(x) ∧ Medium(x)) -- Assumption
| | : -- … fill in the details
| | ∀x Tet(x) -- … to get this
| | # -- Negation Elimination
| ¬∀x (Tet(x) ∧ Medium(x)) -- Negation Introduction
Now you just need to eliminate the universal from that assumption in order to introduce the universal for the derivation …
One way to approach this is to assume the negation of what you are trying to show, that is, assume ∀x(Tet(x) ∧ Medium(x)). From that assumption derive a contradiction. Then you can discharge the assumption and use negation introduction to reach the goal: ¬∀x(Tet(x) ∧ Medium(x))
Using the proof checker associated with the forallx logic textbook, a proof would look like this:
You will need to use whatever inference rules you have available. I replaced Tet(x) with Tx and Medium(x) with Mx to make well formed formulas acceptable by this proof checker. More information on the inference rules can be found in the links below.
The general flow of the proof goes like this:
- On line 2 use change of quantifier (CQ) to write the premise without a negation sign in front.
- On line 3 assume the negation of what I want to derive to reach a contradiction (which is done on line 10).
- On line 4 begin a subproof to attempt to eliminate the existential quantifier on line 2 by replacing x with the name a. I need to discharge the assumption of this subproof for that attempt to succeed. That is done on line 9.
- On line 5 use universal elimination to write line 3 replacing x with a. I can use the same name a because line 3 is true for all values of x.
- Use conjunction elimination on line 6 to obtain Ta which will contradict line 4. This is noted on line 7.
- Use explosion on line 8 to get whatever I want. I want to find a contradiction for line 3 so I choose that.
- Note that contradiction on line 10 and then conclude on line 11 with negation introduction which is the desired goal.
Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/
answered May 28, 2019 at 20:35
-
Thank you Frank. How can I use the change of quantifier (CQ) on fitch? Commented May 28, 2019 at 22:39
-
@philosophicalpigeon I am not familiar with the Stanford Fitch proof checker. You may not need to use this in that proof checker. However, I suspect even there you would want to start off with the negation of what you want to derive, then derive a contradiction and then through indirect proof or negation introduction derive the desired goal. Commented May 29, 2019 at 0:06