4 ms·

> FOL + arithmetic is undecidable for reasons Kurt Godel discovered. Adding finite arithmetic (i.e. on N-bit words rather than mathematical integers) to FOL sh

> FOL + arithmetic is undecidable for reasons Kurt Godel discovered. Adding finite arithmetic (i.e. on N-bit words rather than mathematical integers) to FOL should not change the decidability of FOL, or does it?

a1369209993 4y ago
> Adding finite arithmetic [...] should not change the decidability No (unless you can implement arbitrary-precision arithmetic indirectly, which you frequently can), but then you have insane, nonsensical conclusions[0] due to integer overflow. 0: Eg, the mass of the earth (in grams) is less than the mass of the moon (in grams) if you use 64-bit ints - but that's not true of their masses in kilograms or pounds.
- wizeman 4y ago
  > No To be clear, you're saying that it wouldn't change the decidability, correct? > 0: Eg, the mass of the earth (in grams) is less than the mass of the moon (in grams) if you use 64-bit ints - but that's not true of their masses in kilograms or pounds. Which is why you should have used 256-bit ints for computing that answer ;)
  - a1369209993 4y ago
    Adding (fixed-size) finite arithmetic will not change decidability in principle. In practice it can often be jury-rigged into non-fixed-size arithmetic. Also in practice, anything that requires enumerating all possible values of even a 64-bit integer to decide is bordering on undecidable in practice. > 256-bit ints And now you're well over the border.
    - wizeman 4y ago
      > > 256-bit ints > And now you're well over the border. Here's my plan. I'll wait a few decades until we have sufficiently-large and powerful quantum computers. Those reduce the time complexity from 2^256 to 2^128 just by being capable of performing sufficiently large quantum computations. I will precompute a table for 64-bit integers and store the results. Then for every 256-bit computation of complexity 2^128, I will split the computation in two parts: the first 64 bits of complexity will use raw CPU power to compute, and the last 64 bits will look up the result in the pre-computed table. Easy peasy. Hah! :)
      - PaulHoule 4y ago
        Get frozen cryogenically and wake up inside a simulation Dyson sphere. (Who needs Venus?) That's what SBF was counting on.
      - a1369209993 4y ago
        > the last 64 bits will look up the result in the pre-computed table. You need 2^64 different tables, one for each of the 2^64 different values of the first 64 bits. Also Grover search does not work that way.
        wizeman 4y ago
        > Also Grover search does not work that way. I'm curious, what do you mean by this? Do you mean that Grover's algorithm can't speed up algorithms that use disk storage, or do you mean something else?
        a1369209993 4y ago
        Well, yes (for all practical senses of "disk storage"), but the more general point is that Grover's algorithm applies after other improvements (if not instead of them, which is probably more common). If you have a way to reduce the complexity by a factor of 2^64, you get a classical (brute force) complexity of 2^192, which Grover's algorithm might be able to reduce to 2^96 quantum complexity, at best, assuming the classical optimization doesn't conflict with it. Realistically, the table thing doesn't work at all, so the problems with applying Grover's algorithm don't actually matter. (If you're just brute-forcing a int256_t for any value that makes your for-all predicate fail, Grover works fine to reduce the 2^256 classical operations to O(2^128)-ish quantum operations.)

a1369209993 4y ago

> Adding finite arithmetic [...] should not change the decidability No (unless you can implement arbitrary-precision arithmetic indirectly, which you frequently can), but then you have insane, nonsensical conclusions[0] due to integer overflow. 0: Eg, the mass of the earth (in grams) is less than the mass of the moon (in grams) if you use 64-bit ints - but that's not true of their masses in kilograms or pounds.

wizeman 4y ago
> No To be clear, you're saying that it wouldn't change the decidability, correct? > 0: Eg, the mass of the earth (in grams) is less than the mass of the moon (in grams) if you use 64-bit ints - but that's not true of their masses in kilograms or pounds. Which is why you should have used 256-bit ints for computing that answer ;)
- a1369209993 4y ago
  Adding (fixed-size) finite arithmetic will not change decidability in principle. In practice it can often be jury-rigged into non-fixed-size arithmetic. Also in practice, anything that requires enumerating all possible values of even a 64-bit integer to decide is bordering on undecidable in practice. > 256-bit ints And now you're well over the border.
  - wizeman 4y ago
    > > 256-bit ints > And now you're well over the border. Here's my plan. I'll wait a few decades until we have sufficiently-large and powerful quantum computers. Those reduce the time complexity from 2^256 to 2^128 just by being capable of performing sufficiently large quantum computations. I will precompute a table for 64-bit integers and store the results. Then for every 256-bit computation of complexity 2^128, I will split the computation in two parts: the first 64 bits of complexity will use raw CPU power to compute, and the last 64 bits will look up the result in the pre-computed table. Easy peasy. Hah! :)
    - PaulHoule 4y ago
      Get frozen cryogenically and wake up inside a simulation Dyson sphere. (Who needs Venus?) That's what SBF was counting on.
    - a1369209993 4y ago
      > the last 64 bits will look up the result in the pre-computed table. You need 2^64 different tables, one for each of the 2^64 different values of the first 64 bits. Also Grover search does not work that way.
      - wizeman 4y ago
        > Also Grover search does not work that way. I'm curious, what do you mean by this? Do you mean that Grover's algorithm can't speed up algorithms that use disk storage, or do you mean something else?
        a1369209993 4y ago
        Well, yes (for all practical senses of "disk storage"), but the more general point is that Grover's algorithm applies after other improvements (if not instead of them, which is probably more common). If you have a way to reduce the complexity by a factor of 2^64, you get a classical (brute force) complexity of 2^192, which Grover's algorithm might be able to reduce to 2^96 quantum complexity, at best, assuming the classical optimization doesn't conflict with it. Realistically, the table thing doesn't work at all, so the problems with applying Grover's algorithm don't actually matter. (If you're just brute-forcing a int256_t for any value that makes your for-all predicate fail, Grover works fine to reduce the 2^256 classical operations to O(2^128)-ish quantum operations.)