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!

  • 1
    You must at least want your set of HOL formulas to be c.e., right?2011-05-28
  • 1
    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).2011-05-28
  • 0
    @Quinn: yes, and I even assume the set of HOL formulas is finite.2011-05-28
  • 0
    What thought process suggests the set of HOL formulas being finite?2011-05-29
  • 0
    @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.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
    How about HOL with some general semantics? Not the full semantic?2013-08-22
  • 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
    But the set of axioms must be c.e. in order to enumerate all truths, right?2011-05-28
  • 0
    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).2011-05-28
  • 0
    @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?2011-05-28
  • 0
    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.2011-05-28
  • 0
    I think he means true in every model of the given set of HOL formulas (i.e. axioms), so Godel's completeness still applies.2011-05-28
  • 0
    Only that Godel's completeness works only for FOL. As far as I know, there is no recursive proof system for higher order logics. But I'm no expert.2011-05-28
  • 0
    Thanks for the answer. What might be the reason why this fails for HOL? There could be a sentence that is false, but the HOL proof procedure may never terminate for that sentence. But the catch is that the sentences I need to test are all *ground* -- ie, containing no free or bound variables. Maybe this makes a difference...2011-05-28
  • 0
    I'd say the real wonder is the existence of a complete proof system for FOL.... Remember that the models for a language in FOL can be very complicated sets, so simply "checking all assignments" (as is done in propositional calculus by truth tables) is impossible. A completely syntactic way to determine if something is true is quite a miracle.2011-05-28
  • 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