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:
- 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?
- 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.