Bevisbarhetslogik

Bevisbarhetslogik är en modal logik , där operatorn box (eller "nödvändighet") tolkas som "det är bevisbart att". Poängen är att fånga föreställningen om ett bevispredikat för en rimligt rik formell teori , såsom Peano-arithmetik .

Exempel

Det finns ett antal bevisbarhetslogiker, av vilka några täcks i litteraturen som nämns i § Referenser . Grundsystemet benämns generellt som GL (för Gödel – Löb ) eller L eller K4W ( W står för well-foundedness ). Den kan erhållas genom att lägga till den modala versionen av Löbs sats till logiken K (eller K4 ).

Axiomen för GL är nämligen alla tautologier av klassisk propositionell logik plus alla formler för en av följande former:

• Distributionsaxiom : □( p → q ) → (□ p → □ q );
• Löbs axiom : □(□ p → p ) → □ p .

Och reglerna för slutledning är:

• Modus ponens : Från p → q och p avslutar q ;
• Nödvändighet : Av $\vdash$ p sluta $\vdash$ □ p .

Historia

GL - modellen var pionjär av Robert M. Solovay 1976. Sedan dess, fram till sin död 1996, var fältets främsta inspiratör George Boolos . Betydande bidrag till området har gjorts av Sergei N. Artemov , Lev Beklemishev, Giorgi Japaridze , Dick de Jongh , Franco Montagna, Giovanni Sambin, Vladimir Shavrukov, Albert Visser och andra.

Generaliseringar

Tolkbarhetslogik och Japaridzes polymodala logik presenterar naturliga förlängningar av bevisbarhetslogik.

Se även

• Hilbert–Bernays bevisbarhetsvillkor
• Tolkbarhetslogik
• Kripke semantik
• Japaridzes polymodala logik
• Löbs sats

• George Boolos , bevisbarhetens logik . Cambridge University Press, 1993.
• Giorgi Japaridze och Dick de Jongh, bevisbarhetens logik . I: Handbook of Proof Theory , S. Buss, red. Elsevier, 1998, s. 475–546.
• Sergei N. Artemov och Lev Beklemishev , bevisbarhetslogik . I: Handbook of Philosophical Logic , D. Gabbay och F. Guenthner, red., vol. 13, 2:a uppl., s. 189–360. Springer, 2005.
• Per Lindström , Bevisbarhetslogik — en kort introduktion . Theoria 62 (1996), s. 19–61.
• Craig Smoryński, Självreferens och modal logik . Springer, Berlin, 1985.
• Robert M. Solovay , ``Provability Interpretations of Modal Logic``, Israel Journal of Mathematics , Vol. 25 (1976): 287-304.
• Rineke Verbrugge , bevisbarhetslogik , från Stanford Encyclopedia of Philosophy .