Logika dla informatyków/Język logiki pierwszego rzędu

Język logiki pierwszego rzędu.

Język logiki pierwszego rzędu <ref name="dwa">Logika pierwszego rzędu nazywana jest też rachunkiem predykatów lub rachunkiem kwantyfikatorów.</ref> można traktować jak rozszerzenie rachunku zdań, pozwalające formułować stwierdzenia o zależnościach pomiędzy obiektami indywiduowymi (np. relacjach i funkcjach). Dzięki zastosowaniu kwantyfikatorów, odwołujących się do całej zbiorowości rozważanych obiektów, można w logice pierwszego rzędu wyrażać własności struktur relacyjnych oraz modelować rozumowania dotyczące takich struktur. Do zestawu symboli rachunku zdań dodajemy następujące nowe składniki syntaktyczne:

• Symbole operacji i relacji (w tym symbol równości $=$);
• Zmienne indywiduowe, których wartości mają przebiegać rozważane dziedziny;
• Kwantyfikatory, wiążące zmienne indywiduowe w formułach.

Składnia

Symbole operacji i relacji są podstawowymi składnikami do budowy najprostszych formuł, tzw. formuł atomowych. Z tego względu w języku pierwszego rzędu rezygnuje się ze zmiennych zdaniowych.

Definicja 2.1

Przez sygnaturę $\mathrm{\Sigma }$ rozumieć będziemy rodzinę zbiorów ${\mathrm{\Sigma }}_n^F$, dla $n\ge 0$ oraz rodzinę zbiorów ${\mathrm{\Sigma }}_n^R$, dla $n\ge 1$. Elementy ${\mathrm{\Sigma }}_n^F$ będziemy nazywać symbolami operacji $n$-argumentowych, a elementy ${\mathrm{\Sigma }}_n^R$ będziemy nazywać symbolami relacji $n$-argumentowych. Przyjmujemy, że wszystkie te zbiory są parami rozłączne. Umawiamy się też, że znak równości $=$ nie należy do $\mathrm{\Sigma }$. Symbol ten nie jest zwykłym symbolem relacyjnym, ale jest traktowany na specjalnych prawach. W praktyce, sygnatura zwykle jest skończona i zapisuje się ją jako ciąg symboli. Np. ciąg złożony ze znaków $+,\cdot ,0,1$ (o znanej każdemu liczbie argumentów) tworzy sygnaturę języka teorii ciał.

Definicja 2.2

Ustalamy pewien nieskończony przeliczalny zbiór $X$ symboli, które będziemy nazywać zmiennymi indywiduowymi i zwykle oznaczać symbolami $x,y,z$. Zbiór termów $T_{\mathrm{\Sigma }}(X)$ nad sygnaturą $\mathrm{\Sigma }$ i zbiorem zmiennych $X$ definiujemy indukcyjnie:

• Zmienne indywiduowe są termami.
• Dla każdego $n\ge 0$ i każdego symbolu operacji $f\in {\mathrm{\Sigma }}_n^F$, jeśli $t_1,\dots ,t_n$ są termami, to $f(t_1,\dots ,t_n)$ jest też termem.

Zauważmy, że z powyższej definicji wynika, iż stałe sygnatury $\mathrm{\Sigma }$ (czyli symbole operacji zeroargumentowych) są termami.

Definicja 2.3

Dla każdego termu $t\in T_{\mathrm{\Sigma }}(X)$ definiujemy zbiór Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle \fv t} zmiennych występujących w $t$. Definicja jest indukcyjna:

• $FV(x)=\{x\}$.
• Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle FV(f(t_1,\ldots, t_n))=\bigcup_{i=1}^n \fv{t_i}} .

Definicja 2.4

Następnie zdefiniujemy formuły atomowe języka pierwszego rzędu.

