Logika interpretowalności

Logiki interpretowalności obejmują rodzinę logik modalnych , które rozszerzają logikę dowodzenia , aby opisać interpretowalność lub różne powiązane właściwości i relacje metamatematyczne _, takie jak słaba interpretowalność , konserwatywność Π1 , współinterpretowalność , tolerancja , kotolerancja i złożoność arytmetyczna.

Głównymi współtwórcami tej dziedziny są Alessandro Berarducci, Petr Hájek , Konstantin Ignatiev, Giorgi Japaridze , Franco Montagna, Vladimir Shavrukov, Rineke Verbrugge , Albert Visser i Domenico Zambella.

Przykłady

Logiczny ILM

Język ILM rozszerza język klasycznej logiki zdań, dodając jednoargumentowy operator modalny $displaystyle$$jest$ operator modalny (jak zawsze zdefiniowany $\ Diamond p}$ jak ${\ Displaystyle \ neg \ Box \ neg p}$ ). Arytmetyczna interpretacja $}$$p$ jest do udowodnienia w arytmetyce Peano $PA + p}$ i $q} jest$ jako „ można interpretować w $Displaystyle$ ”.

Schematy aksjomatów:

1. Wszystkie tautologie klasyczne

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 \ strzałka w prawo q) \ strzałka w prawo (p \ trójkąt w prawo q)}$

5. ${\ Displaystyle (p \ trójkąt w prawo q) \ klin (q \ trójkąt w prawo r) \ strzałka w prawo (p \ trójkąt w prawo r)}$

6. ${\ Displaystyle (p \ trójkąt w prawo r) \ klin (q \ trójkąt w prawo r) \ strzałka w prawo ((p \ vee q) \ trójkąt prostokątny r)}$

7. ${\ Displaystyle (p \ trójkąt w prawo q) \ strzałka w prawo (\ Diament p \ strzałka w prawo \ Diament q)}$

8. ${\ Displaystyle \ Diament p \ trójkąt w prawo p}$

9. ${\ Displaystyle (p \ trójkąt w prawo q) \ strzałka w prawo ((p \ klin \ Pole r) \ trójkąt w prawo (q \ klin \ Pudełko r))}$

Reguły wnioskowania:

1. „Od ${\ displaystyle p}$ i ${\ displaystyle p \ rightarrow q}$ wywnioskować ${\ displaystyle q}$ ”

2. „Od wniosku $Displaystyle \ Box p}$$\$ ”.

Kompletność ILM w odniesieniu do jej arytmetycznej interpretacji została niezależnie udowodniona przez Alessandro Berarducciego i Władimira Szawrukowa.

TOL logiki

$który$ operator modalny, może przyjmować dowolną niepustą sekwencję argumentów. Arytmetyczna interpretacja ${\ Displaystyle \ Diament (p_ {1}, \ ldots, p_ {n})}$ to „ ${\ Displaystyle (PA + p_ {1}, \ ldots, PA + p_ {n})}$ to tolerancyjna sekwencja teorii”.

Aksjomaty (przy czym ${\ displaystyle p, q}$ oznacza dowolne formuły, ${\ displaystyle {\ vec {r}}, {\ vec {s}}}$ dla dowolnych sekwencji formuł i ${\ Displaystyle \ Diament ()}$ identyfikowany z ⊤):

1. Wszystkie tautologie klasyczne

2. ${\ Displaystyle \ Diament ({\ vec {r}} ,p,{\vec {s}})\rightarrow \Diament ({\vec {r}},p\klin \neg q,{\vec {s}})\vee \Diament ({\vec {r} },q,{\vec {s}})}$

3. ${\ Displaystyle \ Diament (p) \ strzałka w prawo \ Diament (p \ klin \ neg \ Diament (p))}$

4. ${\ Displaystyle \ Diament ({\ vec {r}} p, {\ vec {s}}) \ rightarrow \ Diament ( {\vec {r}},{\vec {s}})}$

5. ${\ Displaystyle \ Diament ({\ vec {r}}, p, {\ vec {s}}) \ strzałka w prawo \Diament ({\vec {r}},p,p,{\vec {s}})}$

6. ${\ Displaystyle \ Diament (p \ Diament ({\ vec {r}}}) \ rightarrow \ Diament (p \ klin \Diament ({\vec {r}}))}$

7. ${\ Displaystyle \ Diament ({\ vec {r}} \ Diament ({\ vec {s}}) \ rightarrow \Diament ({\vec {r}},{\vec {s}})}$

Reguły wnioskowania:

1. „Od ${\ displaystyle p}$ i ${\ displaystyle p \ rightarrow q}$ wywnioskować ${\ displaystyle q}$ ”

2. „Od ${\ Displaystyle \ neg p}$ zakończyć ${\ Displaystyle \ neg \ diament (p)}$ ”.

Kompletność TOL w odniesieniu do jego interpretacji arytmetycznej została udowodniona przez Giorgi Japaridze .

• Giorgi Japaridze i Dick de Jongh , Logika możliwości udowodnienia . W Handbook of Proof Theory , S. Buss, red., Elsevier, 1998, s. 475-546.