Take the 2-minute tour ×

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!

share|improve this question
You must at least want your set of HOL formulas to be c.e., right? –  Quinn Culver May 28 '11 at 13:20
For first-order logic, the answer is yes, the formulas "entailed" are precisely those that are deducible (provable from assuming the given formulas), and these deductions are recursively enumerable provided the given formulas are r.e. (per Quinn above). –  hardmath May 28 '11 at 13:56
@Quinn: yes, and I even assume the set of HOL formulas is finite. –  Yan King Yin May 28 '11 at 21:41
What thought process suggests the set of HOL formulas being finite? –  Henry May 29 '11 at 16:34
@Henry: I'm pretty sure Cybernetic1 simply means he wants to ask his question with respect to a given finite set of HOL formulas, as thus the given finite set is certainly recursively enumerable. –  hardmath May 30 '11 at 18:36
add comment

3 Answers

This is possible for first-order logic, as a consequence of the completeness theorem.

For second-order logic, it is not possible. One way to see this is that there is a finite axiomatization $P_2$ of Peano arithmetic in second-order logic, which is complete in the sense that for any sentence $\phi$ in this language, either $P_2 \vDash_2\, \phi$ or $P_2 \vDash_2 \lnot \phi$, where $\vDash_2$ indicates second-order logical consequence. In fact we have $P_2 \vDash_2 \,\phi$ if and only if $\phi$ is true in the standard model $\mathbb{N}$. If you could enumerate the set of $\phi$ such that $P_2 \vDash_2 \,\phi$ then this enumeration could be used to construct an enumeration of the set $T$ of all sentences of first-order Peano arithmetic which are true in $\mathbb{N}$. But $T$ is not r.e.; $T$ is not even arithmetically definable. So second-order logical consequence is not even arithmetically definable.

In reality, second-order logical validity encompasses far more than just the first-order theory of $\mathbb{N}$. It also includes, for example, either the continuum hypothesis or its negation: there is a sentence $\psi$ of second-order logic such that if CH holds then $\psi$ is a second-order validity and if CH fails then $\lnot \psi$ is a second-order validity. Other set-theoretic statements can also be captured by second-order sentences in this way.

share|improve this answer
How about HOL with some general semantics? Not the full semantic? –  Cookie Monster Aug 22 '13 at 20:26
HOL with Henkin semantics is just first-order logic, and so it has all the same properties as first-order logic. –  Carl Mummert Aug 22 '13 at 21:09
add comment

In FOL you have Godel's completeness theorem which show that every true proposition can be proved. So you can enumerate everything by simply checking all the possible proofs in the world.

For HOL I don't think this is possible, but can't give a reference.

share|improve this answer
But the set of axioms must be c.e. in order to enumerate all truths, right? –  Quinn Culver May 28 '11 at 13:24
Yes, but "true" propositions mean tautologies, and there is a c.e. proof system for tautologies in FOL (the same goes, indeed, for any c.e. theory, i.e. set of additional axioms in a specific FOL language). –  Gadi A May 28 '11 at 13:27
@Gadi But he's asking about the true propositions that follow from a given set of HOL formulas, so mightn't there be more true propositions than just the tautologies? –  Quinn Culver May 28 '11 at 13:42
By "true", what do you mean? Usually this means "true in every model", and then Godel's completeness theorem kicks inn. If, on the other hand, you say "true in a specific model I have in mind" the Godel's incompleteness theorem kicks in, showing that you might not be able to provide an axiom system capturing this model exactly; i.e. there will be a proposition true in your intended model but false in another model for the axioms. –  Gadi A May 28 '11 at 13:53
I think he means true in every model of the given set of HOL formulas (i.e. axioms), so Godel's completeness still applies. –  Quinn Culver May 28 '11 at 13:55
show 4 more comments

It is possible to enumerate all finite strings using a finite alphabet, in the sense of a countably infinite ordered list. For your enumeration, you then need to be able to:

  • eliminate all strings which are not sentences
  • eliminate all sentences which are not propositions
  • eliminate all propositions which are not true

The third of these is the difficult one

share|improve this answer
Thanks, that's a helpful insight. For the 3rd part I'd be testing for refutation. In FOL the refutation proof procedure is only semi-decidable, ie, for some truth propositions it may never terminate; for false propositions it is guaranteed to terminate. That gives sort of a semi-Yes answer for FOL. –  Yan King Yin May 28 '11 at 21:57
add comment

Your Answer


