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ć {\em symbolami operacji $n$-argumentowych}, aelementy ${\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:

• $FVx=\{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. $+,\cdot$) 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ę \textit{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.\footnote{Taka zamiana zmiennych bywa nazywana $\alpha$-\textit{konwersją}.} Tak w istocie będzie, jak się przekonamy poniżej (Fakt 2.12).

Semantyka formuł

Niech $\mathrm{\Sigma }$ będzie sygnaturą. {\em Struktura} Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} nad sygnaturą $\mathrm{\Sigma }$ (lub po prostu $\mathrm{\Sigma }$-struktura) to niepusty zbiór $A$, zwany {\em 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 Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle r^{\strA}\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ć (nieznana funkcja „\strA”): {\displaystyle \strA = \<A, f_1^\strA,\ldots,f_n^\strA,r_1^\strA,\ldots, r_m^\strA\>} , 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 Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle r^\strA, f^\strA,\dots}

{\em Wartościowaniem} w $\mathrm{\Sigma }$-strukturze Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} nazwiemy dowolną funkcję $\varrho :X\to A$. Dla wartościowania $\varrho$, zmiennej Parser nie mógł rozpoznać (nieznana funkcja „\ZI”): {\displaystyle x\in\ZI} orazelementu $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 „\przypadk”): {\displaystyle \varrho_x^a(y)=\przypadk\prooftree \varrho(y)}{<math>y\neq x} \justifies a \using \textrm{(W)}\endprooftree </math>

Najpierw zdefiniujemy znaczenie termów. Wartość termu Parser nie mógł rozpoznać (nieznana funkcja „\termy”): {\displaystyle t\in\termy} w $\mathrm{\Sigma }$-strukturze Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} przy wartościowaniu $\varrho$ oznaczamy przez Parser nie mógł rozpoznać (nieznana funkcja „\wartt”): {\displaystyle \wartt t\strA\varrho} , lub Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \wfz t\varrho} , gdy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} jest znane. Definicja jest indukcyjna:

• Parser nie mógł rozpoznać (nieznana funkcja „\wartt”): {\displaystyle \wartt x\strA\varrho=\varrho(x)} .
• </math>\wartt {f(t_1,\ldots,t_n)}\strA\varrho= f^\strA(\wartt

{t_1}\strA\varrho,\ldots,\wartt {t_1}\strA\varrho)</math>.

Znaczenie formuł definiujemy poniżej. Napis Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\strA\varrho\var\varphi. } czytamy: formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest spełniona w strukturze Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} przy wartościowaniu $\varrho$. Zakładamy tu, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} oraz Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} 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 Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\strA\varrho\bot} .
• Dla dowolnego $n\ge 1$, $r\in {\mathrm{\Sigma }}_n^R$ oraz dla dowolnych termów

$t_1,\dots ,t_n$, przyjmujemy, że Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\strA\varrho{r(t_1,\ldots,t_n)}} \wtw, gdy </math>\<\\\seml t_1}^{\strA}_{\varrho \semr, \ldots\\\seml t_1}^{\strA}_{\varrho}\>\in r^{\strA \semr</math>.

• </math>\sa\prooftree \strA}{\varrho \justifies t_1=t_2}Parser nie mógł rozpoznać (nieznana funkcja „\wtw”): {\displaystyle , \wtw, gdy } \\seml t_1 \using \textrm{(W) \semr\endprooftree_\varrho^\strA=

\\seml t_2 \semr_\varrho^\strA</math>.

• Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho \justifies \var\varphi\to\psi \using \textrm{(W)}\endprooftree} , gdy nie zachodzi

Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho \justifies \var\varphi \using \textrm{(W)}\endprooftree} lub zachodzi \mbox{Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho \justifies \psi}} \using \textrm{(W)}\endprooftree.

• Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho \justifies \forall x\var\varphi \using \textrm{(W)}\endprooftree} \wtw, gdy dla dowolnego $a\in A$

zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho_x^a \justifies \var\varphi \using \textrm{(W)}\endprooftree} .

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 „\fv”): {\displaystyle \fv\var\varphi} . Uzasadnia ono następującą konwencję notacyjną: napiszemy na przykład Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{x:a,y:b \justifies \var\varphi \using \textrm{(W)}\endprooftree} zamiast Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho \justifies \var\varphi \using \textrm{(W)}\endprooftree} , 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

Dla dowolnej $\mathrm{\Sigma }$-struktury Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} 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 \[ \sat\strA\varrho\var\varphi \hspace{1cm} {\textrm \wtw, gdy}\hspace{1cm} \sat\strA{\varrho'}\var\varphi. \]

Dowód

{{{3}}}

Prawdziwość i spełnialność formuł

Powiemy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi } jest spełnialna w Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} , gdy istnieje wartościowanie $\varrho$ w strukturze Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} takie, że zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\strA\varrho\var\varphi} . Formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest {\em spełnialna}, gdy istnieje struktura Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} , 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 {\em prawdziwa} w Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} , gdy dla każdego wartościowania $\varrho$ w Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\strA\varrho\var\varphi} . W tym przypadku mówimy też, że Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} jest {\em 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 „\strA”): {\displaystyle \strA\models\var\varphi} ). Dla zbioru formuł $\mathrm{\Gamma }$ i $\mathrm{\Sigma }$-struktury Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} powiemy, że Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} jest modelem dla $\mathrm{\Gamma }$ (oznaczamy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\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 „\strA”): {\displaystyle \strA\models\var\varphi} . Formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest {\em 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 rzedu, których nie da się w ten sposób otrzymać.

Fakt

{{{3}}}

<span id="

Aby się przekonać, że formuła (#taut1) jest tautologią, rozpatrzmy dowolną strukturę Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} i jakieś wartościowanie $\varrho$. Załóżmy najpierw, że Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho \justifies \forall x(\var\varphi\to\psi) \using \textrm{(W)}\endprooftree} oraz Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho \justifies \forall x\,\var\varphi \using \textrm{(W)}\endprooftree} . Oznacza to, że dla dowolnego $a\in A$ zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho_x^a \justifies \var\varphi \using \textrm{(W)}\endprooftree} oraz Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho_x^a \justifies \var\varphi\to\psi \using \textrm{(W)}\endprooftree} . Musi więc zajść \mbox{Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho_x^a \justifies \psi}} \using \textrm{(W)}\endprooftree. Z dowolności $a$ mamy Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho \justifies \forall x\,\psi \using \textrm{(W)}\endprooftree} , a stąd \mbox{</math>\sa\prooftree \strA \justifies \varrho \using \textrm{(W)}\endprooftree{\forall x(\var\varphi\to\psi)\to(\forall x\var\varphi\to \forall x\psi)}</math>}.

Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\niesa”): {\displaystyle \niesa\prooftree \strA}{\varrho \justifies \forall x(\var\varphi\to\psi) \using \textrm{(W)}\endprooftree} lub Parser nie mógł rozpoznać (nieznana funkcja „\niesa”): {\displaystyle \niesa\prooftree \strA}{\varrho \justifies \forall x\,\var\varphi \using \textrm{(W)}\endprooftree} , to nasza formuła jest spełniona przez $\varrho$ wprost z definicji. Uzasadnienie części (#taut2a--#taut5) pozostawiamy czytelnikowi. " style="font-variant:small-caps">Dowód

{{{3}}}

Ponadto mamy następujący Fakt

Dla dowolnej tautologii </math>\var\varphi$idowolnejzmiennej$xParser nie mógł rozpoznać (błąd składni): {\displaystyle , formuła } \forall x\var\varphi</math> jest też tautologią.

Dowód

{{{3}}}

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

Przykład

\forall x(p(x)\to q(x))</math> nie jest tautologią. Rozpatrzmy bowiem model Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA = \<\NN, p^\strA, q^\strA\>} , w którym:

• Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle n\in p^\strA} , \wtw, gdy $n$ jest parzyste;
• Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle n\in q^\strA} , \wtw, gdy $n$ jest nieparzyste;