• Symbol fałszu $\mathrm{\perp }$ jest formułą atomową.
• Dla każdego $n\ge 1$, każdego symbolu $r\in {\mathrm{\Sigma }}_n^R$ relacji $n$-argumentowej oraz dla dowolnych termów $t_1,\dots ,t_n\in T_{\mathrm{\Sigma }}(X)$, napis $r(t_1,\dots ,t_n)$ jest formułą atomową.
• Dla dowolnych termów $t_1,t_2$, napis $(t_1=t_2)$ jest formułą atomową.

Konwencja: Niektóre dwuargumentowe symbole relacyjne (np. $\le$) i funkcyjne (np. Parser nie mógł rozpoznać (błąd składni): {\displaystyle +,\cdot&nbsp;} ) są zwyczajowo pisane pomiędzy argumentami. Na przykład formułę atomową $\le (x,y)$ zwykle piszemy jako "$x\le y$".

Definicja 2.5

Formuły nad sygnaturą $\mathrm{\Sigma }$ i zbiorem zmiennych indywiduowych $X$ definiujemy indukcyjnie.

• Każda formuła atomowa jest formułą.
• Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi,\psi} są formułami, to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\to\psi)} jest też formułą.
• Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formułą, a $x\in X$ jest zmienną indywiduową, to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\var\varphi} jest też formułą.

Ponadto, dla każdej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} definiujemy zbiór zmiennych wolnych Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV(\var\varphi)} występujących w tej formule:

• $FV\mathrm{\perp }=\mathrm{\varnothing }$;
• $FVr(t_1,\dots ,t_n)=\bigcup _{i=1}^{n}FV{t}_i$;
• Parser nie mógł rozpoznać (nieznana funkcja „\cupFV”): {\displaystyle FV{t_1=t_2}=FV{t_1}\cupFV{t_2}} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV{\var\varphi\to\psi}=FV\var\varphi\cup FV\psi} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV{\forall x\var\varphi}=FV\var\varphi-\{x\}} .

Formułę bez kwantyfikatorów nazywamy formułą otwartą. Natomiast formuła bez zmiennych wolnych nazywa się zdaniem lub formułą zamkniętą.

Negację, koniunkcję, alternatywę, symbol prawdy i równoważność formuł definiujemy podobnie jak w przypadku rachunku zdań. Kwantyfikator egzystencjalny zdefiniujemy jako skrót notacyjny przy pomocy uogólnionego prawa De Morgana:

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \exists x\var\varphi \hspace{1cm} \textrm{oznacza} \hspace{1cm} \neg\forall x \neg\var\varphi. }

Zmienne wolne a zmienne związane. W Definicji 2.5 nie zakładamy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle x\in FV\var\varphi} . Zauważmy też, że zmienna $x$ może występować w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , podczas gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle x\not\in FV\var\varphi} . Przez wystąpienie zmiennej indywiduowej $x$ rozumiemy tu zwykłe pojawienie się $x$ w jakimkolwiek termie w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . I tak na przykład w formule <ref name="trzy">Zakładamy tu, że $s$ oraz $r$ są symbolami relacji.</ref> $\mathrm{\exists }x\mathrm{\forall }u(r(x,y)\to \mathrm{\forall }y\mathrm{\exists }xs(x,y,z))$ zmienna $u$ nie występuje, podczas gdy $x$ i $y$ wystepują po dwa razy, a $z$ występuje jeden raz.

Bardzo ważną rzeczą jest rozróżnienie wystąpień zmiennych wolnych i związanych w formułach. Wszystkie wystąpienia zmiennych w formułach atomowych są wolne. Wolne (związane) wystąpienia w formułach Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i $\psi$ pozostają wolne (związane) w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\to\psi} . Wszystkie wolne wystąpienia $x$ w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} stają się związanymi wystąpieniami w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \exists x\var\varphi} (związanymi przez dopisanie kwantyfikatora $\mathrm{\exists }$), a charakter pozostałych wystąpień jest taki sam w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \exists x\var\varphi} .

