Siatka dowodowa

W teorii dowodu sieci dowodów to geometryczna metoda przedstawiania dowodów, która eliminuje dwie formy biurokracji różnicującej dowody: (A) nieistotne cechy składniowe regularnych rachunków dowodowych oraz (B) porządek reguł stosowanych w wyprowadzaniu . W ten sposób formalne właściwości dowodu tożsamości bardziej odpowiadają właściwościom pożądanym intuicyjnie. Siatki dowodowe zostały wprowadzone przez Jean-Yvesa Girarda . To odróżnia sieci dowodowe od zwykłych rachunków dowodowych, takich jak dedukcji naturalnej i rachunek sekwencyjny , gdzie te zjawiska występują.

Na przykład te dwa dowody logiki liniowej są identyczne:

, ${\ Displaystyle \ vdash}$ ZA , b , do , re ${\ Displaystyle \ vdash}$ ⅋ b , do re ⊢ { $\ displaystyle \ vdash}$ ⅋ B , do ⅋ re ZA

ZA ${\ Displaystyle \ vdash}$ ZA , b , do , re ${\ Displaystyle \ vdash}$ b , do ⅋ re ⊢ { $displaystyle \ vdash}$ ZA , ⅋ B , do ⅋ re

A odpowiadające im sieci będą takie same.

Kryteria poprawności

Znanych jest kilka kryteriów poprawności pozwalających sprawdzić, czy sekwencyjna struktura dowodowa (tj. coś, co wydaje się być siatką dowodową) jest w rzeczywistości konkretną strukturą dowodową (tj. czymś, co koduje prawidłowe wyprowadzenie w logice liniowej). Pierwszym takim kryterium jest kryterium długiej podróży, które zostało opisane przez Jean-Yvesa Girarda .

Zobacz też

• Logika liniowa
• Ludyka
• Geometria interakcji
• Spójna przestrzeń
• Głębokie wnioskowanie
• Sieci interakcji

Źródła

• Dowody i typy . Girard JY, Lafont Y i Taylor P. Cambridge Press, 1989.
• Roberto Di Cosmo i Vincent Danos, Elementarz logiki liniowej
• Sean A. Fulop, Przegląd sieci dowodowych i macierzy logiki substrukturalnej