I guess I'll assume the answer to my question is "no", since no example has been found for more than a year? =)

@NoahSchweber: That link currently yields a "Forbidden" response.

@PaceNielsen: I don't think this post actually provides an answer, because the very term "ordinal" seems to be ill-defined from a pure meta-logical viewpoint. Just try to define it, and you will see that you cannot without invoking some (almost surely ZFC-based) notions of sets. Worse still, predicativists, not to say formalists, would likely stop around ATR0, but ATR0 is consistent with "there is no uncomputable well-ordering", so on what meta-logical grounds can you justify going further?

Hello! Do you have any idea about this question? It's also about iterating some kind of reflection principle, but starting with predicative theories of arithmetic. Thanks!

@JoséFigueroa-O'Farrill: How do we know that it was actually well-known to Russian mathematicians? If it had not even been published at that time, where is the evidence that your result wasn't simply stolen?

Okay I get what you're saying about "artificially baked", and given your clarification about believing the statements I am now convinced that your example here is a good one for those who believe Con(ZFC+MAH). Thanks!

To be clear, what I meant to say by "no reason to believe" is "no reason to believe just because it is in principle directly checkable", because it is simply false to claim that it can be directly checkable. For instance, you simply cannot directly check and verify Q, nor can you check and refute ¬Q.

Just came across this, but it is not at all convincing. Let Q be a sentence over ZFC such that ZFC ⊢ ( Q ⇔ ( no proof of "Q" over ZFC has length less than 2^(2^1000) ) ), which exists by the fixed-point lemma. Then ZFC+Con(ZFC) proves Q with proof length less than 1 million, but ZFC (if consistent) cannot prove Q with proof length less than 2^(2^1000). It has nothing to do with large cardinals. This example also show that there is no reason to believe truth of Σ0-sentences derived from large cardinal axioms. What if I call ¬Q a large cardinal axiom?

@TimothyChow: I don't disagree that mathematicians unconsciously use something that looks like replacement, but I disagree with saying that they unconsciously use replacement. If everything they do ends up being of the form I described, then it just shows that bounded replacement is intuitive, not that full replacement is.

Hello! I came across the FOM post and was trying to see if anyone on MO had anything to say about it, so I found your post. I don't agree with the claim here, because clearly the sets that ordinary mathematics uses does not go beyond bounded ZFC (i.e. with Specification and Replacement restricted to bounded formulae). In particular, we can have Skolem functions witnessing Pairing and Powerset, and set-builder notation { E : x∈S ∧ Q } where E is a term with only free variable x and Q is a bounded formula, and we would be stuck in bounded ZFC but be able to do all ordinary mathematics easily.

@MattF.: Wait you mean you know the truth-value of my above equation? I would of course guess "false", but why?

@MattF.: I have no idea, which is why I'm asking. I was surprised by your first reply, because I thought that something like $\sin(\exp(\exp(\exp(\exp(\exp(1)))))) = 0$ has not been decided, and that such an example is well-known and yet nobody knows how to prove or disprove it. But if hardly anybody tried this example, then is there any example that they did try?

@MattF.: Then do you have any intuitive idea for why its decidability has not been proven?

@MattF.: Is there any actual such expression whose equality to zero has not been decided?

The point is that reality obeys some laws. Therefore we could invent useful ways of reasoning about the world based on assumptions, and that has led to at least some parts of mathematical reasoning. If reality didn't obey classical FOL, we would not invent classical FOL.