News for hackers. Stuff that matters.
Re:Are unsound type systems wrong? by pas on Saturday April 07, 2018 @08:56AM (#16780518)
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.
Re:Are unsound type systems wrong? by gpm on Saturday April 07, 2018 @11:28AM (#16781147)
(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.

Re:Are unsound type systems wrong? by enugu on Saturday April 07, 2018 @01:41PM (#16781738)
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.

Re:Are unsound type systems wrong? by indexerror on Saturday April 07, 2018 @12:48PM (#16781509)
> 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?

Re:Are unsound type systems wrong? by gpm on Saturday April 07, 2018 @02:07PM (#16781880)
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/