Tw. Niech T będzie systemem dowodzenia. Istnieje funkcja rekurencyjna f taka, że dla dowolnego zdania A, jeśli ciąg (A_0, A_1, ..., A) jest jego dowodem,
f(<A>) >= <(A_0, A_1, ..., A)>
wtedy i tylko wtedy, gdy T jest rozstrzygalny.(<> należy czytać jako ,,numer goedlowski foo".)
Dowód. W prawo: Następująca procedura mówi nam, czy zdanie A jest dowodliwe w T: Wygenerujmy wszystkie dowody w T wedle wielkości ich goedlowskich. Jezeli natrafimy na ciąg zakończony na A, odpowiadamy Tak. Jeżeli przekroczymy f(<A>) nie znalazłszy dowodu, odpowiadamy Nie.
W lewo: Załóżmy, że T jest rozstrzygalny. Możemy założyć bez utraty ogólności, że A jest zdaniem dowodliwym (z założenia istnieje procedura mówiąca nam, czy tak jest) . Niech x_A będzie numerem goedlowskim najkrótszego dowodu A, który znajdziemy. f(A) = x_A.
Q.E.D
Brak komentarzy:
Prześlij komentarz