What can we do with nonenumerable sets of formulas (e.g. formulas of Higher order Logic)?

Question

It is well known textbook fact, that the set of (grammatically correct) sentences/formulas of higher order logic (even of the second order logic) are not enumerable. My question is - what can we do about them and whether the research of infinite can help us?

Specifically, it would be nice to hear the answers on those questions:

1. We can not enumerate all HOL formulas (i.e., there is not algorithm to generate all of them (at least theoretically) as some kind of list, as tree or another data structure over which we can do, e.g., exhaustive search for some optimal formula (e.g. the formula that would be solution of inductive logic programming problem, the formula, that can serve as hypothesis for explaining the truthfulness of set of other formulas). That is clear. But I wanted to check: as I understand, then all of HOL formulas as generated by some Context-Free-Grammar (which is very simple, if we use lambda calculus), so - we should be able to generated (e.g. randomly) some string from this grammar and so - we can use such generated string to explore the entire space of HOL formulas? Is it so? Of course, it can be tricky to come up with random-algorithms (randomness) that generates formulas in uniform way (to explore the formula space uniformly) or in biased way (to explore certain promising regions of the formula space), but it should be possible? As I understand, then the CFG strings are enumerable, so - what is the source of un-enumerability for HOL formulas? Does the requirement that there can be infinite number of variables, leader to the unenumerability?
2. I am reading http://www.logic.univie.ac.at/~sdf/papers/joint.stefan.pdf (which is published in the most recent issue of J. Symb. Logic, as I understand then J. Symb. Logic and Ann. Pur. Appl. Logic are the 2 most important journals about fundamentals of mathematics, there are no better and more focused ones?) and I am suprised to hear about the existence of general structures, inside the infinite and nonenumerable sets (inside the cardinals). Are there methods or research that tries to take the set of HOL formulas (sentences) and that tries to transfer those structural results from the general set theory to the set of HOL formulas? I.d. this article mentions nonstationary ideals, wellorders, antichains. Does the set of HOL formulas have counterparts of those notions, maybe the nonstationary ideals of the set of HOL formulas have some interesting properties, some conclusions?

I just wanted to explore more about applications of HOL. My applied interest is to use HOL for the formal semantics of natural language and that is why I am so fond to learn more about it. Of course, I am reading Ebbinghaus books about logic (with excellent chapter beyond FOL), of course, I am aware of the work of Berlin group about proof automation in HOL, about use of HOL in Isabelle/HOL. But I feel, that maybe the general set theory results can give use some very general results for the HOL for specific theory.

Answer 1

It is well known textbook fact, that the set of (grammatically correct) sentences/formulas of higher order logic (even of the second order logic) are not [computably] enumerable.

This is entirely false.

This question is based on a misconception. The set of grammatically correct HOL sentences absolutely is computably enumerable. What's not computably enumerable is the set of valid HOL (even SOL) sentences, that is, those $\varphi$ which are true in every structure.

• I'm assuming the standard, as opposed to Henkin, semantics here; with the Henkin semantics, SOL (and HOL in general) is really just FOL in disguise

• Also, this is why I dislike the term "valid" here: personally I would interpret "valid sentence" as "grammatically correct sentence," and I suspect that's what happened here. But, its meaning is entrenched now. Oh well.

Your second question seems to reflect an additional error, namely the conflation of computable enumerability with the set-theoretic notion of countability. (There's an annoying terminological issue here, which is that "enumerable" is sometimes used as a synonym of "c.e." and of "countable," which may be the source of the confusion.) The set of HOL sentences is countable, so set-theoretically no different from $\mathbb{N}$; in particular, the combinatorial structures which may or may not exist on uncountable sets have no relevance to the set of HOL sentences (although per the below they can indeed be relevant to the semantic issues around HOL).

---

Where logical issues and HOL interact is in the semantic behavior of HOL (again, with respect to the standard semantics). This has both "local" (= looking at specific sentences or structures) and "global" (= looking at the overall behavior of SOL/HOL) aspects:

• For an example of the former, there is an SOL-sentence $\chi$ such that $\chi$ is valid iff the generalized continuum hypothesis holds, and there is a third-order sentence $\theta$ such that $\mathbb{N}$ (as a pure set!) satisfies $\theta$ iff the continuum hypothesis holds (actually $\theta$ is really just CH itself, no nontrivial work is needed).

• For an example of the latter, we can look at the basic "logical cardinal invariants:" e.g. the Lowenheim-Skolem, Lowenheim-Skolem-Tarski, and Hanf numbers of a given logic. With "nice" logics like first-order logic these are reasonably concrete things; by contrast, with second-order logic they depend wildly on set-theoretic principles, and in particular large cardinal axioms (see e.g. here).

• And of course this isn't a clear divide - e.g. I would argue that this question of mine has both local and global aspects in the sense above.

For analyzing semantic problems like these, set-theoretic techniques are of course indispensible; indeed SOL is arguably just set theory in disguise. But that's not at all what you're talking about - and in fact I'd actually consider it good evidence that you don't want to be looking at HOL (with the standard semantics, at least) in the contexts you describe.