Japaridzes polymodala logik

Japaridzes polymodala logik (GLP) är ett system för bevisbarhetslogik med oändligt många bevisbarhetsmodaliteter . Detta system har spelat en viktig roll i vissa tillämpningar av bevisbarhetsalgebror i bevisteori och har studerats omfattande sedan slutet av 1980-talet. Den är uppkallad efter Giorgi Japaridze .

Språk och axiomatisering

GLP-språket utökar språket för klassisk propositionslogik genom att inkludera den oändliga serien $[0],[1],[2],...$ av nödvändighetsoperatorer. Deras dubbelmöjlighetsoperatorer $<0>,<1>,<2>,...$ definieras av $< n > p = \neg[n]\neg p$ .

Axiomen för GLP är alla klassiska tautologier och alla formler av någon av följande former:

$[n](p \to q) \to ([n] p \to [n] q)$
$[n]([n] p \to p) \to [n] sid$
$[n] p \to [n +1] sid$
$< n > p \to [n +1]< n > p$

Och reglerna för slutledning är:

Av $p$ och $p \to q$ avsluta $q$
Av $p$ sluta $[0] sid$

Bevisbarhetssemantik

Betrakta en tillräckligt stark första ordningens teori $T$ som Peano Arithmetic $PA$ . Definiera serierna $0 T, T 1, T 2,...$ av teorier enligt följande:

$T 0$ är $T$
$T n +1$ är förlängningen av $T n$ genom de ytterligare axiomen $\forall xF (x)$ för varje formel $F (x)$ så att $T n$ bevisar alla formlerna $F (0), F (1), F (2), ...$

För varje $n$ , låt $Pr n (x)$ vara en naturlig aritmetisering av predikatet $" x$ är Gödeltalet för en mening bevisbar i $T n "$ .

En realisering är en funktion $*$ som skickar varje icke-logisk atom $a$ i språket i GLP till en mening $a *$ i språket i $T$ . Den sträcker sig till alla formler för GLP-språket genom att föreskriva att $*$ pendlar med de booleska kopplingarna, och att $([n] F)*$ är $Pr n (' F *')$ , där $' F *'$ står för (siffran för ) Gödeltalet för $F *$ .

En aritmetisk fullständighetssats för GLP säger att en formel $F$ är bevisbar i GLP om och endast om, för varje tolkning $*$ , meningen $F *$ är bevisbar i $T$ .

Ovanstående förståelse av serierna $0 T, T 1, T 2,...$ av teorier är inte den enda naturliga förståelsen som ger sundheten och fullständigheten av GLP. Till exempel kan varje teori $T n$ förstås som $T$ utökad med alla sanna $Π n$ meningar som ytterligare axiom. George Boolos visade att GLP förblir sund och komplett med analys ( andra ordningens aritmetik ) i rollen som basteorin $T$ .

Annan semantik

GLP har visat sig vara ofullständig med avseende på någon klass av Kripke-ramar .

En naturlig topologisk semantik av GLP tolkar modaliteter som derivatoperatorer av ett polytopologiskt utrymme . Sådana utrymmen kallas GLP-rum närhelst de uppfyller alla GLP:s axiom. GLP är komplett med avseende på klassen för alla GLP-utrymmen.

Beräkningskomplexitet

Problemet med att vara ett teorem för GLP är PSPACE-komplett . Så är samma problem begränsat till endast variabelfria formler av GLP.

Historia

GLP, under namnet GP, introducerades av Giorgi Japaridze i sin doktorsavhandling "Modal Logical Means of Investigating Provability" ( Moscow State University , 1986) och publicerades två år senare tillsammans med (a) fullständighetssatsen för GLP med avseende på dess bevisbarhetstolkning (Beklemishev kom senare med ett enklare bevis på samma sats) och (b) ett bevis på att Kripke-ramar för GLP inte existerar. Beklemishev genomförde också en mer omfattande studie av Kripke-modeller för GLP. Topologiska modeller för GLP studerades av Beklemishev, Bezhanishvili, Icard och Gabelaia. Beslutbarheten av GLP i polynomutrymme bevisades av I. Shapirovsky, och PSPACE-hårdheten för dess variabelfria fragment bevisades av F. Pakhomov. Bland de mest anmärkningsvärda tillämpningarna av GLP har varit dess användning i bevisteoretiskt analys av Peano-aritmetik , utarbetande av ett kanoniskt sätt för att återställa ordningsnotation upp till $ɛ 0$ från motsvarande algebra, och konstruera enkla kombinatoriska oberoende uttalanden (Beklemishev ).

En omfattande undersökning av GLP i samband med bevisbarhetslogik i allmänhet gavs av George Boolos i hans bok The Logic of Provability .

Litteratur

L. Beklemishev, "Provabilitetsalgebror och bevisteoretiska ordtal, I" . Annals of Pure and Applied Logic 128 (2004), s. 103–123.
L. Beklemishev, J. Joosten och M. Vervoort, "En finitär behandling av det slutna fragmentet av Japaridzes bevisbarhetslogik" . Journal of Logic and Computation 15 (2005), nr 4, s. 447–463.
L. Beklemishev, "Kripke semantik för bevisbarhetslogik GLP" . Annals of Pure and Applied Logic 161, 756–774 (2010).
L. Beklemishev, G. Bezhanishvili och T. Icar, "Om topologiska modeller av GLP". Ways of proof theory, Ontos Mathematical Logic , 2, eds. R. Schindler, Ontos Verlag, Frankfurt, 2010, s. 133–153.
L. Beklemishev, "Om Craig-interpolationen och fastpunktsegenskaperna hos GLP". Bevis, kategorier och beräkningar . S. Feferman et al., red., College Publications 2010. s. 49–60.
L. Beklemishev, "Ordinell fullständighet av bimodal bevisbarhetslogik GLB" . Lecture Notes in Computer Science 6618 (2011), s. 1–15.
L. Beklemishev, "Ett förenklat bevis på aritmetisk fullständighetsteorem för bevisbarhetslogik GLP" . Proceedings of the Steklov Institute of Mathematics 274 (2011), s. 25–33.
L. Beklemishev och D. Gabelaia, "Topologisk fullständighet av bevisbarhetslogik GLP" . Annals of Pure and Applied Logic 164 (2013), s. 1201–1223.
G. Boolos, "Den analytiska fullständigheten av Japaridzes polymodala logik" . Annals of Pure and Applied Logic 61 (1993), s. 95–111.
G. Boolos, The Logic of Provability Cambridge University Press, 1993.
EV Dashkov, "Om det positiva fragmentet av den polymodala bevisbarhetslogiken GLP". Matematiska anteckningar 2012; 91:318–333.
D. Fernandez-Duque och J.Joosten, "Well-orders in the transfinite Japaridze algebra" ^{[ död länk ]} . Logic Journal of the IGPL 22 (2014), s. 933–963.
G. Japaridze, "Provbarhetens polymodala logik" . Intensionslogik och teoriers logiska struktur . Metsniereba, Tbilisi, 1988, s. 16–48 (ryska).
F. Pakhomov, "Om komplexiteten i det slutna fragmentet av Japaridzes bevisbarhetslogik" . Arkiv för matematisk logik 53 (2014), s. 949–967.
DS Shamkanov, "Interpolationsegenskaper för bevisbarhetslogik GL och GLP" . Proceedings of the Steklov Institute of Mathematics 274 (2011), s. 303–316.
I. Shapirovsky, "PSPACE-beslutbarhet av Japaridzes polymodala logik" . Advances in Modal Logic 7 (2008), s. 289–304.