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