This question is about what kind of "object", from the perspective of mathematical logic, a counterexample is.
In the "usual mathematics" the common definition of a counterexample to a statement $\varphi\equiv\forall x \theta (x)$ would be an object $c$ such that $\theta(c)$ is false.
My question is: How can one formalize this concept in the setting of mathematical logic, where the "usual mathematics" is formalized in, say, the language of first-order logic together with some deduction system and the ZFC axioms ?
My thoughts: Since a counterexample involves some unquantified object, it doesn't seem to me to be part of formalization of the "usual mathematics", since in every axiom (side question: Are the axiom systems/formal theories that make sense and in which there are formulas with free variables ?) all variables are bounded by some quantifier, so we can't formally come up with such a $c$. My impression is that we rather prove that $$\neg \varphi\equiv \exists \hat c \neg \theta(\hat c)\quad\quad (*)$$ is true, by using the ideas we used to construct $c$ and the features of our deduction system that allows us to prove $(*)$.
Thus a counterexample, when working in a formalized setting, is just a syntactic object - a formula we can derive, that is the negation of the statement to which we want to find a counterexample. Is this perspective correct ?