29 ms·

Where do type systems come from? (2017)

201 points by signa11 5y ago

yuchi 5y ago
Awesome read! But throwing the Gödel incompleteness theorem at your face at the end of the article without any specific explanation is rude! Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs!
- reuben364 5y ago
 Not qualified to answer, but my thought is that if you have a statement that is true that cannot be proven, you could write a program whose correctness implies the statement, then proving the program correct amounts to proving something that can not be proven.
- ashton314 5y ago
 Here's a small attempted answer: Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Even some programs that may converge have no type. The Y Combinator, for instance, has no type because it would require an infinite type. From the Wikipedia article under "General Observations": Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value, i.e., a λ abstraction. This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = (λx.x x) (λx.x x) . Recursion can be added to the language by either having a special operator fixₐ of type (α → α) → α or adding general recursive types, though both eliminate strong normalization. Since it is strongly normalising, it is decidable whether or not a simply typed lambda calculus program halts: in fact, it always halts. We can therefore conclude that the language is not Turing complete. Another way to look at it is this via the Curry-Howard correspondence [^2]: for any mathematical proof, you can write down a program that is equivalent to that proof. Verifying the proof's result is the same as running the program. This is a very exciting correspondence that runs deep throughout computer science and mathematics. (I highly recommend the Software Foundations course I linked to below.) Writing a non-terminating program is like writing one of these self-contradictory logic statements: it has no proof of truth or falsehood. Thus, the fact that we can write programs to which we can assign some kind of type but that never terminate is a way of demonstrating the fact that there are theorems that are well-formed but have no truth assignment to them. (Gödel's Incompleteness Theorem) [^1]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; see also https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html https://softwarefoundations.cis.upenn.edu/current/plf-curren... [^2]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
 - reuben364 5y ago
 I'm struggling to fit this into my current understanding. I guess I don't really know how incompleteness looks in a type theory setting. Terms are proofs, types are propositions. _ are theories, _ are models, _ are valid formulas?
 - barrenko 5y ago
 Can I ask in a very "noob" way - are types and theory underneath something that runs in parallel to Turing machine and they together enable modern computing OR is Turing completeness and Turing machine stuff also part of type / lambda calculus theory? Thanks.
 - reuben364 5y ago
 Semantics of programs in type theory are most of the time described by a small step relation which describes, possibly non-deterministically, how to perform one step of computation. Separately one can consider which terms are values, indicating a successful, terminating computation. Type theory would then involve proving properties about the semantics of typed programs. One can give a small step relation for a Turing machine and one could possibly come up for a type system for it, but generally one starts with the semantics for untyped lambda calculus. Some of the more advanced type theory stuff unifies the notions of terms and types, meaning arbitrary computations can happen in type checking and so properties about types can involve properties about computation in general.
 - the_french 5y ago
 > Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Nitpick, because those programs have no type they are not members of the Simply Typed Lambda Calculus but only of the underlying untyped calculus
 - ashton314 5y ago
 You’re right. My bad. Thanks!
- didibus 5y ago
 > Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs I think the article has this a little wrong. The theorem in programming terms I think simply means that there are some programs for which another program can't prove certain properties. But in theory you can restrict yourself to writing programs that can be proven completely. Even then though, you won't eliminate all bugs, and I think that's the part the article gets wrong. Type system don't prevent bugs, they help you prove properties, but the programmer still needs to come up with all properties and edge cases themselves and set things up for the type system to prove those, and there's a lot of opportunity for the programmer to forget about a lot of properties or to have a bug in how they're trying to prove it. Finally, there are only so much you can prove in a general way, in that there are only so many properties you can try to prove. Just think about it, you can't go listing all possible inputs and asserting all possible outputs because as a programmer that would take way too long. So you try to come up with shortcuts, which will be properties, maybe you say alright so for even inputs I'd expect even outputs. Now maybe you use a type system to prove that. But you can still see how you've not proven that it returns the right output for every single input, just the property that even should return even. And that still leaves gaps for bugs. But none of those have anything to do with Godel's incompleteness theorem, those exist even if you restrict yourself to programming only in a language for which type systems can fully operate in. Disclaimer: I'm no expert in this though.
 - barrenko 5y ago
 Is this in a way related to something called "property-based testing"?
 - formerly_proven 5y ago
 Property-based testing is not proof-based, but stochastic; you define the input space for a property fairly well, then the testing framework samples random points within that space. They also generally have reducers, which try to create small failing inputs iteratively after finding one failing input. The difference with fuzzing is mostly that fuzzers are largely black box; the input space is left largely undefined (e.g. AFL: bag of bytes), and the property under test is usually "well, uh, does it explode?". I don't think the popular property-based testing frameworks use instrumentation to guide exploration of the input space.
- shikoba 5y ago
 >Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs! You'll never understand because it's false. Godel theroem proves that theorems aren't enumerable. But they're still computably enumerable.
 - reuben364 5y ago
 A more degenerate argument: a type system that rejects all programs will prevent all bugs.
 - Koshkin 5y ago
 I have seen programmers 1) design a type hierarchy; 2) struggle getting things compiled; 3) give up.
 - ProfHewitt 5y ago
 Theorems of a foundational system are not computationally enumerable (in fact they are not even countable). See the following article: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 In a foundational system, there are true propositions that cannot be proved. For example, is true but unprovable that an algorithm can enumerate the theorems of an order abstracted from strings.
 - shikoba 5y ago
 >there are true propositions that cannot be proved In that case, they're not theorems. Theorem are things that can be proved starting from axioms. And proofs are enumerable, except if the axioms are not enumerable.
- tel 5y ago
 It’s kind of a long range gesture. Normally, a judgement e: B can only capture some truths about the program e, but if B could encode arbitrary logical statements about e, what does the system look like? It turns out that if you have that system in code written as s and then try to assert certain properties of it G, then it’s possible to design G such that s: G is so twisty and self-referential that it can’t be verified. Something to that effect: strong logics have a tough time speaking completely about themselves. So that’s at least one property for one program that’s unprovable no matter how powerful our type system is. But that’s so long range. Practically we can make type systems that let us prove massive amounts of things using judgements like e: B. The real issue is that it’s just very hard and expensive to make those systems practically eliminate even a small subset of bugs.
