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.<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$ 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 „\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

{{{3}}}

\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$?