Here is a very contrived example which almost answers my question:
Say I want to know whether 3 is a root of $x^2-8$. Let $S$ be the set of all roots of $x^2-8$, together with all functions from finite sets to finite sets. I think to myself - if I search through this set and find the number 3, then 3 has to be a root of $x^2-8$, because the only numbers in the set are roots - all the other members of the set are functions. I make a list of all the sets in $S$ written as part of the cumulative hierarchy starting with the empty set, and I find that 3 is an element of this set. So 3 must be a root right?
Now this example was very contrived. In particular I force a type mismatch into the question. I am curious if, given current encoding conventions, situations like this could occur in natural mathematical problems. No one ever actually runs up against these types of problems because no one goes back to raw ZFC, but would we run into these kinds of problems if we did?