- jerf 5y ago
 It's simple. A type system can be complicated to itself do computations. See dependent types, for instance. Once you open that up you have the full range of complications for computing itself in your type system. There are type systems sufficiently complicated to declare "the type of Turing Machines that halt in a finite amount of time" as a type; this causes obvious problems. It is a well-known phenomenon that it can take surprisingly little to turn a computation system Turing complete; witness, for instance, C++'s accidentally-Turing-complete templates. So it can wiggle in without you even realizing it at design time. Or, if you're using a type system with sufficient power like dependent types, it is surprisingly easy to put together four or five recursive types that, on their own, are all perfectly computable, but together turn out to create something that is Turing complete. Write a program with a few hundred of these and Turing completeness is almost bound to sneak in somewhere. See https://www.gwern.net/Turing-complete https://www.gwern.net/Turing-complete , and ponder applications to just-slightly-too-powerful type theories. Or https://github.com/Microsoft/TypeScript/issues/14833 https://github.com/Microsoft/TypeScript/issues/14833 .
- ProfHewitt 5y ago
 [Gödel 1931] proposed the proposition I’mUnprovable (such that I’mUnprovable ⇔⊬I’mUnprovable) for proving inferential undecidability of Russel’s foundational theory, which had the type-restriction on orders of propositions to prevent inconsistencies. I’mUnprovable cannot be constructed in foundational theories because strong types prevent construction of I’mUnprovable using the following recursive definition (see Diagonal Lemma [Gödel 1931]): I’mUnprovable:Proposition≡⊬I’mUnprovable. Note that (⊬I’mUnprovable):Proposition<i+1> in the right-hand side of the definition because I’mUnprovable:Proposition is a propositional variable in the definition ⊬I’mUnprovable. Consequently, I’mUnprovable:Proposition⇒I’mUnprovable:Proposition<i+1>, which is a contradiction.
tel 5y ago
Russell's Hierarchy of Types isn't particularly where type theories came from, though it was an early reference to the word and obviously very adjacent to these developments. It is a type system employed to solve a particular problem, though. Types have existed for a long time as mechanisms to provide classification and structure to formal (and even informal) languages. Even just before Russell, Frege (and many of his contemporaries) made a huge deal of the fine distinctions in type between propositions, expressions of truth, proofs, and their ilk. What really made type theories blow up was the recognition that they corresponded with these very things: propositions, judgements, proofs. Mathematicians developed type theories as follow-on to Russell's (and others) work because they wanted to better describe what kinds of things counted as valid propositions and what kinds of corresponding proofs were formally admissible. They also were critically tied to conversations of syntax and semantics where mathematicians asked hard questions about why funny symbols on pages ought to have any sort of force of knowledge whatsoever. So what made types rich was a recognition of the richness in the structure of first- and higher-order logics. The recognition that the power of the semi-formal language of proofs employed by working mathematicians required sophisticated study in order to describe and formalize. And that doing so required a distinction between the object of mathematical work, the proof, and the intent or semantics, the judgement. Early PL type systems seem to have been convergent evolution. Here we were as computer scientists making and operating new formal languages and needing to describe certain properties of the syntax (but really: its ultimate semantic weight as it is operated by a machine) so that we could, e.g., make sure we used properly sized registers. Only as more sophisticated programming languages were developed that desired to simply the supposed programmer's task of working with abstraction did PL designers begin to converge toward, steal, and ultimately influence these languages of logic. The convergence, in my opinion, occurred because there truly are significant similarities in the kinds of mental processes accomplished by logicians and by programmers. So where do type systems come from, really? I think the good ones represent natural, parsimonious structuring of logic. We land on compositional systems because they're easy to reason about inductively. We land on sums and products because of archetypes from boolean logic, our belief about the "cheapness" of copying knowledge, and because of the natural urge to package together and make choices. We land on modules/quantifiers due to the value of abstraction in compartmentalizing and reusing ideas. We can relax and challenge some of these assumptions to come up with new sorts of logic (and many PL designers and logicians make their bread in this way). We can also imagine totally different approaches to logic (like: state machine transition matrices) which are more challenging for us to work with using human minds or communicate to others using human speech. In this way, our type theories and logics are tailored to how humans most comfortably perceive the world.
kongin 5y ago
The type theory Russell invented has little to do with type theory as used in programming languages other than the name. You could make a strong case that grammar as a type theory for human languages was an even earlier example of using types, but it's one that's just as meaningless to us. The early history of type theory for programming languages comes from research into lambda calculus: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
- jweir 5y ago
  In Church’s “A Formulation of the Simple Theory of Types” he says he is heavily indebted to Russell.
  - Ericson2314 5y ago
    After that, it really gets going with Girard's System F and Martin Loef type thoery.
deleted 5y ago
[deleted]
peter_retief 5y ago
I really enjoyed Bertrand Russell's "A History of Western Philosophy" but never realized how prolific he was in mathemetics and that he wrote "Mathematical Logic as Based on the Theory of Types" I imagine it is a harder read but probably worth adding to my growing stack of books waiting to get read.
- coldacid 5y ago
  Russell was one of the last great polymaths.
lisper 5y ago
It never ceases to amaze me how theorists can take simple concepts and make them impenetrable. A type is a (possibly infinite) subset of all the possible values that can be provided as input to a program, or all the possible results a program can produce. Type theory is about trying to figure out at compile time, if the inputs to a function are of a certain type (i.e. belong to a certain subset) what type the output will be (i.e. what subset of possible values the output will belong to). It is not possible to figure this out in general because that would require solving the halting problem, so the art of designing type systems is choosing subsets of the data that allow you to prove useful things about programs at compile time so that you can find errors before the program runs, and eliminate run-time checks and hence make the programs run faster. The reason people who like dynamically typed languages get frustrated with statically typed languages is that they value development speed more than they value run-time speed or avoiding of run-time errors, so they don't want to put in the extra effort needed to provide the compiler with the information it needs to do these compile-time derivations, or put up with the compiler complaining when it is unable to do them. They just want the program to run, and they're willing to pay for that with some inefficiency and run-time errors. That's pretty much it.
- cjfd 5y ago
  Well, the article does not actually answer 'where do type systems come from?' (as in the type systems of programming languages) but 'where do type theories come from?' (as in the foundations of mathematics). I think type systems would have been invented for programming languages even if the mathematicians had never bothered with type theory, simply because they are necessary. I mean treating an integer stored in memory as a string or vice versa is still not going to work no matter what foundations for mathematics one likes...
  - setr 5y ago
    JS would like to have a word with you.
    - cjfd 5y ago
      Yes, but would I like to have a word with JS? I am quite certain the answer is 'no'..... On a more serious note: JS is in the background also keeping track of types, obviously.
