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}