Twierdzenie z seminarium

Przyjemne twierdzenie, powstałe w ramach dygresji na seminarium Pryncypała:

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

wrażenia z forum

Dzisiaj byliśmy na Forum Logicznym, gdzie referat na temat pełnych klas spełniania wygłosił Henryk Kotlarski. Referat bardzo przyjemny, z jednym wszakże mankamentem: nie zrozumiałem kluczowej definicji, zatem również wszystkiego, co po niej nastąpiło. Ale -- nie ma co się przejmować, ponieważ:

• Nie tylko ja nie zrozumiałem kluczowej definicji. Śmiem twierdzić nawet, że byłem pod tym względem w większości.
• Jak zbiorę siły mogę sobie spokojnie przeczytać artykuł wyjaśniający co i jak: został wydrukowany w bardzo zacnym czasopiśmie, które udostępnia swoje archiwa za darmo w ramach Project Euclid.
  
• José Raul Capablanca nauczył się grać w szachy jedynie patrząc, jak jego ojciec gra z przyjaciółmi. Jeżeli logiki da się nauczyć w sposób analogiczny, to jeślii będę dostatecznie dużo słuchał niezrozumiałych dyskusji i prelekcji, któregoś dnia doznam oświecenia i (ex definitione) wszystko stanie się jasne. Póki co możemy z Mareczkiem pozwolić sobie na całkiem przekonywujące (dla laika, rzecz jasna) udawanie, że prowadzimy wielce fachową i intelektualną dyskusję o logice. Zgodnie z metaforą szachową: już nauczyliśmy się, że figury należy przestawiać, a nie starać się trafić nimi oponenta między oczy. Przykre jest to, że ten prosty fakt zdaje się umykać sporej grupie ludzi uważających się za filozofów (co gorsza biorą za to pieniądze).
  

Ponadto, prelekcja pozwoliła na dwa ciekawe spostrzeżenia lingwistyczne. Otóz, Henryk Kotlarski zafrapował mnie kilka razy mówiąc, że ,,model myśli, że cośtam''. Wpierw podejrzewałem, że jest to tylko jakiś wredny, nieformalny sposób mówienia. Po chwili jednak zdałem sobie sprawę, że owo ,,myśli'' jest po prostu czytaniem znaczka ,,|=''. Po drugie, okazało się, że zdanie może być brutalnie prawdziwe. Jeżeli intuicja mnie nie myli, zdanie brutalnie prawdziwe jest mocniejszym sformułowaniem określającym zdanie trywialnie prawdziwe. Czy można zatem powidzieć na przykład o bandycie, że jest człowiekiem bardzo trywialnym?

wyimek o free logic

W artykule Karela Lamberta Philosophical Foundations of Free Logic (Inquiry, 24, 147-203) znalazłem fragment który bardzo mi się spodobał:

To see this imagine the world to contain as its sole existing object the early twentieth-century logician Mary Caulkins. She is an excellent choice because, I have been told, she was a Solipsist.

Tu następuje przypis, w którym czytamy:

She is also alleged to be rseponsible for a remarkable self-indicting response to a friend who met her as she was about to board a ship for England. “Where are you going, Mary?”, he asked. “To a Solipsist convention in London”, she replied.

W dalszej części artykułu pojawiają się inne ciekawe smaczki, jak nawiązania do Alicji po drugiej stronie lustra, lub też nabijanie się ze swoich (w sensie - Autora) artykułów. Jak widać, zajmowanie się Free Logic dobrze służy na poczucie humoru (chociaż nie aż tak dobrze, jak zajmowanie się logiką niefregowską, o czym wiedzą miłośnicy prof. Omyły).

A co do samego Karela Lamberta - to też jest całkiem ciekawy człowiek. Na początku swojej kariery zajmował się raczej psychologią eksperymentalną niż filozofią. Później jednak przerzucił swoje zainteresowania na tzw. free logic, co ma być wygodnym skrótem dla logic free from existential assumptions, i od pewnego momentu zajmował się już zawodowo raczej logiką. Nawet sukcesfulnie, bo dużo publikował w dobrych czasopismach.

No i jak powinienem był się spodziewać (a nie spodziewałem) - oczywiście, człowiekiem który wymyślił te całe wolne logiki (nie chodzi o nazwę, ale o rachunek predykatów wciąż działający dla dziedziny pustej) jest nikt inny jak Andrzej Mostowski, czyli sławny stryj Pryncypała, który zajął się tym w artykule On the rules of proof in the pure functional calculus, JSL, Vol. 16, No. 2 (Jun. 1951), pp. 107-111.

A swoją drogą, wypadałoby ogłosić konkurs na działy logiki formalnej powstałe za dorosłego życia AM takie, że nie założył ich ani nie wniósł istotnego wkładu...

Ciekawe twierdzonko

Jak się nie ma o czym pisać, to się publikuje na blogu interesujące twierdzenia. Ten blog zapowiada się na nudnego bloga ;-)

Twierdzenie: Niech f będzie dowolną rekurencyjną funkcją zgadującą następny element danego ciągu a na podstawie elementów już pokazanych. Powiemy, że f zgadła a wtw od pewnego momentu wszystkie jej predykcje są prawdziwe. Istnieje rekurencyjny ciąg a' taki, że f nie jest w stanie go zgadnąć.
Dowód. Ustalmy f. a(0) będzie równe 0. Dla każdego n>0, niech a'(n) będzie równe predykcji f na podstawie a'(0), a'(1), ... , a'(n-1) powiększonej o 1. c.b.d.o

K. Kelly, "Learning Theory and Epistemology", na podstawie Putnama.