Fitch Proof Help

Question

I'm having some trouble solving this proof in Fitch. How do the universals switch place from the premise to the goal? There is no negation in the goal so negation introduction is not the way to go, I believe.

∃y∀x Larger(x,y)     ; Premise

∀x∃y Larger(x,y)     ; Goal

Answer 1

As a hint here is a way to show this in another Fitch-style proof checker associated with the forallx text. What you will have to do in Fitch will likely be similar but not exactly the same.

What this proof is doing is eliminating the quantifiers and then introducing them again, but in a different way.

The existential elimination (∃E) may be the most confusing. It references line 1 and then starts a subproof with the name "a" replacing the variable "y". This is a substitution instance of line 1. Once I can get rid of that name, "a", I can discharge the assumption (line 2) and close the subproof. I was able to do that on line 4.

Existential elimination is covered in section 32.5 of the forallx text linked to below.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018.

Answer 2

How do the universals switch place from the premise to the goal?

∃y ∀x Larger(x,y) says that there is a y which every x is larger. Say there is such a thing that every x is larger, then every x is larger than that thing. Ergo ∀x ∃y Larger(x,y).

To present this in fitch, as Frank and Lemontree suggest, use the introduction and elimination rules.

Begin with the existential elimination rule: From Ⱶ ∃y P(y) and P(b) Ⱶ Q you may infer Ⱶ Q . Where b is a witness to the existential we seek to eliminate, presented in Fitch as a raised assumption:

|  :
|  ∃y P(y)      
|  |_[b] P(b)  Assume
|  |  :        
|  |  Q
|  Q           via ∃E

Here, you want that Q to be ∀x ∃y Larger(x,y) and P(y) to be ∀x Larger(x,y)

|  :
|  ∃y ∀x Larger(x,y)      
|  |_[b] ∀x Larger(x,b)   Assume  
|  |  :        
|  |  ∀x ∃y Larger(x,y)
|  ∀x ∃y Larger(x,y)      via ∃E

Well, universal introduction is that from [a] Ⱶ Q(a) infer Ⱶ ∀x Q(x) where a is an arbitrary assumed term. Here you want Q(a) to be ∃y Larger(a,y)

|  :
|  ∃y ∀x Larger(x,y)      
|  |_[b] ∀x Larger(x,b)   Assume
|  |  |_ [a]              Assume
|  |  |   :
|  |  |  ∃y Larger(a,y)     
|  |  ∀x ∃y Larger(x,y)   via ∀I
|  ∀x ∃y Larger(x,y)      via ∃E

So you need to use existential introduction, which is: from Ⱶ Q(b) infer Ⱶ ∃y Q(y) (where b is not an assumed term being discharged).

|  :
|  ∃y ∀x Larger(x,y)      
|  |_[b] ∀x Larger(x,b)   Assume
|  |  |_ [a]              Assume
|  |  |   Larger(a,b)
|  |  |   ∃y Larger(a,y)  via ∃I     
|  |  ∀x ∃y Larger(x,y)   via ∀I
|  ∀x ∃y Larger(x,y)      via ∃E

We are pretty much done, since we only need to note that universal elimination is: from Ⱶ ∀x P(x) infer Ⱶ P(a) (where a is a term in the context).

|_ ∃y ∀x Larger(x,y)      Premise      
|  |_[b] ∀x Larger(x,b)   Assume
|  |  |_ [a]              Assume
|  |  |   Larger(a,b)     via ∀E
|  |  |   ∃y Larger(a,y)  via ∃I     
|  |  ∀x ∃y Larger(x,y)   via ∀I
|  ∀x ∃y Larger(x,y)      via ∃E