Tolkbarhetslogik

Tolkbarhetslogiker omfattar en familj av modala logiker som utökar bevisbarhetslogik för att beskriva tolkningsbarhet eller olika relaterade metamatematiska egenskaper och relationer såsom svag tolkningsbarhet , Π ₁ -konservativitet, samtolkbarhet , tolerans , samtolerans och aritmetiska komplexiteter.

Huvudbidragsgivare till fältet är Alessandro Berarducci, Petr Hájek , Konstantin Ignatiev, Giorgi Japaridze , Franco Montagna, Vladimir Shavrukov, Rineke Verbrugge , Albert Visser och Domenico Zambella.

Exempel

Logik ILM

Språket i ILM utökar den klassiska propositionslogiken genom att lägga till den unära modala operatorn $\Box$ och den binära modala operatorn $\triangleright$ (som alltid är $\Diamond p$ definierade som $\neg \Box \neg p$ ). Den aritmetiska tolkningen av $\Box p$ är " $p$ är bevisbar i Peano-arithmetic (PA)", och $p\triangleright q$ förstås som " $PA+q$ kan tolkas i $PA+p$ ”.

Axiomschema:

1. Alla klassiska tautologier

2. $\Box (p\rightarrow q)\rightarrow (\Box p\rightarrow \Box q)$

3. $\Box (\Box p\rightarrow p)\rightarrow \Box p$

4. $\Box (p\rightarrow q)\rightarrow (p\triangleright q)$

5. $(p\triangleright q)\wedge (q\triangleright r)\högerpil (p\triangleright r)$

6. $(p\triangleright r)\wedge (q\triangleright r)\högerpil ((p\vee q)\ triangelright r)$

7. $(p\triangleright q)\rightarrow (\Diamond p\rightarrow \Diamond q)$

8. $\Diamond p\triangleright p$

9. $(p\triangleright q)\rightarrow ((p\wedge \Box r)\triangleright (q\wedge \ Box r))$

Regler för slutledning:

1. “Från $p$ och $p\rightarrow q$ avsluta $q$ ”

2. “Från $p$ avsluta $\Box p$ ”.

Fullständigheten av ILM med avseende på dess aritmetiska tolkning bevisades oberoende av Alessandro Berarducci och Vladimir Shavrukov.

Logik TOL

Språket i TOL utökar det för klassisk propositionslogik genom att lägga till modaloperatorn $\Diamond$ som tillåts ta vilken icke-tom sekvens av argument som helst. Den aritmetiska tolkningen av $\Diamond (p_{1},\ldots ,p_{n})$$(PA+p_{1},\ldots ,PA+p_{n})$ “ är en tolerant sekvens av teorier”.

Axiom (med $p,q$ står för valfri formler, ${\vec {r}},{\vec {s}}$ för alla formlersekvenser och $\Diamond ()$ identifierad med ⊤):

1. Alla klassiska tautologier

2. $\Diamond ({\vec {r}} ,p,{\vec {s}})\högerpil \Diamond ({\vec {r}},p\wedge \neg q,{\vec {s}})\vee \Diamond ({\vec {r} },q,{\vec {s}})$

3. $\Diamond (p)\högerpil \Diamond (p\wedge \neg \Diamond (p))$

4. $\Diamond ({\vec {r}},p,{\vec {s}})\högerpil \Diamond ( {\vec {r}},{\vec {s}})$

5. $\Diamond ({\vec {r}},p,{\vec {s}})\ högerpil \Diamond ({\vec {r}},p,p,{\vec {s}})$

6. $\Diamond (p,\Diamond ({\vec {r}}))\högerpil \Diamond (p\ kil \Diamond ({\vec {r}}))$

7. $\Diamond ({\vec {r}},\Diamond ({\vec {s}}))\högerpil \Diamond ({\vec {r}},{\vec {s}})$

Regler för slutledning:

1. “Från $p$ och $p\rightarrow q$ avsluta $q$ ”

2. “Från $\neg p$ avsluta $\neg \Diamond (p)$ ”.

TOL:s fullständighet med avseende på dess aritmetiska tolkning bevisades av Giorgi Japaridze .

• Giorgi Japaridze och Dick de Jongh , The Logic of Provability . I Handbook of Proof Theory , S. Buss, red., Elsevier, 1998, s. 475-546.