Przykładowo w formule $\mathrm{\exists }x\mathrm{\forall }u(r(x,\underset{\_}{y})\to \mathrm{\forall }y\mathrm{\exists }xs(x,y,z))$ podkreślone wystąpienie $y$ jest wolne, a nie podkreślone jest związane. Obydwa wystąpienia $x$ są zwiazane, ale przez różne kwantyfikatory.

Na koniec uwaga o nazwach zmiennych związanych. Rozróżnienie pomiędzy zmiennymi wolnymi a związanymi jest analogiczne do rozróżnenia pomiedzy identyfikatorami lokalnymi a globalnymi w językach programowania. Globalne identyfikatory, widoczne na zewnątrz, odpowiadają zmiennym wolnym, podczas gdy lokalne identyfikatory (związane np. deklaracją w bloku) nie są widoczne na zewnątrz zakresu ich deklaracji. Intuicyjnie naturalne jest oczekiwanie, że zmiana zmiennej związanej na inną zmienną (tak aby nie wprowadzić konfliktu wynikającego ze zmiany struktury wiązań) nie powinna zmieniać znaczenia formuły.<ref name="cztery">Taka zamiana zmiennych bywa nazywana $\alpha$-konwersją.</ref> Tak w istocie będzie, jak się przekonamy poniżej (Fakt 2.12).

Semantyka formuł

Niech $\mathrm{\Sigma }$ będzie sygnaturą. Struktura $\mathfrak{𝔄}$ nad sygnaturą $\mathrm{\Sigma }$ (lub po prostu $\mathrm{\Sigma }$-struktura) to niepusty zbiór $A$, zwany nośnikiem, wraz z interpretacją każdego symbolu operacji $f\in {\mathrm{\Sigma }}_n^F$ jako funkcji $n$ argumentowej Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle f^{\strA}:A^n\to A} oraz każdego symbolu relacji $r\in {\mathrm{\Sigma }}_n^R$ jako relacji $n$-argumentowej $r^{\mathfrak{𝔄}}\subseteq A^n$. (Na przykład, jeśli $\mathrm{\Sigma }$ składa się z jednego symbolu relacji dwuargumentowej, to każdy graf zorientowany jest $\mathrm{\Sigma }$-strukturą.) W praktyce, strukturę relacyjną przedstawia się jako krotkę postaci Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathfrak A = \<A, f_1^\mathfrak A,\ldots,f_n^\mathfrak A,r_1^\mathfrak A,\ldots, r_m^\mathfrak A\>} , gdzie $f_1,\dots ,f_n,r_1,\dots ,r_m$ są wszystkimi symbolami danej sygnatury. Często, gdy będzie jasne z kontekstu z jaką strukturą mamy do czynienia, będziemy opuszczać nazwę struktury i pisać po prostu $r,f,\dots$ zamiast $r^{\mathfrak{𝔄}},f^{\mathfrak{𝔄}},\dots$

Wartościowaniem w $\mathrm{\Sigma }$-strukturze $\mathfrak{𝔄}$ nazwiemy dowolną funkcję $\varrho :X\to A$. Dla wartościowania $\varrho$, zmiennej $x\in X$ oraz elementu $a\in A$ definiujemy nowe wartościowanie ${\varrho }_x^a:X\to A$, będące modyfikacją wartościowania $\varrho$ na argumencie $x$, w następujący sposób,

Parser nie mógł rozpoznać (nieznana funkcja „\begin{cases}”): {\displaystyle \varrho_x^a(y)= \begin{cases} \varrho(y)}, \mbox{jeśli} y\neq x \\ a, \mbox{w przeciwnym wypadku} \end{cases}}

Najpierw zdefiniujemy znaczenie termów. Wartość termu $t\in T_{\mathrm{\Sigma }}(X)$ w $\mathrm{\Sigma }$-strukturze $\mathfrak{𝔄}$ przy wartościowaniu $\varrho$ oznaczamy przez ${[[t]]}_{\varrho }^{\mathfrak{𝔄}}$, lub $[[t]]\varrho$, gdy $\mathfrak{𝔄}$ jest znane. Definicja jest indukcyjna:

