Teoria dowodu strukturalnego

W logice matematycznej teoria dowodu strukturalnego jest subdyscypliną teorii dowodu , która bada rachunki dowodowe , które wspierają pojęcie dowodu analitycznego , rodzaj dowodu, którego właściwości semantyczne są odsłonięte . Kiedy wszystkie twierdzenia logiki sformalizowanej w strukturalnej teorii dowodu mają dowody analityczne, wówczas teoria dowodu może być wykorzystana do wykazania takich rzeczy jak spójność , dostarczenie procedur decyzyjnych i pozwalają na wyodrębnienie świadków matematycznych lub obliczeniowych jako odpowiedników twierdzeń, co jest zadaniem częściej powierzanym teorii modeli .

Dowód analityczny

Główny artykuł: dowód analityczny

Pojęcie dowodu analitycznego zostało wprowadzone do teorii dowodu przez Gerharda Gentzena dla rachunku sekwencyjnego ; analityczne dowody to te, które są wolne od cięć . Jego rachunek dedukcji naturalnej wspiera również pojęcie dowodu analitycznego, jak wykazał Dag Prawitz ; definicja jest nieco bardziej złożona — analitycznymi dowodami są postacie normalne , które są związane z pojęciem postaci normalnej w przepisywania terminów .

Konstrukcje i łączniki

Termin struktura w teorii dowodu strukturalnego wywodzi się z technicznego pojęcia wprowadzonego do rachunku sekwencyjnego: rachunek sekwencyjny reprezentuje ocenę dokonaną na dowolnym etapie wnioskowania za pomocą specjalnych, pozalogicznych operatorów zwanych operatorami strukturalnymi: ${\ Displaystyle A_ {1}, \ kropki, A_ {m} \ vdash B_ {1}, \ kropki, B_ {n}},$ przecinki po lewej stronie kołowrotu to operatory zwykle interpretowane jako spójniki, te po prawej jako dysjunkcje, podczas gdy sam symbol kołowrotu jest interpretowany jako implikacja. Należy jednak zauważyć, że istnieje zasadnicza różnica w zachowaniu tych operatorów i spójników logicznych są one interpretowane przez w kolejnym rachunku różniczkowym: operatory strukturalne są używane w każdej regule rachunku różniczkowego i nie są brane pod uwagę przy pytaniu, czy właściwość podformuły ma zastosowanie. Co więcej, reguły logiczne działają tylko w jedną stronę: struktura logiczna jest wprowadzana przez reguły logiczne i nie można jej wyeliminować po utworzeniu, podczas gdy operatory strukturalne można wprowadzać i eliminować w trakcie wyprowadzania.

Pomysł postrzegania cech składniowych sekwencji jako specjalnych, nielogicznych operatorów nie jest stary i został wymuszony przez innowacje w teorii dowodu: kiedy operatory strukturalne są tak proste, jak w oryginalnym rachunku sekwencyjnym Getzena, nie ma potrzeby ich analizować , ale rachunki dowodowe głębokiego wnioskowania , takie jak logika wyświetlania (wprowadzona przez Nuela Belnapa w 1982 r.), obsługują operatory strukturalne tak złożone, jak łączniki logiczne, i wymagają wyrafinowanego traktowania.

Eliminacja cięcia w rachunku sekwencyjnym

Główny artykuł: Eliminacja cięcia

Dedukcja naturalna i zgodność formuł jako typów

Główny artykuł: Odliczenie naturalne

Logiczna dwoistość i harmonia

Główny artykuł: Logiczna harmonia

hipersekwencje

Główny artykuł: hipersekwencyjny

Struktura hipersekwencyjna rozszerza zwykłą strukturę sekwencyjną na wiele zestawów sekwencyjnych, używając dodatkowego łącznika strukturalnego | (nazywany paskiem hipersekwencyjnym ), aby oddzielić różne sekwencje. Został użyty do dostarczenia rachunków analitycznych dla np. logiki modalnej , pośredniej i podstrukturalnej . Hipersekwencja jest strukturą

${\ Displaystyle \ Gamma _ {1} \ vdash \ Delta _ {1} \ mid \ kropki \ mid \ Gamma _ {n} \ vdash \ Delta _ {n} }$

