incompleteness, undecidability

Stream: Is there code for X?

[April Walker]

Is there code around that can reason about formal systems enough to define these notions?

[Aaron Liu]

We have docs#Computable

[Aaron Liu]

We also have docs#FirstOrder.Language.Theory.IsComplete

[Aaron Liu]

Not sure exactly what you mean by "undecidability" though.

[April Walker]

These seem like good starting points, thanks!

[April Walker]

Being able to state that certain theorems/axioms are undecidable in X formal system.

[Aaron Liu]

No but what does "undecidable" mean in this context

[April Walker]

I suppose the most straightforward way is to pick an appropriate formal system S and take the new system S + X (X is whatever statement you're stating facts about). If you can prove the consistency of S in S + X, you have a proof that X is undecidable in S via one of Gödel's incompleteness theorems

[April Walker]

The Paris-Harrington theorem follows this line, but I have no idea if anyone has formalized it yet

[Aaron Liu]

April Walker said:

I suppose the most straightforward way is to pick an appropriate formal system S and take the new system S + X (X is whatever statement you're stating facts about). If you can prove the consistency of S in S + X, you have a proof that X is undecidable in S via one of Gödel's incompleteness theorems

This just shows that X is not derivable from S? I still don't know what you mean by "undecidable".

[April Walker]

Any statement that can be written in the language of a formal system but not provable within it we call "undecidable". The Paris-Harrington theorem, for example, proves that the strengthened finite ramsey theorem (which can be stated in Peano arithmetic) cannot be proven in Peano arithmetic (thus is undecidable in Peano arithmetic)

[Edward van de Meent]

Any statement that cannot be proven nor disproven, presumably

[Aaron Liu]

After some searching, I can't find anything on proofs in mathlib.

[Edward van de Meent]

Otherwise, something like 0 = 1 is undecidable in peano arithmetic

[Aaron Liu]

I do know of Formalized Formal Logic.

[April Walker]

This seems to be the closest to what I had in mind, thank you!