Predikátová logika - dedukčné kalkuly a teórie

Terminológia

Substitúcia (definovaná na predchádzajúcom cvičení) je funkcia na termoch a na formulách, budeme je označovať $σ$.

Gödelova veta o úplnosti (predikátovej logiky) (Gödel's completeness theorem) hovorí, že ak formula $φ$ platí (pravdivá v nezávisle na modely a interpretácii), potom je $φ$ dokázateľná. To znamená:
$$\text{ak}~ \quad Γ \models φ \quad \text{potom}~ \quad Γ \vdash φ.$$

Gödelova veta o neúplnosti (Gödel's incompleteness theorems) hovorí, že akýkoľvek formálny systém, ktorý dokáže vyjadriť základnú aritmetiku bude obsahovať tvrdenia (formuly), ktoré sú pravdivé ale nie je možné ich dokázať a zároveň nie je možné dokázať ani ich negácie.

Prirodzená dedukcia v predikátovej logike

Prirodzená dedukcia v predikátovej logike (systém NK) pozostáva z dedukčných pravidiel výrokovej logiky a je rozšírená o štyri pravidlá pre kvantifikátory.

Prirodzená dedukcia v predikátovej logike je konzistentná a úplná, platí: $$Γ \models φ \quad \text{vtt.}~ \quad Γ \vdash φ.$$

Eliminácia všeobecného kvantifikátora

Dedukčné pravidlo pre elimináciu všeobecného kvantifikátora:

Vychádza z jednoduchého princípu, ak $(∀x)φ$ je pravda, potom viazanú premennú $x$ je možné substituovať ľubovoľným termom $t$ a $φ[t/x]$ musí byť pravda. Vychádza zo zákona $(∀x)P(x) ⇒ P(t)$.

Zavedenie všeobecného kvantifikátora

Dedukčné pravidlo pre zavedenie všeobecného kvantifikátora:

Aby bolo možné dokázať $(∀x)φ$ je potrebné najskôr dokázať $φ[t/x]$ je pravda, pre každý prvok domény. Samozrejme, že nechceme dokázať $φ[t/x]$ pre všetky možnosti, pričom doména môže byť nekonečná. Namiesto toho postačuje ukázať, že $φ[t/x]$ je pravda pre ľubovoľný prvok $t$. To znamená, term $t$ musí byť nový (fresh), t.j. $t$ nesmie mať voľný výskyt v hypotézach, z ktorých je možné dokázať $φ[t/x]$.

Eliminácia existenčného kvantifikátora

Dedukčné pravidlo pre elimináciu existenčného kvantifikátora:

Pravidlo pre elimináciu existenčného kvantifikátora je komplexnejšie. Ak vieme, že platí $(∃x)φ[t/x]$, pre elimináciu existenčného kvantifikátora je potrebné nájsť také $t$, že $φ[t/x]$ je pravdivé. To je zabezpečené jednoduchým trikom a to tak, že vo vedľajšej vetve zavedieme novú hypotézu, kde vo $φ$ substituujeme $x$ za konkrétny prvok $t$ z ktorej dokážeme $ψ$. Term $t$ musí byť nový (fresh), t.j. $t$ nesmie mať voľný výskyt v hypotézach, z ktorých je možné dokázať $φ[t/x]$ ani $ψ$.

Zavedenie existenčného kvantifikátora

Dedukčné pravidlo pre zavedenie existenčného kvantifikátora:

Pravidlo opisuje zákon $P(a) ⇒ (∃x)P(x)$. To znamená, ak je možné dokázať, že $φ[t/x]$ je pravda, tak musí platiť tvrdenie $(∃x)φ$.

Dedukčné pravidlá prirodzenej dedukcie pre predikátovú logiku

Sekventový kalkul v predikátovej logike

Analogicky ako v prirodzenej dedukcii, pri sekventovom kalkule (systém LK) je taktiež potrebné pridať štyri nové dedukčné pravidlá pre kvantifikátory (pre každý kvantifikátor jedno pravidlo pre obe strany sekventu).

Sekventový kalkul v predikátovej logike je konzistentný a úplný, platí: $$Γ \models φ \quad \text{vtt.}~ \quad Γ \vdash φ.$$

Dedukčné pravidlá pre všeobecný kvantifikátor

• Pravidlo $(∀l)$ sa nazýva pravidlo konkretizácie. Term $t$ musí byť substituovateľný za premennú $x$ vo formule $\varphi$.
• Pravidlo $(∀r)$ sa nazýva pravidlo generalizácie. Premenná $y$ musí byť substituovateľná za premennú $x$ vo formule $\varphi$ a nemať žiadny voľný výskyt v množine predpokladov $Γ$, množine záverov $Δ$ a v $(∀x)φ$.

Dedukčné pravidlá pre existenčný kvantifikátor

• Pravidlo $(∃r)$ sa nazýva pravidlo konkretizácie. Term $t$ musí byť substituovateľný za premennú $x$ vo formule $\varphi$.
• Pravidlo $(∃l)$ sa nazýva pravidlo generalizácie. Premenná $y$ musí byť substituovateľná za premennú $x$ vo formule $\varphi$ a nemať žiadny voľný výskyt v množine predpokladov $Γ$, množine záverov $Δ$ a v $(∀x)φ$.

Dedukčné pravidlá sekventového kalkulu pre predikátovú logiku

Pravidlo identity a rezu:

Logické pravidlá:

Negácia

Konjunkcia

Disjunkcia

Implikácia

Konštanty

Kvantifikátory

Štrukturálne pravidlá:

Pravidlá zoslabenia

Pravidlá kontrakcie

Pravidlá výmeny

Predikátová logika s rovnosťou

Rozšírenie jazyka o infixný predikát rovnosti (jeho zavedenie do jazyka ako primitívum) $$t = t$$ rozširuje vyjadrovaciu silu predikátovej logiky o mnohé užitočné vlasnosti. Napríklad v jazyku bez rovnosti nie je možné vyjadriť tvrdenie, že v doméne existujú aspoň dva rôzne elementy. Formula

$$(\exists x) (\exists y) (P(x) \wedge P(y))$$ takéto tvrdenie nevyjadruje, keďže je dokázateľná napr. z predpokladu $P(a)$: $$P(a)\vdash (\exists x) (\exists y) (P(x) \wedge P(y)).$$

V prípade využitia operátora rovnosti je možné jednoducho takéto tvrdenie vyjadriť prostredníctvom nasledujúcej formuly: $$(\exists x) (\exists y) ( x \neq y \wedge P(x) \wedge P(y)).$$

Syntax predikátovej logiky s rovnosťou

Syntax jazyka je rozšírená o infixný binárny predikát rovnosti:

$$ \varphi ::=\ ...\ |\ t = t,$$

pričom platí nasledovná ekvivalencia:

$$\neg(t=s)\ \equiv\ t \neq s.$$

Operátor $=$ je reflexívny, symetricky a tranzitívny.

Prirodzená dedukcia predikátovej logiky s rovnosťou

Dedukčné pravidlá prirodzenej dedukcie pre rovnosť sú nasledovné:

Príklad: Vyjadrovacia sila rozšírenej predikátovej logiky s =

Ako bolo spomenuté, rozšírením predikátovej logiky o operátor rovnosti sa výrazne zväčšila jej vyjadrovacia sila. Okrem tautológií je možné dokázať viacero zaujímavých typov tvrdení.

Napríklad: "Ak existuje prvok $a$ pre ktorý platí vlastnosť $P$ a existuje prvok $b$ pre ktorý neplatí vlastnosť $P$, potom prvky $a$ a $b$ nie su rovnaké."

Takéto tvrdenie je možné vyjadriť v jazyku predikátovej logiky s rovnosťou ako formulu: $$P(a) \wedge \neg P(b) \Rightarrow a \neq b,$$

a následne dokázať prirodzenou dedukciou:

Hypotézy:

• $a=[a=b]$
• $b=[P(a) \wedge \neg P(b)]$

Teórie predikátovej logiky

Teória $T$ predikátovej logiky je definovaná svojim jazykom a množinou axióm, ktoré rozširujú štandardný axiomatický systém predikátovej logiky.

Dôkaz formuly $\varphi$ v teorii $T$ je

$$T \vdash \varphi$$

Robinsonova aritmetika $Q$

Robinsonova aritmetika (označovaná ako $Q$), je teória definovaná pre doménu prirodzených čísel s nulou $\mathbb{N}_0$ a určená nasledujúcim jazykom:

$$ \begin{array}{lcl} Kons & = & \{0\} \\ Func & = & \{s,+,*\} \\ Pred & = & \{=\} \\ \end{array} $$ pričom: $$ \begin{array}{l} s: \mathbb{N}_0 \rightarrow \mathbb{N}_0 \\ +,*: \mathbb{N}_0 \times \mathbb{N}_0 \rightarrow \mathbb{N}_0 \end{array} $$ kde $s$ je operácia nasledovníka čísla.

Axiómy Robinsonovej aritmetiky sú nasledovné:

$$ \begin{array}{lcl} ax1 & = & (\forall x)(\forall y)(s(x)=s(y) \Rightarrow x=y) \\ ax2 & = & (\forall x)(0\neq s(x)) \\ ax3 & = & (\forall x)(x \neq 0 \Rightarrow (\exists y)( x=s(y))) \\ ax4 & = & (\forall x)(x+0=x) \\ ax5 & = & (\forall x)(\forall y)(x+s(y) = s(x+y)) \\ ax6 & = & (\forall x)(x*0=0) \\ ax7 & = & (\forall x)(\forall y)(x*s(y) = (x*y)+x) \end{array} $$

Riešenie

• V koreni stromu sa nachádza dokazovaný výraz.
• Aplikáciou Leibnizovho pravidla bol výraz na pravej strane $3$ nahradený v ľavom predpoklade za výraz $s(1+1)$. Je potrebné si uvedomiť, že číslo $3$ je reprezentované ako nasledovník $2$. Preto v pravom predpoklade je potrebné dokázať, že $1+1=2$.
• Ľavý predpoklad je inštanciou axiómy 5 a to elimináciou všeobecných kvantifikátorov v dvoch krokoch využitím $x=1\ \text{a}\ y=1$.
• Dôkaz pravého predpokladu pokračuje analogicky až pokiaľ všetky vetvy nie sú uzavreté.

  

Konvencia: Pre skrátenie zdĺhavého dôkazu nie je potrebné explicitne uvádzať zrejme aplikácie pravidla pre elimináciu všeobecného kvantifikátora a dôkaz stačí uviesť v nasledujúcom tvare:

Pre lepšie pochopenie uvedieme aj dôkaz využitím notácie teórie Robinsonovej aritmetiky so zvýraznenou častou výrazu (červenou farbou), ktorá bola v prvom kroku substituovaná aplikáciou Leibnizovho pravidla:

Riešenie

Hypotézy:

• $a=[1=2]$