Famously, there is no complete calculus for higher order logic that is effective. Therefore, given the rules and axioms of a effective calculus for higher order logic, we must find formulas that are logical valid but not provable in the calculus.

Effectiveness means: "There is a proof-checking algorithm that can correctly decide whether a given sequence of symbols is a proof or not." - Wikipedia

But there are calculi for higher order logic, which enable us to prove statements formulated in higher order logic.

My question: Do humans really find formulas that are logical valid but not provable in the calculus? (One knows, that one CAN find, but do we really find examples for such unprovable, but valid formulas?)

A very philosophical question: Is the set of **intuitively valid formulas of higher order logic effective? That is, is this set recursively enumerable?

** for humans

  • 2
    This questions seems answerable on math.SE. Can you make clearer where the philosophical question is? i.e., the question you think can be answered by something related to the academic discipline of philosophy. Most of these concerns seem to be either generically empirical or things that relate directly to the basic theory of college-level and above math.
    – virmaior
    Aug 15, 2015 at 13:51
  • 1
    A 'very philosophical question' is not how the word philosophy is generally used in its proper sense ie academic; in mathematics it tends to denote a strategy or a conjecture that are neither firm enough to be either a strategy or a conjecture; for example 'the philosophy of the Langlands Programme'. Aug 15, 2015 at 15:37
  • We entertain logic questions about subjects like Goedel here all the time, which belong firmly within the mathematical discipline of symbolic logic. Why stop at this one? This is surely not the first logic question here I have seeen answered with a theorem.
    – user9166
    Aug 16, 2015 at 15:54
  • @jobermark fair enough, I'll start a meta asking about how much mathematical logic we want to do.
    – virmaior
    Aug 17, 2015 at 2:50

3 Answers 3


See :

THEOREM 41C : The set of Godel numbers of valid second-order sentences is not definable in N by any second-order formula. [...] A fortiori, the set of Godel numbers of second-order validities is not arithmetical and not recursively enumerable. That is, the enumerability theorem fails for second-order logic.

The same result can be found into the treatment of SOL in :

For an "example", see page 381 :

We can exhibit an explicit sentence that is standardly valid but not generally valid [because all generally valid formulae are derivable in second-order predicate calculus (see page 379), this implies that the said formula is not derivable]. The Godel-Rosser incompleteness theorem can be proved for the second-order theory Ar2 [the second-order Peano's arithmetic]. Let R be Rosser's undecidable sentence for Ar2. If Ar2 is consistent, R is true in the standard model of arithmetic. Hence, Ar2 → R is standardly valid. However, Ar2 → R is not generally valid. For, if Ar2 → R were generally valid, it would be provable in second-order predicate calculus. Hence, R would be provable in Ar2, contradicting the fact that it is an undecidable sentence of Ar2.

  • Can second order arithmetic express its own consistency?
    – Conifold
    Aug 15, 2015 at 20:41
  • I don't see how this is an answer. The OP contains "One knows we CAN, but do we...?" So I assume he seeks a natural example, not an abstract existence proof.
    – user9166
    Aug 17, 2015 at 15:52

Famously, the continuum hypothesis, the axiom of choice, and a set of other potentially optional improvements of Zermelo-Frankel Set Theory are potentially true, but unprovable within the formalism of the theory itself.

In such cases, effective proof is absolutely impossible for either the statement itself or its negation. Since one side or the other is classically true, we have candidates for true-but-unprovable results, but, without any agreed criterion for truth beyond language, we can only narrow them down to opposing pairs, and never pick one that is definitely true and unprovable.

These, especially the axiom of choice, seem intuitive to some people, but can be used to produce counterintuitive results, so others feel we have not found the correct intuitive interpretation of them. And still others find other things intuitive, like the determinacy of matrix games, which would contradict the axiom itself. Since we cannot even agree on a criterion for what is intuitive, we cannot possibly imagine that this is a set, much less a recursively enumerable one, because the element operator is ambiguous.

In his Intuitionism, Brouwer sets the bar quite high on what is intuitive. Heyting recasts some of Brouwer's 'basic intuitions' in the form of sets of axioms, and his success here indicates the remainder can probably also be captured that way, though, to some degree, putting them that way defies the intention of the program.

From there we only accept what can be constructed. That means the true statements are recursively enumerable, because only stated axioms and the resulting proven statements are allowed to meet the criteria for intuitiveness.

So by at least one school that attends closely to intuition, you could consider the intuitive propositions recursively enumerable.

  • I am speaking about the Calculus for Higher Order Logic. So with 'formula' I mean 'higher order formula'. Your answer is completely useless. Aug 15, 2015 at 15:49
  • Are you claiming that CH is provable or disprovable in second-order logic? I am pretty sure a full second order theory still allows for it to be either true or false. People studying determinacy do not limit themselves in any way to first-order representations.
    – user9166
    Aug 16, 2015 at 0:31
  • The formula itself would be the full second-order statement of the axioms of ZF and CH together. This is a 'higher-order formula'. Your objection is completely unclear.
    – user9166
    Aug 16, 2015 at 1:41

The pattern shows up more than one would expect because there's so many neat things we wish we could prove with higher order logic.

I have had many conversations with religious individuals who can describe the behavior of the universe they believe in using second order logic, but cannot reduce it to first order logic (the most common reason being the construction of a universe that cannot be modeled as a set). The inability to prove that they are right can be quite frustrating.

  • While an important perspective, this is not an answer. Yes, there is boundless faith in second-order logic as a way out of incompleteness, and a whole theory of transfinite proof theory that hopes to make the ineffective theories still converge (even if it requires presuming determinacy and killing the Axiom of Choice). But the work is really, really hard, and doesn't net much leverage.
    – user9166
    Aug 17, 2015 at 15:53

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .