Formal definition of “counterexample”. What is the preferred formal definition of “counterexample” as in: zero is a counterexample for "every integer is either positive or negative". Where in the literature is the notion of “counterexample” formally defined? And what are the main theorems involving this notion? And what questions concerning it remain open?
 A: You can think of our knowledge of math as divided into (1) knowledge about mathematics itself—theorems of algebra, analysis, number theory, topology, etc.—and (2) knowledge about how to do mathematics—paradigmatic cases, heuristics for approaching a problem, counterexamples, etc.
Counterexamples are part of our knowledge of how to do mathematics. If you wanted a formal definition, I might say:

If you have a statement such as "Every $X$ has the property $P$", a counterexample for the statement is an $X$ that doesn't have the property $P$.

Furthermore, you might have a good reason to believe that every $X$ has the property $P$:


*

*If almost every $X$ has property $P$. For example, "Every rational number has a multiplicative inverse" is true in every case except for 0. 

*If you were formerly studying a special case where everything had the property $P$, and are now studying a more general case. For example, "Squaring a number makes it bigger." is true if you were only looking at natural numbers — but if you extend your view to numbers in $0<x<1$, the statement is false.

*If all of the "practical" examples you've seen have the property. For example, "all functions are continuous" is certainly not true. But if you are working with practical kinematics problems in physics, you may be used to functions that all have this property.


Counterexamples are one of the most important ways we organize our knowledge and sharpen our intuitions. 

See also: Edwina Rissland wrote a dissertation on how we procedurally organize our knowledge of how to do mathematics:

https://dspace.mit.edu/handle/1721.1/6928
A: My guess is that formally, a counterexample to $$\forall(x \in X, y \in Y)\varphi$$ is a basically a substitution $(x:= x_0, y:= y_0)$ together with a proof that $$(x:= x_0, y:= y_0) \varphi \rightarrow \bot.$$
Unfortunately, this means that the "set-of-counterexamples function" fails to be preserved by equality of booleans. For instance, the booleans $$\forall x \in \mathbb{R},x+1=x \qquad \forall x \in \mathbb{R},x^2=x$$ are equal, in that they're both FALSE; but, the corresponding sets of counterexamples are different. For instance, $(x:=1)$ gives a counterexample to the former, but not to the latter.
(I don't know whether or not this is an actual problem.)
By the way, we can think of a substitution like $(x:= x_0,y:= y_0)$ as being a bit like an ordered tuple, in this case $(x_0,y_0)$. The difference is that the "order" is replaced by a name for each individual element; so in this case, $x_0$ is in the "$x$" position (rather than the 1st position) and $y_0$ is in the "$y$" position (rather than the 2nd position.) I think computer scientists call such things records, which are viewed as elements of "named cartesian products" (aka "record types.")
A: First a joke: I don't know what a counterexample is, but I can recognize one when I see one. 
In a first order context, something like the following begins to capture the notion. Let $T$ be a theory over the language $L$. and let $\phi$ be the sentence  $\forall x_1\dots\forall x_n\psi(x_1,\dots,x_n)$. 
Then a counterexample to $\phi$ in the context $T$ is a model $M$ of $T$, and elements $a_1,\dots,a_n$ of $M$ such that $\psi(a_1,\dots,a_n)$ is false in $M$.
A related formal notion is that of semantic tableaux as used in systems of natural deduction. Because it is of interest in Computer Science, there is a considerable recent literature.
A: A counterexample is a special case of a general claim: a case that shows the claim to be false. This is really just a matter of common sense and everyday logic that applies far beyond mathematics. It isn't usually regarded as something that needs formal definition. Once you have a counterexample, you know that the general claim isn't true, and that's the end to it.
A: To use proof by counterexample, the original statement has to be of the form 
"For all x, statement $A_x$ is true". (1)
Thus, showing that for some x, the statement $A_x$ is false, proves that the original statement is false. A formal definition of a counterexample could be "an example that proves a statement false" or something. This is a rigorous way of proof and I don't know what you mean by open questions. For a few examples, see http://www.math.toronto.edu/writing/Counterexample.pdf .
Also the following poof technique is sometimes referred to as counterexample:


*

*We have to prove statement S true

*Let us suppose that S is false

*Show that this leads to something that is false

*Thus, S has to be true

