[ProfHewitt]

Your statement 2 of Gödel's second result is false because

Gödel's second result is false for foundational theories.

Foundational theories can in fact prove their own consistency.

However, the self-proof of consistency is not very convincing

because the proof is valid even if the theory is inconsistent.

Fortunately, there is another way to prove consistency by

showing that a theory has a mathematical model.

See the following for an overview:

https://papers.ssrn.com/abstract=3603021

[mcprwklzpq]

Thank you. I downloaded this paper a month ago to read it eventually. Your comment made me read it yesterday and i have a question.

By using the type system would we exlude potentially consistent theories? Is it similar to how limitimg ourselves to a decidable language instead of a turing complete one would prevent us from writing potentially never halting programms that could still halt?