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 statement 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!

2 deleted 38 characters in body

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 statement 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 provable in ZF (and much weaker theories)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.

1

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 statement 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 provable in ZF (and much weaker theories), 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.