4 ms·

The trope of self-referential paradoxes as the foundation for grander proofs has always bugged me. My gut always says "sure, but what if we just banned self-ref

The trope of self-referential paradoxes as the foundation for grander proofs has always bugged me. My gut always says "sure, but what if we just banned self-referential paradoxes?"

deleted 7y ago
[deleted]
andrewflnr 7y ago
I think those are called type theories. IIRC that was at least the idea behind the original type theories, before they got co-opted by the CS rabble. :)
- dllthomas 7y ago
  Right, IIUC type theory started as Bertrand Russell's attempt to do exactly that (and follow through the ramifications - you can't "just" anything in math). Then suddenly, Haskell. Or something.
  - nl 7y ago
    Then suddenly, Haskell. Sequence of events: Russell publishes Principia Mathematica (1910-1913) David Hilbert studies Principia Mathematica, and keeps working on open questions from it (1913 onwards): He poses the proof of the consistency of arithmetic (and of set theory) again as the main open problems. In both these cases, there seems to be nothing more fundamental available to which the consistency could be reduced other than logic itself. And Hilbert then thought that the problem had essentially been solved by Russell’s work in Principia. Nevertheless, other fundamental problems of axiomatics remained unsolved, including the problem of the “decidability of every mathematical question,” which also traces back to Hilbert’s 1900 address. These unresolved problems of axiomatics led Hilbert to devote significant effort to work on logic in the following years. In 1917, Paul Bernays joined him as his assistant in Göttingen. In a series of courses from 1917–1921, Hilbert, with the assistance of Bernays and Behmann, made significant new contributions to formal logic.[1] In 1928 Haskell Curry moved to Germany to study under David Hilbert Curry's work developed into the Curry–Howard correspondence[2] which led to the language being named after him. [1] https://plato.stanford.edu/entries/hilbert-program/#1.2 https://plato.stanford.edu/entries/hilbert-program/#1.2 [2] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Origin,_scope,_and_consequences https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- nl 7y ago
  the original type theories, before they got co-opted by the CS rabble. They are the same type theory! I realize you are at least partially joking, but it's worth noting. Lambda calculus[0] came out of Church's studies[1] in the Foundations of Mathematics - the same field Russell was working on with his Logicism approach. Haskell Curry co-discovered the Curry–Howard correspondence which shows the direct relationship between computer programs and mathematical proofs. Russell himself developed the idea of Type Hierarchy[2] [0]https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus [1] https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory [2] https://en.wikipedia.org/wiki/Logicism#A_solution_to_impredicativity:_a_hierarchy_of_types https://en.wikipedia.org/wiki/Logicism#A_solution_to_impredi...
samatman 7y ago
Well, and that is the essence of Gödel's first theorem: you can't, any sufficiently powerful system can generate an infinite number of them. Options include not letting this bother you (my favourite) and just ignoring it and hoping it doesn't come up, as indeed, it often doesn't.
- strbean 7y ago
  Well, yah, an infinite number of them exist. I'm curious, though, how many of these principles a la the Halting Problem actually hold if they are excluded? We take as doctrine that the halting problem is generally undecidable, but I haven't heard anything about any results for the Halting Problem (minus self referential paradoxes). Which is concerning because in practice nobody gives a crap about self referential paradoxes and they very rarely actually arise.
  - zajio1am 7y ago
    There is Rice's theorem (which is simple extension of Halting Problem and a basic theorem in computability theory), which states that all non-trivial, purely semantic properties of programs are undecidable. For more details, see https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem .
    - strbean 7y ago
      Interesting, but... The Wikipedia article gives 2 proofs for Rice's theorem. a) As a corollary of Kleene's recursion theorem. This proof seems to rely on quines, and therefore relies on the same principle of self-referential paradox? b) As a proof by reduction to the halting problem. I'm not very confident in my interpretation of (a) ...