lewisjoe 5y ago
I wrote on this topic, trying to simplify where types came from and why it's important - https://docs.google.com/document/d/1-aLUwnN0XzLbzICnFLWfCLuD4ULYXGcKAoyRAqTuAIY/edit#heading=h.bxiqdlerl36p https://docs.google.com/document/d/1-aLUwnN0XzLbzICnFLWfCLuD... Related HN discussion: https://news.ycombinator.com/item?id=21898309 https://news.ycombinator.com/item?id=21898309
pyrale 5y ago
People interested in this topic might also enjoy this video by Philip Wadler describing the way logicians and computer scientists converged towards equivalent ideas. https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU
- vishnugupta 5y ago
  This is a fantastic talk. I've watched a couple of different versions of this. Towards the end he spoke about something in passing that's stayed with me. Through out early/mid 20th century different mathematicians created their own theories of mechanised computation. Turing machine, Lambda calculus, SK combinators etc., However over they all turned out to be equivalent; for example Church-Turing thesis. So this leads one to believe strongly that mechanised computation is "discovered" rather than invented. Also it is a good indication that the computing theory is on a solid foundation. However, when it comes to distributed and parallel computing theories have been proposed but no equivalence has been found (or at least proved). It's an active field which he hopes will result in a similarly solid foundation for the distributed computing. At the moment it seems to be on a shaky ground.
  - zozbot234 5y ago
    > However, when it comes to distributed and parallel computing theories have been proposed but no equivalence has been found Is this really the case? It seems that game semantics ought to be able to model these concerns. The logical side of it would then be some sort of multi-modal logic.
  - kenjackson 5y ago
    What is a distributed or parallel computing theory in this context? They can’t compute anything above and beyond sequential computers.
  - felixyz 5y ago
    This three-part series of (long) posts is a very thorough and fascinating counterpoint to the idea that computation was discovered and that there is anything surprising about the confluence of lambda calculus, Turing machines etc, mostly using primary sources from Leibniz onwards: "Finite of Sense and Infinite of Thought: A History of Computation, Logic and Algebra" https://pron.github.io/posts/computation-logic-algebra-pt1 https://pron.github.io/posts/computation-logic-algebra-pt1
deleted 5y ago
[deleted]
bjornsing 5y ago
> Similarly, type theory wasn’t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic. It wasn’t enough because this goal in its full extent is unattainable. This is an often repeated claim, but I can’t shake the feeling that it’s an incorrectly drawn conclusion (of Gödel’s incompleteness theorems). My understanding: It’s true that there are such “mathematical truths without proofs within axiomatic system X”, but they are unreachable by mathematicians and symbolic logic / machines alike. If a mathematical statement has no proof within ZFC we (usually) don’t call it a “truth”, regardless of if it is true or not. Please correct me if I’m wrong.
- simias 5y ago
  >If a mathematical statement has no proof within ZFC we (usually) don’t call it a “truth”, regardless of if it is true or not. I'm not sure I understand what this changes to the overall situation. Remember that a formal system also can't prove its own consistency, so you can't just ignore bits that you don't like and expect that it doesn't matter, it's possible that one of these "true but unprovable" propositions would actually render your system inconsistent, in which case it ought to be addressed. I mean in the end Godel's own proof effectively relies on this: he builds a proposition using the rule of the system saying "this proposition has no proof" and at this point you either have to accept that the proposition is incorrect, but then your system is inconsistent (it can be used to derive falsehoods) or that it is correct but then the system is incomplete. So you may decide not to call it a truth but you also can't really call it a falsehood. I would also wager that mathematicians generally prefer incomplete to inconsistent systems, if which case you have to accept that these unprovable propositions are indeed truths. It's like the "does the set of all sets not containing themselves contain itself" paradox, you can't just ignore it as irrelevant because it puts into question your entire formal system.
  - Filligree 5y ago
    > I'm not sure I understand what this changes to the overall situation. Remember that a formal system also can't prove its own consistency, so you can't just ignore bits that you don't like and expect that it doesn't matter, it's possible that one of these "true but unprovable" propositions would actually render your system inconsistent, in which case it ought to be addressed. Is that true? It seems to me that if a statement is unprovable, then even if it would in theory render your system inconsistent, there's no way that can actually happen. Since, if you found any example of a chain of logic which leads to an inconsistency, that would count as a proof of the original statement. Which is unprovable, and as such can't have proofs.
cryptica 5y ago
I like Mathematics but I hate the language of Mathematics. Mathematicians chose to sacrifice readability in favor of terseness; they invented a large number of abstractions, often with only tiny differences between them. Also, descriptions of concepts tend to focus on the wrong characteristics... Maths would be far more accessible if mathematicians described everything in plain English and reused abstractions to describe similar concepts instead of inventing entirely new words. It's possible, they just don't want to do this because it wouldn't make them sound as clever. As a developer, I can explain a blockchain as: 1. A decentralized ledger which relies on an asymmetric signature scheme such as EdDSA, zero-knowledge proofs or other mechanism to authenticate on-chain messages. A blockchain network forms either a structured (deterministic) or unstructured (stochastic) P2P mesh, ideally with each node having a partial view and propagating messages through the network via a gossip protocol. Blockchain nodes adhere to a consensus mechanism such as PoW or PoS (or variants) to provide byzantine fault tolerance and resilience to forks given certain finality conditions. Or: 2. A ledger which is replicated across multiple nodes/computers which are connected together. The blockchain is usually a ledger of accounts involving financial transactions. The authenticity of each transaction can be independently verified by anyone by checking that a digital signature on any transaction corresponds to the account which claims to have sent the transaction - This is possible because each account is associated with a 'public key' which anyone can see and which can be used to verify that a signature was generated by the sender since only the sender could have known the 'private key' (secret) which was used to generate this specific signature given this specific transaction and this specific public key.
- tel 5y ago
  Mathematical papers are essentially mathematicians shipping pseudo code back and forth. There are good reasons for it, but it’s not meant for most audiences. Mathematicians absolutely do write accessibly from time to time, but when they do so you have to be fortunate enough to be in the audience. Often these are aimed at only the most general of audiences and thus are pretty sparse in detail.
