Dlaczego potrzebujemy formalnej semantyki dla logiki predykatów?

Rozważ to pytanie rozwiązane. Nie wybiorę najlepszej odpowiedzi, ponieważ wszystkie one przyczyniły się do mojego zrozumienia tego tematu.

Nie jestem pewien, jakie korzyści przyniesie nam formalne zdefiniowanie semantyki logiki predykatów. Ale widzę wartość posiadania formalnego rachunku próbnego. Chodzi mi o to, że nie potrzebowalibyśmy formalnej semantyki, aby uzasadnić reguły wnioskowania rachunku kalkulacyjnego.

Możemy zdefiniować rachunek, który naśladuje „prawa myślenia”, tj. Reguły wnioskowania stosowane przez matematyków od setek lat w celu udowodnienia ich twierdzeń. Taki rachunek już istnieje: naturalne odliczenie. Następnie zdefiniowalibyśmy ten rachunek jako solidny i kompletny.

Można to uzasadnić, zdając sobie sprawę, że semantyka formalna logiki predykatów jest tylko modelem. Odpowiedniość modelu można uzasadnić jedynie intuicyjnie. Zatem wykazanie, że naturalna dedukcja jest rozsądna i kompletna w odniesieniu do formalnej semantyki, nie czyni jej naturalnej bardziej „prawdziwą”. Byłoby równie dobrze, gdybyśmy intuicyjnie bezpośrednio uzasadnili reguły naturalnego odliczenia. Objazd z wykorzystaniem semantyki formalnej nic nam nie daje.

Następnie, po zdefiniowaniu naturalnej dedukcji jako solidnej i kompletnej, moglibyśmy wykazać solidność i kompletność innych obliczeń, pokazując, że dowody, które produkują, można przełożyć na naturalną dedukcję i odwrotnie.

Czy moje powyższe refleksje są prawidłowe? Dlaczego ważne jest udowodnienie poprawności i kompletności rachunku kalkulacyjnego poprzez odniesienie do semantyki formalnej?

Drobny komentarz i poważniejsza odpowiedź.

Po pierwsze, nie ma sensu ogłaszać, że system odliczeń naturalnych jest kompletny przez fiat. Naturalna dedukcja jest interesująca właśnie dlatego, że ma naturalne wewnętrzne pojęcie spójności i / lub kompletności - mianowicie eliminację cięć. To fantastyczne twierdzenie, a IMO w pełni uzasadnia próby nadania czysto teoretycznej semantyki (a przez korespondencję CH podobnie uzasadnia zastosowanie metod operacyjnych w semantyce języka programowania). Jest to jednak interesujące właśnie dlatego, że oferuje bardziej wyrafinowane pojęcie prawidłowej logiki niż spójności. Podjęcie teoretycznej drogi dowodu oznacza, że ​​będziesz musiał wykonać więcej pracy, ale w zamian uzyskasz lepsze wyniki.

Zdarza się jednak, że czasami logika sama w sobieodgrywa drugorzędną rolę. Możemy zacząć od (rodziny) modeli, a następnie szukać sposobów syntaktycznego mówienia o nich przy użyciu logiki. Solidność i kompletność logiki w odniesieniu do rodziny modeli wskazuje, że logika naprawdę oddaje wszystko, co interesujące i prawdziwe, co można powiedzieć o klasie modeli. Konkretny przykład tego, kiedy modele są bardziej interesujące niż teorie logiczne, występuje w analizie programu i sprawdzaniu modelu. Tam zwykle należy wziąć model za wykonanie programu, a logika to fragment logiki czasowej. Twierdzenia, które możesz wypowiedzieć w tych językach, nie są (celowo) niezbyt ekscytujące - np. Zerowe odchylenie wskaźnika nigdy nie występuje - ale to fakt, że odnosi się do rzeczywistych przebiegów programu, budzi jego zainteresowanie.

