Logika interpretovatelnosti - Interpretability logic

Logika interpretovatelnosti tvoří rodinu modální logika to se prodlužuje logika prokazatelnosti popsat interpretovatelnost nebo různé související metamatematické vlastnosti a vztahy jako např slabá interpretovatelnost, Π₁-konzervativnost, interpretovatelnost, tolerance, cotolerance a aritmetické složitosti.

Hlavními přispěvateli do této oblasti jsou Alessandro Berarducci, Petr Hájek, Konstantin Ignatiev, Giorgi Japaridze Franco Montagna, Vladimir Shavrukov, Rineke Verbrugge, Albert Visser a Domenico Zambella.

Příklady

Logická ILM

Jazyk ILM rozšiřuje jazyk klasické výrokové logiky přidáním unárního modálního operátoru ${ displaystyle Box}$ a binární modální operátor ${ displaystyle triangleright}$ (jako vždy, ${ displaystyle Diamond p}$ je definován jako ${ displaystyle neg Box neg p}$). Aritmetická interpretace ${ displaystyle Box p}$ je "${ displaystyle p}$ je prokazatelný v Peano Arithmetic PA “, a ${ displaystyle p triangleright q}$ je chápáno jako „${ displaystyle PA + q}$ je interpretovatelný v ${ displaystyle PA + p}$”.

Schémata axiomu:

1. Všechny klasické tautologie

2. ${ displaystyle Box (p rightarrow q) rightarrow ( Box p rightarrow Box q)}$

3. ${ displaystyle Box ( Box p rightarrow p) rightarrow Box p}$

4. ${ displaystyle Box (p rightarrow q) rightarrow (p triangleright q)}$

5. ${ displaystyle (p triangleright q) klín (q triangleright r) rightarrow (p triangleright r)}$

6. ${ displaystyle (p triangleright r) klín (q triangleright r) rightarrow ((p vee q) triangleright r)}$

7. ${ displaystyle (p triangleright q) rightarrow ( Diamond p rightarrow Diamond q)}$

8. ${ displaystyle Diamond p triangleright p}$

9. ${ displaystyle (p triangleright q) rightarrow ((p wedge Box r) triangleright (q wedge Box r))}$

Pravidla závěru:

1. „Od ${ displaystyle p}$ a ${ displaystyle p rightarrow q}$ uzavřít ${ displaystyle q}$”

2. „Od ${ displaystyle p}$ uzavřít ${ displaystyle Box p}$”.

Úplnost ILM s ohledem na její aritmetickou interpretaci nezávisle prokázali Alessandro Berarducci a Vladimir Shavrukov.

Logika TOL

Jazyk TOL rozšiřuje jazyk klasické výrokové logiky přidáním modálního operátoru ${ displaystyle Diamond}$ což může přijmout jakoukoli neprázdnou posloupnost argumentů. Aritmetická interpretace ${ displaystyle Diamond (p_ {1}, ldots, p_ {n})}$ je "${ displaystyle (PA + p_ {1}, ldots, PA + p_ {n})}$ je tolerantní sekvence teorií “.

Axiomy (s ${ displaystyle p, q}$ znamená jakékoli vzorce, ${ displaystyle { vec {r}}, { vec {s}}}$ pro libovolné sekvence vzorců a ${ displaystyle Diamond ()}$ označeno ⊤):

1. Všechny klasické tautologie

2. ${ displaystyle Diamond ({ vec {r}}, p, { vec {s}}) rightarrow Diamond ({ vec {r}}, p wedge neg q, { vec {s} }) vee Diamond ({ vec {r}}, q, { vec {s}})}$

3. ${ displaystyle Diamond (p) rightarrow Diamond (p klín neg Diamond (p))}$

4. ${ displaystyle Diamond ({ vec {r}}, p, { vec {s}}) rightarrow Diamond ({ vec {r}}, { vec {s}})}$

5. ${ displaystyle Diamond ({ vec {r}}, p, { vec {s}}) rightarrow Diamond ({ vec {r}}, p, p, { vec {s}})}$

6. ${ displaystyle Diamond (p, Diamond ({ vec {r}})) rightarrow Diamond (p klín Diamond ({ vec {r}}))}$

7. ${ displaystyle Diamond ({ vec {r}}, Diamond ({ vec {s}})) rightarrow Diamond ({ vec {r}}, { vec {s}})}$

Pravidla závěru:

1. „Od ${ displaystyle p}$ a ${ displaystyle p rightarrow q}$ uzavřít ${ displaystyle q}$”

2. „Od ${ displaystyle neg p}$ uzavřít ${ displaystyle neg Diamond (p)}$”.

Úplnost TOL s ohledem na jeho aritmetický výklad prokázal Giorgi Japaridze.

Reference

• Giorgi Japaridze a Dick de Jongh, Logika prokazatelnosti. v Příručka teorie důkazůS. Buss, ed., Elsevier, 1998, str. 475-546.