- Jtsummers 5y ago
  > Maths would be far more accessible if mathematicians described everything in plain English Are you sure about that? Take Kepler's Laws of Planetary Motion as an explanation of orbital mechanics and try and do anything with just these plaintext definitions (courtesy of Wikipedia): The three laws state that: 1. The orbit of a planet is an ellipse with the Sun at one of the two foci. 2. A line segment joining a planet and the Sun sweeps out equal areas during equal intervals of time. 3. The square of a planet's orbital period is proportional to the cube of the length of the semi-major axis of its orbit. Now try and apply this without ever falling into mathematical notations. And translate this into every language under the Sun unless you really want it to only be comprehensible to English readers. Or take this formula, converted into plain English: The distance of a planet from the sun is proportional to the semi-latus rectum and one more than the product of the eccentricity of the orbit and the cosine of the angle between the planet's current position and its nearest approach. To help out since at least one term in there may be unfamiliar to most readers (courtesy of Wikipedia): The latus rectum is the chord parallel to the directrix and passing through a focus; its half-length is the semi-latus rectum (ℓ). Now, take that and suppose we have the distance from the sun and all the other values, but not the angle, rephrase that abomination so that we can solve for the angle. Without using mathematical notation. The only good thing about dropping mathematical notation is that we'd be able to slow down technological process substantially as we wouldn't even be able to get to orbit anymore. That idea of "solve for θ" is "just" a basic application of algebra. An act that would become impossible to do with any kind of reasonable efficiency and confidence about correctness without something like our current mathematical notation, and plain English (very anglocentric, guess we don't want anyone outside the anglosphere to participate) would be a poor alternate.
nathias 5y ago
It was actually Frege that developed types as a solution to Russell's paradox.
cb321 5y ago
If by "type systems/checking" one refers to constraints on "valid operations in context" like comparisons, subtractions, additions (or maybe in a prog.lang context assignment to lexically static identifiers) then physical units of measure (seconds, meters|its ancient cousins, etc.) were the first type system. I.e., one cannot add/compare/etc. meters & seconds without conversion and not all conversions are possible. This remains the first such system most people learn in elementary school. Historically such ideas arose along with measurements themselves and computations upon their results like comparison/subtraction/even taxation. Yes, this is all (typically) manually checked and explicit metadata symbols are carried through calculations. I still think it's the primordial example that few mention in discussions like these.
- tel 5y ago
  Yeah, saying Russell invented types is fun but horribly wrong. He invented other things and stood at the center of an explosion in formal logics. But types are way old.
  - JoBrad 5y ago
    Maybe he invented it the way that many people think the color blue was invented? Causing everyone to see something for the first time (especially when it was right under our noses) is certainly impressive.
    - EarthLaunch 5y ago
      In my game design I've imagined two parallels to invention; discovery and identification. All three are learning about the world, but in slightly different ways. Invention: I created that. Discovery: I found that lying around. Identification: I conceptualized a definition for that.
    - tel 5y ago
      This is certainly more true. That explosion of logics I mentioned was a big movement of many authors to expand our understanding of types (among other things).
justshowpost 5y ago
They should stop teaching students stringly-typed scripting languages and all the confusion will magically disappear. Toy language like Pascal would suffice almost any educational faculty if they are afraid what introductory C course is too hard for audience.
golemotron 5y ago
"When a program and a programmer love each other very much..."
hootbootscoot 5y ago
Maybe I'm being terribly naive, but I don't see this from a maths perspective at all, I see this as about the shape of data and about memory allocation. If one increments pointers across an array of data, one should know the stepping size, for example. How is this (programming/practical) side of the word "type systems" related to formal/mathematical "type systems"? I missed that part
- Koshkin 5y ago
  Types are a kind of constraints on what kind of logical constructs in one case, and what kinds of computational constructs in the other, are allowable. Logic and computation are related, but they are not the same. (This difference is also evident in how people think about monads in programming vs. how they are defined and used in category theory.)
deleted 5y ago
[deleted]
chrisbrandow 5y ago
I'm still reeling from the three things I learned in this post: 1. Bertrand Russell studied the "I am lying" paradox, which I always thought was nothing more than a clever meme. 2. Bertrand Russell is responsible for type theory 3. That type theory came out of his study of the paradox.
- __MatrixMan__ 5y ago
 The distinction between countable and uncountable infinities also stems from the liar's paradox.
 - Koshkin 5y ago
 How so? The set of reals is uncountably infinite. Looks like a self-contained fact (that can be proved by a "diagonal argument").
 - kazinator 5y ago
 But diagonalization and self-referential paradoxes are related (in ways that are not necessarily obvious). Think along the lines that you have some sentence Px which asserts that sentence Py is false. Now imagine a table where both the rows and columns are P0, P1, P2, .. populated with these sentences. The diagonal is where you have the self-reference: Pi asserting that Pi is false.
- ProfHewitt 5y ago
 Bertrand Russell introduced orders on propositions to block construction of paradoxes such as “The Liar” [Russell 1908]. Without orders on propositions, the “self-referential” proposition I’mFalse (such that I’mFalse⇔¬I’mFalse) could be constructed using the following recursive definition: I’mFalse:Proposition≡¬I’mFalse. Since Ψ is a propositional variable in the definition, ¬Ψ:Proposition <i+1>. Consequently, I’mFalse:Proposition ⇒I’mFalse:Proposition<i+1>, which is a contradiction. For more information see the following: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 https://www.youtube.com/watch?v=AJP1VL7shiI https://www.youtube.com/watch?v=AJP1VL7shiI

201 points by signa11 5y ago

