True by accident (and therefore not amenable to proof) 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!
 A: Apart from your specific example, the idea of
truth-by-accident has been studied in the context of formal
first-order languages, which includes the language of graph
theory, and in his dissertation, Kurt Gödel proved
that the statements that happen to be true in all models of
a first order theory $T$ are exactly the statements that
are provable in $T$. This is his famous completeness
theorem.
Thus, any statement expressible in the first-order theory
of groups that happens to be true in all groups will be
provable from the group axioms, and any statement
expressible in the first-order theory of graphs that
happens to be true in all graphs will be provable from the
axioms of graph theory.
Your statement, however, does not seem to be expressible
directly in the language of graph theory, since it also
uses the concept of cardinality and of subgraphs, so the
completeness theorem does not apply directly to it for the
language of graphs. Rather, it is a statement of number
theory, and the relevant models for this case would include
all the standard and nonstandard models of arithmetic.
So the relevant conclusion would be that if the statement
were not provable in the first-order Peano's axioms
PA, then there
is a nonstandard model of arithmetic having a bad
(pseudo)finite graph.
But the particular form of the statement means that it has
complexity $\Pi^0_1$, which means it is a universal
statement quantifying over the natural numbers, and if any
such statement is independent of PA, then it is true, because if it is true in any
model, then because the standard model is an initial
segment of all the others, it follows that it must be true
in the standard model and hence true. This level of
complexity is the same complexity as many of the
interesting independent statements, including consistency
statements.

Incidentally, this seems to be my 500th answer on mathoverflow. It's been a lot of fun, and I've surely learned a lot of mathematics!
A: 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 https://en.wikipedia.org/wiki/Coincidence ). One way to put it on rigorous 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 perceive 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 capture 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 $n \log n$ 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 interesting.) It is known that various graph invariants must have the same value on such two graphs.
A: Yes, this is what constructivism is all about! In intuitionistic logic, the law of excluded middle doesn't generally hold, so it is not always possible to derive $A$ (i.e. $A$ is true) from $\lnot\lnot A$ (i.e. $A$ is not false).
The particular case you're considering is a form of Markov's Principle, which can be worded as if it is not the case that there is no example, then an example does exist. Symbolically, the rule is $$\lnot\forall x\lnot A(x) \to \exists x A(x),$$ where $A(x)$ is required to be decidable: $\forall x(A(x) \lor \lnot A(x))$. In constructive mathematics, existence is very strong — it is not acceptable to merely show that there must be an example, one needs to actually produce an example in some way or another. Markov's principle says that showing that there must be an example is enough to prove existence. Thus this principle is not generally accepted by most schools of constructivism, except in limited instances.
A: I first encountered this kind of speculation in Chapter 3 of Richard Stanley's book Enumerative Combinatorics, where Exercise 3(c) (or, in the second edition, Exercise 5(c)) suggests that if $f(n)$ is the number of non-isomorphic posets on $n$ elements, then the assertion that infinitely many $f(n)$ are palindromes in base ten is independent of the axioms of ZF. Clearly, this exercise is not intended to be tackled seriously; it's really an expression of the sentiment that there are some statements out there that are either true or false, but that we cannot hope to prove one way or another because they almost certainly lack the "structure" that we normally seek when doing mathematics.
If you want to try to formalize this notion, then one approach is to look at certain proofs of Gödel's incompleteness theorem.  For example, if you fix an axiomatic system such as ZF, then the theorems of the system are computably enumerable, but the set of arithmetical truths is not computably enumerable, so there must exist some truths that are not provable simply because (informally speaking) they are "too complicated to compute."  If you want to emphasize the idea that the unprovable statements are "complex" or "unstructured" in some sense, then you might prefer Chaitin's proof of the incompleteness theorem, which shows that for any formal system $S$, there is a constant $L$ such that the statement "$K(s) > L$" is unprovable in $S$ for all strings $s$ (here $K$ denotes Kolmogorov complexity).  The vast majority of such statements are true "at random" because a random string will have high Kolmogorov complexity.
However, you might not be satisfied with the above approach, because your intuition about the graph reconstruction conjecture is not based on the idea that the formal statement of the conjecture is so complex or uncomputable that it cannot be proved.  The conjecture, after all, can be stated very simply.  It's the apparent lack of relevant structure in the set of all graphs that is causing trouble.
It might be helpful to specify more carefully what kinds of "true by accident" statements you are thinking of.  One approach would be to construct a heuristic probabilistic model that predicts that certain things ought to be true just for "random reasons."  For example, there is Cramér's random model for the primes, which can be used to give heuristic "proofs" of various number-theoretic conjectures; e.g., one can use the model to predict that there will be only finitely many primes with such-and-such a property, because the probability that a prime $p$ has the property decreases rapidly to zero as $p\to\infty$.  It is easy to come up with many such conjectures that have a "true by accident" feel to them.  (In particular, I think it would be interesting if you could come up with a heuristic probabilistic model for graph theory, in the spirit of Cramér's model, that could "predict" various well-known graph-theoretic conjectures, including the reconstruction conjecture.)
The trouble with this approach is that there doesn't seem to be any clear way to declare that some particular statement of interest (such as the graph reconstruction conjecture) doesn't have a nice proof.  In a related MO question, Goldbach's conjecture is proposed as an example of something that might be "true by accident," but there's enough relevant structure that such a claim is highly controversial.  The space of all possible proofs is itself a highly complex mathematical object, so who is to say that the statement "Intractable-looking conjecture X has a simple proof" couldn't be "true by accident"?  Maybe there exists a beautifully simple proof out there, but it's a tiny needle buried in a totally unstructured haystack, and so we humans will never be able to find it.
In summary, there are some ways one could try to formalize this notion, but unfortunately, I don't think any of them lead in a promising direction (other than perhaps my suggestion above that it would be interesting to formulate a heuristic probabilistic model for graph theory that could "predict" the truth of certain conjectures without actually proving them).