Ponieważ Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle p^\strA\neq\NN} , więc Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\not\models \forall x p(x)} . (Mamy tu do czynienia ze zdaniem, więc wartościowanie jest nieistotne i dlatego je pomijamy.) Stąd otrzymujemy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models \forall x p(x)\to\forall x q(x)} . Z drugiej strony </math>\strA\not\models \forall x(p(x)\to q(x))</math>, ponieważ \mbox{Parser nie mógł rozpoznać (nieznana funkcja „\niesa”): {\displaystyle \niesa\prooftree \strA}{x:2 \justifies p(x)\to q(x)}} . \using \textrm{(W)}\endprooftree Rzeczywiście, \mbox{Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle 2\in p^\strA-q^\strA} }. %\hfil\qed

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 „\subst”): {\displaystyle \subst\var\varphi tx} oznacza wynik podstawienia $t$ na wszystkie \textit{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 {\em 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 {\em 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,\footnote{Podstawianie termu $t$ do termu $s$ na miejsce zmiennej $x$ oznaczamy podobnie: Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst stx} . Takie podstawienie jest zawsze wykonalne.} w której każda lewa strona jest dopuszczalna pod warunkiem, że prawa strona jest dopuszczalna.

• Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst\bot tx = \bot} , gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle x\not\in FV(\var\varphi)} ;
• </math>\subst{r(t_1,\ldots,t_n)}tx =

r(\subst{t_1}tx,\ldots,\subst{t_n}tx)</math>;

• </math>\subst{(t_1=t_2)}tx =

(\subst{t_1}tx=\subst{t_2}tx)</math>;

• Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst{(\var\varphi\to\psi)}tx = \subst\var\varphi tx\to\subst\psi tx} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst{(\forall x\,\var\varphi)}tx = \forall x\,\var\varphi} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst{(\forall y\,\var\varphi)}tx = \forall y\,\subst\var\varphi tx} ,

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.

\begin{lemat}[o podstawieniu] Niech Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} będzie dowolną strukturą oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \varrho:X\arr A} dowolnym wartościowaniem w Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} . Niech $t$ będzie dowolnym termem.

1. Dla dowolnego termu $s$ i zmiennej $x$ mamy

Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\strA\varrho{\subst\var\varphi tx}\hspace{1cm}\textrm{\wtw, gdy}\hspace{1cm} gdzie <math>a=\wartt t\strA\varrho} .

1. 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 </math> gdzie Parser nie mógł rozpoznać (nieznana funkcja „\wartt”): {\displaystyle a=\wartt t\strA\varrho} .

\end{lemat}

\begin{dowodbezqed} Część 1 dowodzimy przez indukcję ze względu na budowę termu $s$. Jeśli $s$ jest zmienną $x$, to obie strony są równe Parser nie mógł rozpoznać (nieznana funkcja „\wartt”): {\displaystyle \wartt t\strA\varrho} . 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. ( \wartt {\subst stx}\strA\varrho &=& \wartt {f(\subst {s_1}tx,\ldots, \subst {s_n}tx)}\strA\varrho \\ &=& f^\strA(\wartt{\subst{s_1}tx}\strA\varrho,\ldots, \wartt{\subst{s_n}tx}\strA\varrho) \\ & =& f^\strA(\wartt{s_1}\strA{\varrho^a_x},\ldots, \wartt{s_n}\strA{\varrho^a_x}) \\ & = & \wartt{f(s_1,\ldots,s_n)}\strA{\varrho^a_x}= \wartt s\strA {\varrho^a_x}. )

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: ( \sat\strA\varrho{\subst\var\varphi tx} & \textrm{\wtw, gdy} & \wartt{\subst{s_1}tx}\strA\varrho= \wartt{\subst{s_1}tx}\strA\varrho\\ & \textrm{\wtw, gdy} & \wartt{s_1}\strA{\varrho^a_x}=\wartt{s_2}\strA{\varrho^a_x}\\ & \textrm{\wtw, gdy} & \sat\str\prooftree \varrho^a_x \justifies s_1=s_2 \using \textrm{(W)}\endprooftree. ) 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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \psi\arr\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 #zm-wolne. 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: ( \sat\strA\varrho{\forall y\subst\psi tx} &\textrm{\wtw, gdy} & \mbox{dla każdego } d\in A,\ \sat\str\prooftree \varrho^d_y \justifies \subst\psi tx \using \textrm{(W)}\endprooftree \\ & \textrm{\wtw, gdy} & \mbox{dla każdego } d\in A, \ \sat\strA{\varrho^{d\: a'}_{y\: x}}\psi, ) gdzie Parser nie mógł rozpoznać (nieznana funkcja „\wartt”): {\displaystyle a'=\wartt t\strA{\varrho^d_y}} . Ponieważ $y$ nie występuje w $t$, więc Parser nie mógł rozpoznać (nieznana funkcja „\wartt”): {\displaystyle a'=\wartt t\strA{\varrho^d_y}=\wartt t\strA{\varrho}=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ć (nieznana funkcja „\sat”): {\displaystyle \sat\strA{\varrho^{d\: a'}_{y\: x}}\psi } jest równoważny warunkowi Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\strA{\varrho^{a\: d}_{x\: y}}\psi} , dla każdego $d\in A$. Czyli

