# I've been working on this for way too long :/

I've made a lot of progress on the proof below, but I am stuck on the last steps where I need to add existential quantifiers back in: ¬∃x ∃y Smaller(x,y)

For context, I'm a logic novice, but I'm trying my best to figure this out using everything I know. If anyone can help me get unstuck on this last step it would be MUCH appreciated

• The gist of this problem is you have to leverage the fact that there must be only objects with same size given the first 2 line premises. I don't see you explicate this in your proof yet, though you seem spending effort and time to duplicate this problem into 2 posts today in this site.. Commented May 12, 2022 at 4:49
• Maybe you have to follow the hint here Commented May 12, 2022 at 11:59

Your attempted application of Existential Elimination rule is incorrect. It takes the following form.

`````` | m. Ǝx Px
|  |_n. [a] Pa       Assume a witness
|  |  :
|  | p. R            Derive a statement not containing the witness variable (a)
|  q. R        m,n-p Existential Elimination
``````

The contradiction constant is a statement not containing any variables, so would be valid to use here; if you can somehow derive it.

Your attempted proof is to assume `Ǝx Ǝy Sxy` aiming is to derive a contradiction under this context, so you can then use negation introduction.

Well, in between, you have three existences to eliminate; two in that assumption and one in the premises. So raise three assumptions of witnesses, derive the contradiction, then discharge back to the first context, and so finish.

``````|  Ɐx Ɐy (Sxy → ¬Qxy)                  S : Smaller
|_ Ǝx Ɐy Qxy                           Q : SameSize
|   |_ Ǝx Ǝy Sxy
|   |   |_ [a] Ɐy Qay                  Assume witness [a]
|   |   |   |_ [b] Ǝy Sby               Assume witness [b]
|   |   |   |   |_ [c] Sbc               Assume witness [c]
|   |   |   |   |  Ɐy (Sby → ¬Qby)       Universal Elimination
|   |   |   |   |  Sbc → ¬Qbc            Universal Elimination
|   |   |   |   |  ¬Qbc                  Conditional Elimination
|   |   |   |   |  :
|   |   |   |   |  :
|   |   |   |   |  :
|   |   |   |   |  Qbc                   Somehow
|   |   |   |   |  ┴                     Negation Elimination
|   |   |   |  ┴                        Existential Elimination [c]
|   |   |  ┴                           Existential Elimination [b]
|   |  ┴                              Existential Elimination [a]
|  ¬Ǝx Ǝy Sxy                        Negation Introduction
``````

Now... all you need is to derive `Qbc`. However, there is no valid way to do so... unless you have access to Analytic Consequences regarding `SameSize` . After all, the second premise says "There is a thing that is the same size as everything."

Such as...

``````  Ɐx Qxx                         Reflexivity
Ɐx Ɐy (Qxy → Qyx)              Symmetry
Ɐx Ɐy Ɐz (Qxy → (Qyz → Qxz))   Transitivity

``````

If so, then put them to good use.

Grahams answer above is excellent. Samesize is an equivalence relation, and that fact must be used. Informally, the argument is as follows.

Assume that x < y implies that x and y are not the same size. also assume that there exists an x such that x is the same size as every object in the domain. then, assume for contradiction that there are an a and b such that a < b. Now we know there exists some c that is the same size as a and b, by second premise. This in conjunction with the equivalence relation properties should be enough to obtain contradiction.

• Yes! I have re-configured my proof and have added an edited version to my original post. The only issue I'm running into now is adding quantifiers after proving that a is not smaller than b. Commented May 11, 2022 at 19:34
• to clarify, what exactly is the formula you are trying to prove? Commented May 11, 2022 at 19:37
• ¬∃x ∃y Smaller(x,y) Commented May 11, 2022 at 19:40
• sorry, i read too fast. i will edit. Commented May 11, 2022 at 19:46
• no worries, thank you very much for your help so far :) Commented May 11, 2022 at 19:48