I think I got it, could you take a look, please.
1
-
1What have you tried?– Graham KempApr 2, 2021 at 10:48
Add a comment
|
2 Answers
Let's start you on your journey. You want to derive a negation. Use a proof by negation introduction. Assume Tmm, introduce an existential, and then use the premises to derive the contrary too.
| (∃x)(Rx) (Premise)
| (∃x)(~Sx) (Premise)
|_ (∀x)(∀y)(~(Rx → Sy) → ~(∃z)(Tmz)) (Premise)
| |_ Tmm (Assumption)
| | (∃z)(Tmz) (Existential Introduction)
| | :
| | :
| | ~(∃z)(Tmz) (Negation Introduction)
| | # (Negation Elimination)
| ~Tmm (Negation Introduction)
I have followed your steps and also uploaded where I get stuck. Could you take a look and give me some suggestions, please. Thank you – Stanley
1 | (Ex)Rx Premise 2 | (Ex)~Sx Premise 3 |_ (Ax)(Ay)(~(Rx > Sy) > ~(Ez)Tmz) Premise 4 | |_ Ra Assumption 5 | | |_ ~Sb Assumption 6 | | | (Ra & ~Sb) 4,5 &I : : :
That is not according to my advice. My suggested goal is to derive ~(Ez)Tmz so that you can derive a contradiction under the assumption of Tmm. You could do that if you could derive ~(Ra > Sb); since universal eliminations of the third premise gives ~(Ra > Sb) > ~(Ez)Tmz . So... try that.
1 | (Ex)Rx Premise
2 | (Ex)~Sx Premise
3 |_ (Ax)(Ay)(~(Rx > Sy) > ~(Ez)Tmz) Premise
4 | |_ Tmm Assumption
5 | | (Ez)Tmz E Introduction 4
6 | | |_ Ra Assumption
7 | | | |_ ~Sb Assumption
8 | | | | |_ Ra > Sy Assumption
: : : : : :
: : : : :
m | | | | ~(Ez)Tmz :
n | | | ~(Ez)Tmz E Elimination 2,7-m
o | | ~(Ez)Tmz E Elimination 1,6-n
p | | # ~ Elimination 5,o
q | ~Tmm ~ Introduction 4-p
-
Hi Graham Kemp, I have followed your steps and also uploaded where I get stuck. Could you take a look and give me some suggestions, please. Thank you– StanleyApr 2, 2021 at 19:14
-
Hi, I tried it and I think I got it. Could you take a look and check it?– StanleyApr 3, 2021 at 5:22
-
Also, I have another question posted if you can take a look.philosophy.stackexchange.com/questions/81003/…– StanleyApr 3, 2021 at 6:55
-
... Just use Conditional Elimination.
Ra, (Ra -> Sb) |- Sb, so thereforeRa, ~Sb |- ~(Ra -> Sb)Apr 3, 2021 at 9:19
Well, at a broad level, ∀x ∀y [~(~Rx ∨ Sy) → ~(∃z Tmz)] is equivalent to ∀x ∀y [(Rx ∧ ~Sy) → ~(∃z Tmz)]. Your other two premises tell you that there is an x and a y such that (Rx ∧ ~Sy). This implies the conclusion, ~(∃z Tmz). This is equivalent to ∀z ~Tmz, and then you can instantiate z with m, yielding ~Tmm.
Your proof should generally follow that logic. You just need to translate each step into a Fitch proof in your system.
-
I only know (∃x)Rx and (∃x)~Sx can be combined to ((∃x)Rx & (∃x)~Sx), but this can not imply ~(∃z Tmz) because they are not ∀x ∀y ~(Rx → Sy). Could you tell me what move should I take to make it happen? Thank you– StanleyApr 2, 2021 at 18:58
-
@Stanley you first need to use existential elimination on the first two premises to obtain Rx ∧ ~Sy (where x and y have not yet been used as free variables). Then use universal elimination to obtain (Rx ∧ ~Sy) → ~(∃z Tmz). Apr 2, 2021 at 19:03
-
Ok, I got the result of (∃x)(∃y)(Rx & ~Sy), but can I use universal elimination directly to (∀x)(∀y)~(Rx → Sy) → ~(∃z)Tmz? since it is a conditional sentence.– StanleyApr 2, 2021 at 19:43
-
@Stanley you need to use existential elimination, to go from (∃x)(∃y)(Rx & ~Sy) to just Rx & ~Sy (where x and y have not been used as free variables before in your proof). Apr 2, 2021 at 20:10
-
1@Stanley logic.stanford.edu/intrologic/notes/chapter_08.html scroll down to where it says "existential elimination." The rule is that from ∃x p(x), you can derive the plain expression p(x), provided you have not previously used x as a free variable. (If you have already used x as a free variable you would instead instantiate as p(y) or p(w) or something you haven't used.) Apr 2, 2021 at 22:03