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)
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."
Ɐ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.