2
$\begingroup$

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!

  • 0
    @Henry: I'm pretty sure Cybernet$i$c1 simply means he wants to ask his question with $r$espect to a given finite set of HOL formulas, as thus the given finite set is certainly recursively enumerable.2011-05-30

3 Answers 3

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.

  • 0
    HOL with Henkin semantics is just first-order logic, and so it has all the same properties as first-order logic.2013-08-22
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.

  • 0
    I guess it also depends on the domain. If the domain is finite, it must be possible even for HOL axioms, right? So the question exists only if the domain is infinite...2011-05-29
1

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

  • 0
    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.2011-05-28