> It shows that no significantly expressive system can be designed that won't allow paradoxical statements.
The above is a complete misrepresentation of Gödel’s second incompleteness theorem.
The theorem holds for any sufficiently expressive system, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressive consistent system can prove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means.
Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8].
All of these languages are designed to be consistent. Of course, implementation bugs do happen[9].
If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11].
I like your paraphrase but I think it muddies the water. We really want to prove that axioms of a system cannot be contradicted if the system is inconsistent.
To be even more precise, the system or theory T proves that there is no number n which provides a proof of contradiction for the axioms of T.
So its the axioms of the systems which all formal systems assume and hold to be true. Basically its impossible to prove that axioms are true with the same system.
In short, no formal system can define its own consistency because in order for its axioms to be true, the system must be inconsistent.
The above is a complete misrepresentation of Gödel’s second incompleteness theorem.
The theorem holds for any sufficiently expressive system, where the term ‘sufficiently expressive’ has a precise formal meaning[1]. Moreover, it is not the case that any sufficiently expressive system must be inconsistent! The theorem could perhaps be paraphrased as ‘no sufficiently expressive consistent system can prove its own consistency’[2], as long as we are prepared to explain what ‘its own’ really means.
Importantly, there are systems that do not allow paradoxical statements, and are nevertheless quite expressive, in an informal sense. For example, any dependently typed[3] total functional programming language[4], such as Agda[5], Coq[6], Idris[7], or Lean[8].
All of these languages are designed to be consistent. Of course, implementation bugs do happen[9].
If you would like to learn more about dependent types, ‘The Little Typer’[10] is newly out and a lot of fun to read. For an accessible introduction to the concept of total functional programming, see Turner 2004[11].
[1] Hilbert-Bernays provability conditions, https://en.wikipedia.org/wiki/Hilbert–Bernays_provability_co...
[2] Gödel’s second incompleteness theorem, https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...
[3] Dependent type, https://en.wikipedia.org/wiki/Dependent_type
[4] Total functional programming, https://en.wikipedia.org/wiki/Total_functional_programming
[5] Agda programming language, http://agda.readthedocs.io
[6] Coq proof assistant, http://coq.inria.fr
[7] Idris programming language, http://www.idris-lang.org
[8] Lean theorem prover, http://leanprover.github.io
[9] The rise and fall of @proofmarket, https://twitter.com/i/moments/921153475836305408
[10] Friedman, D.P., Christiansen, D.T. (2018) ‘The Little Typer’, https://mitpress.mit.edu/books/little-typer
[11] Turner, D. (2004) ‘Total Functional Programming’, http://www.jucs.org/jucs_10_7/total_functional_programming