I have some idea about what you do and don't know about definition and definability (in general) given the words you've said so far and the way you've used them.
Prospective theorems are not theorems until a proof is presented. At which point they become retrospective theorems.
All that "falsification" and counter-examples prove is that the so-called "proof" of a "theorem" wasn't. If you have indeed provided a counter-example that's a proof of negation which raises questions: what was wrong with the original "proof" of the theorem? Since proofs are programs - there must have been a bug in the proof. Better type-check that proof/program...
The presence of a counter-example to Sean Hunter's "theorem" simply demonstrates that it's not a theorem. It's a misnomer. Theorems are exactly those Mathematical stataments for which no proof of negation exists.
You seem to be presupposing some particular kind of mathematics. I am talking about all possible Mathematics in general; of which the particular Mathematics you are currently using is just one particular instance. A historical and cultural coincidence.
There's a Mathematical paradigm in which proof-by-contradiction is a valid proof method e.g mathematics founded upon classical logic.
And there's a Mathematical paradigm in which proof-by-contradiction is not a valid proof method e.g mathematics founded upon intuitionistic logic. This is basically what we call Computer Science. It has fewer axioms than Classical Mathematics (e.g the axiom of choice is severely restricted) and so it's a much stronger proof-system. You could even say Intuitionistic Mathematics (which is basically CS) is "more foundational" (it is much closer to the foundations?) than Mathematics.
The fact that you are admitting proof-by-contradiction in your methodology tells me about your choice of foundations, but so what? There's a foundation which axiomatically pre-supposes choice; and a foundation which doesn't.
And in the foundations where choice is not axiomatic "proof" by contradiction is not a valid proof.
The reasoning goes something like this:
1. Choice implies excluded middle. 2. Excluded middle implies all proposition are either true or false. 3. Excluded middle implies that proof by contradiction is valid.
Rejecting 1 results in the rejection of 2 and 3 also.