• $[[x]{]}_{\varrho }^{\mathfrak{𝔄}}=\varrho (x)$.
• $[[f(t_1,\dots ,t_n)]{]}_{\varrho }^{\mathfrak{𝔄}}=f^{\mathfrak{𝔄}}([[t_1]]{\mathfrak{𝔄}}_{\varrho },\dots ,[[t_1]{]}_{\varrho }^{\mathfrak{𝔄}})$.

Znaczenie formuł definiujemy poniżej. Napis

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A , \varrho ) \vDash \var\varphi. }

czytamy: formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest spełniona w strukturze $\mathfrak{𝔄}$ przy wartościowaniu $\varrho$. Zakładamy tu, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} oraz $\mathfrak{𝔄}$ są nad tą samą sygnaturą. Spełnianie definiujemy przez indukcję ze względu na budowę formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} .

• Nie zachodzi $(\mathfrak{𝔄},\varrho )\models \mathrm{\perp }$.
• Dla dowolnego $n\ge 1$, $r\in {\mathrm{\Sigma }}_n^R$ oraz dla dowolnych termów $t_1,\dots ,t_n$, przyjmujemy, że $(\mathfrak{𝔄},\varrho )\models r(t_1,\dots ,t_n)$ wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \langle [[t_1]]^{\mathfrak A}_\varrho, \ldots [[t_2]]^{\mathfrak A}_\varrho \rangle \in r^{\mathfrak A } .
• $(\mathfrak{𝔄},\varrho )\models t_1=t_2$, wtedy i tylko wtedy, gdy $[[t_1]{]}_{\varrho }^{\mathfrak{𝔄}}=[[t_2]{]}_{\varrho }^{\mathfrak{𝔄}}$
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A , \varrho ) \vDash \var\varphi \to \psi } , gdy nie zachodzi $(\mathfrak{𝔄},\varrho )\models \phi$ lub zachodzi $(\mathfrak{𝔄},\varrho )\models \psi$
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A , \varrho ) \vDash \forall x\var\varphi } wtedy i tylko wtedy, gdy dla dowolnego $a\in A$ zachodzi $(\mathfrak{𝔄},{\varrho }_x^a)\models \phi$

Nastepujące twierdzenie pokazuje, że spełnianie formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} w dowolnej strukturze zależy jedynie od wartości zmiennych wolnych Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle FV(\var\varphi)} . Uzasadnia ono następującą konwencję notacyjną: napiszemy na przykład Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle ( \mathfrak A , x:a,y:b ) \vDash \var\varphi } zamiast Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A, \varrho )\vDash \var\varphi } , gdy $\varrho (x)=a$ i $\varrho (y)=b$, a przy tym wiadomo, że w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} występują wolno tylko zmienne $x$ i $y$. Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest zdaniem, to wartościowanie można całkiem pominąć.

Fakt 2.6

Dla dowolnej $\mathrm{\Sigma }$-struktury $\mathfrak{𝔄}$ i dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , jeśli wartościowania $\varrho$ i ${\varrho }^{\prime }$ przyjmują równe wartości dla wszystkich zmiennych wolnych w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , to

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho) \vDash\var\varphi } wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle ( \mathfrak A, \varrho') \vDash\var\varphi. }

Dowód

Ćwiczenie.

Prawdziwość i spełnialność formuł

Powiemy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi } jest spełnialna w $\mathfrak{𝔄}$, gdy istnieje wartościowanie $\varrho$ w strukturze $\mathfrak{𝔄}$ takie, że zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho) \vDash\var\varphi} . Formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest spełnialna, gdy istnieje struktura $\mathfrak{𝔄}$, w której Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest spełnialna.

Formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest prawdziwa w $\mathfrak{𝔄}$, gdy dla każdego wartościowania $\varrho$ w $\mathfrak{𝔄}$ zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho)\vDash\var\varphi} . W tym przypadku mówimy też, że $\mathfrak{𝔄}$ jest modelem dla formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} (oznaczamy to przez Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A\models\var\varphi} ). Dla zbioru formuł $\mathrm{\Gamma }$ i $\mathrm{\Sigma }$-struktury $\mathfrak{𝔄}$ powiemy, że $\mathfrak{𝔄}$ jest modelem dla $\mathrm{\Gamma }$ (piszemy $\mathfrak{𝔄}\models \mathrm{\Gamma }$), gdy dla każdej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\in\Gamma} , zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \mathfrak A\models\var\varphi} . Formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest tautologią (oznaczamy to przez Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi} ), gdy jest ona prawdziwa w każdej $\mathrm{\Sigma }$-strukturze.

Oczywiście jeśli weźmiemy dowolną tautologię rachunku zdań, to po podstawieniu na miejsce zmiennych zdaniowych dowolnych formuł logiki pierwszego rzędu dostaniemy tautologię logiki pierwszego rzędu. Poniżej podajemy przykłady tautologii logiki pierwszego rzędu, których nie da się w ten sposób otrzymać.

Fakt 2.7

Następujące formuły są tautologiami logiki pierwszego rzedu:

1. $\mathrm{\forall }x(\phi \to \psi )\to (\mathrm{\forall }x\phi \to \mathrm{\forall }x\psi )$.
2. Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle \varphi\to \forall x \varphi$, o ile $x\not\in\fv\varphi} .
3. $\mathrm{\forall }x\phi \to \phi$.
4. $x=x$.
5. $x_1=y_1\to (x_2=y_2\to \cdots \to (x_n=y_n\to f(x_1,\dots ,x_n)=f(y_1,\dots ,y_n))\cdots )$, dla $f\in {\mathrm{\Sigma }}_n^F$, $n\ge 0$.
6. $x_1=y_1\to (x_2=y_2\to \cdots \to (x_n=y_n\to r(x_1,\dots ,x_n)\to r(y_1,\dots ,y_n))\cdots )$, dla $r\in {\mathrm{\Sigma }}_n^R,n\ge 1$.

Dowód

Aby się przekonać, że formuła (1) jest tautologią, rozpatrzmy dowolną strukturę $\mathfrak{𝔄}$ i jakieś wartościowanie $\varrho$. Załóżmy najpierw, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho) \vDash \forall x(\var\varphi\to\psi)} oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho) \vDash \forall x\,\var\varphi } . Oznacza to, że dla dowolnego $a\in A$ zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho^a_x) \vDash \var\varphi } oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho^a_x) \vDash \var\varphi\to\psi} . Musi więc zajść $(\mathfrak{𝔄},{\varrho }_x^a)\models \psi$ Z dowolności $a$ mamy $(\mathfrak{𝔄},\varrho )\models \mathrm{\forall }x\psi$, a stąd Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\mathfrak A,\varrho) \vDash \forall x(\var\varphi\to\psi) \to (\forall x \varphi \to \forall x \psi)} .

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle ( \mathfrak A, \varrho) \not\models \forall x(\var\varphi\to\psi)} lub $(\mathfrak{𝔄},\varrho )\models ̸\mathrm{\forall }x\phi$, to nasza formuła jest spełniona przez $\varrho$ wprost z definicji. Uzasadnienie części (3-6) pozostawiamy czytelnikowi.

Ponadto mamy następujący

Fakt 2.8

Dla dowolnej tautologii Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i dowolnej zmiennej $x$, formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\var\varphi} jest też tautologią.

Dowód

Ćwiczenie.

Uzasadnienie, że dana formuła jest tautologią, polega na analizie jej spełniania w dowolnych modelach (por. Fakt 2.7). Natomiast wykazanie, że tak nie jest, polega na podaniu odpowiedniego kontrprzykładu. Takiego jak ten:

Przykład 2.9

