Yorumlanabilirlik mantığı - Interpretability logic

Yorumlanabilirlik mantığı , yorumlanabilirliği veya çeşitli ilgili meta-matematiksel özellikleri ve zayıf yorumlanabilirlik , Π ₁ -koruma, birlikte yorumlanabilirlik , tolerans , kotolerans ve aritmetik karmaşıklıklar gibi ilişkileri tanımlamak için kanıtlanabilirlik mantığını genişleten bir modal mantık ailesini içerir .

Alana ana katkıda bulunanlar; Alessandro Berarducci, Petr Hájek , Konstantin Ignatiev, Giorgi Japaridze , Franco Montagna, Vladimir Shavrukov, Rineke Verbrugge, Albert Visser ve Domenico Zambella.

Örnekler

Mantık ILM

ILM'nin dili, tek modlu operatör ve ikili mod operatörü (her zaman olduğu gibi tanımlanır ) ekleyerek klasik önerme mantığını genişletir . Aritmetik yorumu " Peano aritmetiğinde (PA) kanıtlanabilir " ve " yorumlanabilir " olarak anlaşılır . ${\ displaystyle \ Box}$${\ displaystyle \ triangleright}$${\ displaystyle \ Diamond p}$${\ displaystyle \ neg \ Box \ neg p}$${\ displaystyle \ Box p}$${\ displaystyle p}$${\ displaystyle p \ triangleright q}$${\ displaystyle PA + q}$${\ displaystyle PA + p}$

Aksiyom şemaları:

1. Tüm klasik totolojiler

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

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

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

5. ${\ displaystyle (p \ triangleright q) \ kama (q \ triangleright r) \ rightarrow (p \ triangleright r)}$

6. ${\ Displaystyle (p \ triangleright r) \ kama (q \ triangleright r) \ rightarrow ((p \ vee q) \ triangleright r)}$

7. ${\ displaystyle (p \ triangleright q) \ sağ (\ Elmas p \ sağ \ Elmas q)}$

8. ${\ displaystyle \ Diamond p \ triangleright p}$

9. ${\ displaystyle (p \ triangleright q) \ rightarrow ((p \ kama \ Kutu r) \ triangleright (q \ kama \ Kutu r))}$

Çıkarım kuralları:

1. "Başlangıç ve bitiş " ${\ displaystyle p}$${\ displaystyle p \ rightarrow q}$${\ displaystyle q}$

2. " Sonuçtan ". ${\ displaystyle p}$${\ displaystyle \ Box p}$

ILM'nin aritmetik yorumu açısından bütünlüğü, Alessandro Berarducci ve Vladimir Shavrukov tarafından bağımsız olarak kanıtlanmıştır.

Mantık TOL

TOL'un dili, herhangi bir boş olmayan argüman dizisini almasına izin verilen mod operatörü ekleyerek klasik önermesel mantığın dilini genişletir . Aritmetik yorumu “ toleranslı bir teori dizisidir ”. ${\ displaystyle \ Diamond}$${\ displaystyle \ Diamond (p_ {1}, \ ldots, p_ {n})}$${\ displaystyle (PA + p_ {1}, \ ldots, PA + p_ {n})}$

Aksiyomlar ( herhangi bir formül, herhangi bir formül dizisi için duran ve ⊤ ile tanımlanan): ${\ displaystyle p, q}$${\ displaystyle {\ vec {r}}, {\ vec {s}}}$${\ displaystyle \ Elmas ()}$

1. Tüm klasik totolojiler

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

3. ${\ Displaystyle \ Elmas (p) \ sağ \ Elmas (p \ kama \ neg \ Elmas (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 \ Elmas (p, \ Elmas ({\ vec {r}})) \ sağ \ Elmas (p \ kama \ Elmas ({\ vec {r}}))}$

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

Çıkarım kuralları:

1. "Başlangıç ve bitiş " ${\ displaystyle p}$${\ displaystyle p \ rightarrow q}$${\ displaystyle q}$

2. " Sonuçtan ". ${\ displaystyle \ neg p}$${\ displaystyle \ neg \ Elmas (p)}$

TOL'un aritmetik yorumu açısından bütünlüğü Giorgi Japaridze tarafından kanıtlandı .

Referanslar

• Giorgi Japaridze ve Dick de Jongh , The Logic of Provability . Gelen Korumalı Teorinin Handbook , G. Buss, ed., Elsevier, 1998, s. 475-546.