\hfil\hfil\hfil Parser nie mógł rozpoznać (nieznana funkcja „\sat”): {\displaystyle \sat\str\prooftree \varrho^a_x \justifies \forall y\psi \using \textrm{(W)}\endprooftree} .\hfil\qed\hfil \end{dowodbezqed}

Natychmiastowym wnioskiem z Lematu #lem-pier-1 jest następujący przykład tautologii.

Fakt

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 \[\forall x\var\varphi\arr\subst\var\varphi tx\] jest tautologią logiki pierwszego rzędu.

Dowód

{{{3}}}

Fakt

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 \[ \models(\forall x\var\varphi)\\leftrightarrow (\forall y \subst\var\varphi yx). \]

\begin{dowodbezqed} Z Faktu #fa-pier-1 oraz Faktu #fakt-gen otrzymujemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\forall y(\forall x\var\varphi\to\subst\var\varphi yx). } Zatem na mocy Faktu #fakt-przyklad-taut(#taut1) wnioskujemy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models(\forall y\forall x\var\varphi)\to(\forall y\subst\var\varphi yx). } Na mocy Przykładu #fakt-przyklad-taut(#taut2) otrzymujemy \rightarrowlikację $\to$. Odwrotna \rightarrowlikacja wynika z już udowodnionej \rightarrowlikacji 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 „\subst”): {\displaystyle \subst\var\varphi yx} .

• Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle y\not\in\fv\var\varphi} , to $x$ nie występuje wolno w

Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst\var\varphi yx} .

• Wynik podstawienia Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst{\subst\var\varphi yx}xy} jest identyczny

z Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} .\hfil\qed

Fakt #alfa-konw 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 #alfa-konw: znaczenie formuły nie ulega zmianie także przy wymianie zmiennych związanych kwantyfikatorami wystepującymi wewnątrz formuły.

\subsection*{Ćwiczenia}\begin{small}

1. Niech Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA =\<\NN, p^\strA, q^\strA\>} , gdzie:

\hfil Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<a,b\>\in p^\strA} \wtw, gdy $a+b\ge 6$;\hfil

\hfil Parser nie mógł rozpoznać (błąd składni): {\displaystyle \<a,b\>\in q^\strA} \wtw, gdy $b=a+2$.

Zbadać czy formuły

1. 1. $\mathrm{\forall }xp(x,y)\to \mathrm{\exists }xq(x,y)$;
   2. $\mathrm{\forall }xp(x,y)\to \mathrm{\forall }xq(x,y)$;
   3. $\mathrm{\forall }xp(x,y)\to \mathrm{\exists }xq(x,z)$;

są spełnione przy wartościowaniu $v(y)=7$, $v(z)=1$ w strukturze Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} .