Zdanie $(\mathrm{\forall }xp(x)\to \mathrm{\forall }xq(x))\to \mathrm{\forall }x(p(x)\to q(x))$ nie jest tautologią. Rozpatrzmy bowiem model $\mathfrak{𝔄}=<\mathbb{\mathbb{N}},p^{\mathfrak{𝔄}},q^{\mathfrak{𝔄}}>$, w którym:

• $n\in p^{\mathfrak{𝔄}}$, wtedy i tylko wtedy, gdy $n$ jest parzyste;
• $n\in q^{\mathfrak{𝔄}}$, wtedy i tylko wtedy, gdy $n$ jest nieparzyste;

Ponieważ $p^{\mathfrak{𝔄}}\ne \mathbb{\mathbb{N}}$, więc $\mathfrak{𝔄}\models ̸\mathrm{\forall }xp(x)$. (Mamy tu do czynienia ze zdaniem, więc wartościowanie jest nieistotne i dlatego je pomijamy.) Stąd otrzymujemy $\mathfrak{𝔄}\models \mathrm{\forall }xp(x)\to \mathrm{\forall }xq(x)$. Z drugiej strony $\mathfrak{𝔄}\models ̸\mathrm{\forall }x(p(x)\to q(x))$, ponieważ $(\mathfrak{𝔄},x:2)\models ̸p(x)\to q(x)$. Rzeczywiście, $2\in p^{\mathfrak{𝔄}}-q^{\mathfrak{𝔄}}$.

Podstawianie termów

Dla formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , termu $t$ i zmiennej $x$, napis Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi (t/x)} oznacza wynik podstawienia $t$ na wszystkie wolne wystąpienia $x$ w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Wykonywanie takiego podstawienia bez dodatkowych zastrzeżeń może prowadzić do kłopotów. Na przykład sens formuł $\mathrm{\forall }y(y\le x)$ oraz $\mathrm{\forall }z(z\le x)$ jest taki sam. Tymczasem "naiwne" podstawienie $y$ w miejsce $x$ w obu tych formułach daje w wyniku odpowiednio $\mathrm{\forall }y(y\le y)$ i $\mathrm{\forall }z(z\le y)$, a te dwie formuły znaczą całkiem co innego. Przyczyną jest to, że w pierwszym przypadku zmienną $y$ wstawiono w zasięg kwantyfikatora $\mathrm{\forall }y$.

Źródłem problemu w powyższym przykładzie było to, że po wykonaniu podstawienia pojawiały się nowe wiązania kwantyfikatorem. Sugeruje to następującą definicję. Powiemy, że term $t$ jest dopuszczalny dla zmiennej $x$ w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} (lub że podstawienie Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst\var\varphi tx} jest dopuszczalne, jeśli dla każdej zmiennej $y$ występującej w $t$, żadne wolne wystąpienie $x$ w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} nie jest zawarte w zasięgu kwantyfikatora $\mathrm{\forall }y$ lub $\mathrm{\exists }y$. Mamy więc następującą indukcyjną definicję dopuszczalnego podstawienia,<ref name="piec">Podstawianie termu $t$ do termu $s$ na miejsce zmiennej $x$ oznaczamy podobnie: $s(t/x)$. Takie podstawienie jest zawsze wykonalne.</ref> w której każda lewa strona jest dopuszczalna pod warunkiem, że prawa strona jest dopuszczalna.

• $\mathrm{\perp }(t/x)=\mathrm{\perp }$, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle x\not\in FV(\var\varphi)} ;
• $r(t_1,\dots ,t_n)(t/x)=r(t_1(t/x),\dots ,t_n(t/x))$;
• $(t_1=t_2)(t/x)=(t_1(t/x)=t_2(t/x)$;
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\to\psi)(t/x) = \var\varphi(t/x)\to\psi(t/x)} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\forall x\var\varphi)(t/x) = \forall x\var\varphi} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\forall y\var\varphi)(t/x) = \forall y\var\varphi(t/x)} , gdy $y=x$, oraz $y\in ̸FV(t)$;
• W pozostałych przypadkach podstawienie jest niedopuszczalne.

