Computational Metaphysics

Źródło: byłem dzisiaj na wykładzie dr haba-kiedy-go-nostryfikują-i-prawdopodobnie-od-jesieni-na-UJ T. Kowalskiego w ramach konferencji w pierwszą rocznicę śmierci prof. Perzanowskiego. Kowalski mówił o interesująco wyglądającym projekcie Computational Metaphysics. O co chodzi? Pomysł jest prosty: formalizacja argumentów to znana sprawa i wiemy że działa dobrze, więc pójdźmy o krok dalej i sprawdzajmy poprawność odpowiednimi programami.

Projekt jest dość nowy i odpowiednie programy są dopiero budowane. Tj., oczywiście, nowy w kontekście filozoficznym, bo historyjkę o dowodzie twierdzenia z Principia Mathematica chyba każdy zna, o ile wiem trochę ważnych faktów o grafach udowodniono takimi metodami i pewnie nawet powierzchowny search znajdzie dużo więcej. Kowalski mówił że istniejące programy działają nieźle dla logiki rzędu I, ale jeśli rozszerzy się dziedzinę kwantyfikacji - np. będzie w standardowy reprezentowało pożądane fragmenty logiki II rzędu via sorty - to już przy trzech sortach robią się problemy.

Nie miałem jeszcze okazji się tym pobawić (i pewnie nieprędko, brak czasu i takie tam), ale wygląda interesująco. Niestety, wydaje się że bardziej zaawansowane rozumowania sprawiałaby problemy techniczne - np. tak byłoby z Herzbergera dowodem zabawnego Peirce'owskiego twierdzenia o redukowalności relacji (dowolne n-argumentowe relacje, dla n naturalnego, da się zredukować do maxymalnie 3-argumentowych, 3-argumentowe nie redukują się dalej), czy z często przytaczanym dowodem van Benthema z "The Logic of Time" (że jedyne relacje definiowalne w terminach porządku na czasoprzestrzeniach Minkowskiego to relacja identycznościowa i relacja uniwersalna), bo trzebaby wrzucić dość rozbudowaną aksjomatykę, a sam dowód jest geometryczny. Ale byłoby fajnie to sprawdzić, bo dalej nie jestem przekonany że rekonstrukcja jakiej dokonaliśmy jest (1) poprawna i (2) że tak działa dowód van Benthema. Chyba w wolnej chwili wrzucę tam fragment z Rakić "Past, Present, Future, and Special Relativity", były tam niejasne fragmenty a formalizacja wydaje się odpowiednia dla tego narzędzia. Łatwo mogę sobie wyobrazić przydatne zastosowanie tego rodzaju metod nie tylko jako dodatkowego sposobu sprawdzania poprawności wnioskowań (co, jak Kowalski zauważył, znacząco może zwiększyć np. szanse na publikację w Journal of Philosophical Logic ;-)), ale w szczególności do sprawdzania często niepopartych dobrymi argumentami deklaracji o niesprzeczności czegoś z teorią.
 
Poza tym ostatnio narzędzia informatyczne są coraz bardziej modne (korpusy, głupcze! i tak dalej), więc warto wiedzieć i o tym.

Computational Metaphysics.