4 ms·

I'm curious, given Godels incompleteness theory, isn't it impossible to have both soundness and completeness in the same language?

by s_kilk 9y ago

karatinversion 9y ago
Gödel's incompleteness is for proof systems for languages which contain enough arithmetic to express its own syntax. Lots of things don't go this far - first order predicate logic is sound and complete, for example (see Gödel's completeness theorem(!)).
- pas 9y ago
  Could you please expand on the soundness and completeness of first order logic? Isn't that false generally? Because you need a deductive/axiom system, so that you can ask the question of completeness/soundness. And ZFC is too strong, hence cannot prove its soundness and correctness at the same time. But you can formalize weaker systems in first order logic, that are provably complete and sound.
  - gpm 9y ago
    (It's been a year and a half since I took a course on this, so I apologize for any mistakes) You do need to define a deductive/axiom system before you can ask the question. We can use a few different standard deductive systems. We require that the axioms are sound. Then the system is complete. (I think one should also always be able to prove false if the axioms aren't sound... but I don't recall proving that) ZFC isn't too strong. That sounds like a contradiction, but it isn't, because we don't have a rich enough vocabularly in first order logic to state the problematic statements that make it either inconsistent or incomplete in stronger logic systems. Every true statement you can state about ZFC in first order logic is provable.
    - indexerror 9y ago
      > It's been a year and a half since I took a course on this Can you please recommend a MOOC/resource for learning more about this?
      - gpm 9y ago
        My only real exposure to it is the course I took, csc438 at UofT taught by Steven Cook. There are pretty complete notes for the course as well as assignments here [0], but not videos or planned lessons. You certainly could learn about it by reading them, but I don't know if it would be the most efficient way. [0] http://www.cs.toronto.edu/~sacook/csc438h/ http://www.cs.toronto.edu/~sacook/csc438h/
    - enugu 9y ago
      We can state a lot of things in first order logic about natural numbers or set theory which are not provable (in some given set of axioms like Peano axioms or ZFC, you can extend the axiom set but then one can generate a new unprovable statement if not a contradiction). The issue here is first order logic is complete for statements that are true for all models of the axioms. As an example, imagine a infinite land which cant be completely described by any computable map(a programmable set of facts about the territory). The map will only tell you some true things about the territory. But we can say this - if there is some statement that the map cant decide, then there are two different territories for both of which the map is accurate, and the statement is true for one territory and false for another. So the deductive system is complete description of true statements which hold for all territories for which the map applies. But if we are interested in a single given territory, no computable system of facts suffices. For example deciding whether a diophantine equation has solutions in the standard set of Natural Numbers or a more familiar example for this site, whether a program halts. No computable deductive system(ie there is a program which generates all deductions) will suffice.
- varjag 9y ago
  Propositional calculus is sound and complete, first order predicate logic isn't.
  - jonnycomputer 9y ago
    fol logic is sound and complete (and effective). second order logic is not.
    - mcguire 9y ago
      For reference: https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...
snnw 9y ago
Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.
- vanderZwan 9y ago
  Would a type system that can verify whether array access is always in-bound implicitly encode arithmetic somehow? My gut feeling says yes, since I don't know how one would prove bounds without arithmetic, but I don't have the mathematical knowledge to back this up.
  - lmm 9y ago
    It would need a certain amount of arithmetic, but Presburger arithmetic (addition and constant multiplication, essentially) is complete and consistent and might be enough for all the array use we care about?
baq 9y ago
you can design a complete and sound type system in which any program can be checked in polynomial time. https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...
vilhelm_s 9y ago
Yes, although I would appeal to Rice's theorem rather than Gödel.

I'm curious, given Godels incompleteness theory, isn't it impossible to have both soundness and completeness in the same language?

by s_kilk 9y ago

I'm curious, given Godels incompleteness theory, isn't it impossible to have both soundness and completeness in the same language?

karatinversion 9y ago

Gödel's incompleteness is for proof systems for languages which contain enough arithmetic to express its own syntax. Lots of things don't go this far - first order predicate logic is sound and complete, for example (see Gödel's completeness theorem(!)).

pas 9y ago
Could you please expand on the soundness and completeness of first order logic? Isn't that false generally? Because you need a deductive/axiom system, so that you can ask the question of completeness/soundness. And ZFC is too strong, hence cannot prove its soundness and correctness at the same time. But you can formalize weaker systems in first order logic, that are provably complete and sound.
- gpm 9y ago
  (It's been a year and a half since I took a course on this, so I apologize for any mistakes) You do need to define a deductive/axiom system before you can ask the question. We can use a few different standard deductive systems. We require that the axioms are sound. Then the system is complete. (I think one should also always be able to prove false if the axioms aren't sound... but I don't recall proving that) ZFC isn't too strong. That sounds like a contradiction, but it isn't, because we don't have a rich enough vocabularly in first order logic to state the problematic statements that make it either inconsistent or incomplete in stronger logic systems. Every true statement you can state about ZFC in first order logic is provable.
  - indexerror 9y ago
    > It's been a year and a half since I took a course on this Can you please recommend a MOOC/resource for learning more about this?
    - gpm 9y ago
      My only real exposure to it is the course I took, csc438 at UofT taught by Steven Cook. There are pretty complete notes for the course as well as assignments here [0], but not videos or planned lessons. You certainly could learn about it by reading them, but I don't know if it would be the most efficient way. [0] http://www.cs.toronto.edu/~sacook/csc438h/ http://www.cs.toronto.edu/~sacook/csc438h/
  - enugu 9y ago
    We can state a lot of things in first order logic about natural numbers or set theory which are not provable (in some given set of axioms like Peano axioms or ZFC, you can extend the axiom set but then one can generate a new unprovable statement if not a contradiction). The issue here is first order logic is complete for statements that are true for all models of the axioms. As an example, imagine a infinite land which cant be completely described by any computable map(a programmable set of facts about the territory). The map will only tell you some true things about the territory. But we can say this - if there is some statement that the map cant decide, then there are two different territories for both of which the map is accurate, and the statement is true for one territory and false for another. So the deductive system is complete description of true statements which hold for all territories for which the map applies. But if we are interested in a single given territory, no computable system of facts suffices. For example deciding whether a diophantine equation has solutions in the standard set of Natural Numbers or a more familiar example for this site, whether a program halts. No computable deductive system(ie there is a program which generates all deductions) will suffice.
varjag 9y ago
Propositional calculus is sound and complete, first order predicate logic isn't.
- jonnycomputer 9y ago
  fol logic is sound and complete (and effective). second order logic is not.
  - mcguire 9y ago
    For reference: https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...

snnw 9y ago

Godel's theorem only applies to proof systems that can encode basic arithmetic, which most type systems cannot.

vanderZwan 9y ago
Would a type system that can verify whether array access is always in-bound implicitly encode arithmetic somehow? My gut feeling says yes, since I don't know how one would prove bounds without arithmetic, but I don't have the mathematical knowledge to back this up.
- lmm 9y ago
  It would need a certain amount of arithmetic, but Presburger arithmetic (addition and constant multiplication, essentially) is complete and consistent and might be enough for all the array use we care about?

baq 9y ago

you can design a complete and sound type system in which any program can be checked in polynomial time. https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_sy...

vilhelm_s 9y ago

Yes, although I would appeal to Rice's theorem rather than Gödel.