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 \begin{eqnarray*}np. relacjach i funkcjach\end{eqnarray*}. Dzięki zastosowaniu {\em 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:

• {\em Symbole operacji i relacji\/} \begin{eqnarray*}w tym symbol równo¶ci $=$\end{eqnarray*};
• {\em Zmienne indywiduowe\/}, których warto¶ci maj± przebiegać rozważane

dziedziny;

• {\em Kwantyfikatory\/}, wi±ż±ce zmienne indywiduowe w formułach.

Składnia

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

Definicja

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$-ar\-gu\-men\-to\-wych}, a\Delta\vdashlementy ${\mathrm{\Sigma }}_n^R$ będziemy nazywać {\em 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$ \begin{eqnarray*}o znanej każdemu liczbie argumentów\end{eqnarray*} tworzy sygnaturę języka teorii ciał.

Definicja

Ustalamy pewien nieskończony przeliczalny zbiór Parser nie mógł rozpoznać (nieznana funkcja „\ZI”): {\displaystyle \ZI} symboli, które będziemy nazywać \textit{zmiennymi indywiduowymi} i zwykle oznaczać symbolami $x,y,z$. Zbiór \textit{termów} Parser nie mógł rozpoznać (nieznana funkcja „\termy”): {\displaystyle \termy} nad sygnatur± $\mathrm{\Sigma }$ i zbiorem zmiennych Parser nie mógł rozpoznać (nieznana funkcja „\ZI”): {\displaystyle \ZI} 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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle f\begin{eqnarray*}t_1,\ldots,t_n\end{eqnarray*}} jest też termem.

Zauważmy, że z powyższej definicji wynika iż stałe sygnatury $\mathrm{\Sigma }$ \begin{eqnarray*}czyli symbole operacji zeroargumentowych\end{eqnarray*} s± termami.

Definicja

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

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

Definicja

Następnie zdefiniujemy \textit{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 Parser nie mógł rozpoznać (nieznana funkcja „\termy”): {\displaystyle t_1,\ldots,t_n\in\termy} , napis Parser nie mógł rozpoznać (błąd składni): {\displaystyle r\begin{eqnarray*}t_1,\ldots,t_n\end{eqnarray*}} jest formuł± atomow±.

• Dla dowolnych termów $t_1,t_2$, napis Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}t_1=t_2\end{eqnarray*}} jest formuł± atomow±.

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

Definicja

\textit{Formuły} nad sygnatur± $\mathrm{\Sigma }$ i zbiorem zmiennych indywiduowych Parser nie mógł rozpoznać (nieznana funkcja „\ZI”): {\displaystyle \ZI} 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ć (błąd składni): {\displaystyle \begin{eqnarray*}\var\varphi\to\psi\end{eqnarray*}}

jest też formuł±.

• Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formuł± a Parser nie mógł rozpoznać (nieznana funkcja „\ZI”): {\displaystyle x\in\ZI} 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 \textit{zmiennych wolnych} Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle \fv\var\varphi} występuj±cych w tej formule:

• Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle \fv\bot=\emptyset} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle \fv{r\begin{eqnarray*}t_1,\ldots,t_n\end{eqnarray*}} =\bigcup_{i=1}^n \fv{t_i}} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle \fv{t_1=t_2}=\fv{t_1}\cup\fv{t_2}} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\displaystyle \fv{\var\varphi\to\psi}=\fv\var\varphi\cup\fv\psi} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\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\Delta\vdashgzystencjalny zdefiniujemy jako skrót notacyjny przy pomocy \textit{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. }

