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 appreciatedenter image description here

  • 1
    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.. May 12, 2022 at 4:49
  • Maybe you have to follow the hint here May 12, 2022 at 11:59

2 Answers 2


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. May 11, 2022 at 19:34
  • to clarify, what exactly is the formula you are trying to prove?
    – emesupap
    May 11, 2022 at 19:37
  • ¬∃x ∃y Smaller(x,y) May 11, 2022 at 19:40
  • sorry, i read too fast. i will edit.
    – emesupap
    May 11, 2022 at 19:46
  • no worries, thank you very much for your help so far :) May 11, 2022 at 19:48

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .