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(!)).

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.

(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.

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.

> 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?

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/

Propositional calculus is sound and complete, first order predicate logic isn't.

fol logic is sound and complete (and effective). second order logic is not.

For reference: https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_th...

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

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.

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?

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_sy...

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