Set theory provides a good example. It is often convenient in set theory to work with the concept of "classes" and treat them as mathematical objects of their own kind. The standard axiomatization of set theory with classes is called Goedel-Bernays set theory, denoted GBC, whereas the usual ZFC axioms have only set objects. But there is a general theorem that any statement purely about sets that is proved by using classes in GBC can be proved without them purely in ZFC. This is what it means to say that GBC is a conservative extension of ZFC. To prove this general theorem, it suffices to observe that any ZFC model can be expanded to a model of GBC, by adding only the classes definable from parameters.
There are many other examples of conservative extensions in mathematics, and all of them would seem to be examples of the type that you seek. For example, PA has a conservative extension to the analogous theory true in the collection HF of hereditarily finite sets. Thus, to prove a theorem about numbers in PA, one can freely use heredtiarily finite sets (e.g. sequences of numbers, sequences of sets of numbers, etc.), not just as coded by numbers via Goedel coding, but as actual mathematical objects. And surely this makes proofs much easier.
Perhaps another type of example arises in the absoluteness phenomenon in set theory. For example, the Shoenfield Absoluteness theorem states that any Sigma^1_2 statement has the same truth value in any two models of set theory with the same ordinals. In particular, to prove that a particular Sigma^1_2 statement is true in ZFC, it suffices to prove it under the assumption also that V=L, where one also has all kinds of additional structure available. The Absoluteness Theorems (and there are many) can therefore be viewed under the rubric you mention.
But of course, in all these cases, we have an actual proof in the weaker theory. To prove that there is a proof, is a proof, so I believe ultimately there will be no way to avoid the quibbling over whether it is easy or hard to translate the high-level proof into a low level proof, since in principle it will always be possible to do this.
Gödel's Incompleteness Theorem says that if a system is
- consistent,
- recursively axiomatised and
- adequate for arithmetics
then it is cannot prove its own consistency.
If your formal system can prove its own consistency, it must either
- be able to prove anything, eg that $0=1$, or
- be (consistent,) recursively axiomatised and adequate for arithmetic.
So the question comes down to whether you can prove $0=1$ in it.
In general this is undecidable.
Indeed, this is exactly the Entcheidungsproblem, if I recall correctly.
Best Answer
In theory, David’s answer is correct. Nevertheless, in practice it is perfectly possible to prove the existence of a proof non-constructively (such as by manipulating models and then appealing to the completeness theorem) where no one has a clue how to actually find the proof.
One example which springs to mind is Jacobson’s theorem: if $R$ is a ring such that for every $a\in R$ there exists an integer $n > 1$ such that $a=a^n$, then $R$ is commutative. By completeness of equational logic, this implies that for any $n > 1$, there exists an equational derivation of $xy=yx$ from the axioms of rings and $x^n=x$. Already finding such derivation for $n=3$ is a nontrivial exercise; explicit derivations are known for some $n$, but not in general.