The following is my attempt to formalize Berkeley's argument that it's not possible for a sensible object to exist without conceiving it. Line $3$ involves a meta-argument which I believe might be formalized in a better way than how I did it.
Although this proof seems to have the form of a valid proof, I believe there is something wrong with my application of Universal Introduction on line $8$. It seems intuitively invalid to assert that all things are conceived of simply in virtue of being able to assume their existence as on line $2$. The potential to conceive is not the same as actually conceiving, so there seems to be no valid basis to universalize a particular instance of assuming in this way. I believe the problem has to do with my unorthodox meta-argument on line $3$.
My question: Is there some formal reason to explain why this application of Universal Introduction seems invalid? Or is there an alternative way to formalize this argument to make its validity/invalidity more clear?
- Ax = x is an assumption
- Cx = x is conceived of
\begin{array}{l} & \{1\} & 1. & \forall x[Ax \to Cx] & \text{ Prem. }\\ & \{2\} & 2. & \neg Ca & \text{ Assum. }\\ & \{2\} & 3. & Aa & \text{ (a) is assumed on 2 }\\ & \{1\} & 4. & Aa \to Ca & \text{ 1 UE }\\ & \{1,2\} & 5. & Ca & \text{ 3,4 MP }\\ & \{1,2\} & 6. & Ca \land \neg Ca & \text{ 2,5 $\land$I }\\ & \{1\} & 7. & Ca & \text{ 2,6 RAA }\\ & \{1\} & 8. & \forall x[Cx] & \text{ 7 UI - invalid }\\ & \{1\} & 9. & \neg \neg \forall x[Cx] & \text{ 8 DNI }\\ & \{1\} & 10. & \neg \exists x[\neg Cx] & \text{ 9 QI }\\ \end{array}
The issue is with $a$.
The rule of $\forall$-intro is:
where in $x$ may not occur free in any hypothesis on which $\varphi(x)$ depends,
while $\forall$-elim is:
where $t$ is free for $x$.
Thus, if $a$ is a free variable in 2, you cannot "generalize" it in 8, due to 3.
Intuitively, it is quite obvious: if you stop at 8, we can say: "all fishes live in the sea" (by 1) and thus "everything (in the universe) lives in the sea" (by 8), that "sounds wrong"...