\text\\seml Zmienne wolne a zmienne zwi±zane. \semr W Definicji #def-form nie zakładamy, że Parser nie mógł rozpoznać (nieznana funkcja „\fv”): {\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 „\fv”): {\displaystyle x\not\in\fv\var\varphi} . Przez \textit{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\footnote{Zakładamy tu, że $s$ oraz $r$ s± symbolami relacji.} Parser nie mógł rozpoznać (nieznana funkcja „\def”): {\displaystyle \exists x\forall\boldsymbol{s}}\def\blank{\hbox{\sf B\begin{eqnarray*}r\begin{eqnarray*}x,y\end{eqnarray*}\to \forall y\exists x\,s\begin{eqnarray*}x,y,z\end{eqnarray*}\end{eqnarray*}} 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 \textit{wolnych} i \textit{zwi±zanych} w formułach. Wszystkie wyst±pienia zmiennych w formułach atomowych s± wolne. Wolne \begin{eqnarray*}zwi±zane\end{eqnarray*} wyst±pienia w formułach \mbox{Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i $\psi$} pozostaj± wolne \begin{eqnarray*}zwi±zane\end{eqnarray*} 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} \begin{eqnarray*}zwi±zanymi przez dopisanie kwantyfikatora $\mathrm{\exists }$\end{eqnarray*}, a charakter pozostałych wyst±pień jest taki sam w </math>\var\varphi$iw$\exists x\var\varphi</math>. Przykładowo w formule </math>\exists x\forall\boldsymbol{s}}\def\blank{\hbox{\sf B\begin{eqnarray*}r\begin{eqnarray*}x,\underline{y}\end{eqnarray*}\to \forall y\exists x\,s\begin{eqnarray*}x,y,z\end{eqnarray*}\end{eqnarray*}</math> 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\boldsymbol{s}}\def\blank{\hbox{\sf Bwaga 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 \begin{eqnarray*}zwi±zane np. deklaracj± w bloku\end{eqnarray*} nie s± widoczne na zewn±trz zakresu ich deklaracji. Intuicyjnie naturalne jest oczekiwanie, że zmiana zmiennej zwi±zanej na inn± zmienn± \begin{eqnarray*}tak aby nie wprowadzić konfliktu wynikaj±cego ze zmiany struktury wi±zań\end{eqnarray*} 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 \begin{eqnarray*}Fakt #alfa-konw\end{eqnarray*}.

Semantyka formuł

Niech $\mathrm{\Sigma }$ będzie sygnatur±. {\em Struktura} Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA} nad sygnatur± $\mathrm{\Sigma }$ \begin{eqnarray*}lub po prostu $\mathrm{\Sigma }$-struktura\end{eqnarray*} 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} . \begin{eqnarray*}Na przykład, je¶li $\mathrm{\Sigma }$ składa się z jednego symbolu relacji dwuargumentowej, to każdy graf zorientowany jest $\mathrm{\Sigma }$-struktur±.\end{eqnarray*} 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} oraz\Delta\vdashlementu $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ć (błąd składni): {\displaystyle \varrho_x^a\begin{eqnarray*}y\end{eqnarray*}=\przypadk\prooftree \varrho\begin{eqnarray*}y\end{eqnarray*}}{<math>y\neq x} \justifies a \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\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\begin{eqnarray*}x\end{eqnarray*}} .
• </math>\wartt {f\begin{eqnarray*}t_1,\ldots,t_n\end{eqnarray*}}\strA\varrho= f^\strA\begin{eqnarray*}\wartt

{t_1}\strA\varrho,\ldots,\wartt {t_1}\strA\varrho\end{eqnarray*}</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\begin{eqnarray*}t_1,\ldots,t_n\end{eqnarray*}}} \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{\begin{eqnarray*}W\end{eqnarray*} \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{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree} , gdy nie zachodzi

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

• Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho \justifies \forall x\var\varphi \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\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{\begin{eqnarray*}W\end{eqnarray*}}\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{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree} zamiast Parser nie mógł rozpoznać (nieznana funkcja „\sa”): {\displaystyle \sa\prooftree \strA}{\varrho \justifies \var\varphi \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree} , gdy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \varrho\begin{eqnarray*}x\end{eqnarray*}=a} i Parser nie mógł rozpoznać (błąd składni): {\displaystyle \varrho\begin{eqnarray*}y\end{eqnarray*}=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} \begin{eqnarray*}oznaczamy to przez Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\var\varphi} \end{eqnarray*}. 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 }$ \begin{eqnarray*}oznaczamy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models\Gamma} \end{eqnarray*}, 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±} \begin{eqnarray*}oznaczamy to przez Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi} \end{eqnarray*}, 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}}}

Dowód

{{{3}}}

