Techniki wykazywania nieprzekraczalności w logice i innych formalnych systemach dowodowych

W systemach dowodowych dla klasycznej logiki zdań, jeśli chce się wykazać, że pewna formuła nie jest pochodna, po prostu pokazuje, że można uzyskać (chociaż z pewnością możliwe są inne techniki). Brak możliwości wyprowadzenia wynika zasadniczo z prawidłowości i kompletności systemu dowodowego. $\psi$ $\neg\psi$

Niestety w przypadku nieklasycznej logiki i bardziej egzotycznych systemów dowodowych (takich jak zasady leżące u podstaw semantyki operacyjnej) nie istnieje taka bezpośrednia technika. Może to być spowodowane tym, że niemożność wyprowadzenia nie oznacza, że jest pochodna, jak ma to miejsce w przypadku intuicyjnej logiki, lub po prostu, że nie istnieje pojęcie negacji. $\psi$ $\neg\psi$

Moje pytanie otrzymuje system dowodowy , gdzie (i przypuszczalnie jego semantyka), jakie techniki istnieją wykazać brak pochodności? $(\mathcal{L},\vdash)$ $\vdash\;\subseteq\mathcal{L}^*\times\mathcal{L}$

Interesujące systemy dowodowe mogą obejmować semantykę operacyjną języków programowania, logikę Hoare'a, systemy typów, logikę nieklasyczną lub reguły wnioskowania dla tego, co masz.

lo.logic

— Dave Clarke
źródło

Dave, myślę, że w pytaniu jest literówka. Aby pokazać, że nie jest pochodna, nie pokazujemy, że jest pochodna, po prostu pokazujemy, że jest spójna, a to opiera się tylko na spójności klasycznej logika. Jeśli logika jest logiką klasyczną pierwszego rzędu, istnieją zdania, których nie możemy ani udowodnić, ani obalić (chyba że mówimy o pełnej teorii ). A może źle rozumiem twoje pytanie?

φ

$\varphi$

\neg φ

$\lnot \varphi$

— Kaveh

Zmieniłem to na klasyczną logikę zdań. Pytanie wymaga jakiejkolwiek techniki oprócz udowodnienia negacji, ponieważ wiele formalnych systemów (zbiór aksjomatów i reguł wnioskowania) nie ma negacji, aw rzeczywistości może nawet nie wyglądać jak „logika”.

— Dave Clarke

Dzięki za wyjaśnienie, domyślam się logiki pierwszego rzędu, kiedy czytam logikę klasyczną. :)

— Kaveh

IME, poniższa lista jest najłatwiejsza do najtrudniejszej (oczywiście jest również najmniej wydajna):

Jeśli twój system jest sprawny i możesz udowodnić , wtedy masz oczywiście wynik niemożliwy do przywrócenia. $\lnot \phi$
Jeśli masz logikę opartą na teoretyce kratowej, względem której wszystkie reguły dowodu są poprawne, to jeśli znaczenie zdania nie jest najwyższym elementem sieci, to nie jest to zdanie dające się wyprowadzić.
Jeśli wiesz, że twoja logika jest kompletna w odniesieniu do klasy modeli, sprawdź, czy istnieje jakiś model w tej klasie, który unieważnia . $\phi$
Czasami możesz uciec od tłumaczenia na inną logikę i pokazać, że pochodna tutaj oznacza znany wynik niemożności do uzyskania.
Jeśli masz naturalne odliczenie lub rachunek sekwencyjny, sprawdź, czy znany jest wynik eliminacji cięć lub czy możesz go udowodnić. Jeśli tak, to często można wykorzystać właściwość podformularza, aby podać proste argumenty indukcyjne na temat niemożności ustalenia. (Np. Spójność poprzez eliminację cięć jest tylko stwierdzeniem, że nie ma dowodów fałszywych na bezcięcie, a więc jeśli wszystkie cięcia można wyeliminować, nie ma niespójności).
Jeśli nic więcej nie działa, często można wyświetlić wyniki spójności / braku możliwości ustalenia za pomocą argumentu relacji logicznych. Jest to wielki pistolet, który działa, gdy nic innego nie działa - w ujęciu teoretycznym sprowadza się do użycia aksjomatu Zamiennik, który pozwala pokazać, że ogromne zestawy są dobrze uporządkowane. (Dlatego możesz go użyć, aby udowodnić takie rzeczy, jak normalizacja Systemu F.)

— Neel Krishnaswami
źródło

F

$F$

P A^{2}

$PA^2$

F^{2}

$F^2$

Dzięki, teraz rozumiem, co miałeś na myśli przez „takie rzeczy jak normalizacja Systemu F”. :)

— Kaveh

@Kaveh, @Neel: Silna normalizacja systemu F nie jest twierdzeniem PA2, lecz jest równoważna w stosunku do PA do spójności PA2. Przeciwnie, silną normalizację dla wszystkich warunków rangi n (ranga będąca miarą maksymalnej głębokości kwantyfikatorów typu nsteda) można udowodnić za pomocą ACA- n . Lubię rozmawiać o budowaniu modeli snopków w tajemnicy ...

— Charles Stewart

@Charles: Dowiedziałem się o tym pomyśle z kilku artykułów Jean Galliera, które są zaskakująco niedoceniane. Nieco przewrotnie ten fantazyjny pogląd pomógł mi zrozumieć prostsze konto Mitchella i Scedrowa.

— Neel Krishnaswami,