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!