\item Niech Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA = \<\ZZ, f^\strA, r^\strA\>} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB = \<\ZZ, f^\strB, r^\strB\>} , gdzie

\hfil Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle f^\strA(m,n) = \min(m,n)} , dla Parser nie mógł rozpoznać (nieznana funkcja „\ZZ”): {\displaystyle m,n\in\ZZ} , a Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle r^\strA} jest relacją $\ge$;

\hfil Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle f^\strB(m,n) = m^2+n^2} , dla Parser nie mógł rozpoznać (nieznana funkcja „\ZZ”): {\displaystyle m,n\in\ZZ} , a Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle r^\strB} jest relacją $\le$.

Zbadać czy formuły

1. $\mathrm{\forall }y(\mathrm{\forall }x(r(z,f(x,y))\to r(z,y)))$;
2. $\mathrm{\forall }y(\mathrm{\forall }x(r(z,f(x,y)))\to r(z,y))$,

są spełnione przy wartościowaniu $v(z)=5$, $v(y)=7$ w strukturach Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} i Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle \strB} .

\item Czy formuła $\mathrm{\forall }x(\mathrm{\neg }r(x,y)\to \mathrm{\exists }z(r(f(x,z),g(y))))$ jest spełniona przy wartościowaniu $v(x)=3$, $w(x)=6$ i $u(x)=14$

1. w strukturze Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA = \<\NN, r^\strA\>} , gdzie Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle r^\strA} jest

relacją podzielności?

1. [(b)] w strukturze Parser nie mógł rozpoznać (nieznana funkcja „\B”): {\displaystyle \B = \<\NN, r^\strB\>} , gdzie Parser nie mógł rozpoznać (nieznana funkcja „\strB”): {\displaystyle r^\strB} jest

relacją przystawania modulo 7?

\item W jakich strukturach prawdziwa jest formuła $\mathrm{\exists }y(y\ne x)$? A formuła $\mathrm{\exists }y(y\ne y)$ otrzymana przez ,,naiwne podstawienie $y$ na $x$?

\item Podaj przykład modelu i wartościowania, przy którym formuła

\hfil $p(x,f(x))\to \mathrm{\forall }x\mathrm{\exists }yp(f(y),x)$

jest:\quad a) spełniona;\quad b) nie spełniona.

\item Zbadać, czy następujące formuły są tautologiami i czy są spełnialne: %%Rozwiazanie: %84%97bc

$\mathrm{\exists }x\mathrm{\forall }y(p(x)\vee q(y))\to \mathrm{\forall }y(p(f(y))\vee q(y))$;

1. $\mathrm{\forall }y(p(f(y))\vee q(y))\to \mathrm{\exists }x\mathrm{\forall }y(p(x)\vee q(y))$;
2. %97b

$\mathrm{\exists }x(\mathrm{\forall }yq(y)\to p(x))\to \mathrm{\exists }x\mathrm{\forall }y(q(y)\to p(x))$;

1. %97c

$\mathrm{\exists }x(\mathrm{\forall }yq(y)\to p(x))\to \mathrm{\exists }x(q(x)\to p(x))$.

\item Niech $f$ będzie jednoargumentowym symbolem funkcyjnym, który nie występuje w formule Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Pokazać, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x\exists y \var\varphi} jest spełnialna wtedy i tylko wtedy gdy formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \forall x \var\varphi[f(x)/y]} jest spełnialna.

\item Udowodnić, że zdanie

\hfil </math>\forall x\exists y\,p(x,y)\wedge \forall x\neg p(x,x) \wedge \forall x\forall y\forall z(p(x,y)\wedge p(y,z)\to p(x,z))</math>.

ma tylko modele nieskończone.

\item Dla każdego $n$ napisać takie zdanie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_n} , że Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\var\varphi_n} zachodzi \wtw, gdy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} ma dokładnie $n$elementów.

\item Czy jeśli Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA \models \exists x\,\var\varphi} , to także Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA \models \var\varphi[t/x]} , dla pewnego termu $t$?