Awesome read! But throwing the Gödel incompleteness theorem at your face at the end of the article without any specific explanation is rude! Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs!

reuben364 5y ago
Not qualified to answer, but my thought is that if you have a statement that is true that cannot be proven, you could write a program whose correctness implies the statement, then proving the program correct amounts to proving something that can not be proven.
ashton314 5y ago
Here's a small attempted answer: Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Even some programs that may converge have no type. The Y Combinator, for instance, has no type because it would require an infinite type. From the Wikipedia article under "General Observations": Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value, i.e., a λ abstraction. This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term Ω = (λx.x x) (λx.x x) . Recursion can be added to the language by either having a special operator fixₐ of type (α → α) → α or adding general recursive types, though both eliminate strong normalization. Since it is strongly normalising, it is decidable whether or not a simply typed lambda calculus program halts: in fact, it always halts. We can therefore conclude that the language is not Turing complete. Another way to look at it is this via the Curry-Howard correspondence [^2]: for any mathematical proof, you can write down a program that is equivalent to that proof. Verifying the proof's result is the same as running the program. This is a very exciting correspondence that runs deep throughout computer science and mathematics. (I highly recommend the Software Foundations course I linked to below.) Writing a non-terminating program is like writing one of these self-contradictory logic statements: it has no proof of truth or falsehood. Thus, the fact that we can write programs to which we can assign some kind of type but that never terminate is a way of demonstrating the fact that there are theorems that are well-formed but have no truth assignment to them. (Gödel's Incompleteness Theorem) [^1]: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus; see also https://softwarefoundations.cis.upenn.edu/current/plf-current/Stlc.html https://softwarefoundations.cis.upenn.edu/current/plf-curren... [^2]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- reuben364 5y ago
  I'm struggling to fit this into my current understanding. I guess I don't really know how incompleteness looks in a type theory setting. Terms are proofs, types are propositions. _ are theories, _ are models, _ are valid formulas?
- barrenko 5y ago
  Can I ask in a very "noob" way - are types and theory underneath something that runs in parallel to Turing machine and they together enable modern computing OR is Turing completeness and Turing machine stuff also part of type / lambda calculus theory? Thanks.
  - reuben364 5y ago
    Semantics of programs in type theory are most of the time described by a small step relation which describes, possibly non-deterministically, how to perform one step of computation. Separately one can consider which terms are values, indicating a successful, terminating computation. Type theory would then involve proving properties about the semantics of typed programs. One can give a small step relation for a Turing machine and one could possibly come up for a type system for it, but generally one starts with the semantics for untyped lambda calculus. Some of the more advanced type theory stuff unifies the notions of terms and types, meaning arbitrary computations can happen in type checking and so properties about types can involve properties about computation in general.
- the_french 5y ago
  > Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs. Nitpick, because those programs have no type they are not members of the Simply Typed Lambda Calculus but only of the underlying untyped calculus
  - ashton314 5y ago
    You’re right. My bad. Thanks!
didibus 5y ago
> Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs I think the article has this a little wrong. The theorem in programming terms I think simply means that there are some programs for which another program can't prove certain properties. But in theory you can restrict yourself to writing programs that can be proven completely. Even then though, you won't eliminate all bugs, and I think that's the part the article gets wrong. Type system don't prevent bugs, they help you prove properties, but the programmer still needs to come up with all properties and edge cases themselves and set things up for the type system to prove those, and there's a lot of opportunity for the programmer to forget about a lot of properties or to have a bug in how they're trying to prove it. Finally, there are only so much you can prove in a general way, in that there are only so many properties you can try to prove. Just think about it, you can't go listing all possible inputs and asserting all possible outputs because as a programmer that would take way too long. So you try to come up with shortcuts, which will be properties, maybe you say alright so for even inputs I'd expect even outputs. Now maybe you use a type system to prove that. But you can still see how you've not proven that it returns the right output for every single input, just the property that even should return even. And that still leaves gaps for bugs. But none of those have anything to do with Godel's incompleteness theorem, those exist even if you restrict yourself to programming only in a language for which type systems can fully operate in. Disclaimer: I'm no expert in this though.
- barrenko 5y ago
  Is this in a way related to something called "property-based testing"?
  - formerly_proven 5y ago
    Property-based testing is not proof-based, but stochastic; you define the input space for a property fairly well, then the testing framework samples random points within that space. They also generally have reducers, which try to create small failing inputs iteratively after finding one failing input. The difference with fuzzing is mostly that fuzzers are largely black box; the input space is left largely undefined (e.g. AFL: bag of bytes), and the property under test is usually "well, uh, does it explode?". I don't think the popular property-based testing frameworks use instrumentation to guide exploration of the input space.
shikoba 5y ago
>Now I want to understand in a similar fashion why the incompleteness theorem makes type systems incapable of preventing all bugs! You'll never understand because it's false. Godel theroem proves that theorems aren't enumerable. But they're still computably enumerable.
- reuben364 5y ago
  A more degenerate argument: a type system that rejects all programs will prevent all bugs.
  - Koshkin 5y ago
    I have seen programmers 1) design a type hierarchy; 2) struggle getting things compiled; 3) give up.
- ProfHewitt 5y ago
  Theorems of a foundational system are not computationally enumerable (in fact they are not even countable). See the following article: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 In a foundational system, there are true propositions that cannot be proved. For example, is true but unprovable that an algorithm can enumerate the theorems of an order abstracted from strings.
  - shikoba 5y ago
    >there are true propositions that cannot be proved In that case, they're not theorems. Theorem are things that can be proved starting from axioms. And proofs are enumerable, except if the axioms are not enumerable.
