[mcprwklzpq]

I can ELIP (Explain Like I am a Programmer) statements and consequences of both incompleteness theorems and two related problems.

So the pemise is that you have to write 4 programs, but you can not, they all would fail for some inputs.

1. The first Gödel's incompleteness theorem. A program has to take a set of axioms and a set of true statements about natural numbers. It has to return proofs for all the statements. How it will fail? It would either for some statements return a proof that contradicts itself (so the set of axioms is inconsistent) or return no proof at all (so the set of axioms is incomplete).

2. The second Gödel's incompleteness theorem. A program has to take a set of axioms. I has to return true if program 1 given theese axioms would never retrun a proof that contradicts itself. How it will fail? It would return true for some set of axioms that are inconsistent.

3. Entscheidungsproblem. A program has to take a set of axioms and a statement. It has to return true if the statement is true. How it will fail? It would return true for some false statement.

4. Halting problem. A program has to take a program (in a Turing complete language). It has to return true if the program will ever finish. How will it fail? It would return true for program that would never finish. Or probably would itself never finish. This is also possible for all other programs.

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

[ProfHewitt]

Your statement 1 of Gödel's first result is not quite correct.

Suppose that Halt[e] means that expression e halts.

The predicate Halt is algorithmically undecidable. That is,

there is no algorithm that decides Halt.

But this does not directly say that Halt is inferentially

undecidable. That is, Halt[e] can always be proved or

disproved.