gdzie $.$ zwykłą sekwencją zwaną Jeśli chodzi o sekwencje, hipersekwencje mogą być oparte na zbiorach, multisekwencjach lub sekwencjach, a komponenty mogą być sekwencjami z jednym lub wieloma wnioskami . Interpretacja formuły hipersekwencji zależy od rozważanej logiki, ale prawie zawsze jest to jakaś forma dysjunkcji. Najczęstsze interpretacje to prosta dysjunkcja

${\ Displaystyle (\ bigwedge \ Gamma _ {1} \ rightarrow \ bigvee \ Delta _ {1}) \ lor \ kropki \ lor (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})}$

dla logiki pośredniej lub jako alternatywa pudełek

${\ Displaystyle \ Box (\ bigwedge \ Gamma _ {1} \ rightarrow \ bigvee \ Delta _ {1}) \ lor \dots \lor \Box (\bigwedge \Gamma _{n}\rightarrow \bigvee \Delta _{n})}$

dla logiki modalnej.

Zgodnie z dysjunktywną interpretacją taktu hipersekwencyjnego, zasadniczo wszystkie rachunki hipersekwencyjne obejmują zewnętrzne reguły strukturalne , w szczególności regułę zewnętrznego osłabienia

${\ Displaystyle {\ Frac {\ Gamma _ {1} \ vdash \ Delta _ {1 }\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\ vdash \Delta _{n}\mid \Sigma \vdash \Pi }}}$

i reguła kontrakcji zewnętrznej

${\ Displaystyle {\ Frac {\ Gamma _ {1} \ vdash \ Delta _ {1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Gamma _{n}\vdash \Delta _{n}}{\Gamma _{1}\vdash \ Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}}}}$

Dodatkową ekspresyjność struktury hipersekwencyjnej zapewniają reguły manipulujące strukturą hipersekwencyjną. Ważnym przykładem jest zmodalizowana reguła podziału

${\ Displaystyle {\ Frac {\ Gamma _ {1} \ vdash \ Delta _ {1} \ mid \ kropki \ mid \ Gamma _ {n} \ vdash \ Delta _ {n} \ mid \ Box \ Sigma, \ Omega \vdash \Box \Pi ,\Theta }{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Box \ Sigma \vdash \Box \Pi \mid \Omega \vdash \Theta }}}$

dla logiki modalnej S5 , gdzie oznacza, że ​​każda formuła w $Sigma$ \ $}$ ma postać ${\ Displaystyle \ Box \$

Inny przykład podaje reguła komunikacji dla logiki pośredniej LC

${\ Displaystyle {\ Frac {\ Gamma _ {1} \ vdash \ Delta _ {1} \ mid \ kropki \ mid \ Gamma _ {n} \ vdash \Delta _{n}\mid \Omega \vdash A\qquad \Sigma _{1}\vdash \Pi _{1}\mid \dots \mid \Sigma _{m}\vdash \Pi _{m} \mid \Theta \vdash B}{\Gamma _{1}\vdash \Delta _{1}\mid \dots \mid \Gamma _{n}\vdash \Delta _{n}\mid \Sigma _{1 }\vdash \Pi _{1}\mid \dots \mid \Sigma _{m}\vdash \Pi _{m}\mid \Omega \vdash B\mid \Theta \vdash A}}}$

Należy zauważyć, że w regule komunikacji składowe są sekwencjami z jednym wnioskiem.

Rachunek struktur

Główny artykuł: Rachunek struktur

Zagnieżdżony rachunek sekwencyjny

Główny artykuł: zagnieżdżony rachunek sekwencyjny

Zagnieżdżony rachunek sekwencyjny to formalizacja, która przypomina rachunek dwustronny struktur.

Notatki

•   Sara Negri ; Jan von Platon (2001). Teoria dowodu strukturalnego . Wydawnictwo Uniwersytetu Cambridge. ISBN 978-0-521-79307-0 .
•   Anna Sjerp Troelstra ; Helmuta Schwichtenberga (2000). Podstawowa teoria dowodu (wyd. 2). Wydawnictwo Uniwersytetu Cambridge. ISBN 978-0-521-77911-1 .