tel 5y ago
It’s kind of a long range gesture. Normally, a judgement e: B can only capture some truths about the program e, but if B could encode arbitrary logical statements about e, what does the system look like? It turns out that if you have that system in code written as s and then try to assert certain properties of it G, then it’s possible to design G such that s: G is so twisty and self-referential that it can’t be verified. Something to that effect: strong logics have a tough time speaking completely about themselves. So that’s at least one property for one program that’s unprovable no matter how powerful our type system is. But that’s so long range. Practically we can make type systems that let us prove massive amounts of things using judgements like e: B. The real issue is that it’s just very hard and expensive to make those systems practically eliminate even a small subset of bugs.
jerf 5y ago
It's simple. A type system can be complicated to itself do computations. See dependent types, for instance. Once you open that up you have the full range of complications for computing itself in your type system. There are type systems sufficiently complicated to declare "the type of Turing Machines that halt in a finite amount of time" as a type; this causes obvious problems. It is a well-known phenomenon that it can take surprisingly little to turn a computation system Turing complete; witness, for instance, C++'s accidentally-Turing-complete templates. So it can wiggle in without you even realizing it at design time. Or, if you're using a type system with sufficient power like dependent types, it is surprisingly easy to put together four or five recursive types that, on their own, are all perfectly computable, but together turn out to create something that is Turing complete. Write a program with a few hundred of these and Turing completeness is almost bound to sneak in somewhere. See https://www.gwern.net/Turing-complete https://www.gwern.net/Turing-complete , and ponder applications to just-slightly-too-powerful type theories. Or https://github.com/Microsoft/TypeScript/issues/14833 https://github.com/Microsoft/TypeScript/issues/14833 .
ProfHewitt 5y ago
[Gödel 1931] proposed the proposition I’mUnprovable (such that I’mUnprovable ⇔⊬I’mUnprovable) for proving inferential undecidability of Russel’s foundational theory, which had the type-restriction on orders of propositions to prevent inconsistencies. I’mUnprovable cannot be constructed in foundational theories because strong types prevent construction of I’mUnprovable using the following recursive definition (see Diagonal Lemma [Gödel 1931]): I’mUnprovable:Proposition≡⊬I’mUnprovable. Note that (⊬I’mUnprovable):Proposition<i+1> in the right-hand side of the definition because I’mUnprovable:Proposition is a propositional variable in the definition ⊬I’mUnprovable. Consequently, I’mUnprovable:Proposition⇒I’mUnprovable:Proposition<i+1>, which is a contradiction.

tel 5y ago

Russell's Hierarchy of Types isn't particularly where type theories came from, though it was an early reference to the word and obviously very adjacent to these developments. It is a type system employed to solve a particular problem, though. Types have existed for a long time as mechanisms to provide classification and structure to formal (and even informal) languages. Even just before Russell, Frege (and many of his contemporaries) made a huge deal of the fine distinctions in type between propositions, expressions of truth, proofs, and their ilk. What really made type theories blow up was the recognition that they corresponded with these very things: propositions, judgements, proofs. Mathematicians developed type theories as follow-on to Russell's (and others) work because they wanted to better describe what kinds of things counted as valid propositions and what kinds of corresponding proofs were formally admissible. They also were critically tied to conversations of syntax and semantics where mathematicians asked hard questions about why funny symbols on pages ought to have any sort of force of knowledge whatsoever. So what made types rich was a recognition of the richness in the structure of first- and higher-order logics. The recognition that the power of the semi-formal language of proofs employed by working mathematicians required sophisticated study in order to describe and formalize. And that doing so required a distinction between the object of mathematical work, the proof, and the intent or semantics, the judgement. Early PL type systems seem to have been convergent evolution. Here we were as computer scientists making and operating new formal languages and needing to describe certain properties of the syntax (but really: its ultimate semantic weight as it is operated by a machine) so that we could, e.g., make sure we used properly sized registers. Only as more sophisticated programming languages were developed that desired to simply the supposed programmer's task of working with abstraction did PL designers begin to converge toward, steal, and ultimately influence these languages of logic. The convergence, in my opinion, occurred because there truly are significant similarities in the kinds of mental processes accomplished by logicians and by programmers. So where do type systems come from, really? I think the good ones represent natural, parsimonious structuring of logic. We land on compositional systems because they're easy to reason about inductively. We land on sums and products because of archetypes from boolean logic, our belief about the "cheapness" of copying knowledge, and because of the natural urge to package together and make choices. We land on modules/quantifiers due to the value of abstraction in compartmentalizing and reusing ideas. We can relax and challenge some of these assumptions to come up with new sorts of logic (and many PL designers and logicians make their bread in this way). We can also imagine totally different approaches to logic (like: state machine transition matrices) which are more challenging for us to work with using human minds or communicate to others using human speech. In this way, our type theories and logics are tailored to how humans most comfortably perceive the world.

kongin 5y ago

The type theory Russell invented has little to do with type theory as used in programming languages other than the name. You could make a strong case that grammar as a type theory for human languages was an even earlier example of using types, but it's one that's just as meaningless to us. The early history of type theory for programming languages comes from research into lambda calculus: https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus

jweir 5y ago
In Church’s “A Formulation of the Simple Theory of Types” he says he is heavily indebted to Russell.
- Ericson2314 5y ago
  After that, it really gets going with Girard's System F and Martin Loef type thoery.

deleted 5y ago

[deleted]

peter_retief 5y ago

I really enjoyed Bertrand Russell's "A History of Western Philosophy" but never realized how prolific he was in mathemetics and that he wrote "Mathematical Logic as Based on the Theory of Types" I imagine it is a harder read but probably worth adding to my growing stack of books waiting to get read.

coldacid 5y ago
Russell was one of the last great polymaths.

lisper 5y ago

It never ceases to amaze me how theorists can take simple concepts and make them impenetrable. A type is a (possibly infinite) subset of all the possible values that can be provided as input to a program, or all the possible results a program can produce. Type theory is about trying to figure out at compile time, if the inputs to a function are of a certain type (i.e. belong to a certain subset) what type the output will be (i.e. what subset of possible values the output will belong to). It is not possible to figure this out in general because that would require solving the halting problem, so the art of designing type systems is choosing subsets of the data that allow you to prove useful things about programs at compile time so that you can find errors before the program runs, and eliminate run-time checks and hence make the programs run faster. The reason people who like dynamically typed languages get frustrated with statically typed languages is that they value development speed more than they value run-time speed or avoiding of run-time errors, so they don't want to put in the extra effort needed to provide the compiler with the information it needs to do these compile-time derivations, or put up with the compiler complaining when it is unable to do them. They just want the program to run, and they're willing to pay for that with some inefficiency and run-time errors. That's pretty much it.

