# What is a counterexample in a formalized setting of mathematics

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 ?

Even if all the axioms in your favourite axiomatisation of ZFC are quantified, that doesn't stop you being able to prove in ZFC theorems of the form "There is exactly one set which is $F$" -- e.g., boringly, there is exactly one empty set. We can then conservatively add to our initial formalisation of ZFC a name for such a uniquely identified object -- as we do for the empty set, or $\omega$, or more exciting ordinals!
So we are now in a position, inside our formal theory, to specify a counter-example to a conjecture $\forall x\varphi(x)$ just as we might do in informal mathematics, i.e. by naming a particular object -- in our example, a set -- which fails to satisfy $\varphi$.
A counterexample in this sense to a set-theoretic conjecture of the form $\forall x\varphi(x)$ is a set. And since sets aren't syntactic objects, it isn't true that "a counterexample, when working in formalized setting [ZFC in our example], is just a syntactic object".
• +1 Great answer! But one thing is not yet clear to me: You seem to be assuming the counterexample to be unique, since you say (if I understood it right) that $\hat x$ is a counterexample to $\forall x \varphi (x)$ if we can deduce from our axioms $\exists ! \hat x \neg \varphi (\hat x)$, because then we can add $\hat x$ conservatively to our language. But how do we proceed if $\exists \hat x \neg \varphi (\hat x)$ is true instead of $\exists ! \hat x \neg \varphi (\hat x)$, that is how do we "choose" one counterexample among the collection of all counterexamples ? – user17793 Jan 18 '14 at 10:00
• @Peter Smith - We can say [see Godel (1930), pag.585 of van Heijenoort edition, footnote 10] that : " '$A$ is refutable' is to mean '$\lnot A$ is provable' ." So, I think taht can be useful to distinguish between : a refutation of a conjecture $\phi$, that is a proof of $\lnot \phi$, from a counterexample to $\phi$, that is (as you said) : " a particular object -- in our example, a set -- which fails to satisfy $\phi$ ". Of course, if the conjecture is of the "form" $\forall \phi$, a refutation will be a proof of $\exists \lnot \phi$, and in this case your first comment applies. – Mauro ALLEGRANZA Jan 19 '14 at 18:18