3 ms·

Isn't that backwards? Why care about type without a corresponding programm? The systematic problem with higher order incompleteness is propositions fro syntact

Isn't that backwards? Why care about type without a corresponding programm? The systematic problem with higher order incompleteness is propositions fro syntactic argument, without consideration for semantics.

yorwba 9y ago
The Curry-Howard correspondence is about types as propositions and programs as proofs. Gödel's first incompleteness theorem that "In any consistent formal system with [enough arithmetic to make a Gödel encoding], there is a proposition P such that neither P nor ¬P have a proof." translates as: "In any type system that does not allow construction of functions from inhabited types to the empty type ⊥ (this corresponds to consistency), with [enough types and functions to make a Gödel encoding], there is a type T such that neither a program of type T, nor a program of type T → ⊥ (this corresponds to negation), can be constructed." The semantics of the programs involved don't matter, only the way they manipulate types do. Commutativity of conjunction, for example, is encoded by a function of type (A, B) → (B, A). That this function swaps the values in its input tuples is, for the Curry-Howard correspondence, just an unimportant side effect.
- posterboy 9y ago
  OK I really don't know anymore what this has to do with the topic, but I always take the chance to discuss this, as opportunity to be lectured. Where was that quote taken from? Surely, the second conclusion is just one of the premisses. Not just T but any inhabited type couldn't be used as the input to a function that returns nil, if that's axiomatic. Correct? But still, for the first conclusion how can a type without corresponding program be said to exist in the first place? One way around seems to add a higher order axiom about the truth of the liar paradoxons, to assume all unprovable sentences are wrong. The common example is not a lie nor true, but just not a sentence, IMHO. Then that introduced a new set (or what) of unprovable propositions (incomplete), if not inconsistency? That would be a new insight to me. I'd rather expected a second order axiom could be removed to achieve completeness, instead. I haven't seen the axioms of goedel that omega_0-complete systems be higher order.
  - yorwba 9y ago
    > Where was that quote taken from? The quote was a restatement from memory (so not really a quote), but you can find a similar summary on Wikipedia https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#First_incompleteness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... > Surely, the second conclusion is just one of the premisses. Not just T but any inhabited type couldn't be used as the input to a function that returns nil, if that's axiomatic. Correct? I think my choice of T for the arbitrary type was confusing (putting it in italics apparently didn't help). If I had been talking about the top type, I would have used ⊤, not T. (See the difference? Probably not.) > But still, for the first conclusion how can a type without corresponding program be said to exist in the first place? A simple syntactic type without corresponding program is "Λa.Λb. a → b" (the capital lambdas are type abstractions, meaning "for all types"). This is actually the same type as "⊥", but that isn't immediately obvious. So given a specific syntactic type expression, the question is whether there are values of that type and if there are, whether you can construct values of such a type. One type with values that you can't actually construct is the type that says "No value of this type can be constructed." using a Gödel encoding in type-level numbers. That type will be a huge function signature, so it isn't actually relevant to everyday programming, but it has to exist, and there have to be values in that type. Since you can't actually write down these values, their existence is very annoying, but they are a bit like non-standard numbers in that regard: You can't effectively outlaw them without shooting yourself in the foot. > One way around seems to add a higher order axiom about the truth of the liar paradoxons, to assume all unprovable sentences are wrong. That will introduce inconsistency, since Gödel was able to transform a self-referential sentence into a sentence without self-reference, using a construction that is intuitively correct. So if all self-referential sentences without proofs were wrong, the non-self-referential version of "This sentence has no proof." would have to be wrong as well, which means that it has a proof, which makes the original reason for labeling it false invalid. You could avoid the paradox by claiming that Gödel's construction isn't actually intuitively correct, but since the point of the exercise was to show that mathematical intuition can't be formalized, that doesn't really help.

yorwba 9y ago

The Curry-Howard correspondence is about types as propositions and programs as proofs. Gödel's first incompleteness theorem that "In any consistent formal system with [enough arithmetic to make a Gödel encoding], there is a proposition P such that neither P nor ¬P have a proof." translates as: "In any type system that does not allow construction of functions from inhabited types to the empty type ⊥ (this corresponds to consistency), with [enough types and functions to make a Gödel encoding], there is a type T such that neither a program of type T, nor a program of type T → ⊥ (this corresponds to negation), can be constructed." The semantics of the programs involved don't matter, only the way they manipulate types do. Commutativity of conjunction, for example, is encoded by a function of type (A, B) → (B, A). That this function swaps the values in its input tuples is, for the Curry-Howard correspondence, just an unimportant side effect.

posterboy 9y ago
OK I really don't know anymore what this has to do with the topic, but I always take the chance to discuss this, as opportunity to be lectured. Where was that quote taken from? Surely, the second conclusion is just one of the premisses. Not just T but any inhabited type couldn't be used as the input to a function that returns nil, if that's axiomatic. Correct? But still, for the first conclusion how can a type without corresponding program be said to exist in the first place? One way around seems to add a higher order axiom about the truth of the liar paradoxons, to assume all unprovable sentences are wrong. The common example is not a lie nor true, but just not a sentence, IMHO. Then that introduced a new set (or what) of unprovable propositions (incomplete), if not inconsistency? That would be a new insight to me. I'd rather expected a second order axiom could be removed to achieve completeness, instead. I haven't seen the axioms of goedel that omega_0-complete systems be higher order.
- yorwba 9y ago
  > Where was that quote taken from? The quote was a restatement from memory (so not really a quote), but you can find a similar summary on Wikipedia https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems#First_incompleteness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_... > Surely, the second conclusion is just one of the premisses. Not just T but any inhabited type couldn't be used as the input to a function that returns nil, if that's axiomatic. Correct? I think my choice of T for the arbitrary type was confusing (putting it in italics apparently didn't help). If I had been talking about the top type, I would have used ⊤, not T. (See the difference? Probably not.) > But still, for the first conclusion how can a type without corresponding program be said to exist in the first place? A simple syntactic type without corresponding program is "Λa.Λb. a → b" (the capital lambdas are type abstractions, meaning "for all types"). This is actually the same type as "⊥", but that isn't immediately obvious. So given a specific syntactic type expression, the question is whether there are values of that type and if there are, whether you can construct values of such a type. One type with values that you can't actually construct is the type that says "No value of this type can be constructed." using a Gödel encoding in type-level numbers. That type will be a huge function signature, so it isn't actually relevant to everyday programming, but it has to exist, and there have to be values in that type. Since you can't actually write down these values, their existence is very annoying, but they are a bit like non-standard numbers in that regard: You can't effectively outlaw them without shooting yourself in the foot. > One way around seems to add a higher order axiom about the truth of the liar paradoxons, to assume all unprovable sentences are wrong. That will introduce inconsistency, since Gödel was able to transform a self-referential sentence into a sentence without self-reference, using a construction that is intuitively correct. So if all self-referential sentences without proofs were wrong, the non-self-referential version of "This sentence has no proof." would have to be wrong as well, which means that it has a proof, which makes the original reason for labeling it false invalid. You could avoid the paradox by claiming that Gödel's construction isn't actually intuitively correct, but since the point of the exercise was to show that mathematical intuition can't be formalized, that doesn't really help.