cjfd 5y ago
Well, the article does not actually answer 'where do type systems come from?' (as in the type systems of programming languages) but 'where do type theories come from?' (as in the foundations of mathematics). I think type systems would have been invented for programming languages even if the mathematicians had never bothered with type theory, simply because they are necessary. I mean treating an integer stored in memory as a string or vice versa is still not going to work no matter what foundations for mathematics one likes...
- setr 5y ago
  JS would like to have a word with you.
  - cjfd 5y ago
    Yes, but would I like to have a word with JS? I am quite certain the answer is 'no'..... On a more serious note: JS is in the background also keeping track of types, obviously.

lewisjoe 5y ago

I wrote on this topic, trying to simplify where types came from and why it's important - https://docs.google.com/document/d/1-aLUwnN0XzLbzICnFLWfCLuD4ULYXGcKAoyRAqTuAIY/edit#heading=h.bxiqdlerl36p https://docs.google.com/document/d/1-aLUwnN0XzLbzICnFLWfCLuD... Related HN discussion: https://news.ycombinator.com/item?id=21898309 https://news.ycombinator.com/item?id=21898309

pyrale 5y ago

People interested in this topic might also enjoy this video by Philip Wadler describing the way logicians and computer scientists converged towards equivalent ideas. https://www.youtube.com/watch?v=IOiZatlZtGU https://www.youtube.com/watch?v=IOiZatlZtGU

vishnugupta 5y ago
This is a fantastic talk. I've watched a couple of different versions of this. Towards the end he spoke about something in passing that's stayed with me. Through out early/mid 20th century different mathematicians created their own theories of mechanised computation. Turing machine, Lambda calculus, SK combinators etc., However over they all turned out to be equivalent; for example Church-Turing thesis. So this leads one to believe strongly that mechanised computation is "discovered" rather than invented. Also it is a good indication that the computing theory is on a solid foundation. However, when it comes to distributed and parallel computing theories have been proposed but no equivalence has been found (or at least proved). It's an active field which he hopes will result in a similarly solid foundation for the distributed computing. At the moment it seems to be on a shaky ground.
- zozbot234 5y ago
  > However, when it comes to distributed and parallel computing theories have been proposed but no equivalence has been found Is this really the case? It seems that game semantics ought to be able to model these concerns. The logical side of it would then be some sort of multi-modal logic.
- kenjackson 5y ago
  What is a distributed or parallel computing theory in this context? They can’t compute anything above and beyond sequential computers.
- felixyz 5y ago
  This three-part series of (long) posts is a very thorough and fascinating counterpoint to the idea that computation was discovered and that there is anything surprising about the confluence of lambda calculus, Turing machines etc, mostly using primary sources from Leibniz onwards: "Finite of Sense and Infinite of Thought: A History of Computation, Logic and Algebra" https://pron.github.io/posts/computation-logic-algebra-pt1 https://pron.github.io/posts/computation-logic-algebra-pt1

deleted 5y ago

[deleted]

bjornsing 5y ago

> Similarly, type theory wasn’t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic. It wasn’t enough because this goal in its full extent is unattainable. This is an often repeated claim, but I can’t shake the feeling that it’s an incorrectly drawn conclusion (of Gödel’s incompleteness theorems). My understanding: It’s true that there are such “mathematical truths without proofs within axiomatic system X”, but they are unreachable by mathematicians and symbolic logic / machines alike. If a mathematical statement has no proof within ZFC we (usually) don’t call it a “truth”, regardless of if it is true or not. Please correct me if I’m wrong.

simias 5y ago
>If a mathematical statement has no proof within ZFC we (usually) don’t call it a “truth”, regardless of if it is true or not. I'm not sure I understand what this changes to the overall situation. Remember that a formal system also can't prove its own consistency, so you can't just ignore bits that you don't like and expect that it doesn't matter, it's possible that one of these "true but unprovable" propositions would actually render your system inconsistent, in which case it ought to be addressed. I mean in the end Godel's own proof effectively relies on this: he builds a proposition using the rule of the system saying "this proposition has no proof" and at this point you either have to accept that the proposition is incorrect, but then your system is inconsistent (it can be used to derive falsehoods) or that it is correct but then the system is incomplete. So you may decide not to call it a truth but you also can't really call it a falsehood. I would also wager that mathematicians generally prefer incomplete to inconsistent systems, if which case you have to accept that these unprovable propositions are indeed truths. It's like the "does the set of all sets not containing themselves contain itself" paradox, you can't just ignore it as irrelevant because it puts into question your entire formal system.
- Filligree 5y ago
  > I'm not sure I understand what this changes to the overall situation. Remember that a formal system also can't prove its own consistency, so you can't just ignore bits that you don't like and expect that it doesn't matter, it's possible that one of these "true but unprovable" propositions would actually render your system inconsistent, in which case it ought to be addressed. Is that true? It seems to me that if a statement is unprovable, then even if it would in theory render your system inconsistent, there's no way that can actually happen. Since, if you found any example of a chain of logic which leads to an inconsistency, that would count as a proof of the original statement. Which is unprovable, and as such can't have proofs.

cryptica 5y ago

I like Mathematics but I hate the language of Mathematics. Mathematicians chose to sacrifice readability in favor of terseness; they invented a large number of abstractions, often with only tiny differences between them. Also, descriptions of concepts tend to focus on the wrong characteristics... Maths would be far more accessible if mathematicians described everything in plain English and reused abstractions to describe similar concepts instead of inventing entirely new words. It's possible, they just don't want to do this because it wouldn't make them sound as clever. As a developer, I can explain a blockchain as: 1. A decentralized ledger which relies on an asymmetric signature scheme such as EdDSA, zero-knowledge proofs or other mechanism to authenticate on-chain messages. A blockchain network forms either a structured (deterministic) or unstructured (stochastic) P2P mesh, ideally with each node having a partial view and propagating messages through the network via a gossip protocol. Blockchain nodes adhere to a consensus mechanism such as PoW or PoS (or variants) to provide byzantine fault tolerance and resilience to forks given certain finality conditions. Or: 2. A ledger which is replicated across multiple nodes/computers which are connected together. The blockchain is usually a ledger of accounts involving financial transactions. The authenticity of each transaction can be independently verified by anyone by checking that a digital signature on any transaction corresponds to the account which claims to have sent the transaction - This is possible because each account is associated with a 'public key' which anyone can see and which can be used to verify that a signature was generated by the sender since only the sender could have known the 'private key' (secret) which was used to generate this specific signature given this specific transaction and this specific public key.