\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{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree} , a st±d \mbox{</math>\sa\prooftree \strA \justifies \varrho \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree{\forall x\begin{eqnarray*}\var\varphi\to\psi\end{eqnarray*}\to\begin{eqnarray*}\forall x\var\varphi\to \forall x\psi\end{eqnarray*}}</math>}.

Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\niesa”): {\displaystyle \niesa\prooftree \strA}{\varrho \justifies \forall x\begin{eqnarray*}\var\varphi\to\psi\end{eqnarray*} \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree} lub Parser nie mógł rozpoznać (nieznana funkcja „\niesa”): {\displaystyle \niesa\prooftree \strA}{\varrho \justifies \forall x\,\var\varphi \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree} , to nasza formuła jest spełniona przez $\varrho$ wprost z definicji. Uzasadnienie czę¶ci \begin{eqnarray*}#taut2a--#taut5\end{eqnarray*} pozostawiamy czytelnikowi. }}

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 \begin{eqnarray*}por. Fakt #fakt-przyklad-taut\end{eqnarray*}. Natomiast wykazanie, że tak nie jest polega na podaniu odpowiedniego kontrprzykładu. Takiego jak ten:

Przykład

\forall x\begin{eqnarray*}p\begin{eqnarray*}x\end{eqnarray*}\to q\begin{eqnarray*}x\end{eqnarray*}\end{eqnarray*}</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\begin{eqnarray*}x\end{eqnarray*}} . \begin{eqnarray*}Mamy tu do czynienia ze zdaniem, więc warto¶ciowanie jest nieistotne i dlatego je pomijamy.\end{eqnarray*} St±d otrzymujemy Parser nie mógł rozpoznać (nieznana funkcja „\strA”): {\displaystyle \strA\models \forall x p\begin{eqnarray*}x\end{eqnarray*}\to\forall x q\begin{eqnarray*}x\end{eqnarray*}} . Z drugiej strony </math>\strA\not\models \forall x\begin{eqnarray*}p\begin{eqnarray*}x\end{eqnarray*}\to q\begin{eqnarray*}x\end{eqnarray*}\end{eqnarray*}</math>, ponieważ

\mbox{Parser nie mógł rozpoznać (nieznana funkcja „\niesa”): {\displaystyle \niesa\prooftree \strA}{x:2 \justifies p\begin{eqnarray*}x\end{eqnarray*}\to q\begin{eqnarray*}x\end{eqnarray*}}} . \using \textrm{\begin{eqnarray*}W\end{eqnarray*

\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ł Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall y \begin{eqnarray*}y \leq x\end{eqnarray*}} oraz Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall z \begin{eqnarray*}z \leq x\end{eqnarray*}} jest taki sam. Tymczasem ,,naiwne podstawienie $y$ w miejsce $x$ w obu tych formułach daje w wyniku odpowiednio Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall y \begin{eqnarray*}y \leq y\end{eqnarray*}} i Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall z \begin{eqnarray*}z \leq y\end{eqnarray*}} , 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} \begin{eqnarray*}lub, że podstawienie Parser nie mógł rozpoznać (nieznana funkcja „\subst”): {\displaystyle \subst\var\varphi tx} jest {\em dopuszczalne}\end{eqnarray*} 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ć (błąd składni): {\displaystyle x\not\in FV\begin{eqnarray*}\var\varphi\end{eqnarray*}} ;
• </math>\subst{r\begin{eqnarray*}t_1,\ldots,t_n\end{eqnarray*}}tx =

r\begin{eqnarray*}\subst{t_1}tx,\ldots,\subst{t_n}tx\end{eqnarray*}</math>;

• </math>\subst{\begin{eqnarray*}t_1=t_2\end{eqnarray*}}tx =

\begin{eqnarray*}\subst{t_1}tx=\subst{t_2}tx\end{eqnarray*}</math>;

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

gdy $y=x$, oraz Parser nie mógł rozpoznać (błąd składni): {\displaystyle y\not\in FV\begin{eqnarray*}t\end{eqnarray*}} ;