EDIT (August 2022): I recently learned of John Conway's 2013 Amer. Math. Monthly article, On unsettleable arithmetical problems, which among other things gives examples of probabilistic reasoning in support of a claim that some proposition is "unsettleable."  To give you the flavor, let me quote from Conway's Postscript:

The following argument has convinced me
that the Collatz $3n + 1$ Conjecture is itself very likely to be unsettleable, rather than
this merely having the slight chance mentioned above. It uses the fact that there are
arbitrarily tall “mountains” in the graph of the Collatz game. To see this, observe that
$2m − 1$ passes in two moves to $3m − 1$, from which it follows that $2^k m − 1$ passes
in $2k$ moves to $3^k m − 1$. Now by the Chinese Remainder Theorem we can arrange
that $3^k m − 1$ has the form $2^l n$, which passes by $l$ moves to $n$. There is a very slight
possibility that $n$ happens to be the same as the number $2^k m − 1$ that we started with.
Let’s suppose that the starting number $2^k m − 1$ is about a googol; then the downward
slope of the mountain certainly contains a number between one and two googols, so
the chance that this is the same as the starting number is at least one googolth. (This
is justified by observations for smaller $n$ showing that the first iterate that lies in the
range $[n, 2n)$ is approximately uniformly distributed in this range.) In my view the
fact that this probability, though very small, is positive, makes it extremely unlikely
that there can be a proof that the Collatz game has no cycles that contain only large
numbers. This should not be confused with a suggestion that there actually are cycles
containing large numbers. After all, events whose probability is around one googolth
are distinctly unlikely to happen!

A: The statement in question can be formalized in the language of Peano Arithmetic, and I will treat it as a statement in that language.  A similar analysis works for any effective theory stronger than PA, such as ZFC.
Consider the set of all sentences in the language of PA; define an order relation $R$ so that $\phi \mathbin{R} \psi$ if $\phi \to \psi$ is provable in PA. This gives a pre-order; if we perform the usual equivalence class construction then the resulting algebra is a partial order called a Lindenbaum algebra (*).
Because the graph reconstruction conjecture corresponds to a sentence $G$ in PA, it corresponds to a particular node in this algebra.

*

*If $G$ is provable in PA, then $G$ corresponds to the bottom element of the algebra

*If $G$ is false, it corresponds to the top node of the algebra, but in this case we're not very worried about its provability

*Otherwise, $G$ corresponds to some intermediate node of the algebra. In that case, we cannot prove $G$ from PA, but we can prove $G$ by assuming PA plus any axiom either in the equivalence class of sentences that forms $G$'s node or in the equivalence class of any node higher than $G$'s node.

In every case, unless $G$ is false, $G$ is amenable to proof, but the proof will have to assume axioms that are strong enough to prove the desired conclusion. There is no sentence which could "never actually be proved", although there are plenty of sentences that cannot be proved in PA, and false sentences can only be proved from false axioms. The question is simply which axioms are required to prove a particular sentence.

*: Traditionally, a "Lindenbaum algebra" or "Lindenbaum–Tarski algebra" should be defined with the dual ordering of the ordering I use. But the ordering in which $0=1$ corresponds to the top of the algebra matches better with the diagrams we create to illustrate relationships between different axiom systems, such as 1. People also use the reverse ordering in the context of set theory, where large cardinal axioms are sorted by consistency strength, e.g. 2.
A: This is a take on this question of a form different from the other answers, along the lines of the comments of Gjergji Zaimi and André Henriques.
No doubt in present day mathematics there are some conjectures or perhaps even results that have an 'accidental' feel, while others do not have this feel.
However, it seems to me that to a certain and I believe considerable extent this is a subjective impression, or perhaps subjective is not really the right term and I should rather say, this impression is informed by the current state of mathematics.
I do not have really good and precise historical examples at hand, but I think it is true that for example certain results on diophantine equations (finiteness results of solutions, say) a long time ago had a much more accidental feel. But now with the developement of Arithmetic Geometry (eg Mordell conj.) some of them are much better and conceptually understood and now feel natural or at least not accidental anymore.
Perhaps some of the results and conjectures that today look accidental will at some point in the future be natural consequence of theories yet to be developped.
Indeed, I believe it to be a quite common pattern of progress in mathematics that developements begin with concrete and isolated results and questions, and then theories follow that explain the 'accidents' and 'miracles'.
Goldbach's conjecture got mentioned and gets mentioned frequently as accidental. Let us look at something not too far away. 
The prime numbers contain infinitely many 3-term arithmetic progressions (van der Corput, 1930s). Accident, yes or no? Perhaps one could have thought so, when it was proved, but today the situation is different and it is widely conjectured (very recent results of Sanders achieve this for sets of just a slightly larger density) that any set of positive integers with the density of the primes has this property.
Who knows where the Theory of Set Addition (more generally Additive Combinatorics/Number Theory) will stand in some decades or centuries? Perhaps, then Goldbach conjecture will be a corollary of some natural theory.
In brief, I believe 'true by accident' (in the informal way I understand it, which seems not that far from the questioners intent) is to a considerable extent a time-dependent notion; it seems thus difficult for me to imagine that its spirit can be captured in a formal (time-independent) theory.