tel 5y ago
Mathematical papers are essentially mathematicians shipping pseudo code back and forth. There are good reasons for it, but it’s not meant for most audiences. Mathematicians absolutely do write accessibly from time to time, but when they do so you have to be fortunate enough to be in the audience. Often these are aimed at only the most general of audiences and thus are pretty sparse in detail.
Jtsummers 5y ago
> Maths would be far more accessible if mathematicians described everything in plain English Are you sure about that? Take Kepler's Laws of Planetary Motion as an explanation of orbital mechanics and try and do anything with just these plaintext definitions (courtesy of Wikipedia): The three laws state that: 1. The orbit of a planet is an ellipse with the Sun at one of the two foci. 2. A line segment joining a planet and the Sun sweeps out equal areas during equal intervals of time. 3. The square of a planet's orbital period is proportional to the cube of the length of the semi-major axis of its orbit. Now try and apply this without ever falling into mathematical notations. And translate this into every language under the Sun unless you really want it to only be comprehensible to English readers. Or take this formula, converted into plain English: The distance of a planet from the sun is proportional to the semi-latus rectum and one more than the product of the eccentricity of the orbit and the cosine of the angle between the planet's current position and its nearest approach. To help out since at least one term in there may be unfamiliar to most readers (courtesy of Wikipedia): The latus rectum is the chord parallel to the directrix and passing through a focus; its half-length is the semi-latus rectum (ℓ). Now, take that and suppose we have the distance from the sun and all the other values, but not the angle, rephrase that abomination so that we can solve for the angle. Without using mathematical notation. The only good thing about dropping mathematical notation is that we'd be able to slow down technological process substantially as we wouldn't even be able to get to orbit anymore. That idea of "solve for θ" is "just" a basic application of algebra. An act that would become impossible to do with any kind of reasonable efficiency and confidence about correctness without something like our current mathematical notation, and plain English (very anglocentric, guess we don't want anyone outside the anglosphere to participate) would be a poor alternate.

nathias 5y ago

It was actually Frege that developed types as a solution to Russell's paradox.

cb321 5y ago

If by "type systems/checking" one refers to constraints on "valid operations in context" like comparisons, subtractions, additions (or maybe in a prog.lang context assignment to lexically static identifiers) then physical units of measure (seconds, meters|its ancient cousins, etc.) were the first type system. I.e., one cannot add/compare/etc. meters & seconds without conversion and not all conversions are possible. This remains the first such system most people learn in elementary school. Historically such ideas arose along with measurements themselves and computations upon their results like comparison/subtraction/even taxation. Yes, this is all (typically) manually checked and explicit metadata symbols are carried through calculations. I still think it's the primordial example that few mention in discussions like these.

tel 5y ago
Yeah, saying Russell invented types is fun but horribly wrong. He invented other things and stood at the center of an explosion in formal logics. But types are way old.
- JoBrad 5y ago
  Maybe he invented it the way that many people think the color blue was invented? Causing everyone to see something for the first time (especially when it was right under our noses) is certainly impressive.
  - EarthLaunch 5y ago
    In my game design I've imagined two parallels to invention; discovery and identification. All three are learning about the world, but in slightly different ways. Invention: I created that. Discovery: I found that lying around. Identification: I conceptualized a definition for that.
  - tel 5y ago
    This is certainly more true. That explosion of logics I mentioned was a big movement of many authors to expand our understanding of types (among other things).

justshowpost 5y ago

They should stop teaching students stringly-typed scripting languages and all the confusion will magically disappear. Toy language like Pascal would suffice almost any educational faculty if they are afraid what introductory C course is too hard for audience.

golemotron 5y ago

"When a program and a programmer love each other very much..."

hootbootscoot 5y ago

Maybe I'm being terribly naive, but I don't see this from a maths perspective at all, I see this as about the shape of data and about memory allocation. If one increments pointers across an array of data, one should know the stepping size, for example. How is this (programming/practical) side of the word "type systems" related to formal/mathematical "type systems"? I missed that part

Koshkin 5y ago
Types are a kind of constraints on what kind of logical constructs in one case, and what kinds of computational constructs in the other, are allowable. Logic and computation are related, but they are not the same. (This difference is also evident in how people think about monads in programming vs. how they are defined and used in category theory.)

deleted 5y ago

[deleted]

chrisbrandow 5y ago

I'm still reeling from the three things I learned in this post: 1. Bertrand Russell studied the "I am lying" paradox, which I always thought was nothing more than a clever meme. 2. Bertrand Russell is responsible for type theory 3. That type theory came out of his study of the paradox.

__MatrixMan__ 5y ago
The distinction between countable and uncountable infinities also stems from the liar's paradox.
- Koshkin 5y ago
  How so? The set of reals is uncountably infinite. Looks like a self-contained fact (that can be proved by a "diagonal argument").
  - kazinator 5y ago
    But diagonalization and self-referential paradoxes are related (in ways that are not necessarily obvious). Think along the lines that you have some sentence Px which asserts that sentence Py is false. Now imagine a table where both the rows and columns are P0, P1, P2, .. populated with these sentences. The diagonal is where you have the self-reference: Pi asserting that Pi is false.
ProfHewitt 5y ago
Bertrand Russell introduced orders on propositions to block construction of paradoxes such as “The Liar” [Russell 1908]. Without orders on propositions, the “self-referential” proposition I’mFalse (such that I’mFalse⇔¬I’mFalse) could be constructed using the following recursive definition: I’mFalse:Proposition≡¬I’mFalse. Since Ψ is a propositional variable in the definition, ¬Ψ:Proposition <i+1>. Consequently, I’mFalse:Proposition ⇒I’mFalse:Proposition<i+1>, which is a contradiction. For more information see the following: https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021 https://www.youtube.com/watch?v=AJP1VL7shiI https://www.youtube.com/watch?v=AJP1VL7shiI