The graph reconstruction conjecture claims that (barring trivial examples) a graph on n vertices is determined (up to isomorphism) by its collection of (n-1)-vertex induced subgraphs (again up to isomorphism).
The way it is phrased ("reconstruction") suggests that a proof of the conjecture would be a procedure, indeed an algorithm, that takes the collection of subgraphs and then ingeniously "builds" the original graph from these.
But based on some experience with a related conjecture (the vertex-switching reconstruction conjecture), I am led to wonder whether this is something that is simply true "by accident". By this I mean that it is something that is just overwhelmingly unlikely to be false … there would need to be a massive coincidence for two non-isomorphic graphs to have the same "deck" (as the collection of (n-1)-vertex induced subgraphs is usually called). In other words, the only reason for the statement to be true is that it "just happens" to not be false.
Of course, this means that it could never actually be proved.. and therefore it would be a very poor choice of problem to work on!
My question (at last) is whether anyone has either formalized this concept – results that can't be proved or disproved, not because they are formally undecidable, but just because they are "true by accident" – or at least discussed it with more sophistication than I can muster.
EDIT: Apologies for the delay in responding and thanks to everyone who contributed thoughtfully to the rather vague question. I have accepted Gil Kalai's answer because he most accurately guessed my intention in asking the question.
I should probably not have used the words "formally unprovable" mostly because I don't really have a deep understanding of formal logic and while some of the "logical foundations" answers contained interesting ideas, that was not really what I was trying to get at.
What I was really trying to get at is that some assertions / conjectures seem to me to be making a highly non-obvious statement about combinatorial objects, the truth of which depends on some fundamental structural understanding that we currently lack. Other assertions / conjectures seem, again, to me, to just be saying something that we would simply expect to be true "by chance" and that we would really be astonished if it were false.
Here are a few unproved statements all of which I believe to be true: some of them I think should reflect structure and others just seem to be "by chance" (which is which I will answer later, if anyone is still interested in this topic).
(1) Every projective plane has prime power order
(2) Every non-desarguesian projective plane contains a Fano subplane
(3) The graph reconstruction conjecture
(4) Every vertex-transitive cubic graph has a hamilton cycle (except Petersen, Coxeter and two related graphs)
(5) Every 4-regular graph with a hamilton cycle has a second one
Certainly there is a significant chance that I am wrong, and that something that appears accidental will eventually be revealed to be a deep structural theorem when viewed in exactly the right way. However I have to choose what to work on (as do we all) and one of the things I use to decide what NOT to work on is whether I believe the statement says something real or accidental.
Another aspect of Gil's answer that I liked was the idea of considering a "finite version" of each statement: let S(n) be the statement that "all non-desarguesian projective planes of order at most n have a Fano subplane". Then suppose that all the S(n) are true, and that for any particular n, we can find a proof – in the worst case, "simply" enumerate all the projective planes of order n and check each for a Fano subplane. But suppose that the length of the shortest possible proof of S(n) tends to infinity as n tends to infinity – essentially there is NO OTHER proof than checking all the examples. Then we could never make a finite length proof covering all n. This is roughly what I would mean by "true by accident".
More comments welcome and thanks for letting me ramble!
Best Answer
This is a very interesting (yet rather vague) question. Most answers were in the direction of mathematical logic but I am not sure this is the only (or even the most appropriate) way to think about it. The notion of coincidence is by itself very complicated. (See http://en.wikipedia.org/wiki/Coincidence ). One way to put it on rigurous grounds is using probabilistic/statistical framework. Indeed, as Timothy mentioned it is sometimes possible to give a probabilistic heuristic in support of some mathematical statement. But its is notorious statistical problem to try to determine aposteriori if some events represent a coincidence.
I am not sure that (as the OP assumes) if a statement is "true by accident" it implies that it can never be proved. Also I am not sure (as implied by most answers) that "can never be proved" should be interpreted as "does not follow from the axioms". It can also refers to situations where the statement admits a proof, but the proof is also "accidental" as the original statement is, so it is unlikely to be found in the systematic way mathematics is developed.
In a sense (as mentioned in quid's answer), the notion of "true by accident" is related to mathematics psychology. It is more related to the way we precieve mathematical truths than to some objective facts about them.
Regarding the reconstruction conjecture. Note that we can ask if the conjecture is true for graphs with at most million vertices. Here, if true it is certainly provable. So the logic issues disappear but the main issue of the question remains. (We can replace the logic distinctions by computational complexity distinctions. But still I am not sure this will cpature the essence of the question.) There is a weaker form of the conjecture called the edge reconstruction conjecture (same problem but you delete edges rather than vertices) where much is known. There is a very conceptual proof that every graph with n vertices and more than nlogn edges is edge-reconstructible. So this gives some support to the feeling that maybe vertex reconstruction can also be dealt with.
Finally I am not aware of a heuristic argument that "there would need to be a massive coincidence for two non-isomorphic graphs to have the same 'deck'" as the OP suggested. (Coming up with a convincing such heuristic would be intereting.) It is known that various graph invariants must have the same value on such two graphs.