Apparently (∀x)(Fx v Gx) is not equivalent to (∀x)Fx v (∀x)Gx, however I seem to be able to prove it syntactically:
(∀x)(Fx v Gx) ⊬ (∀x)Fx v (∀x)Gx
(1) (∀x)(Fx V Gx)-----premise
(2) Fa v Ga------------1 UE
(3) Fa------------------2 A for v-E
(4) (x)Fx---------------3 UI
(5) (x)Fx v (x)Gx------4 vI
(6) Ga------------------2 A for v-E
(7) (x)Gx---------------6 UI
(8) (x)Fx v (x)Gx------7 vI
(9) (x)Fx v (x)Gx------2,3,5,6,8 v-E
What am I doing wrong? (Please excuse my poor formatting)
On
This probably won't be useful to you at this point, but the Curry-Howard perspective on this makes it very clear what goes wrong. Your proof attempt looks something like (using Agda syntax):
prf : {A : Set}{F G : A → Set} → ((a : A) → F a ∨ G a) → ((a : A) → F a) ∨ ((a : A) → G a)
prf p = disjunctionElimination (p a) (λ fa → inl (λ a → fa)) (λ ga → inr (λ a → ga))
You can ignore the first line. That just states the theorem we want to prove. In the second line, which corresponds to the actual proof, we use the variable a in the expression p a even though it is not bound. If a was bound to a value of type A, then p a would be a value of type F a ∨ G a. You then perform a case analysis on this disjunction. For the left case, you are given a value of type F a. You then attempt to bind a. To someone familiar with Agda, or even functional programming in general, the code above is just obviously incorrect.
To re-express your proof attempt and the above malformed Agda code in English, specialized to a particular case, let $F(n)\equiv n < 0$ and $G(n)\equiv n\geq 0$ where $n$ is taken to be a natural. Your proof attempt would then go as follows: Assume we have some natural $n$. If $n<0$ then, since $n$ was arbitrary, $\forall n.n<0$. Otherwise, if $n\geq 0$, then, since $n$ was arbitrary $\forall n.n\geq 0$. Thus, we have $(\forall n.n<0)\lor(\forall n.n\geq 0)$.
The issue with the above is that $n$ isn't arbitrary, it's some particular $n$, and further, in the left case it's an $n$ known to be less than $0$. (This is the assumption Graham Kemp mentions.) This is enforced in the Universal Generalization rule by requiring $n$ not to be free in the context. Universal Generalization binds $n$, but if $n$ occurs in the context, then $n$ has to be bound in a wider scope. Attempting to bind it in a narrower scope, which in the Agda code above corresponds to the nested lambdas, would make the bound variable and the free variable unrelated. This corresponds to the fact that the a bound (by λ) in λ a → fa is not the a that occurs in p a which is the a that occurs in the type of fa. You end up with something like $\forall b.F(a)$, i.e. $\forall m.n < 0$ in our example.
Line 4. It is only valid to use Universal Introduction to discarge an arbitrary free variable. The variable $a$ is not arbitrary within the subproof raised by assuming $Fa$ (you have made an assumption about it), so that subproof cannot be discharged by universal introduction.
$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{1.~\forall x~(Fx\lor Gx)}{\fitch{1.1.~[a]~\qquad\gets{\text{declare $a$ to be a new free variable}\\\text{sometimes this step is not explicitly made}}}{2.~Fa\lor Ga \quad\text{UE: instantiate the universal, since $a$ is arbitrary }\\\fitch{3.~Fa\qquad\text{Assumption: may only be true for certain instances}}{}\\\require{cancel}\cancel{4.~\forall x~Fx}\quad\gets\text{cannot use UI here; unable to generalise when not generally true}\\\vdots}\\\qquad\qquad\gets\text{UI may be used here to discharge free variable $a$}}$