nwallin 7y ago
That's not a thing. The problem isn't self referential statements. The problem is much larger, and self referential statements are the easiest way to construct a counterexample. Self referential statements are a symptom, not a cause. Trying to construct a mathematical system of axioms is like trying to construct the most powerful system of computation possible that isn't subject to the halting problem. You want to prove stuff, so you want a powerful system. Eventually, you end up with a system of axioms that is so powerful it can prove contradictory results, or you end up with a language where you cannot prove it halts or does not halt. You want to not be able to prove untrue true, and you want true things to be unable to be proven false, so you weaken your tools. Either you fail to weaken your tools enough, or you eventually end up unable to prove true statements are true. In programming, the fact that it's unprovable that a program halts isn't actually a big deal. Most of the normal problems we deal with don't need algorithms which probe the boundaries of halting, and QA picks up the stuff we miss. (usually, and if not, it's the customer's problem, not mine) That doesn't work in math. In math, if you want to publish a paper that proves x, you want to be sure that nobody's going to publish a paper proving !x anytime soon. So you need a restricted language, unlike programmers. It turns out banning self referential statements makes it really, really hard to prove stuff.
- strbean 7y ago
  > The problem is much larger, and self referential statements are the easiest way to construct a counterexample. Self referential statements are a symptom, not a cause. I'm curious, though, if things like the halting problem actually hold in the absence of (certain types of) self-referential statements. To my (very limited) knowledge, all proofs in these areas rely on them. > Most of the normal problems we deal with don't need algorithms which probe the boundaries of halting, and QA picks up the stuff we miss. But QA gets a bunch of excuses derived from the halting problem! For example: > Boss: We have A which works, and we wrote B that is much faster, make sure they are functionally identical. > QA: I can write a lot of tests, run fuzzers, but actually proving that A == B is undecidable! Also, partially as a consequence of the halting problem, running untrusted code in a sandbox inherently means setting hard timeouts. > It turns out banning self referential statements makes it really, really hard to prove stuff. I'm not advocating for stripping out reflection from whatever system. Just saying (based on dumb gut feelings) that maybe we've stopped short of valuable results on things like "The halting problem (ignoring that one gotcha)".

The trope of self-referential paradoxes as the foundation for grander proofs has always bugged me. My gut always says "sure, but what if we just banned self-referential paradoxes?"

deleted 7y ago

[deleted]

andrewflnr 7y ago

I think those are called type theories. IIRC that was at least the idea behind the original type theories, before they got co-opted by the CS rabble. :)

dllthomas 7y ago
Right, IIUC type theory started as Bertrand Russell's attempt to do exactly that (and follow through the ramifications - you can't "just" anything in math). Then suddenly, Haskell. Or something.
- nl 7y ago
  Then suddenly, Haskell. Sequence of events: Russell publishes Principia Mathematica (1910-1913) David Hilbert studies Principia Mathematica, and keeps working on open questions from it (1913 onwards): He poses the proof of the consistency of arithmetic (and of set theory) again as the main open problems. In both these cases, there seems to be nothing more fundamental available to which the consistency could be reduced other than logic itself. And Hilbert then thought that the problem had essentially been solved by Russell’s work in Principia. Nevertheless, other fundamental problems of axiomatics remained unsolved, including the problem of the “decidability of every mathematical question,” which also traces back to Hilbert’s 1900 address. These unresolved problems of axiomatics led Hilbert to devote significant effort to work on logic in the following years. In 1917, Paul Bernays joined him as his assistant in Göttingen. In a series of courses from 1917–1921, Hilbert, with the assistance of Bernays and Behmann, made significant new contributions to formal logic.[1] In 1928 Haskell Curry moved to Germany to study under David Hilbert Curry's work developed into the Curry–Howard correspondence[2] which led to the language being named after him. [1] https://plato.stanford.edu/entries/hilbert-program/#1.2 https://plato.stanford.edu/entries/hilbert-program/#1.2 [2] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence#Origin,_scope,_and_consequences https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