Po prostu dodam inną perspektywę, aby wzmocnić powyższe odpowiedzi. Po pierwsze, te refleksje są warte zachodu i wiele osób ma podobne pomysły. W filozofii jest to czasami nazywane „semantyką dowodową”, odwołując się do pracy Nuela Belnapa, Daga Prawitza, Michaela Dummetta i innych w latach 60. i 70., którzy sami odwołują się do pracy Gentzena na temat dedukcji naturalnej. Per Martin-Löf i Jean-Yves Girard również wydają się proponować warianty tego stanowiska w swoich pismach. Mówiąc bardzo szeroko, w językach programowania jest to „syntaktyczne podejście do poprawności dźwięku”.

Chodzi o to, że nawet jeśli zaakceptujesz, że reguły logiki nie wymagają osobnej interpretacji semantycznej, nie jest zbyt interesujące / użyteczne stwierdzenie, że są one uzasadnione i pozostaw to. Pytanie brzmi: co osiąga semantyka formalna i czy można to osiągnąć przy mniejszej liczbie objazdów. Jednak projekt ujednolicenia teorii modeli z analityczną teorią dowodu jest ważny, ale wciąż nierozwiązany, ponieważ jest aktywnie realizowany na wielu różnych frontach, w tym logice kategorycznej, semantyce gry i „ludyce” Girarda. Na przykład, oprócz tego, co wspomniano Charles, kolejny jakościowy korzyścią z posiadania modeli jest zdolność do zapewnienia konkretnych kontrprzykładów na zakaz-twierdzenia, a pytania brzmią, jak to zrozumieć w podejściu „bezpośrednim”. Jedna odpowiedź inspirowana ludycznością znajduje się w „O znaczeniu logicznej kompletności” Michele Basaldelli i Kazushige Terui.

Formalna semantyka zapewnia bezpośrednie znaczenie terminów w rachunku różnym od składniowych reguł dowodowych służących do manipulowania nimi. Bez formalnej semantyki, w jaki sposób możesz stwierdzić, czy reguły dedukcji są prawidłowe (poprawność), czy też masz ich dość (kompletność)?

Zaproponowano „prawa myśli”, zanim nastąpiła naturalna dedukcja. Sylogizmy Arystotelesa były jedną z takich kolekcji. Gdybyśmy zdefiniowali je jako solidne i kompletne, być może nadal używalibyśmy ich dzisiaj, zamiast rozwijać bardziej zaawansowane techniki logiczne. Chodzi o to, że jeśli sylogizmy całkowicie wychwytują prawa myśli, dlaczego mielibyśmy wymyślić jakąkolwiek dalszą logikę. A gdyby tak naprawdę były niespójne? Posiadanie semantyki wraz z formalnym rachunkiem dowodowym oraz łączącymi je dowodami poprawności i kompletności zapewnia miarkę do oceny wartości takiego systemu rozumowania. Nie będzie już dłużej odizolowany.

$X\lor \neg X$nawet posunąć się nawet do argumentowania, że ​​powinniśmy zaakceptować, że nie ma jednej prawdziwej logiki i przyjąć postawę pluralistyczną, stosując najbardziej odpowiednią logikę na tę okazję. Biorąc pod uwagę mnóstwo logiki dostępnej dla informatyków (logika liniowa, logika separacji, logika konstruktywna wyższego rzędu, wiele logiki modalnej, wszystkie w klasycznych i intuicyjnych odmianach), przyjęcie pluralistycznej postawy jest czymś, czego większość z nas prawdopodobnie nie dała sekundy pomyślałem, ponieważ logika jest narzędziem do rozwiązania konkretnego problemu i staramy się wybrać najbardziej odpowiedni. Formalna semantyka jest jednym ze sposobów oceny stosowności logiki.

