Czy da się udowodnić że istnieje twierdzenie którego najkrótszy dowód jest wiekszy niż miliard znaków?

[alfacentaur]

Pytanie jak w temacie, trochę offtopic ale nie wiedziałem do jakiego działu się nadaje.

[matmatmm]

Wystarczy, że wypowiedź tego twierdzenia ma ponad miliard znaków.

[Janusz Tracz]

Wystarczy, że wypowiedź tego twierdzenia ma ponad miliard znaków.

Czy ja wiem. A czy dowód nie może być krótszy od twierdzenia którego dotyczy?

Czy da się udowodnić że istnieje twierdzenie którego najkrótszy dowód jest wiekszy niż miliard znaków?

Tak można to zrobić

Kod: Zaznacz cały

https://en.wikipedia.org/wiki/Reverse_mathematics#The_big_five_subsystems_of_second-order_arithmetic

. Być może zainteresuje Cię to:

Kod: Zaznacz cały

https://en.wikipedia.org/wiki/Kruskal%27s_tree_theorem#TREE%283%29

. W szczególności:

For each \(\displaystyle{ n}\), Peano arithmetic can prove that \(\displaystyle{ P(n)}\) is true, but Peano arithmetic cannot prove the statement "\(\displaystyle{ P(n)}\) is true for all \(\displaystyle{ n}\)". Moreover the length of the shortest proof of \(\displaystyle{ P(n)}\) in Peano arithmetic grows phenomenally fast as a function of n, far faster than any primitive recursive function or the Ackermann function for example. The least m for which \(\displaystyle{ P(n)}\) holds similarly grows extremely quickly with \(\displaystyle{ n}\).

Zatem miliard znaków to nic. Powyższe twierdzenie pokazuje, że możesz pomyśleć o dowolnie dużej liczbie znaków która i tak okaże się za mała by udowodnić \(\displaystyle{ P(n)}\) dla pewnych \(\displaystyle{ n}\).

[matmatmm]

Mój post tyczył się dowodów formalnych tzn. ciągów formuł. Taki dowód jako ostatnią formułę ma twierdzenie, które jest dowodzone. Mam wrażenie, że przytoczony fragment o dowodach w arytmetyce Peana również dotyczy tego typu dowodów.

Pytanie o najkrótszy dowód pisany językiem naturalnym jest raczej pozbawione ścisłego matematycznego sensu.