W dalszym ciągu będziemy rozważać jedynie podstawienia dopuszczalne.

Lemat 2.10 (o podstawieniu)

Niech $\mathfrak{𝔄}$ będzie dowolną strukturą oraz $\varrho :X\to A$ dowolnym wartościowaniem w $\mathfrak{𝔄}$. Niech $t$ będzie dowolnym termem.

1. Dla dowolnego termu $s$ i zmiennej $x$ mamy $[[s(t/x)]{]}_{\varrho }^{\mathfrak{𝔄}}=[[s]{]}_{{\varrho }_x^a}^{\mathfrak{𝔄}}$ gdzie $a=[[t]{]}_{\varrho }^{\mathfrak{𝔄}}$.
2. Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , jeśli term $t$ jest dopuszczalny dla $x$ w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , to

$(\mathfrak{𝔄},\varrho )\models \phi (t/x)$ wtedy i tylko wtedy, gdy $(\mathfrak{𝔄},{\varrho }_x^a)\models \phi$ gdzie $a=[[t]{]}_{\varrho }^{\mathfrak{𝔄}}$.

Dowód

Część 1 dowodzimy przez indukcję ze względu na budowę termu $s$. Jeśli $s$ jest zmienną $x$, to obie strony są równe $[[t]{]}_{\varrho }^{\mathfrak{𝔄}}$. Jeśli $s$ jest zmienną $y$ (różną od $x$), to obie strony są równe $\varrho (y)$. Jeśli $s$ jest postaci $f(s_1,\dots ,s_n)$, to mamy następujące równości.

$[[s(t/x)]{]}_{\varrho }^{\mathfrak{𝔄}}=[[f(s_1(t/x),\dots ,s_n(t/x))]{]}_{\varrho }^{\mathfrak{𝔄}}$

$=f^{\mathfrak{𝔄}}([[s_1(t/x)]{]}_{\varrho }^{\mathfrak{𝔄}},\dots ,[[s_n(t/x)]{]}_{\varrho }^{\mathfrak{𝔄}})$
$=f^{\mathfrak{𝔄}}([[s_1]{]}_{{\varrho }_x^a}^{\mathfrak{𝔄}},\dots ,[[s_n]{]}_{{\varrho }_x^a}^{\mathfrak{𝔄}})$
$=[[f(s_1,\dots ,s_n)]{]}_{{\varrho }_x^a}^{\mathfrak{𝔄}}=[[s]{]}_{{\varrho }_x^a}^{\mathfrak{𝔄}}$

Dowód części 2 przeprowadzamy przez indukcję ze względu na budowę formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi}  jest postaci $\mathrm{\perp }$, to teza jest oczywista. Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formułą atomową, to tezę natychmiast dostajemy z wyżej udowodnionej części 1. Na przykład, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest postaci $s_1=s_2$ to mamy:

$(\mathfrak{𝔄},\varrho )\models \phi (t/x)$ wtedy i tylko wtedy, gdy $[[s_1(t/x)]{]}_{\varrho }^{\mathfrak{𝔄}}=[[s_1(t/x)]{]}_{\varrho }^{\mathfrak{𝔄}}$

wtedy i tylko wtedy, gdy $[[s_1]{]}_{{\varrho }_x^a}^{\mathfrak{𝔄}}=[[s_2]{]}_{{\varrho }_x^a}^{\mathfrak{𝔄}}$
wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\varrhp”): {\displaystyle (\mathfrak A, \varrhp^a_x) \models s_1 = s_2 }

Druga z powyższych równoważności wynika z części 1.

Krok indukcyjny dla przypadku, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest postaci $\psi \to \vartheta$ jest oczywisty i pozostawimy go czytelnikowi. Rozważymy przypadek, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest postaci $\mathrm{\forall }y\psi$. Jeśli zmienne $x$ oraz $y$ są równe, to $x$ nie występuje wolno w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i wówczas teza wynika natychmiast z Faktu 2.6. Tak więc przyjmijmy, że $x$ oraz $y$ są różnymi zmiennymi. Wówczas z dopuszczalności $t$ dla $x$ w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} wynika, że $y$ nie występuje w $t$. Ponadto Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst\var\varphi tx} jest identyczne z Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \forall y\subst\psi tx} . Mamy następujące równoważności:

