I think I got it, could you take a look, please.
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
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.