• 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$ \begin{eqnarray*}różn± od $x$\end{eqnarray*}, to obie strony s± równe Parser nie mógł rozpoznać (błąd składni): {\displaystyle \varrho\begin{eqnarray*}y\end{eqnarray*}} . Je¶li $s$ jest postaci Parser nie mógł rozpoznać (błąd składni): {\displaystyle f\begin{eqnarray*}s_1,\ldots,s_n\end{eqnarray*}} , to mamy następuj±ce równo¶ci. \begin{eqnarray*} \wartt {\subst stx}\strA\varrho &=& \wartt {f\begin{eqnarray*}\subst {s_1}tx,\ldots, \subst {s_n}tx\end{eqnarray*}}\strA\varrho \\ &=& f^\strA\begin{eqnarray*}\wartt{\subst{s_1}tx}\strA\varrho,\ldots, \wartt{\subst{s_n}tx}\strA\varrho\end{eqnarray*} \\ & =& f^\strA\begin{eqnarray*}\wartt{s_1}\strA{\varrho^a_x},\ldots, \wartt{s_n}\strA{\varrho^a_x}\end{eqnarray*} \\ & = & \wartt{f\begin{eqnarray*}s_1,\ldots,s_n\end{eqnarray*}}\strA{\varrho^a_x}= \wartt s\strA {\varrho^a_x}. \end{eqnarray*}

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\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnionej 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: \begin{eqnarray*} \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{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree. \end{eqnarray*} 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: \begin{eqnarray*} \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{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree \\ & \textrm{\wtw, gdy} & \mbox{dla każdego } d\in A, \ \sat\strA{\varrho^{d\: a'}_{y\: x}}\psi, \end{eqnarray*} 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{\begin{eqnarray*}W\end{eqnarray*}}\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\begin{eqnarray*}\forall x\var\varphi\end{eqnarray*}\\leftrightarrow \begin{eqnarray*}\forall y \subst\var\varphi yx\end{eqnarray*}. \]

\begin{dowodbezqed} Z Faktu #fa-pier-1 oraz Faktu #fakt-gen otrzymujemy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \models\forall y\begin{eqnarray*}\forall x\var\varphi\to\subst\var\varphi yx\end{eqnarray*}. } Zatem na mocy Faktu #fakt-przyklad-taut\begin{eqnarray*}#taut1\end{eqnarray*} wnioskujemy, że Parser nie mógł rozpoznać (błąd składni): {\displaystyle \models\begin{eqnarray*}\forall y\forall x\var\varphi\end{eqnarray*}\to\begin{eqnarray*}\forall y\subst\var\varphi yx\end{eqnarray*}. } Na mocy Przykładu #fakt-przyklad-taut\begin{eqnarray*}#taut2\end{eqnarray*} otrzymujemy \rightarrowlikację $\to$. Odwrotna \rightarrowlikacja wynika z już\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnionej \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\boldsymbol{s}}\def\blank{\hbox{\sf Bogólnić Fakt #alfa-konw: znaczenie formuły nie\boldsymbol{s}}\def\blank{\hbox{\sf Blega 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. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall x p\begin{eqnarray*}x,y\end{eqnarray*} \to \exists x q\begin{eqnarray*}x,y\end{eqnarray*}} ;
   2. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall x p\begin{eqnarray*}x,y\end{eqnarray*} \to \forall x q\begin{eqnarray*}x,y\end{eqnarray*}} ;
   3. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall x p\begin{eqnarray*}x,y\end{eqnarray*} \to \exists x q\begin{eqnarray*}x,z\end{eqnarray*}} ;

s± spełnione przy warto¶ciowaniu Parser nie mógł rozpoznać (błąd składni): {\displaystyle v\begin{eqnarray*}y\end{eqnarray*} = 7} , Parser nie mógł rozpoznać (błąd składni): {\displaystyle v\begin{eqnarray*}z\end{eqnarray*} = 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\begin{eqnarray*}m,n\end{eqnarray*} = \min\begin{eqnarray*}m,n\end{eqnarray*}} , 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\begin{eqnarray*}m,n\end{eqnarray*} = 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. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall y\begin{eqnarray*}\forall x\begin{eqnarray*}r\begin{eqnarray*}z,f\begin{eqnarray*}x,y\end{eqnarray*}\end{eqnarray*}\to r\begin{eqnarray*}z,y\end{eqnarray*}\end{eqnarray*}\end{eqnarray*}} ;
2. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall y\begin{eqnarray*}\forall x\begin{eqnarray*}r\begin{eqnarray*}z,f\begin{eqnarray*}x,y\end{eqnarray*}\end{eqnarray*}\end{eqnarray*}\to r\begin{eqnarray*}z,y\end{eqnarray*}\end{eqnarray*}} ,

