7 ms·

> the same probability that seven billion people collectively hallucinated elementary theory Just for fun, it's not unprecedented that the entire human race is

by cvoss 3y ago

> the same probability that seven billion people collectively hallucinated elementary theory Just for fun, it's not unprecedented that the entire human race is disposed to mislearn basic truths about the universe which have to be unlearned when you get to the point where it matters. See quantum mechanics. One hopes that conscientious mathematicians are careful to select axiomatizations (such as ZF set theory or the type system of Lean) which faithfully reflect reality. And, within such a system, we can be extremely confident in what we're doing. But the distinct possibility remains that the axiomatization doesn't actually match our universe and, say, admits a proof of false or implies something not physically realizable, such as that a certain computation should terminate, when no real life physical machine obeying the laws of physics can ever do so.

mcguire 3y ago
Be careful with things like "faithfully reflect reality". :-) Euclidean geometry is intuitively good and seems to work on relatively small areas of the Earth's surface, but non-Euclidean geometries are inconsistent with it and more faithfully reflect a reality that lacks infinite flat planes.
- mcphage 3y ago
  Or even Newtonian Physics, which faithfully reflects reality—as long as you're not too large, or you're not traveling too fast. And then it starts to break down.
- commonlisp94 3y ago
  This is not true. They are incompatible sets of axioms, but they can describe the same set of shapes, although one system is going to be a lot more inconvenient than the other. The differences are logically interesting, but about as incompatible as choosing to make the origin of a euclidean system one corner of the room instead of another. In contrast physical theories contradict each other by making different predictions which can be falsified.
  - ukj 3y ago
    At that level of pedantry even the halting problem is solvable. Just choose a suitable representation for the Turing machines in question. Describe/represent the ones that halt using 1; and the ones that don’t halt using 0. This produces the pairs (TM1, 1), (TM2, 1), (TM3, 0) etc. Using this encoding the problem becomes trivial. It’s all other encodings which are unwieldy, complex and inconvenient.
    - consilient 3y ago
      That's no longer the halting problem: formally, the input to a halting oracle is an index for some fixed choice of admissible numbering of the set of Turing machines, meaning one that can be computed from the standard numbering induced by some universal Turing machine. Your encoding is not admissible.
      - ukj 3y ago
        >That's no longer the halting problem Just your luck. Under Univalence identity is equivalent to equivalence and it's computationally decidable. So you should be able to produce a decider which determines whether any alternative encoding/representation is equivalent to the halting problem; or not. Formally speaking Turing machines are formal language recognizers, so in which formal language is the formal statement of the Halting problem expressed in? I'd also like to see the decider for "admissible" vs "inadmissible" encodings. Input validation is an Interesting problem-domain for sure. (Of course, this is all for the sake of maximum pedantry)
        consilient 3y ago
        > Just your luck. Under Univalence identity is equivalent to equivalence and it's computationally decidable. So you should be able to produce a decider which determines whether any alternative encoding/representation is equivalent to the halting problem; or not. Moving to a constructive setting lets you say things like "all functions are computable" because it has a restricted notion of function. It does not give you any new information about classical objects.
- mistermann 3y ago
  > Be careful with things like "faithfully reflect reality". :-) Let's be careful with our terms! There is the universe, and then there's reality. They are not the same thing, they only seem that way because that is the model everyone's been raised on, and that "fact" is reinforced and defended daily.

by cvoss 3y ago

mcguire 3y ago

Be careful with things like "faithfully reflect reality". :-) Euclidean geometry is intuitively good and seems to work on relatively small areas of the Earth's surface, but non-Euclidean geometries are inconsistent with it and more faithfully reflect a reality that lacks infinite flat planes.

mcphage 3y ago
Or even Newtonian Physics, which faithfully reflects reality—as long as you're not too large, or you're not traveling too fast. And then it starts to break down.
commonlisp94 3y ago
This is not true. They are incompatible sets of axioms, but they can describe the same set of shapes, although one system is going to be a lot more inconvenient than the other. The differences are logically interesting, but about as incompatible as choosing to make the origin of a euclidean system one corner of the room instead of another. In contrast physical theories contradict each other by making different predictions which can be falsified.
- ukj 3y ago
  At that level of pedantry even the halting problem is solvable. Just choose a suitable representation for the Turing machines in question. Describe/represent the ones that halt using 1; and the ones that don’t halt using 0. This produces the pairs (TM1, 1), (TM2, 1), (TM3, 0) etc. Using this encoding the problem becomes trivial. It’s all other encodings which are unwieldy, complex and inconvenient.
  - consilient 3y ago
    That's no longer the halting problem: formally, the input to a halting oracle is an index for some fixed choice of admissible numbering of the set of Turing machines, meaning one that can be computed from the standard numbering induced by some universal Turing machine. Your encoding is not admissible.
    - ukj 3y ago
      >That's no longer the halting problem Just your luck. Under Univalence identity is equivalent to equivalence and it's computationally decidable. So you should be able to produce a decider which determines whether any alternative encoding/representation is equivalent to the halting problem; or not. Formally speaking Turing machines are formal language recognizers, so in which formal language is the formal statement of the Halting problem expressed in? I'd also like to see the decider for "admissible" vs "inadmissible" encodings. Input validation is an Interesting problem-domain for sure. (Of course, this is all for the sake of maximum pedantry)
      - consilient 3y ago
        > Just your luck. Under Univalence identity is equivalent to equivalence and it's computationally decidable. So you should be able to produce a decider which determines whether any alternative encoding/representation is equivalent to the halting problem; or not. Moving to a constructive setting lets you say things like "all functions are computable" because it has a restricted notion of function. It does not give you any new information about classical objects.
mistermann 3y ago
> Be careful with things like "faithfully reflect reality". :-) Let's be careful with our terms! There is the universe, and then there's reality. They are not the same thing, they only seem that way because that is the model everyone's been raised on, and that "fact" is reinforced and defended daily.