Is it possible to enumerate all propositions (ie, sentences containing no quantified or free variables) that are true given a set of formulas in higher-order logic? (ie, those propositions entailed by the set of HOL fomulas.)
The same question can be asked of first-order logic, and I don't know the answer either.
Thanks in advance!