s± spełnione przy warto¶ciowaniu Parser nie mógł rozpoznać (błąd składni): {\displaystyle v\begin{eqnarray*}z\end{eqnarray*} =5} , Parser nie mógł rozpoznać (błąd składni): {\displaystyle v\begin{eqnarray*}y\end{eqnarray*}=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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall x\begin{eqnarray*}\neg r\begin{eqnarray*}x,y\end{eqnarray*}\to\exists z\begin{eqnarray*}r\begin{eqnarray*}f\begin{eqnarray*}x,z\end{eqnarray*},g\begin{eqnarray*}y\end{eqnarray*}\end{eqnarray*}\end{eqnarray*}\end{eqnarray*}} jest spełniona przy warto¶ciowaniu Parser nie mógł rozpoznać (błąd składni): {\displaystyle v\begin{eqnarray*}x\end{eqnarray*} =3} , Parser nie mógł rozpoznać (błąd składni): {\displaystyle w\begin{eqnarray*}x\end{eqnarray*} = 6} i Parser nie mógł rozpoznać (błąd składni): {\displaystyle u\begin{eqnarray*}x\end{eqnarray*} = 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. [\begin{eqnarray*}b\end{eqnarray*}] 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 Parser nie mógł rozpoznać (błąd składni): {\displaystyle \exists y \begin{eqnarray*}y\neq x\end{eqnarray*}} ? A formuła Parser nie mógł rozpoznać (błąd składni): {\displaystyle \exists y \begin{eqnarray*}y\neq y\end{eqnarray*}} otrzymana przez ,,naiwne podstawienie $y$ na $x$?

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

\hfil Parser nie mógł rozpoznać (błąd składni): {\displaystyle p\begin{eqnarray*}x,f\begin{eqnarray*}x\end{eqnarray*}\end{eqnarray*} \to \forall x\exists y\, p\begin{eqnarray*}f\begin{eqnarray*}y\end{eqnarray*},x\end{eqnarray*}}

jest:\quad a\end{eqnarray*} spełniona;\quad b\end{eqnarray*} nie spełniona.

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

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \exists x\forall y\begin{eqnarray*}p\begin{eqnarray*}x\end{eqnarray*} \vee q\begin{eqnarray*}y\end{eqnarray*}\end{eqnarray*} \to \forall y\begin{eqnarray*}p\begin{eqnarray*}f\begin{eqnarray*}y\end{eqnarray*}\end{eqnarray*}\vee q\begin{eqnarray*}y\end{eqnarray*}\end{eqnarray*}} ;

1. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \forall y\begin{eqnarray*}p\begin{eqnarray*}f\begin{eqnarray*}y\end{eqnarray*}\end{eqnarray*}\vee q\begin{eqnarray*}y\end{eqnarray*}\end{eqnarray*} \to \exists x\forall y\begin{eqnarray*}p\begin{eqnarray*}x\end{eqnarray*} \vee q\begin{eqnarray*}y\end{eqnarray*}\end{eqnarray*}} ;
2. %97b

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \exists x\begin{eqnarray*}\forall y q\begin{eqnarray*}y\end{eqnarray*}\to p\begin{eqnarray*}x\end{eqnarray*}\end{eqnarray*}\to \exists x\forall y\begin{eqnarray*}q\begin{eqnarray*}y\end{eqnarray*}\to p\begin{eqnarray*}x\end{eqnarray*}\end{eqnarray*}} ;

1. %97c

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \exists x\begin{eqnarray*}\forall y q\begin{eqnarray*}y\end{eqnarray*}\to p\begin{eqnarray*}x\end{eqnarray*}\end{eqnarray*} \to\exists x\begin{eqnarray*}q\begin{eqnarray*}x\end{eqnarray*}\to p\begin{eqnarray*}x\end{eqnarray*}\end{eqnarray*}} .

\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\begin{eqnarray*}x\end{eqnarray*}/y]} jest spełnialna.

\item Udowodnić, że zdanie

\hfil </math>\forall x\exists y\,p\begin{eqnarray*}x,y\end{eqnarray*}\wedge \forall x\neg p\begin{eqnarray*}x,x\end{eqnarray*} \wedge \forall x\forall y\forall z\begin{eqnarray*}p\begin{eqnarray*}x,y\end{eqnarray*}\wedge p\begin{eqnarray*}y,z\end{eqnarray*}\to p\begin{eqnarray*}x,z\end{eqnarray*}\end{eqnarray*}</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$\Delta\vdashlementó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$?</ref>