Calculus for Higher Order Logic

Question

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

Answer 1

See :

• Herbert Enderton, A Mathematical Introduction to Logic (2nd ed - 2001), page 286 :

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 :

• Elliott Mendelson, Introduction to mathematical logic (4th ed - 1997), page 375.

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.

Answer 2

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.

Answer 3

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.