nl 7y ago
the original type theories, before they got co-opted by the CS rabble. They are the same type theory! I realize you are at least partially joking, but it's worth noting. Lambda calculus[0] came out of Church's studies[1] in the Foundations of Mathematics - the same field Russell was working on with his Logicism approach. Haskell Curry co-discovered the Curry–Howard correspondence which shows the direct relationship between computer programs and mathematical proofs. Russell himself developed the idea of Type Hierarchy[2] [0]https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus [1] https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory [2] https://en.wikipedia.org/wiki/Logicism#A_solution_to_impredicativity:_a_hierarchy_of_types https://en.wikipedia.org/wiki/Logicism#A_solution_to_impredi...

samatman 7y ago

Well, and that is the essence of Gödel's first theorem: you can't, any sufficiently powerful system can generate an infinite number of them. Options include not letting this bother you (my favourite) and just ignoring it and hoping it doesn't come up, as indeed, it often doesn't.

strbean 7y ago
Well, yah, an infinite number of them exist. I'm curious, though, how many of these principles a la the Halting Problem actually hold if they are excluded? We take as doctrine that the halting problem is generally undecidable, but I haven't heard anything about any results for the Halting Problem (minus self referential paradoxes). Which is concerning because in practice nobody gives a crap about self referential paradoxes and they very rarely actually arise.
- zajio1am 7y ago
  There is Rice's theorem (which is simple extension of Halting Problem and a basic theorem in computability theory), which states that all non-trivial, purely semantic properties of programs are undecidable. For more details, see https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem .
  - strbean 7y ago
    Interesting, but... The Wikipedia article gives 2 proofs for Rice's theorem. a) As a corollary of Kleene's recursion theorem. This proof seems to rely on quines, and therefore relies on the same principle of self-referential paradox? b) As a proof by reduction to the halting problem. I'm not very confident in my interpretation of (a) ...

nwallin 7y ago

That's not a thing. The problem isn't self referential statements. The problem is much larger, and self referential statements are the easiest way to construct a counterexample. Self referential statements are a symptom, not a cause. Trying to construct a mathematical system of axioms is like trying to construct the most powerful system of computation possible that isn't subject to the halting problem. You want to prove stuff, so you want a powerful system. Eventually, you end up with a system of axioms that is so powerful it can prove contradictory results, or you end up with a language where you cannot prove it halts or does not halt. You want to not be able to prove untrue true, and you want true things to be unable to be proven false, so you weaken your tools. Either you fail to weaken your tools enough, or you eventually end up unable to prove true statements are true. In programming, the fact that it's unprovable that a program halts isn't actually a big deal. Most of the normal problems we deal with don't need algorithms which probe the boundaries of halting, and QA picks up the stuff we miss. (usually, and if not, it's the customer's problem, not mine) That doesn't work in math. In math, if you want to publish a paper that proves x, you want to be sure that nobody's going to publish a paper proving !x anytime soon. So you need a restricted language, unlike programmers. It turns out banning self referential statements makes it really, really hard to prove stuff.

strbean 7y ago
> The problem is much larger, and self referential statements are the easiest way to construct a counterexample. Self referential statements are a symptom, not a cause. I'm curious, though, if things like the halting problem actually hold in the absence of (certain types of) self-referential statements. To my (very limited) knowledge, all proofs in these areas rely on them. > Most of the normal problems we deal with don't need algorithms which probe the boundaries of halting, and QA picks up the stuff we miss. But QA gets a bunch of excuses derived from the halting problem! For example: > Boss: We have A which works, and we wrote B that is much faster, make sure they are functionally identical. > QA: I can write a lot of tests, run fuzzers, but actually proving that A == B is undecidable! Also, partially as a consequence of the halting problem, running untrusted code in a sandbox inherently means setting hard timeouts. > It turns out banning self referential statements makes it really, really hard to prove stuff. I'm not advocating for stripping out reflection from whatever system. Just saying (based on dumb gut feelings) that maybe we've stopped short of valuable results on things like "The halting problem (ignoring that one gotcha)".