• silent_water [she/her]@hexbear.net
    link
    fedilink
    English
    arrow-up
    1
    ·
    1 year ago

    the model provided is a lazy cauchy sequence so any given real number can be computed to arbitrary precision. the theorems about real numbers are directly provable and potentially machine checkable, assuming decidable type checking works out.

    • Kogasa@programming.dev
      link
      fedilink
      arrow-up
      1
      ·
      1 year ago

      Nothing about what you said contradicts what I said. You can either change the definition of the computable real numbers, or agree that they are countable.