A question about HOL
by Dennis J. Darland
July 30, 2008
Last revised 30.07.2008 21.41 time
Copyright © 2008 Dennis J. Darland
A thought I had:

  1. I had thought of representing a proposition R(a,b, ..., z) in HOL as apply(R,a,b,...,z) in FOL.
  2. But FOL is complete while HOL is not so obviously something was wrong.
  3. What is wrong is that there have to be additional rules in the second [FOL like] representation for the predicates.
  4. E.g. (R(a,b) ∧ S(a,b)) ⇒ T(a,b) for a T = (R ∧ S).
  5. There must be such a T in such a HOL, but there is nothing to guarantee that there is such a T in the FOL.
  6. But for any HOL with a finite number of predicates, it seems to me that it could be guaranteed.
  7. But any such HOL could only have a finite number of individuals [according to Leibniz's Law]
  8. Thus it seems the incompleteness of HOL essentially depends on an infinity of primitive [indefinable] predicates.
  9. But it is impossible that humans could ever know such an infinity of primitive predicates.
  10. Thus does the incompleteness of HOL have any practical importance?
  11. Or is there an error in my reasoning?
  12. The error, it would seem, is that Peano's axioms can be used to define an infinite number of individuals with a finite number of predicates.
  13. Let aRb if b is the successor of a.
  15. Then if there is a individual '0' and for every individual a there is a b [≠ a] such that aRb.
  16. See Peano's axioms for full details.
  17. But, so restricted, this is no longer a general HOL.
  18. A purely general HOL, would not have such restrictions on any relation on its individuals.
  19. Such a relation could hold only if its individuals were countable.
  20. Why make such a restriction?
  21. Goedel does make this assumption - Goedel, "On Formally Undecidable Propositions of Principia Mathematica and Related Systems", in van Heijennort, From Frege to Goedel, page 599.
  22. Goedel's theorem does not apply to a system which takes, say, real numbers, which are not countable, as its individuals.
  23. Or is there an error in my reasoning?
  24. Or take any uncountable subset of the real numbers
  25. I think the fact that the set of propositions of the form 'x = x' would be uncountable proves that there this logic would have to be incomplete.
  26. But reconsider the countable set - does there actually have to exist a counting [i.e. successor relation] holding just because a class is countable? Couldn't it be that for any a in some world that for any R there exist b,c,...,y,z if aRb and bRc, ...., yRz and z = a --- or does this result in a contradiction?
  27. I think that if you assume that all there are, are the natural numbers, then Goedel's result follows - but this assumption is obviously false and his result seems to depend on this assumption.


    28. Back to Top