I think I got it, could you take a look, please.

• What have you tried? Commented Apr 2, 2021 at 10:48

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 Commented Apr 2, 2021 at 19:14
• Hi, I tried it and I think I got it. Could you take a look and check it? Commented Apr 3, 2021 at 5:22
• Also, I have another question posted if you can take a look.philosophy.stackexchange.com/questions/81003/… Commented Apr 3, 2021 at 6:55
• ... Just use Conditional Elimination. `Ra, (Ra -> Sb) |- Sb`, so therefore `Ra, ~Sb |- ~(Ra -> Sb)` Commented 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 Commented Apr 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). Commented 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. Commented Apr 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). Commented Apr 2, 2021 at 20:10
• @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.) Commented Apr 2, 2021 at 22:03