$(\mathfrak{𝔄},\varrho )\models \mathrm{\forall }y\psi (t/x)$ wtedy i tylko wtedy, gdy dla każdego $d\in A,(\mathfrak{𝔄},{\varrho }_y^d)\models \psi (t/x)$

wtedy i tylko wtedy, gdy dla każdego $d\in A,(\mathfrak{𝔄},{\varrho }_{yx}^{d{a}^{\prime }})\models \psi$

gdzie $a^{\prime }=[[t]{]}_{{\varrho }_y^d}^{\mathfrak{𝔄}}$. Ponieważ $y$ nie występuje w $t$, więc $a^{\prime }=[[t]{]}_{{\varrho }_y^d}^{\mathfrak{𝔄}}=[[t]{]}_{\varrho }^{\mathfrak{𝔄}}=a$. Skoro zmienne $x$ oraz $y$ są różne, to Parser nie mógł rozpoznać (błąd składni): {\displaystyle \varrho^{d\: a}_{y\: x}=\varrho^{a\: d}_{x\:y}} . Tak więc warunek Parser nie mógł rozpoznać (błąd składni): {\displaystyle (\mathfrak A, \varrho^{d\: a'}_{y\: x}) \models \psi } jest równoważny warunkowi Parser nie mógł rozpoznać (błąd składni): {\displaystyle ( \mathfrak A, \varrho^{a\: d}_{x\: y}) \models \psi} , dla każdego $d\in A$. Czyli

$(\mathfrak{𝔄},{\varrho }_x^a)\models \mathrm{\forall }y\psi$

Natychmiastowym wnioskiem z Lematu 2.10 jest następujący przykład tautologii.

Fakt 2.11

Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , zmiennej $x$ i termu $t$ dopuszczalnego dla $x$ w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , formuła

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\var\varphi\to\var\varphi(t/x)}

jest tautologią logiki pierwszego rzędu.

Dowód

Ćwiczenie.

Fakt 2.12

Jeśli zmienna $y$ jest dopuszczalna dla $x$ w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} oraz Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle y\not\in\fv\var\varphi} , to

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models(\forall x\var\varphi)\leftrightarrow (\forall y \var\varphi(y/x))} .

Dowód

Z Faktu 2.11 oraz Faktu 2.8 otrzymujemy

$\models \mathrm{\forall }y(\mathrm{\forall }x\phi \to \phi (y/x))$

Zatem na mocy Faktu 2.7(1) wnioskujemy, że

$\models (\mathrm{\forall }y\mathrm{\forall }x\phi )\to (\mathrm{\forall }y\phi (y/x))$.

Na mocy Przykładu 2.7(2) otrzymujemy implikację $\to$. Odwrotna implikacja wynika z już udowodnionej implikacji oraz z następujących prostych obserwacji:

• Jeśli $y$ jest dopuszczalna dla $x$ w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , to $x$ jest dopuszczalna dla $y$ w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(y/x)} .
• Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle y\not\in FV\var\varphi} , to $x$ nie występuje wolno w Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(y/x)} .
• Wynik podstawienia Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi(y/x)(x/y)} jest identyczny z Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} .

Fakt 2.12 pozwala zamieniać zmienne związane dowolnie, tak długo jak są spełnione założenia. W szczególności jeśli chcemy wykonać podstawienie termu do formuły w sytuacji, gdy ten term nie jest dopuszczalny to wystarczy zamienić nazwy pewnych zmiennych związanych, tak aby term stał się dopuszczalny. Łatwo jest uogólnić Fakt 2.12: znaczenie formuły nie ulega zmianie także przy wymianie zmiennych związanych kwantyfikatorami wystepującymi wewnątrz formuły.

Przypisy

<references/>