• barsoap@lemm.ee
    link
    fedilink
    English
    arrow-up
    1
    ·
    6 days ago

    first order logic validity problem

    Validity is RE (semidecidable), Satisfiability is undecidable.

    How do we figure out that your fancy new law is actually the oracle you claim it is? It could be lying to us, to establish the thing as an oracle we’d have to be able to either inspect it or unit-test it over the whole infinite range.

    • zeca
      link
      fedilink
      English
      arrow-up
      1
      ·
      6 days ago

      Right, validity is semidecidable, just like the halting problem.

      We might never know for certain that any natural law is true, we might never be certain that that oracle actually solves validity. But that doesnt prevent the oracle from working. My point is that its existence is possible, not that we will ever be able to trust it.

      Besides, we dont know that the physical laws we work with today are true, but we nevetheless use them for practical purpuses all the time.

      • barsoap@lemm.ee
        link
        fedilink
        English
        arrow-up
        1
        ·
        6 days ago

        I mean if the point is that we know that we know nothing then I’ll agree.

        • zeca
          link
          fedilink
          English
          arrow-up
          1
          ·
          6 days ago

          Not my point… and you know it. My point is that even if we consider that proven theorems are known facts, we still dont know if hypercomputers are infeasible. We know, however, that i’ll never write python code that decides Validity because it is not (classically) decidable. But we have no theorems on the impossibility of hypercomputation.

          • barsoap@lemm.ee
            link
            fedilink
            English
            arrow-up
            1
            ·
            6 days ago

            Back to the context though: If the brain can access it, why would AGI be unable to?

            • zeca
              link
              fedilink
              English
              arrow-up
              1
              ·
              6 days ago

              Never said AGI would be unable to.