logic question: enumerating propositions

Question

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!

Answer 1

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.

Answer 2

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

Answer 3

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.