Innym powodem formalnej semantyki jest to, że logiki jest więcej niż rachunek predykatów. Wiele z tych logiki zaprojektowano z myślą o konkretnym systemie. (Myślę o logice modalnej). Tutaj klasa systemów jest znana, a logika pojawia się później (choć historycznie nie jest to również prawdą). Ponownie, solidność mówi nam, czy aksjomaty logiki poprawnie wychwytują „zachowanie” systemu, a kompletność mówi nam, czy mamy wystarczającą liczbę aksjomatów. Bez semantyki, skąd mielibyśmy wiedzieć, czy reguły dedukcji są wystarczające, a nie nonsensowne?

Jedną przykładową logiką, która została zdefiniowana czysto syntaktycznie i nadal trwają prace nad zapewnieniem jej formalnej semantyki, jest logika BAN do rozumowania protokołów kryptograficznych. Logiczne reguły wnioskowania wydają się rozsądne, więc po co zapewniać formalną semantykę? Niestety logiki BAN można użyć do udowodnienia poprawności protokołu, ale mogą istnieć ataki na takie protokoły. Zasady dedukcji są zatem błędne , przynajmniej w odniesieniu do oczekiwanej semantyki.

Zgadzam się z supercooldave, ale istnieje jeszcze jeden, bardziej pragmatyczny powód, aby chcieć więcej niż jakiś zestaw lub inne reguły wnioskowania, które charakteryzują logikę: dany zestaw reguł wnioskowania zwykle nie jest odpowiedni do rozwiązywania problemów, jakie napotyka się przy układaniu logiki używać.

Jeśli masz logikę określoną przez listę aksjomatów i kilka reguł jako system Hilberta, zwykle ciężko będzie wymyślić, jak udowodnić dane twierdzenie w systemie, i bez teoretycznego wglądu nie pójdziesz być w stanie udowodnić, że dana propozycja nie może zostać udowodniona w systemie. Tradycyjne modele sprawdzają się w przypadku właściwości, które zachowują całą logikę przez indukcję.

Cztery rodzaje narzędzi są przydatne do rozwiązywania problemów, które większość logików chce rozwiązać, od najmniej do najbardziej semantycznych:

1. Systemy w stylu Hilberta są dobre do scharakteryzowania logicznej relacji konsekwencji logiki i zwykle są dobre do kategoryzacji kilku logik, takich jak konkurencyjne logiki modalne;
2. Systemy Tableau są dobre do formalizowania algorytmów decyzyjnych. Zazwyczaj, jeżeli logika jest rozstrzygalna, można znaleźć końcowy system tablicowy jako algorytm decyzyjny, a jeśli nie, można znaleźć potencjalnie nie kończący się system tablicowy, który zapewnia procedurę półdecyzji. Jeśli chcemy wykazać górną granicę złożoności rozstrzygalności (tj. Klasy złożoności logiki), systemy tablicowe są na ogół pierwszym miejscem, na które się patrzy.
3. Teorie dowodów analitycznych, takie jak naturalna dedukcja i rachunek sekwencyjny Gentzen, dają reprezentacje dowodów, które są dobre do rozumowania, i oferują pojęcie dowodu analitycznego, które jest przydatne do udowodnienia użytecznych właściwości, takich jak interpolacja teorii.
4. Teorie modeli w stylu Tarskiego są często jeszcze lepsze do wnioskowania o logice, ponieważ prawie całkowicie odbiegają od syntaktycznych szczegółów logiki. W logice modalnej i teorii mnogości są znacznie lepsi w dostarczaniu wyników, że ci logicy zwykle mają bardzo ograniczone zainteresowanie tabelą i teorią dowodów analitycznych.

Odkąd supercoave wspomniał o intuicyjnej logice: bez reguły wykluczonego środka teoria modeli staje się znacznie bardziej skomplikowana, a analityczne teorie dowodowe stają się ważniejsze, zwykle semantyka wyboru. Techniki algebraiczne, takie jak teoria kategorii, stają się preferowane do abstrakcji od złożoności syntaktycznej.