Zasada strukturalna

Aby zapoznać się z typem reguły używanej w językoznawstwie, zobacz regułę struktury fraz .

W teorii dowodu reguła strukturalna jest regułą wnioskowania , która nie odnosi się do żadnego logicznego spójnika , ale zamiast tego działa bezpośrednio na osądzie lub sekwencjach . Reguły strukturalne często naśladują zamierzone metateoretyczne właściwości logiki. Logiki zaprzeczające jednej lub kilku regułom strukturalnym są klasyfikowane jako logiki podstrukturalne .

Wspólne reguły strukturalne

Trzy wspólne reguły strukturalne to:

• Osłabienie , gdzie hipotezy lub konkluzja konkluzji może zostać rozszerzona o dodatkowych członków. $reguły$ można zapisać jako po i ${\ Displaystyle {\ Frac {\ Gamma \ vdash \ Sigma} {\ Gamma \ vdash \ Sigma, A}}}$ po prawej stronie.
• Skrócenie , w którym dwa równe (lub dające się połączyć) elementy po tej samej stronie sekwencji można zastąpić pojedynczym elementem (lub wspólną instancją). Symbolicznie: ${\ Displaystyle {\ Frac {\ Gamma, A, A \ vdash \ Sigma} {\ Gamma, A \ vdash \ Sigma}}}$ i ${\ Displaystyle {\ Frac {\ Gamma \ vdash A, A, \ Sigma} {\ Gamma \ vdash A, \ Sigma}}$ . Znany również jako faktoring w zautomatyzowanych systemach dowodzenia twierdzeń z wykorzystaniem rozdzielczości . Znana jako idempotencja implikacji w logice klasycznej.
• Wymiana , gdzie można zamienić dwóch członków po tej samej stronie sekwencji. Symbolicznie: ${\ Displaystyle {\ Frac {\ Gamma _ {1}, A \ Gamma _ { 2},B,\Gamma _{3}\vdash \Sigma }{\Gamma _{1},B,\Gamma _{2},A,\Gamma _{3}\vdash \Sigma }}}$ i ${\ Displaystyle {\ Frac {\ Gamma \ vdash \ Sigma _ {1}, A \ Sigma _ {2} ,B,\Sigma _{3}}{\Gamma \vdash \Sigma _{1},B,\Sigma _{2},A,\Sigma _{3}}}}$ . (Jest to również znane jako reguła permutacji ).

Logika bez żadnej z powyższych reguł strukturalnych interpretowałaby boki sekwencji jako czyste sekwencje ; z wymianą są multisetami ; i zarówno z kontrakcją, jak iz wymianą są zbiorami .

Nie są to jedyne możliwe reguły strukturalne. Słynna reguła strukturalna jest znana jako cięcie . Teoretycy dowodu wkładają wiele wysiłku w wykazanie, że reguły cięcia są zbędne w różnych logikach. Dokładniej, pokazano, że cięcie jest tylko (w pewnym sensie) narzędziem do skracania dowodów i nie dodaje do twierdzeń, które można udowodnić. Udane „usunięcie” reguł cięcia, znane jako eliminacja cięcia , jest bezpośrednio związane z filozofią obliczeń jako normalizacji (patrz korespondencja Curry – Howard ); często daje dobrą wskazówkę złożoność decydowania o danej logice.

Zobacz też

• Logika afiniczna - logika podstrukturalna, której teoria dowodu odrzuca strukturalną regułę kontrakcji Strony wyświetlające opisy danych wikidanych jako rozwiązanie awaryjne
• Logika liniowa - System logiki świadomej zasobów
• logika uporządkowana (logika liniowa)
• Logika istotności - system logiki matematycznej, który nakłada pewne ograniczenia na implikacje Strony wyświetlające opisy wikidanych jako rozwiązanie awaryjne
• Logika separacji