%& --translate-file=cp1250pl

%%% kodowanie jest codepage 1250 (windowsowe :)

%%% aby miec ISO mozna uzyc iconv'a
%%%	iconv -f WINDOWS-1250 -t ISO8859-2 logic.tex > logiciso.tex
%%% trzeba tez zmienic pierwsza linijke pliku na
%& --translate-file=il2-pl                       

%%% (c) 2005 Witold Bo�t, Tadeusz Andrzej Kad�ubowski

\documentclass[12pt,a4paper,titlepage]{article}

\makeatletter
\def\thickhrulefill{\leavevmode \leaders \hrule height 2pt\hfill \kern \z@}
\renewcommand{\maketitle}{\begin{titlepage}%
    \let\footnotesize\small
    \let\footnoterule\relax
    \parindent \z@
    \reset@font
    \null
    \vskip 10\p@
    \hbox{\mbox{\hspace{5em}}%
      \vrule depth 0.2\textheight%
      \mbox{\hspace{2em}}
      \vbox{
        \vskip 40\p@
        \begin{flushleft}
          \Large \@author \par
        \end{flushleft}
        \vskip 80\p@
        \begin{flushleft}
          \huge \bfseries \@title \par
        \end{flushleft}
        \vskip 220\p@
        \begin{flushleft}
          \small \bfseries \@date \par
        \end{flushleft}
        \vfil
        }}
    \null
  \end{titlepage}%
  \setcounter{footnote}{0}%
}
\makeatother

\title{Logika matematyczna}
\author{Witold Bo�t \\ Taduesz Andrzej Kad�ubowski}
\date{wersja 0.94 \\ (\today)}


\usepackage{polski}	
\usepackage[OT4]{fontenc}
\usepackage{amsthm,amsmath,amsfonts,amssymb}	
\usepackage{enumerate}	
\usepackage{mathrsfs}
\usepackage{url}
\usepackage{multicol}

\newtheorem{tw}{Twierdzenie}[section]
\newtheorem{fakt}[tw]{Fakt}
\newtheorem{lemat}[tw]{Lemat}

\theoremstyle{definition}
\newtheorem{definicja}[tw]{Definicja}
\newtheorem{przyklad}[tw]{Przyk�ad}
\newtheorem{uwaga}[tw]{Uwaga}
\newtheorem{wniosek}[tw]{Wniosek}
\newtheorem{zadanie}{Zadanie}

\oddsidemargin  0.0in
\evensidemargin 0.0in
\textwidth      6.5in
\headheight     0.0in
\headsep	0.0in
\topmargin      -0.5in
\textheight	10.5in


\begin{document}
\maketitle

\tableofcontents
\newpage

%%%
\addcontentsline{toc}{section}{Wst�p}
\section*{Wst�p}
Opracowanie ,,Logika matematematyczna'', powsta�o w oparciu o wyk�ad prowadzony
w semestrze letnim roku akademickiego 2004/2005, na wydziale Mat--Fiz--Inf
Uniwersytetu Gda�skiego, przez prof. dr hab. Ireneusza Rec�awa dla II roku
informatyki. Autorzy opracowania w �aden spos�b nie zamierzali naruszy� praw
autorskich lub jakichkolwiek innych, nale��cych do wyk�adowcy (lub kogokolwiek
innego).

Opracowanie to jest udost�pnione w stanie ,,jak jest'', tzn. autorzy do�o�yli
stara�, by opracowanie to by�o przyzwoite i rzetelne, jednak nie mog� udzieli�
�adnej gwarancji. W szczeg�lno�ci nie gwarantuj� merytorycznej poprawno�ci,
zgodno�ci z tre�ci� wyk�adu, u�yteczno�ci do jakichkolwiek cel�w, czy w ko�cu
sensowno�ci matematycznej zawartych tu tre�ci. W przypadku znalezienie
jakichkolwiek b��d�w, niejasno�ci lub fragment�w kt�re s� zupe�nie
niezrozumia�e, prosimy o kontakt na adres e--mail: \url{houp@tlen.pl}, lub
\url{tkadlubo@manta.math.univ.gda.pl}. Aktualn� wersje skryptu mo�na zawsze
znale�� na stronie: \url{http://manta.univ.gda.pl/~wbolt/logic/}.


%%% 
\section{Systemy relacyjne}

Ca�a logika matematyczna o jakiej b�dziemy tutaj m�wi�, zajmuje si� opisem i badaniem
r�nych, tzw. system�w relacyjnych. Zaczniemy wi�c od zdefiniowania tego poj�cia.

\begin{definicja}[system relacyjny]
Systemem relacyjnym $\mathbb{A}$ nazywamy uporz�dkowany uk�ad zbior�w:
$$\mathbb{A} = \langle \mathcal{A}, \{r_i^{\mathbb{A}}\}_{i\in I}, \{f_j^{\mathbb{A}}\}_{j\in J}, \{c_k^{\mathbb{A}}\}_{k\in K}\rangle,$$
gdzie: $\mathcal{A}$ to pewien niepusty zbi�r\footnote{Zdaniem niekt�rych, w tym
prof. Mostowskiego, dodanie warunku $\mathcal{A} \neq \emptyset$ wi�cej
szkodzi, ni� pomaga.}, $\{r_i^{\mathbb{A}}\}_{i\in I}$ to zbi�r
relacji okre�lonych na zbiorze $\mathcal{A}$, $\{f_j^{\mathbb{A}}\}_{j\in J}$ to zbi�r
funkcji: $\mathcal{A}^{n_j} \to \mathcal{A}$, natomiast zbi�r $\{c_k^{\mathbb{A}}\}_{k\in K}$ to
zbi�r wyr�nionych sta�ych nale��cych do $\mathcal{A}$.
\end{definicja}

Zbiory relacji, funkcji i sta�ych, o kt�rych mowa w powy�szej definicji, mog�
by� puste.

\begin{przyklad}
Oto kilka przyk�ad�w system�w relacyjnych:
\begin{itemize}
\item $\langle \mathbb{R}, \leq \rangle$, czyli zbi�r liniowo uporz�dkowanych liczb
rzeczywistych,
\item $\langle \mathbb{R}, +, *, 0, 1\rangle$, czyli cia�o liczb rzeczywistych,
\item $\langle \textrm{�wiat matematyczny}, \in \rangle$.
\end{itemize}
\end{przyklad}

Aby m�c opisywa� systemy relacyjne, musimy w jaki� spos�b je charakteryzowa�.
Wprowadzamy wi�c poj�cie typu systemu relacyjnego.

\begin{definicja}[typ systemu relacyjnego]
Typ systemu relacyjnego, to uporz�dkowana tr�jka funkcji, postaci:
$$\tau = ( \tau_1, \tau_2, \tau_3),$$
gdzie: $\tau_1(i)$ to liczba argument�w $i$-tej relacji w systemie relacyjnym,
$\tau_2(j)$ to liczba argument�w $j$-tej funkcji w systemie relacyjnym,
$\tau_3(k)$ jest r�wne zero, dla ka�dego $k\in K$, dzi�ki $\tau_3$ dostajemy
wiec tylko informacj� ile jest sta�ych w danym systemie.
\end{definicja}


%%% 
\section{J�zyk, termy i formu�y}

\subsection{J�zyk}

\begin{definicja}[j�zyk]
J�zykiem $\mathscr{L}$ typu $\tau$ nazywamy uporz�dkowan� pi�tk� zbior�w symboli:
$$\mathscr{L}(\tau) = \langle R,F,C,X,S\rangle,$$
gdzie:
\begin{itemize}
\item zbi�r $R$ to zbi�r symboli relacyjnych: $R=\{r_i:i\in I\}$,
\item zbi�r $F$ to zbi�r symboli funkcyjnych: $F=\{f_j:j\in J\}$,
\item zbi�r $C$ to zbi�r symboli sta�ych: $C=\{c_k:k\in K\}$,
\item zbi�r $X$ to zbi�r symboli zmiennych: $X=\{x_n:n\in\mathbb{N}\}$ (uwaga: jest
to zawsze zbi�r niesko�czony!),
\item zbi�r $S$ to zbi�r symboli logicznych: $S=\{\neg,\to,\forall,=,(,)\}$.
\end{itemize}
\end{definicja}

J�zyk nale�y rozumie� jako zbi�r symboli, kt�re nie musz� mie� jakiegokolwiek
znaczenia - jest to po prostu co� z czego sk�ada� b�dziemy jakie� napisy, kt�re
dopiero, gdy b�d� mia�y jaki� model, nabior� znaczenia. Napisy, kt�re dalej
nazywa� b�dziemy formu�ami, budujemy z mniejszych ,,klock�w'', kt�re nazywa�
b�dziemy termami. Poni�ej podajemy definicj� zbioru wszystkich term�w j�zyka $\mathscr{L}$.

\subsection{Termy i warto�ciowanie}

\begin{definicja}[zbi�r term�w]
Zbi�r wszystkich term�w oznaczamy przez $T_m$. Jest on postaci:
$$T_m = \bigcup_n T_{m_{n}},$$
gdzie $T_{m_{0}} = X\cup C$, $T_{m_{n+1}} = T_{m_{n}}\cup\{f_j(t_1,\ldots,t_{n_{j}}): j\in J,t_1,\ldots,t_{n_{j}}\in T_{m_{k}},k\leq n\}$.
\end{definicja}

Zgodnie z t� definicj�, termami s� zmienne i sta�e z j�zyka $\mathscr{L}$, oraz
wszystkie symbole funkcji ,,liczone'' na wcze�niej zdefiniowanych termach. 
Zauwa�my, �e symbole relacyjne nie s� termami!

\begin{definicja}[podstawienie]
Podstawieniem (lub inaczej warto�ciowaniem) nazywamy dowoln� funkcj� $p\colon X\to \mathcal{A}$.
\end{definicja}

Aby zdefiniowa� warto�� termu, musimy rozszerzy� funkcj� $p$ tak aby jej
dziedzin� by� zbi�r $T_m$. Przyjmujemy wi�c dodatkowo: $p(c_k) = c^{\mathbb{A}}_{k}$
dla ka�dego $k\in K$,
oraz $p(f_j(t_1,\ldots,t_{n_{j}})) = f^{\mathbb{A}}_j(p(t_1),\ldots,p(t_{n_{j}}))$ dla
ka�dego $j\in J$. W
ten spos�b mo�emy wyliczy� warto�� dowolnego termu $t$. Warto�� t� oznaczamy
przez $p(t)$ lub $t[p]$.

\subsection{Formu�y}

Podobnie jak w przypadku term�w, zdefiniujemy zbi�r wszystkich formu�.

\begin{definicja}[zbi�r formu�]
Zbi�r wszystkich formu� j�zyka $\mathscr{L}$, kt�ry okre�lamy przez $F_m$, jest
zbiorem postaci: $F_m = \bigcup_{n} F_{m_{n}}$, gdzie $F_{m_{0}} = \{t_1 = t_2, r_i(t_1,\ldots,t_{n_{i}}): t_1,\ldots,t_{n_{i}}\in T_m, i\in I\}$,
$F_{m_{n+1}} = F_{m_{n}} \cup \{(F\to G), (\neg F), (\forall_x F) : F,G \in F_{m_{n}}\}$.
\end{definicja}

Zbi�r $F_{m_{0}}$ z powy�szej definicji, zawiera tak zwane formu�y atomowe. Jak �atwo
mo�na zauwa�y�, w definicji tej zak�adamy, �e wszystkie formu�y powstaj� wy��cznie
z formu� atomowych, implikacji, negacji i kwantyfikatora og�lnego. Cz�sto w
dowodach twierdze� metamatematycznych trzeba rozpatrzy� wszystkie mo�liwo�ci
��czenia formu� prostszych w bardziej skomplikowane. W�a�nie dlatego tylko tyle
sposob�w na konstruowanie nowych formu� w powy�szej definicji si� znalaz�o ---
lepiej mie� mniej mo�liwo�ci. 

Oczywi�cie w praktyce stosuje si� r�wnie� inne sp�jniki i operatory logiczne
ni� te z naszej definicji. Mo�na udowodni�, �e ten zestaw, kt�ry wybrali�my
wystarczy, aby skonstruowa� wszystkie inne sp�jniki logiczne. Nale�y wiedzie�,
�e gdy u�ywamy innych symboli do konstruowania formu�, to traktujemy je jedynie
jako skr�ty poj�� z powy�szej definicji.:

\begin{itemize}
\item Zapis $F\lor G$ nale�y rozumie� jako $\neg F\to G$.
\item Zapis $F\land G$ odpowiada zapisowi $\neg (F\to\neg G)$.
\item Zapis $F\iff G$ to tak naprawd� $(F\to G)\land(G\to F)$, czyli w my�l
poprzedniego napisu $\neg ((F\to G)\to\neg(G\to F))$.
\item Zapis $\exists_x F$ zast�pujemy natomiast przez $\neg\forall_x\neg F$.
\end{itemize}

\subsection{Zmienne wolne, zwi�zane i zdania}

Nieformalnie mo�na powiedzie�, �e zmienne wolne to takie kt�re nie s� ,,zwi�zane''
�adnym kwantyfikatorem\footnote{Uwaga: poj�cie zmiennej wolnej i zwi�zanej jest tutaj
potraktowane bardzo nieformalnie, gdy� mog� zda�y� si� formu�y w kt�rych
zmienna jest wolna w jednym miejscu formu�, a zwi�zana w innym -- tzn. gdy zasi�g jakiego�
kwantyfikatora jest ograniczony przez nawiasy. W takim przypadku og�lnie przyjmujemy,
�e zmienna jest wolna. Tak czy inaczej, aby pozby� si� takich problem�w, zawsze mo�emy
za�o�y�, �e na samym pocz�tku zamieniamy oznaczenia zmiennych kt�re mog�by powodowa�
kontrowersje -- mamy do dyzpozycji niesko�czenie wiele symboli zmiennych, wi�c
nie ma z tym problemu.}. Na przyk�ad w formule $\forall_x x+y < x$, zmienna $y$ jest
zmienn� woln�, natomiast $x$ jest zmienn� zwi�zan�. W zwi�zku z tym, �e w termach
nie wyst�puj� kwantyfikatory, przyjmuje si�, �e wszystkie zmienne w termie s�
wolne. Zbi�r wszystkich zmiennych wolnych termu b�d� formu�y oznaczamy odpowiednio
przez $V(t)$ lub $V(F)$. Zmiennymi wolnymi formu�y, zale�nie od jej postaci, s�:
\begin{itemize}
\item $V(t_1=t_2) = V(t_1)\cup V(t_2)$,
\item $V(r_i(t_1,\ldots,t_{n_{i}})) = V(t_1)\cup \ldots \cup V(t_{n_{i}})$,
\item $V(F\to G) = V(F) \cup V(G)$,
\item $V(\neg F) = V(F)$,
\item $V(\forall_x F) = V(F) \backslash \{x\}$.
\end{itemize}

Bardzo cz�sto rozwa�a� b�dziemy formu�y w kt�rych nie ma zmiennych wolnych.
Ze wzgl�du na swoj� wag� i powszechno��, takie formu�y maj� swoj� w�asn� nazw�.

\begin{definicja}[zdanie]
Formu�� $F$ nazywamy zdaniem, je�li $V(F) = \emptyset$.
\end{definicja}

\subsection{Prawdziwo�� formu�y w systemie relacyjnym}
Definicja spe�niania formu�y w systemie relacyjnym, przy danym
podstawieniu, musi obejmowa� wszystkie mo�liwe postaci formu�y $F$. W definicji
b�dziemy u�ywa� oznaczenia $\mathbb{A}\models F[p]$, kt�re nale�y czyta� ,,formu�a
$F$ jest spe�niona w modelu $\mathbb{A}$ przy podstawieniu $p$''.

Obok definicji warto�ciowania term�w jest to tak naprawd� jedyne miejsce, gdzie
warstwa j�zyka $\mathscr{L}$ styka si� z prawdziwymi obiektami matematycznymi.
Formu�y to tylko ustawianie literek obok siebie, dopiero tutaj przypisujemy im
znaczenie.

\begin{definicja}[spe�nianie formu�y w systemie relacyjnym]
Zale�nie od postaci formu�y $F$ definiujemy kiedy $A\models F[p]$.
\begin{itemize}
\item M�wimy, �e $\mathbb{A}\models (t_1=t_2)[p] $, je�li warto�ci tych
	dw�ch term�w s� sobie r�wne, czyli $t_1[p]=t_2[p]$.
\item M�wimy, �e $\mathbb{A}\models r_i(t_1,\ldots,t_n)[p]$, je�li zachodzi pomi�dzy
	warto�ciami tych term�w relacja $r_i^{\mathbb{A}}(t_1[p],\ldots,t_n[p])$.
\item M�wimy, �e $\mathbb{A}\models (F\to G)[p]$, je�li $\mathbb{A}\models F[p]$ implikuje  $\mathbb{A}\models G[p]$.
\item M�wimy, �e $\mathbb{A}\models (\neg F)[p]$, je�li nieprawda, �e $\mathbb{A}\models F[p]$.
\item M�wimy, �e $\mathbb{A}\models (\forall_x F)[p]$, je�li dla ka�dego elementu $a\in\mathcal{A}$ zachodzi $\mathbb{A}\models F[p(a/x)]$,
gdzie $p(a/x)(y)=\left\{\begin{array}{ll}a&y=x\\p(y)&y\neq x\end{array}\right.$.
\end{itemize}
\end{definicja}

%%%
\section{Izomorfizmy system�w relacyjnych}

\begin{definicja}[izomorfizm system�w relacyjnych\footnote{To zagadnienie nie zosta�o
zawarte w spisie zagadnie� na egzamin pisemny z Logiki.}]
Niech $\mathbb{A}$ i $\mathbb{B}$ b�d� systemami relacyjnymi tych samych typ�w.
Funkcja $h\colon\mathbb{A}\to\mathbb{B}$ jest izomorfizmem, je�li:
\begin{enumerate}
\item $h$ jest bijekcj�, tzn. jest r�nowarto�ciowa i ,,na'',
\item dla ka�dego $i\in I$ zachodzi $r_i^\mathbb{A}(x_1,\ldots,x_k) \equiv r_i^\mathbb{B}(h(x_1),\ldots,h(x_k))$,
\item dla ka�dego $j\in J$ zachodzi $h(f_j^{\mathbb{A}}(x_1,\ldots,x_n)) = f_j^{\mathbb{B}}(h(x_1),\ldots,h(x_k))$,
\item dla ka�dego $k\in K$ zachodzi $h(c_k^\mathbb{A})=c_k^{\mathbb{B}}$.
\end{enumerate}
\end{definicja}

\begin{tw}
Niech $\mathbb{A}$ i $\mathbb{B}$ systemy relacyjne tych samych typ�w, oraz
$h\colon\mathbb{A}\to\mathbb{B}$ izomorfizm. Niech $p$ b�dzie dowolnym podstawieniem.
Wtedy, dla ka�dej formu�y $F$, zachodzi:
$$\mathbb{A}\models F[p] \equiv \mathbb{B}\models F[h\circ p].$$
A gdy $F$ jest zdaniem, zachodzi:
$$\mathbb{A}\models F \equiv \mathbb{B}\models F.$$
\end{tw}

\noindent\textbf{Dow�d:} Aby poda� dow�d tego� twierdzenia, najpierw udowodnimy lemat.

\begin{lemat}
Dla dowolnego termu $t$, podstawienia $p$ i izomorfizmu $h$, 
zachodzi: $h(t[p]) = t[h\circ p]$.
\end{lemat}

\noindent\textbf{Dow�d lematu:} Dow�d b�dzie indukcyjny w zale�no�ci od najmniejszego
indeksu $n$ takiego, �e $t\in T_{m_{n}}$. Pierwszy krok to $t\in T_{m_{0}}$. Czyli
$t$ jest albo zmienn� albo sta��. Je�li $t=x_m\in X$, to $h(x_m[p]) = h(p(x_m)) = h\circ p(x_m) = x_m[h\circ p]$.
Je�li natomiast $t=c\in C$, to $h(c[p]) = h(c^{\mathbb{A}}) = c^{\mathbb{B}}$. Sta�a
oczywi�cie nie zale�y od podstawienia, wi�c mo�emy napisa� $c^{\mathbb{B}} = c[h\circ p]$.
Pierwszy krok indukcji mamy w ten spos�b za sob�. Za��my wi�c, �e je�li term $t$
nale�y do $T_{m_{n}}$ to lemat jest prawdziwy. Zastan�wmy si� co si� dzieje, je�li
term $t$ nale�y do $T_{m_{n+1}}$. Jest on wtedy na pewno postaci $f(t_1,\ldots,t_n)$, gdzie
dla term�w $t_1,\ldots,t_n$ mo�emy korzysta� z za�o�enia indukcyjnego. Mamy wi�c
$$h(f(t_1,\ldots,t_n)[p]) = h(f^{\mathbb{A}}(t_1[p],\ldots,t_n[p])) =$$
Z definicji izomorfizmu mamy dalej:
$$= f^{\mathbb{B}}(h(t_1[p]),\ldots,h(t_n[p])) = $$
Korzystaj�� z za�o�enia indukcyjnego mamy:
$$= f^{\mathbb{B}}(t_1[h\circ p],\ldots,t_n[h\circ p]) =$$
No a z definicji warto�ciowania termu mamy:
$$= f(t_1,\ldots,t_n)[h\circ p]. \quad\square$$

W ten spos�b udowodnili�my nasz lemat. Przejd�my do dowodu w�a�ciwego twierdzenia.
Przeprowadzimy dow�d indukcyjny ze wzgl�du na posta� i rozbudowanie formu�y,
to znaczy ze wzgl�du na $n$ -- indeks $F_{m_m}$ do kt�rego nale�y $F$. W pierwszym
kroku indukcyjnym rozwa�amy formu�y $F$ z $F_{m_0}$. Wobec tego, $F$ mo�e by�
postaci $t_1=t_2$ lub $r(t_1,\ldots,t_n)$.
\begin{itemize}
\item Niech $F$ b�dzie postaci: $t_1=t_2$. W�wczas $A\models F[p]$ jest spe�nione
wtedy i tylko wtedy, gdy $t_1[p] = t_2[p]$. Korzystaj�c z definicji izomorfizmu $h$
mo�emy napisa� r�wnowa�nie: $h(t_1[p]) = h(t_2[p])$. No ale zgodnie z udowodnionym
lematem, jest to r�wnowa�ne: $t_1[h\circ p] = t_2[h\circ p]$, co z godnie z definicj�
spe�niania r�wno�ci, jest r�wnowa�ne warunkowi: $\mathbb{B}\models (t_1=t_2)[h\circ p]$.
\item Niech $F$ b�dzie postaci: $r(t_1,\ldots,r_n)$. Wtedy $A\models F[p]$ jest
spe�nione tylko i wy��cznie, gdy $r^{\mathbb{A}}(t_1[p],\ldots,t_n[p])$. Korzystaj�c
z definicji $h$ mamy: $r^{\mathbb{B}}(h(t_1[p]), \ldots,h(t_n[p]))$, co na
mocy lematu daje nam: $r^{\mathbb{B}}(t_1[h\circ p],\ldots,t_n[h\circ p])$. Z definicji
spe�niania formu�y, dostajemy: $\mathbb{B}\models r(t_1,\ldots,r_n)[h\circ p]$.
\end{itemize}
W ten spos�b zako�czyli�my pierwszy krok indukcyjny. Za��my wi�c, �e twierdzenie
jest poprawne dla formu� $F$, kt�re nale�� do $F_{m_n}$ dla pewnego $n$. Poka�emy,
�e wynika z tego r�wnie� jego prawdziwo�� dla $G\in F_{m_{n+1}}$. Ograniczymy si�
do przypadku, gdy $G$ jest postaci $\forall_x F$ (pozosta�e przypadki przebiegaj� bowiem
analogicznie): $\mathbb{A}\models (\forall_x F)[p]$ zachodzi wtedy i tylko wtedy, gdy dla
ka�dego $a\in\mathcal{A}$ zachodzi $\mathbb{A}\models F[p(a/x)]$. Korzystaj�c z
za�o�enia indukcyjnego, warunek ten jest r�wnowa�ny warunkowi: dla ka�dego $a\in\mathcal{A}$
zachodzi $\mathbb{B}\models F[(h\circ p(a/x))]$. To natomiast mo�emy r�wnowa�nie
przestawi� w postaci: dla ka�dego $a\in\mathcal{A}$ zachodzi $\mathbb{B}\models F[(h\circ p)(h(a)/x)]$.
No a z tego, �e $h$ jest bijekcj�, mo�emy r�wnie� napisa�: dla ka�dego $b\in\mathcal{B}$ 
zachodzi $\mathbb{B}\models F[(h\circ p)(b/x)]$, co znaczy dok�adnie
$\mathbb{B}\models (\forall_x F)[h\circ p]$. $\square$

\begin{wniosek}
Je�li $\mathbb{A}$ oraz $\mathbb{B}$ s� izomorficzne, to s� w nich prawdziwe
te same zdania.
\end{wniosek}

\section{Teoria i model}

\subsection{Poj�cie teorii i modelu}

Zak�adamy, �e mamy dany j�zyk $\mathscr{L}(\tau)$.

\begin{definicja}[teoria]
Teori� nazywamy dowolny zbi�r zda�, b�d�cy podzbiorem zbioru formu� $F_m$ j�zyka
$\mathscr{L}$. Zazwyczaj ten zbi�r oznaczmy liter� $T$.
\end{definicja}

\begin{definicja}[model]
Modelem teorii $T$ nazywamy dowolny system relacyjny $\mathbb{A}$ typu $\tau$, taki �e
dla ka�dego zdania $F\in T$ zachodzi: $$\mathbb{A}\models F.$$
\end{definicja}

Zauwa�my, �e w powy�szych definicjach zak�adali�my, �e teoria jest zbiorem zda�,
a nie og�lnie formu�. Cz�sto jednak rozszerzamy t� definicje, tak aby teoria
by�a og�lnie zbiorem formu�.

\begin{definicja}[teoria i model -- rozszerzone dla formu�]
Teori� $T$ nazywamy dowolny zbi�r formu�, b�d�cy podzbiorem zbioru $F_m$ j�zyka
$\mathscr{L}$. Modelem takiej teorii $T$ nazywamy dowolny system relacyjny $\mathbb{A}$
wraz z podstawieniem $p$, je�li dla ka�dej formu�y $F\in T$ zachodzi:
$$\mathbb{A}\models F[p].$$
M�wimy w�wczas, �e modelem jest para $\langle\mathbb{A},p\rangle$.
\end{definicja}

\begin{uwaga}
O elementach zbioru $T$ cz�sto m�wimy, i� s� to aksjomaty teorii $T$.
\end{uwaga}

W dalszych rozwa�aniach za definicj� teorii i modelu, przyjmujemy wersje rozszerzone
dla formu�.

\subsection{Przyk�ady teorii i ich modeli}

\begin{przyklad}[teoria cia�]
Rozpatrzmy teori� cia�. Nasz j�zyk zawiera dwa symbole sta�ych $0$, $1$ 
oraz dwa symbole dzia�a� dwuargumentowych: $+$ i $*$. Aksjomaty teorii cia� to:
$$\forall_{x,y,z}((x+y)+z = x+(y+z))$$
$$\forall_{x,y,z}((x*y)*z = x*(y*z))$$
$$\forall_{x,y} x+y = y+x$$
$$\forall_{x,y} x*y = y*x$$
$$\forall_x x+0 = x$$
$$\forall_x x*1 = x$$
$$\forall_x\exists_y x+y = 0$$
$$\forall_{x\neq 0}\exists_y x*y = 1$$
$$\forall_{x,y,z} x*(y+z) = x*y + x*z$$
\end{przyklad}

\begin{przyklad}[modele teorii cia�]
Modelami teorii cia�, s� na przyk�ad:
\begin{enumerate}
\item $\langle\mathbb{Q}, 0, 1, +, *\rangle$, czyli cia�o liczb wymiernych ze standardowymi dzia�aniami.
\item $\langle\mathbb{R}, 0, 1, +, *\rangle$, czyli podobne cia�o liczb rzeczywistych.
\item $\langle\mathbb{Z}_p, 0, 1, +, *\rangle$, czyli cia�o reszt modulo $p$, gdzie $p$ jest liczb� pierwsz�, a wszystkie dzia�ania s� ,,modulo $p$''.
\end{enumerate}
\end{przyklad}

\begin{przyklad}[teoria porz�dk�w cz�ciowych i liniowych]
Rozparzmy teori� porz�dk�w cz�ciowych. J�zyk zawiera jedynie jeden
symbol relacyjny $\{\leq\}$. Aksjomatami teorii porz�dk�w cz�ciowych s�:
$$\forall_x x\leq x$$
$$\forall_x\forall_y\forall_z (x\leq y \land y\leq z \to x\leq z)$$
$$\forall_x\forall_y (x\leq y \land y\leq x \to x=y)$$
W tym samym j�zyku mo�emy wyrazi� r�wnie� teori� porz�dk�w liniowych. Do podanych
wy�ej aksjomat�w nale�y w�wczas doda� jeszcze:
$$\forall_x\forall_y (x\leq y \lor y\leq x).$$
\end{przyklad}

\begin{przyklad}[modele teorii porz�dk�w cz�ciowych i liniowych]
Rozwa�my modele:
\begin{enumerate}
\item $\langle\mathbb{R},\leq\rangle$, czyli zbi�r liczb rzeczywistych ze standardow�
relacj� ,,mniejszy--r�wny'', jest modelem zar�wno dla teorii porz�dk�w
cz�ciowych, jak i liniowych.
\item $\langle P(\mathbb{N}),\subset\rangle$, czyli zbi�r wszystkich podzbior�w
liczb naturalnych z relacj� bycia podzbiorem, jest modelem dla teorii porz�dk�w
cz�ciowych. Nie jest to jednak model dla teorii porz�dk�w liniowych.
\end{enumerate}
\end{przyklad}

\begin{przyklad}[teoria mnogo�ci]
Teoria mnogo�ci (kt�ra oznacza� b�dziemy dalej $ZFC$\footnote{Zermelo-Frankel set theory with the axiom of Choice.}) 
jest bardzo wa�na i do�� specyficzna, gdy� logika korzysta
z niej r�wnie� jako z tzw. metateorii -- czyli teorii w kt�rej uprawiamy
logik� matematyczn�. Mo�na uzna�, �e teoria mnogo�ci jest to podstawowa
teoria ca�ej matematyki. Do jej opisu u�ywamy j�zyka z jednym tylko symbolem
relacyjnym $\{\in\}$ -- relacj� nale�enia. Oto aksjomaty teorii mnogo�ci (nie
wszystkie b�d� zapisane formalnie):

\begin{enumerate}
\item Ekstensjonalno��: zbiory s� r�wne, je�li maj� te same elementy.
\item Istnieje zbi�r pusty, tzn.
$$\exists_x\forall_y \neg(y\in x).$$
Zbi�r pusty oznaczamy dalej jako $\emptyset$.
\item Aksjomat pary: istnieje zbi�r $\{x,y\}$ dla dowolnych $x$ i $y$.
\item Aksjomat sumy: istnieje $\bigcup x$ dla dowolnego $x$.
\item Aksjomat zbioru pot�gowego\footnote{Zbi�r pot�gowy to zbi�r wszystkich
podzbior�w danego zbioru. Zbi�r ten oznaczamy r�wnie� przez $2^X$.}: istnieje zbi�r $P(x)$ dla dowolnego $x$.
\item Aksjomat niesko�czono�ci: istniej zbi�r $A$ taki, �e $\emptyset\in A$,
oraz je�li jaki� $x$ nale�y do $A$ to r�wnie� $x\cup\{x\}$ nale�y do $A$, co
formalnie mo�na zapisa�:
$$x\in A \to x\cup\{x\}\in A.$$
Zbi�r $A$ mo�na sobie wyobrazi� jako zbi�r postaci:
$$A=\{\emptyset, \{\emptyset\}, \{\emptyset,\{\emptyset\}\},\ldots\}.$$
\textit{Najmniejszym takim zbiorem $A$ jest zbi�r liczby naturalnych $\mathbb{N}$ --
czyli do zdefiniowania zbioru liczb naturalnych nie potrzebujemy �adnych liczb, wystarczy
nam tylko zbi�r pusty.}
\item Aksjomat wyboru: z ka�dej rodziny zbior�w niepustych, parami roz��cznych,
mo�na wybra� tzw. ,,selektor'', czyli zbi�r, kt�ry ma po jednym punkcie wsp�lnym
z ka�dym ze zbior�w rodziny.
\item Aksjomat ufundowania: w ka�dym zbiorze istnieje element z nim roz��czny,
czyli:
$$\forall_x\exists_y y\in x\land y\cap x=\emptyset.$$
Wyklucza to sytuacj� $x\in x$.
\item Aksjomat wyr�niania: je�li $Z$ jest pewnym zbiorem, oraz $\varphi(x)$ pewn�
formu��, to istnieje zbi�r $\{x:x\in Z\land \varphi(x)\}$. Zapis ten nale�y traktowa�
jako schemat aksjomatu, opisuj�cy niesko�czenie wiele aksjomat�w -- dla ka�dej
mo�liwej formu�y $\varphi$ jest to inny aksjomat.
\item Aksjomat zast�powania\footnote{Na wyk�adzie aksjomat ten zosta� inaczej
sformu�owany, w tym opracowaniu podano jednak sformu�owanie bardziej zrozumia�e dla
autora -- znalezione na stronie: \url{http://www.mif.pg.gda.pl/kmd/ami/cz2.pdf}.}: je�li dla pewnej
formu�y $F(x,y)$ spe�niony jest 
warunek, �e dla ka�ego $x\in X$ istnieje $y\in Y$ taki, �e $F(x,y)$, to dla
ka�dego zbioru $A\subset X$ istnieje zbi�r $B\subset Y$, kt�rego elementami s�
te i tylko te elementy $y$, dla kt�rych przy pewnym $x\in A$, zachodzi $F(x,y)$.
\end{enumerate}
\end{przyklad}

\begin{uwaga}[model teorii mnogo�ci]
Nie mo�na udowodni�, �e istnieje model teorii mnogo�ci. By� mo�e, mo�na udowodni�,
�e taki model nie istnieje.
\end{uwaga}

%%% 
\section{Aksjomaty logiki, definicja dowodu}

Poni�ej zebrano schematy aksjomat�w logiki. Og�lnie aksjomat�w jest niesko�czenie
wiele. Podajemy je jednak w sko�czenie wielu schematach. J�zyk jakim si� pos�ugujemy
opisuj�c logik� nie pozwala nam tak naprawd� u�ywa� kwantyfikatora ,,dla ka�dej
formu�y''. Dlatego te� wszelkie aksjomaty zawieraj�ce w sobie ,,dowoln� formu�� $F$'', 
nale�y rozumie� jako schemat z kt�rego powstaje niesko�czenie wiele aksjomat�w
przez podstawianie ka�dej mo�liwej formu�y w miejsce $F$.

\paragraph{Aksjomaty logiki:}

\begin{multicols}{2}
\begin{itemize}
\item Aksjomaty rachunku zda�. Dla dowolnych formu� $F,G,H$ mamy:
$$F\to (G\to F),$$
$$F\to (G\to H)\to((F\to G)\to(F\to H)),$$
$$(\neg G \to \neg F) \to (F\to G).$$

\item Aksjomaty podstawienia:
$$\forall_x F \to F(t/x),$$
gdzie $F(t/x)$ to podstawienie w�a�ciwe\footnote{Podstawienie jest w�a�ciwe, kiedy wszystkie
zmienne z termu $t$ kt�ry podstawiamy w miejsce $x$ s� wolne w formule $F$.}.

\item Aksjomat o rozdzielczo�ci:
$$\forall_x (F\to G) \to (\forall_x F \to \forall_x G).$$

\item Je�li $x$ nie jest zmienn� woln� w $F$, to zachodzi:
$$F\to\forall_x F.$$

\item Aksjomaty r�wno�ci\footnote{Relacja r�wno�ci jest tak specyficzna, �e
bardzo cz�sto traktuje si� j� jako co� dodatkowego, niezale�nego od systemu
relacyjnego. R�wnie dobrze mogliby�my po prostu doda� do zbioru relacji jeszcze
jedn� relacj� $=(t_1,t_2)$, i punkt o r�wno�ci wyrzuci� z tej definicji. Nie
robimy tego troch� dla wygody, a pewnie te� troch� ze wzgl�d�w historycznych, a
pewnie jeszcze i innych subtelno�ci, kt�rych studenci nie s� sobie w stanie
wyobrazi�.}
. Dla dowolnych term�w $t_1,t_2,t_3$:
$$t_1 = t_1,$$
$$t_1 = t_2 \to t_2 = t_1,$$
$$t_1 = t_2 \to (t_2=t_3 \to t_1=t_3),$$
$$t_1 = s_1 \to ( \ldots \to (t_n=s_n \to $$$$(r(t_1,\ldots,t_n) \to r(s_1,\ldots,s_n))\ldots),$$
$$t_1 = s_1 \to ( \ldots \to (t_n = s_n \to$$$$(f(t_1,\ldots,t_n)=f(s_1,\ldots,s_n))\ldots).$$
\end{itemize}
\end{multicols}

\begin{uwaga}
Do wszystkich aksjomat�w logiki mo�na dopisa� dowoln� liczb� kwantyfikator�w og�lnych.
\end{uwaga}

Poza aksjomatami logiki, kt�re oznacza� b�dziemy przez $Log$ u�ywa� te� b�dziemy
regu�y wnioskowania zwanej ,,regu�� odrywania'' lub ,,\textsl{modus ponens}''.
Regu�a ta m�wi, �e je�li formu�y $F\to G$ oraz $F$ uznali�my za prawdziwe,
formu�� $G$ te� powinni�my uzna� za prawdziw�. Korzystaj�c z tej regu�y
b�dziemy budowa� dowody twierdze� logiki.

\begin{definicja}[dow�d]
Dowodem formu�y $F$ w oparciu o teori� $T$ nazywamy dowolny sko�czony ci�g formu�
$F_1,\ldots,F_n$, taki, �e $F_n = F$, a ka�da inna formu�a tego ci�gu jest
albo aksjomatem (tzn. nale�y do $Log\cup T$) albo powsta�a z regu�y odrywania
z poprzednich wyraz�w ci�gu.
\end{definicja}

Z definicji dowodu nie wynika wcale, �e powinien on mie� jaki� wi�kszy sens czy
porz�dek. Wszystko si� dzieje w warstwie syntaktycznej, nie wnikamy w
matematyczne znaczenie, lecz tylko interesuje nas wygl�d napis�w. Dow�d
logiczny mo�e by� ca�kiem ,,nielogiczny'', wystarczy tylko by spe�nia� warunki
definicji i ju� jest poprawnym dowodem.

\begin{wniosek}
Je�li formu�a $F$ ma jaki� dow�d w oparciu o $T$, to ma niesko�czenie wiele
r�nych dowod�w.
\end{wniosek}

\begin{definicja}
Twierdzenie teorii $T$, to formu�a, kt�ra ma dow�d w oparciu o teori� $T$.
\end{definicja}

Je�li formu�a $F$ ma dow�d w oparciu o teori� $T$, piszemy $T\vdash F$. Je�li
jaka� formu�a $F$ ma dow�d w ka�dej teorii, to znaczy je�li wynika z aksjomat�w
logiki, piszemy $\vdash F$. Formu�y $F$ o kt�rych mo�emy napisa� $\vdash F$, nazywamy
twierdzeniami logiki.

\begin{uwaga}
Od tej pory wszystkie twierdzenia logiki b�dziemy traktowa� w miar� na r�wni z
aksjomatami logiki. Dla uproszczenia, gdy w dowodzie b�dziemy chcieli
wykorzysta� jakie� twierdzenie logiki, to b�dziemy pomijali fragment polegaj�cy
na dowodzie tego twierdzenia.
\end{uwaga}

\begin{tw}
Je�li w $T$ da si� udowodni� formu�� $F$, to istnieje sko�czony podzbi�r $T_0\subset T$,
taki, �e $T_0\vdash F$.
\end{tw}

\noindent\textbf{Dow�d:} Skoro w $T$ da si� udowodni� formu�� $F$ to istnieje jaki�
dow�d. Niech dowodem tym b�dzie ci�g $F_1,\ldots,F_n$. Mo�emy zbudowa�
teori� $T_0$, korzystaj�c z wyraz�w tego ci�gu, a dok�adniej:
$$T_0 = \{F_i: \textrm{$F_i$ jest aksjomatem}\}.$$
Takie $T_0$ jest na pewno zbiorem sko�czonym, na pewno jest podzbiorem $T$ i
na pewno zachodzi $T_0 \vdash F$. $\square$


\subsection{Przyk�ady twierdze� logiki}

Podamy dwa przyk�ady twierdze� logiki w raz z ich formalnymi dowodami rozumianymi
w kontek�cie naszej definicji dowodu.

\begin{fakt}
Dla dowolnej formu�y $F$ mamy: $\vdash F\to F$.
\end{fakt}

\noindent\textbf{Dow�d:} �eby wyra�niej pokaza�, i� dow�d logiczny mo�e by� zupe�nie
nie jasny i niezrozumia�y, podamy najpierw po prostu ci�g formu� kt�ry b�dzie
ju� kompletnym dowodem -- bez �adnych komentarzy. Nast�pnie ka�dy wyraz ci�gu
opatrzymy stosownym komentarzem, jednak z formalnego punktu widzenia komentarz
ten jest zb�dny. Oto pe�ny dow�d naszego faktu:
$$F\to ((F\to F)\to F)$$
$$(F\to((F\to F)\to F)) \to ((F\to (F\to F))\to(F\to F))$$
$$(F\to(F\to F))\to (F\to F)$$
$$F\to(F\to F)$$
$$F\to F\quad \square$$

Dow�d ten, mimo �e kompletny i poprawny, dla wi�kszo�ci czytelnik�w mo�e okaza�
si� nieco niezrozumia�y (dla autor�w r�wnie�). Dlatego teraz ka�d� linijk� 
dodatkowo opatrzono komentarzem.\\*

\noindent Korzystamy z aksjomatu $F\to (G\to F)$, gdzie za $G$ podstawiamy $F\to F$:
$$F\to ((F\to F)\to F)$$
Drugi aksjomat rachunku zda�:
$$(F\to((F\to F)\to F)) \to ((F\to (F\to F))\to(F\to F))$$
T� formu�� otrzymujemy z dw�ch poprzednich, korzystaj�c z regu�y odrywania.
$$(F\to(F\to F))\to (F\to F)$$
Ponownie korzystamy z aksjomatu $F\to (G\to F)$, gdzie za $G$ podstawiamy $F$. 
$$F\to(F\to F)$$
Z regu�y odrywania otrzymujemy formu�� (korzystaj�c z dw�ch poprzednich linijek), kt�ra ko�czy dow�d -- jest w�a�nie t� formu�� kt�r� chcieli�my udowodni�:
$$F\to F\quad\square$$

\begin{fakt}
Niech $F(x)$ b�dzie formu�� w kt�rej nie wyst�puje zmienna $y$. Wtedy:
$$\{\forall_x F(x)\} \vdash \forall_y F(y/x).$$
\end{fakt}

\noindent\textbf{Dow�d:}
\begin{enumerate}
\item Korzystamy z aksjomatu:
$$\forall_x F(x) \to F(y/x)$$
\item Aksjomaty mo�emy ,,domyka�'' kwantyfikatorami og�lnymi:
$$\forall_y \left(\forall_x F(x) \to F(y/x)\right)$$
\item Korzystamy z aksjomatu o rozdzielczo�ci:
$$\forall_y \left(\forall_x F(x)\to F(y/x)\right) \to \left(\forall_y\forall_x F(x)\to\forall_y F(y/x)\right)$$
\item Z regu�y odrywania mamy:
$$\forall_y\forall_x F(x)\to\forall_y F(y/x)$$
\item Zapisujemy kolejny aksjomat:
$$\forall_x F(x) \to \forall_y \forall_x F(x)$$
\item Zapisujemy aksjomat naszej teorii, kt�r� za�o�yli�my w tre�ci twierdzenia:
$$\forall_x F(x)$$
\item Z regu�y odrywania dostajemy:
$$\forall_y\forall_x F(x)$$
\item Ponownie z regu�y odrywania, mamy:
$$\forall_y F(y/x)\quad\square$$
\end{enumerate}


\subsection{Zbi�r konsekwencji teorii $T$}
Kiedy znamy ju� aksjomaty logiki, z kt�rych korzystamy przy dowodzeniu
twierdze�, mo�emy poda� konstrukcj� zbioru konsekwencji danej teorii.

\begin{definicja}[zbi�r konsekwencji teorii $T$]
Zbi�r konsekwencji teorii $T$, kt�ry oznaczamy $T^\ast$, to zbi�r postaci:
$$T^\ast = \bigcup_n T_n,$$
gdzie $T_0 = Log \cup T$, $T_{n+1} = T_n \cup \{G: \exists_{F} (F\in T_n \land F\to G\in T_n)\}$.
\end{definicja}

Zbi�r $T^\ast$ r�wnie� jest pewn� teori� (zgodnie z definicj� teorii 
jako dowolnego podzbioru zbioru formu�). Co wi�cej zachodz� nast�puj�ce fakty.

\begin{fakt}
Dla dowolnej teorii $T$, mamy:
$$T^\ast = T^{\ast\ast}.$$
Innymi s�owy, je�li $T^\ast \vdash F$, to $T\vdash F$.
\end{fakt}

\noindent\textbf{Dow�d:} Niech $F_1, F_2, \cdots,  F_n$ b�dzie dowodem $F$ w
$T^\ast$. Ka�dy element $F^\ast$ z definicji ma dow�d w $F$. Ci�g b�d�cy
dowodem formu�y $F$ w $T$ otrzymamy, gdy zamiast ka�dego formu�y ci�gu $F_i$ nie
otrzymanej w wyniku u�ycia regu�y odrywania, lecz b�d�cej aksjomatem teorii
$T^\ast$ podstawimy dow�d tej�e formu�y. $\square$

\begin{fakt}
Formu�a $F$ nale�y do zbioru $T^\ast$ wtedy i tylko wtedy, gdy ma dow�d w
oparciu o $T$.
\end{fakt}

\noindent\textbf{Dow�d:} Implikacja ,,$\Leftarrow$'': Przeprowadzimy dow�d indukcyjny
ze wzgl�du na d�ugo�� dowodu formu�y $F$. Pierwszy krok indukcyjny jest
spe�niony, bo gdy d�ugo�� dowodu wynosi jeden, to znaczy, �e $F$ musi by�
aksjomatem, czyli nale�e� do $T$ a co za tym idzie do $T^\ast$. Za��my, wi�c
�e je�li dow�d jest d�ugo�ci $n$ to twierdzenie jest spe�nione. Zobaczymy co
dzieje si�, gdy $F$ ma dow�d d�ugo�ci $n+1$. Niech dowodem tym b�dzie: $F_1,\ldots,F_n,F_{n+1}$.
Zauwa�my, �e na mocy za�o�enia indukcyjnego, wszystkie wyrazy od $F_1$ do $F_n$ musz�
nale�e� do $T^\ast$. Co wi�cej istnieje takie $k$, �e wszystkie te wyrazy nale��
do $T_k$. Rozparzmy dwa przypadki w zale�no�ci od postaci $F_{n+1}$. Je�li
$F_{n+1}$ jest aksjomatem (a mo�e tak by�), to na pewno nale�y do $T$ czyli tym
bardziej do $T^\ast$. Je�li $F_{n+1}$ nie jest aksjomatem, to musia�o powsta�
z regu�y odrywania. W�r�d formu� $F_1,\ldots,F_n$ musz� wi�c istnie� formu�y
$F_i = G\to F_{n+1}$ oraz $F_j = G$, kt�re nale�� do $T_k$. Zgodnie z definicj�
zbioru $T^\ast$, $F_{n+1}$ nale�y w takim razie na pewno do $T_{k+1}$, czyli
do $T^\ast$. Na mocy twierdzenia o indukcji matematycznej, udowodnili�my
jedn� cz�� naszego twierdzenia.

Implikacja ,,$\Rightarrow$'': Musimy pokaza�, �e je�li $F$ nale�y do $T^\ast$ to
ma dow�d. Przeprowadzimy dow�d indukcyjny ze wzgl�du na $n$ takie, �e $F\in T_n$ oraz
$F\not\in T_{n-1}$. Pierwszy krok indukcyjny jest spe�niony, ze wzgl�du na to, �e
je�li $F\in T_0$ to dowodem $F$ jest po prostu samo $F$. Za��my wi�c, �e twierdzenie
jest prawdziwe dla formu� kt�re nale�� do $T_n$. Poka�emy, �e jest te� dobre dla
tych, kt�re nale�� do $T_{n+1}$ a nie nale�� do $T_n$. Je�li formu�a $F$ nale�y
do $T_{n+1}$ to istniej� formu�y $G\to F$ oraz $G$, kt�re nale�� do $T_n$. Zgodnie
z za�o�eniem indukcyjnym, maj� one swoje dowody. Niech $H_1,\ldots,H_m$ b�dzie
dowodem $G\to F$, oraz $G_1,\ldots,G_k$ b�dzie dowodem $G$. W�wczas ci�g:
$H_1,\ldots,H_m,G_1,\ldots,G_k,F$ jest dowodem $F$ w oparciu o $T$. $\square$

\begin{tw}
Je�li $F\in T^\ast$, to $F$ jest prawdziwe w ka�dym modelu teorii $T$.
\end{tw}

\noindent\textbf{Dow�d:} Przeprowadzimy indukcj� ze wzgl�du na indeks $n$ zbior�w $T_n$ taki, �e
$F\in T_{n+1}\backslash T_n$. Je�li $F$ nale�y do $T_0$, to jest aksjomatem logiki
lub aksjomatem teorii $T$, wi�c na pewno jest spe�nione w ka�dym modelu tej teorii.
Za��my wi�c, �e twierdzenie jest prawdziwe dla formu� kt�re nale�� do $T_n$. Poka�emy
�e r�wnie� dla formu� nale��cych do $T_{n+1}\backslash T_n$ jest poprawne. Niech
$F$ b�dzie tak� formu��. Wtedy na pewno istniej� formu�y $G$ i $G\to F$, kt�re nale��
do $T_n$. Zgodnie z za�o�eniem indukcyjnym w ka�dym modelu $\mathbb{A}$ teorii $T$
zachodzi: $\mathbb{A}\models G[p]$ oraz $\mathbb{A}\models (G\to F)[p]$. Zgodnie
z definicj� spe�niania symbolu ,,$\to$'', skoro w $\mathbb{A}$ jest spe�nione
zar�wno $G[p]$ jak i $(G\to F)[p]$, musi te� by� spe�nione $F[p]$. $\square$

\begin{uwaga}
Odwrotne twierdzenie jest r�wnie� prawdziwe. Jest ono om�wione p�niej.
\end{uwaga}

%%%
\section{Twierdzenie o dedukcji}

\begin{tw}[o dedukcji]
Niech $T$ -- dowolna teoria, $F, G$ -- formu�y. Wtedy zachodzi: 
$T\cup\{F\}\vdash G$ wtedy i tylko wtedy, gdy $T\vdash (F\to G)$.
\end{tw}

\noindent\textbf{Dow�d:} Wynikanie ,,$\Leftarrow$'': Niech ci�g $F_1,\ldots,F_n$ b�dzie
dowodem zdania $F\to G$ w $T$. Oczywi�cie $F_n$ musi by� r�wne $F\to G$. W�wczas
ci�g $F_1,\ldots,F_{n-1},F\to G, F, G$ jest dowodem zdania $G$ w teorii $T\cup\{F\}$.

\noindent Wynikanie ,,$\Rightarrow$'': Zak�adamy, �e $T\cup\{F\}\vdash G$, co 
znaczy, �e $G$ nale�y do zbioru konsekwencji $(T\cup\{F\})^{\ast}$. No a
to znaczy, �e $G\in \bigcup_n(T\cup\{F\})_n$. Dalsza cz�� dowodu to indukcja,
wzgl�dem $n$. Musimy rozpatrze� wiele przypadk�w, zale�nie od tego w kt�rym
$(T\cup\{F\})_n$ znajduje si� $G$.

\begin{enumerate}[I]
\item Niech $G\in(T\cup\{F\})_0$, czyli $G\in Log\cup T\cup \{F\}$. Rozpatrzymy
oddzielnie dwa przypadki:

\begin{enumerate}
\item Je�li $G\in Log\cup T$, w�wczas zachodzi $T\vdash G\to(F\to G)$ (zgodnie
z aksjomatem logiki). Ci�g: $G\to(F\to G), G, F\to G$ jest wi�c dowodem zdania
$F\to G$ w oparciu o $T$.
\item Je�li $G=F$ to te� jest ,,dobrze'' bo w ka�dej teorii da si� udowodni�,
�e $F\to F$.
\end{enumerate}

\item Za��my, �e je�li $H\in(T\cup\{F\})_n$ to zachodzi $T\vdash F\to H$. Poka�emy,
�e z tego wynika, �e je�li $G\in(T\cup\{F\})_{n+1}$ to $T\vdash F\to G$. Wiemy na pewno,
�e $G$ powsta�o z regu�y odrywania, tak wi�c istnieje jakie� $H_1$, takie, �e:
$H_1\in (T\cup\{F\})_n$ oraz $H_1\to G\in(T\cup\{F\})_n$. Z za�o�enia indukcyjnego
mamy wi�c, �e $T\vdash F\to H_1$ oraz $T\vdash F\to(H_1\to G)$. Niech wi�c teraz
ci�g $K_1,\ldots,K_n$ b�dzie dowodem $F\to H_1$, natomiast $J_1,\ldots,J_m$ b�dzie
dowodem $F\to(H_1\to G)$. Wtedy ci�g:
$$K_1,\ldots,K_n,J_1,\ldots,J_m,(F\to(H_1\to G))\to((F\to H_1)\to(F\to G)),$$
$$(F\to H_1)\to(F\to G),F\to G$$
jest dowodem zdania $F\to G$ w oparciu o $T$, innymi s�owy: $T\vdash F\to G$.
\end{enumerate}

Na mocy zasady indukcji matematycznej, twierdzenie o dedukcji jest prawdziwe
dla dowolnego zdania $G$. $\square$

\begin{wniosek}
Je�li $T\cup\{\neg G\}\vdash \neg F$ to $T\vdash F\to G$.
\end{wniosek}

\noindent\textbf{Dow�d wniosku:} Z tw. o dedukcji otrzymujemy, �e $T\vdash\neg G\to\neg F$.
Niech $F_1,\ldots,F_n$ b�dzie dowodem zdania $\neg G\to \neg F$ w oparciu o $T$.
Wtedy ci�g: $F_1,\ldots,F_n,(\neg G\to \neg F)\to(F\to G),F\to G$ jest dowodem
$F\to G$ w oparciu o $T$. $\square$

%%% 
\section{Twierdzenie Lindenbauma, zdania nierozstrzygalne}

\subsection{Poj�cie sprzeczno�ci i niesprzeczno�ci}
\begin{definicja}
Teoria $T$ jest sprzeczna, je�li istnieje taka
formu�a $F$, �e zarazem $T\vdash F$ i $T\vdash \neg F$.
\end{definicja}

\begin{fakt}
W teorii sprzecznej da si� udowodni� wszystko, czyli $\forall_{G \in \mathrm{F_m}} T\vdash G$.
\end{fakt}

\noindent\textbf{Dow�d:}
Nie b�dzie dowodu ultra-formalnego. Je�eli mamy dowody $F$ i $\neg F$, to mo�emy z nich zrobi� dow�d $ F \land \neg F$, co jest zawsze fa�szem. Potem dok�adamy $(F \land \neg F) \to G$, kt�ra to implikacja jest twierdzeniem logiki, bo ma fa�szywy poprzednik, wi�c jest zawsze prawdziwa. Potem stosujemy regu�� odrywania i dostajemy $G$.

\begin{definicja}
Teoria niesprzeczna to teoria, kt�ra nie jest sprzeczna.
\end{definicja}

\begin{fakt} 
Je�li teoria ma model, to jest ona niesprzeczna.
\end{fakt}

\noindent\textbf{Dow�d:}
W modelu o wszystkim mo�emy powiedzie�, czy jest prawd�, czy nie. W teorii
sprzecznej da si� udowodni� wszystko, wi�c wszystko nale�y uzna� za prawd�, bo
do tego dowody s�u��. Model nie mo�e spe�nia� wszystkich zda�. Zawsze mamy albo
$\mathbb{M}\models\psi$, albo $\mathbb{M}\models\neg\psi$. Oba na raz nie
maj� sensu wobec definicji prawdziwo�ci zda� w modelu. $\square$

\begin{fakt}
Teoria jest niesprzeczna, je�li ka�da jej sko�czona podteoria jest niesprzeczna.
Innymi s�owy: je�li istnieje sko�czona podteoria sprzeczna, to ca�a teoria jest sprzeczna.
\end{fakt}

\noindent\textbf{Szkic dowodu, albo komentarz} Sprzeczno�� zawsze objawia si� w
sko�czonym zbiorze aksjomat�w. Chodzi o to, �e je�eli teoria $T$ jest
sprzeczna, to bierzemy dowoln� formu�� $F$ i robimy dow�d $F_1, F_2, \cdots, F_n$ 
formu�y $F$ i dow�d $G_1, G_2, \cdots, G_m$ formu�y $\neg F$. Zar�wno ci�g
$F_i$, jak i $G_j$ s� sko�czone, korzystaj� wi�c ze sko�czonej ilo�ci
aksjomat�w z teorii $T$. Wi�c mamy sko�czon� podteori� $T\cap(\{F_i\} \cup
\{G_j\})$, kt�ra zawiera wszystko, czego potrzebujemy, by przeprowadzi� dow�d zar�wno
$F$, jak i $\neg F$, jest wi�c sprzeczna. $\square$

\begin{fakt}
Je�li teoria $T$ jest niesprzeczna, to zbi�r konsekwencji $T^\ast$ jest r�wnie� niesprzeczny.
\end{fakt}

\begin{tw}[reductio ad absurdum\footnote{Z �ac. \textsl{reduction ad absurdum} 
znaczy sprowadzenie do niedorzeczno�ci. Twierdzenie to u�ywane jest w�a�nie
do konstruowania dowod�w ,,przez zaprzecznie''.}]
$T \cup \{ \neg F\} $ jest sprzeczna wtedy i tylko wtedy, gdy $T\vdash F$.
\end{tw}

\noindent\textbf{Dow�d:}
Implikacja ,,$\Rightarrow$'' : Albo $T$ jest sprzeczna sama w sobie, wtedy na mocy definicji
sprzeczno�ci dow�d $T \vdash F$ istnieje. Je�eli $T$ jest niesprzeczna, za�
do�o�enie do niej jednego aksjomatu $\neg F$ t� niesprzeczno�� popsuje, to na pewno
$T\vdash F$.

Implikacja ,,$\Leftarrow$'': Albo $T$ jest sprzeczna sama w sobie, wi�c 
powi�kszona o jeden
aksjomat tym bardziej --- wtedy implikacja jest zawsze prawdziwa, bo ma
nast�pnik prawdziwy. Je�eli $T$ jest niesprzeczna i istnieje dow�d $T\vdash F$,
to po powi�kszeniu teorii o dodatkowy aksjomat to tym bardziej mamy
$T\cup\{\neg F\} \vdash F$, co jest jawn� oznak� sprzeczno�ci. $\square$


\begin{przyklad}[teorie sprzeczne i niesprzeczne]
Przyk�adem najprostszej teorii sprzecznej mo�e by� teoria $\{F,\neg F\}$, gdzie
$F$ to dowolna formu�a.

Przyk�adem teorii niesprzecznej mo�e by� teoria grup. Teoria ta jest niesprzeczna,
poniewa� istnieje model -- istniej� przecie� grupy w matematyce.
\end{przyklad}

\subsection{Poj�cie rozstrzygalno�ci}

\begin{definicja}
M�wimy, �e formu�a $F$ jest rozstrzygalna w teorii $T$, je�eli $T\vdash F$ 
albo $T\vdash\neg F$.
\end{definicja}

\begin{przyklad}
Istniej� zar�wno grupy przemienne, jak i nieprzemienne,
czego teoria grup nie rozstrzyga, co opiszemy formalnie. Aksjomaty teorii grup
to:
$$\forall_{x,y,z} ((x+y)+z = x+(y+z))$$
$$\forall_{x} (x+e = e+x = x)$$
$$\forall_{x}\exists_{z}(x+z = e)$$

Istnieje model $\langle\mathbb{Z}, +\rangle$, w kt�rym te� jest prawdziwe dodatkowe zdanie:

$$\forall_{x,y} ((x+y) = (y+x))$$

Istnieje jednak model $\langle S_n, \circ\rangle$, czyli permutacje zbioru
$n$-elementowego z operacj� sk�adania w roli dzia�ania ,,$+$'', w kt�rym to
dodatkowe zdanie nie jest spe�nione.
\end{przyklad}


\subsection{Poj�cie zupe�no�ci}

\begin{definicja}[zupe�ny zbi�r twierdze�]
M�wimy, �e niesprzeczny zbi�r formu� $T$ jest zupe�ny, je�eli dla ka�dej 
formu�y $F$ albo zachodzi $F\in T$ albo $\neg F \in T$.
\end{definicja}

\begin{definicja}[zupe�ny zbi�r aksjomat�w]
M�wimy, �e zbi�r aksjomat�w $T$ jest zupe�nym zbiorem aksjomat�w, je�li
zbi�r $T^\ast$ jest zupe�ny.
\end{definicja}

\subsection{Twierdzenie Lindenbauma}
\begin{tw}[Lindenbauma]
Ka�d� teori� niesprzeczn� $T$ mo�na rozszerzy� do teorii zupe�nej $T'$.
\end{tw}

\noindent\textbf{Dow�d:}
Dow�d b�dzie uproszczony tylko dla j�zyk�w przeliczalnych, czyli gdy
$|\mathscr{L}|=\aleph_0$. Wtedy te� $|F_m| = \aleph_0$, czyli mo�na formu�y
ustawi� w ci�g: $F_m =\{F_n:n\in\mathbb{N}\}$. Nale�y przeprowadzi� indukcj� 
po tym ci�gu.

\begin{enumerate}[(1)]
\item \begin{enumerate}[(a)]
\item Je�li $T\cup\{\neg F_0\}$ jest sprzeczna, to wtedy $T\vdash F_0$, wi�c $T\cup \{F_0\} \subset T^\ast$ b�dzie niesprzeczny. $T\cup\{F_0\}$ oznaczmy jako ${T_0}'$.
\item Je�li $T\cup\{\neg F_0\}$ jest niesprzeczna, to po prostu przyjmujemy ${T_0}' := T\cup\{\neg F_0\}$.
\end{enumerate} 
Czyli mo�emy rozbudowa� teori� $T$ tak, by rozstrzyga�a r�wnie� $F_0$, a przy tym nadal by�a niesprzeczna.
\item Mo�emy dok�adnie tak samo, w oparciu o niesprzeczn� teori� ${T_n}'$ zbudowa� ${T_{n+1}}'$, kt�ra
b�dzie nadal niesprzeczna, a przy tym b�dzie rozstrzyga�a r�wnie� $F_{n+1}$.
\end{enumerate}
Przy pomocy indukcji matematycznej mo�emy w ten spos�b rozstrzygn�� wszystkie 
$F_i$. Dostajemy teori� $T'$ rozstrzygaj�c� wszystkie formu�y: 
$$T' = \bigcup_i {T_i}'.$$
Takie $T'$ jest niesprzeczne, dlatego, �e ci�g teorii $T_i$ jest wst�puj�cy,
tzn. $\forall_{i, j} (i<j) T_i\subset T_j $, przy czym ka�dy element tego ci�gu
jest niesprzeczny. To jest troch� tak, jakby bra� granic� w niesko�czono�ci,
ale granica to poj�cie z analizy matematycznej, tutaj go nie mamy, ale suma
teorio-mnogo�ciowa nam w zupe�no�ci wystarczy.

Dow�d dla j�zyk�w dowolnie du�ej mocy opiera si� na lemacie
Kuratowskiego--Zorna. $\square$

%%%
\section{Twierdzenie o pe�no�ci oraz twierdzenie o zwarto�ci}

\subsection{Twierdzenie G\"odla o pe�no�ci}

\begin{tw}[G\"odla o pe�no�ci]
Ka�da teoria niesprzeczna $T$ ma model.
\end{tw}

\noindent\textbf{Szkic dowodu:}
Niech $T$ b�dzie teori� pewnego j�zyka $\mathscr{L}$. Chcemy zbudowa� model dla teorii
$T$. Zbudujemy go z term�w j�zyka b�d�cego rozszerzeniem $\mathscr{L}$. Dow�d bazuje
na rozszerzeniu teorii $T$ do teorii $T'$, oraz j�zyka $\mathscr{L}$ do j�zyka $\mathscr{L}'$, tak
aby spe�niony by� warunek: \textit{dla ka�dej formu�y $F$ i zmiennej $x$
istnieje sta�a $c$ taka, �e formu�a $\exists_x F \to F(c/x)$ nale�y do $T'$}.
Potrzebowa� b�dziemy wi�c dodatkowych sta�ych w j�zyku. Budujemy j�zyk $\mathscr{L}_1$
z j�zyka $\mathscr{L}$ dok�adaj�c tam odpowiednio du�o sta�ych $c(F,x)$ (dla ka�dej formu�y
i zmiennej potrzebujemy sta�� - czyli sta�e te zale�� od formu�y $F$ i zmiennej $x$;
b�dzie ich tyle ile wszystkich formu� z $T$ i zmiennych z $\mathscr{L}$). Budujemy te�
teori� $T_{1}$ na bazie teorii $T$ dorzucaj�c w�a�nie odpowiednie formu�y. Mamy
wi�c: 
$$T_{1} = T \cup \left\{\exists_x F \to F(c(F,x)/x): x\in X, F\in F_m\right\}.$$
Nale�a�oby udowodni�, �e $T_1$ jest r�wnie� niesprzeczna - dow�d pomijamy.

Powy�sze post�pwanie mo�emy powtarza� w niesko�czono�� buduj�c kolejne teorie $T_n$ 
na bazie teorii $T_{n-1}$ oraz j�zyki $\mathscr{L}_n$ na bazie $\mathscr{L}_{n-1}$. Ostatecznie,
przyjmuj�c, �e $L=L_0$ oraz $T=T_0$ mamy:
$$T' = \bigcup_n T_n,\quad L' = \bigcup_n L_n.$$

Teori� $T'$ rozszerzamy do teorii zupe�nej, kt�ra rozstrzyga wszystkie formu�y
(mo�emy to zrobi� na mocy twierdzenia Lindenbauma). Dla takiej teorii $T'$
zbudujemy model. Model ten b�dziemy budowa� z term�w. Aby to zrobi�,
zdefiniujemy relacj� r�wnowa�no�ci term�w. Relacja okre�limy bardzo
intuicyjnie:
$$t_1 \sim t_2\quad\textrm{wtedy i tylko wtedy gdy forum�a: } t_1=t_2\in T'.$$ 
Relacja $\sim$ m�wi wi�c, �e dwa termy s� w relacji r�wnowa�no�ci, je�li w teorii
$T'$, rzeczywi�cie jest formu�a m�wi�c, �e te dwa termy s� r�wne (do�� oczywiste,
prawda?). Ze wzgl�du na to, �e $T'$ jest zupe�na, to dla ka�dych dw�ch term�w
$t_1$ i $t_2$ w $T'$ jest zdanie $t_1=t_2$ lub $t_1\neq t_2$, wi�c relacja jest
dobrze zdefiniowana.

Nasz model $\mathbb{A}$ b�dzie oparty na zbiorze postaci:
$$\mathcal{A} = \left\{ [t]_{\sim} : t\in T_m\right\}.$$
Czyli zbi�r $\mathcal{A}$ jest zbiorem wszystkich klas abstrakcji relacji $\sim$.
Musimy jeszcze, aby dok�adnie zdefiniowa� model $\mathbb{A}$ poda� definicje
relacji, funkcji i sta�ych w zbiorze $\mathcal{A}$ oraz definicj� podstawienia:

\begin{itemize}
\item Dla ka�dego symbolu relacyjnego $r$ z j�zyka $\mathscr{L}'$, definiujemy relacj� $r^{\mathbb{A}}$:
$$r^{\mathbb{A}}([t_1],\ldots,[t_n]) \textrm{ zachodzi, wtedy i tylko wtedy, gdy }
r(t_1,\ldots,t_n)\in T'.$$

\item Dla ka�dego symbolu funkcyjnego $f$ z j�zyka $\mathscr{L}'$, definiujemy
funkcj� $f^{\mathbb{A}}$:
$$f^{\mathbb{A}}([t_1],\ldots,[t_n]) = [f(t_1),\ldots,f(t_n)].$$

\item Dla ka�dego symbolu sta�ej $c$ z j�zyka $\mathscr{L}'$, definiujemy
sta�� $c^{\mathbb{A}}$:
$$c^{\mathbb{A}} = [c].$$

\item Definiujemy te� podstawienie $p: X\to \mathcal{A}$:
$$p(x) = [x].$$
\end{itemize}

Model $\langle\mathbb{A},p\rangle$ jest modelem teorii $T'$. Jest on r�wnie� modelem teorii $T$,
co nale�a�oby jeszcze pokaza� (dow�d pomijamy). $\square$

\begin{uwaga}
Model $\mathbb{A}$ z dowodu jest mocy co najwy�ej r�wnej mocy j�zyka. Je�li 
wi�c j�zyk $\mathscr{L}$ jest przeliczalny, to r�wnie� model jest przeliczalny.
\end{uwaga}

\subsection{Wnioski z twierdzenia G\"odla o pe�no�ci}

\begin{wniosek}
Je�li $ZFC$ (teoria mnogo�ci) jest niesprzeczna, to ma model przeliczalny.
\end{wniosek}

\begin{wniosek}
Niech $T=\{F:\mathbb{R}\models F\}$ -- zbi�r wszystkich zda� spe�nionych w 
zbiorze liczb rzeczywistych. Istnieje jaki� model $\mathbb{A}$ dla teorii
$T$ kt�ry jest przeliczalny. Innymi s�owy istnieje przeliczalny zbi�r kt�ry
spe�nia wszystkie te same zdania co zbi�r liczb rzeczywistych.
\end{wniosek}

\begin{wniosek}
Je�li zdanie $F$ jest spe�nione w ka�dym modelu teorii $T$ to da si� je
udowodni� w oparciu o teori� $T$.
\end{wniosek}


\noindent\textbf{Dow�d wniosku:} Za��my przeciwnie, �e $\neg (T\vdash F)$. W�wczas
teoria $T\cup\{\neg F\}$ jest niesprzeczna. No ale wtedy istnieje model
dla $T\cup\{\neg F\}$. Czyli istnieje model teorii $T$ w kt�rym nie zachodzi
$F$, co jest sprzeczne z za�o�eniem, �e $F$ jest spe�nione w ka�dym modelu 
teorii $T$. $\square$


\subsection{Twierdzenie G\"odla o zwarto�ci}

\begin{tw}[G\"odla o zwarto�ci]
Je�li ka�da sko�czona podteoria teorii $T$ ma model, to r�wnie� ca�a teoria
$T$ ma model.
\end{tw}

\noindent\textbf{Dow�d:} Je�li ka�da sko�czona podteoria ma model, to znaczy �e
jest niesprzeczna, w zwi�zku z czym ca�a teoria $T$ jest niesprzeczna. Zgodnie
z twierdzeniem o pe�no�ci, teoria $T$ musi wi�c mie� model. $\square$

%%% 
\section{Arytmetyka Peano}

\subsection{Aksjomaty arytmetyki Peano}
\begin{enumerate}[(1)]
\item $$\forall_x\forall_y x+y = y+x$$
\item $$\forall_x\forall_y x\cdot y = y\cdot x$$
\item $$\forall_x\forall_y\forall_z (x+y)+z = x+(y+z)$$
\item $$\forall_x\forall_y\forall_z (x\cdot y)\cdot z = x\cdot(y\cdot z)$$
\item $$\forall_x\forall_y\forall_z x\cdot (y + z) = (x\cdot y) + (x \cdot z)$$
\item $$\forall_x x+\Delta_0 = x$$
\item $$\forall_x x\cdot\Delta_1 = x$$
\item $$\forall_x\forall_y\forall_z x+y = x+z \to y=z$$
\item Ka�da liczba r�na od zera jest nast�pnikiem:
$$\forall_x x\neq\Delta_0 \to \exists_y y+\Delta_1=x.$$

\item Zasada indukcji matematycznej. Podamy tu schemat aksjomatu opisuj�cy
niesko�czenie wiele aksjomat�w -- oddzielny dla ka�dej formu�y. Niech $F$ b�dzie
formu�� a $x$ zmienn�:
$$\left(F(\Delta_0 / x)\land \forall_x \left(F(x)\to F(x+\Delta_1/x)\right)\right)\to$$
$$\to\forall_x F(x)$$
\end{enumerate}

\subsection{Standardowy model arytmetyki Peano}
Standardowym modelem arytmetyki Peano jest $\langle\mathbb{N},+,\cdot,0,1\rangle$, przy
czym oczywi�cie liczba $0$ odpowiada symbolowi $\Delta_0$, liczba $1$ symbolowi
$\Delta_1$, standardowe dzia�anie dodawania symbolowi $+$, oraz standardowe dzia�anie
mno�enia symbolowi $\cdot$. Istniej� jednak niestandardowe modele arytmetyki Peano.

\subsection{Niestandardowe modele arytmetyki Peano}
Podamy konstrukcj� niestandardowego modelu arytmetyki Peano. Niech symbolowi
$\Delta_0$ odpowiada liczba $0$, symbolowi $\Delta_1$ liczba $1$. A symbolom
$\Delta_{n+1}$ odpowiednio $\Delta_n + \Delta_1$.

Niech $F_n$ to b�d� formu�y postaci: $\exists_y x = \Delta_n + y$, co
w skr�cie mo�na by zapisa� $x\geq \Delta_n$, gdyby�my mieli relacj� wi�kszy
r�wny (ale nie mamy). Niech $T$ b�dzie zbiorem wszystkich zda� kt�re s�
spe�nione w arytmetyce Peano (w liczbach $\mathbb{N}$):
$$T=\{F:\mathbb{N}\models F\land \textrm{$F$ jest zdaniem}\}.$$
Niech teoria $T'$ b�dzie postaci:
$$T' = T\cup\{F_n:n\in\mathbb{N}\}.$$
Niech $T_0$ b�dzie sko�czon� podteori� $T'$. W�wczas na pewno $T_0$ jest
postaci:
$$T_0 = (T_0 \cap T) \cup \{F_{n_1},\ldots,F_{n_k}\}.$$
Modelem dla teorii $T_0$ s� liczby naturalne z podstawieniem $p$ takim, �e
element $p(x)$ jest wi�kszy od liczb $n_i$ dla ka�dego $i$ od $1$ do $k$.
W zwi�zku z tym, �e $T_0$ ma model, r�wnie� $T'$ musi mie� model. Niech tym
modelem b�dzie $\langle\mathbb{A},p\rangle$. Zauwa�my jednak, �e w tym modelu element
$p(x)$ musi by� wi�kszy od wszystkich element�w $\Delta_i$ tego modelu, bo dla
ka�dego $i$ $\mathbb A\models F_i$. Modelem $\mathbb{A}$
nie mo�e wi�c by� zbi�r liczb naturalnych, gdy� tam nie ma takiego elementu.
Taki model jest niestandardowym modelem arytmetyki Peano. Spe�nia te same zdania
co model $\langle\mathbb{N},+,\cdot,0,1\rangle$. Zauwa�my te�, �e na mocy aksjomatu 9
ten dodatkowy element ma swoje nast�pniki, poprzedniki pewnie te�. Pojawia si� wi�c
du�o wi�cej dodatkowych element�w, ni� tylko ten jeden.

\begin{uwaga}
Niestandardowy model arytmetyki Peano, kt�rego konstrukcje podano wy�ej, mo�e
by� przeliczalny.
\end{uwaga}

\subsection{Zupe�no�� i definiowalno�� a arytmetyka Peano i $ZFC$}

Aksjomaty matematyki, kt�re okre�lamy cz�sto przez $ZFC$ stanowi� niezupe�ny
zbi�r aksjomat�w, gdy� istnieje chocia�by hipoteza continuum
$CH$\footnote{Hipoteza ta m�wi, �e nie ma �adnej liczby kardynalnej pomi�dzy
$\aleph_0$ a $\mathfrak{C}$.  Przyj�cie tej hipotezy lub jej zaprzeczenia jako
aksjomatu nie powoduje �adnej sprzeczno�ci, czyli z ju� przyj�tych za�o�e� nic
na ten temat nie wiadomo.}, kt�ra jest niezale�na od aksjomat�w. Nie jest to
jednak jedyne niezale�ne zdanie, tzn.  nie da si� tak uzupe�ni� $ZFC$ aby by�
to zbi�r zupe�ny. \footnote{Uwaga: Twierdzenie Lindenbauma m�wi, �e takie uzupe�nienie
istnieje, ale absolutnie nie m�wi nam nic o tym, jak je zdefiniowa�.} Podobnie
jest z arytmetyk� Peano.  Co wi�cej zachodz� poni�sze fakty (podajemy je bez
dowod�w).

\begin{tw}[G\"odla]
Ka�de ,,definiowalne'' rozszerzenie arytmetyki Peano lub $ZFC$ jest niezupe�ne.
\end{tw}

\begin{tw}[Tarskiego o niedefiniowalno�ci prawdy]
Niech $T$ b�dzie rozszerzeniem arytmetyki Peano (lub $ZFC$) oraz $\mathbb{A}$
niech b�dzie modelem teorii $T$. W�wczas zbi�r $\{F:\mathbb{A}\models F\}$ jest
niedefiniowalny w $\mathbb{A}$.
\end{tw}

\begin{tw}[G\"odla]
W $ZFC$ nie mo�na udowodni�, �e $ZFC$ jest niesprzeczny o ile jest niesprzeczny.
\end{tw}

%%% 
\section{Twierdzenia Skolema--L\"owenheima i inne twierdzenia o mocach modeli}

\begin{tw}
Je�li teoria $T$ ma modele sko�czone, dowolnie du�e, to ma model niesko�czony.
\end{tw}

\noindent\textbf{Dow�d:} Niech zdania $F_n$ b�d� zdaniami ,,\textit{istnieje co najmniej
$n$ r�nych element�w}''\footnote{Mo�na poda� konstrukcj� takiego zdania. Na
przyk�ad zdanie $F_3$ ma posta�: $\exists_x\exists_y\exists_z (x\neq y)\land(y\neq z)\land(x\neq z)$. 
Oczywi�cie dla du�ych $n$ zdania te s� do�� d�ugie.}. Niech $T'=T\cup\{F_n:n\in\mathbb{N}\}$.
Ka�da sko�czona podteoria $T'$ ma model, poniewa� w�r�d zda� z tej podteorii da
si� znale�� $F_i$ gdzie $i$ jest najwi�ksze, wi�c wystarczy wzi�� model teorii $T$
kt�ry ma przynajmniej $i$ element�w (a zgodnie z za�o�eniami twierdzenia taki model
istnieje). Skoro ka�da sko�czona podteoria $T'$ ma model, to na mocy tw. o zwarto�ci,
teoria $T'$ ma model. Model ten musi by� niesko�czony. Co wi�cej jest to r�wnie�
model teorii $T$. $\square$

\begin{tw}[Skolema--L\"owenheima]
Je�li teoria $T$ ma model niesko�czony, to ma r�wnie� model dowolnej mocy
wi�kszej r�wnej od mocy j�zyka.
\end{tw}

\noindent\textbf{Dow�d:} Poka�emy jak skonstruowa� model dowolnej mocy wi�kszej r�wnej
mocy j�zyka. Niech zbi�r $I$ b�dzie zbiorem szukanej mocy. Zdefiniujmy sta�e
$\{C_i:i\in I\}$ i dodajmy je do j�zyka. Niech $T=\{F:\mathbb{A}\models F\}$.
Stw�rzmy teori� $T' = T\cup\{\neg(C_i = C_j) : i,j\in I \land i\neq j\}$.
Teoria $T'$ ma model, bo ka�da sko�czona podteoria $T'$ ma model tym modelem jest
$\mathbb{A}$. A skoro $T'$ ma model to w modelu tym musi by� co najmniej tyle sta�ych
ile moc $I$. Model teorii $T'$ jest r�wnie� modelem teorii $T$. $\square$

\begin{wniosek}
Je�li istnieje model niesko�czony, to istniej� przynajmniej dwa modele nieizomorficzne.
\end{wniosek}

\begin{przyklad}
Niech $T = \{F:\mathbb{R}\models F\}$ -- teoria sk�adaj�ca si� ze wszystkich zda�
spe�nionych w zbiorze liczb rzeczywistych. Zgodnie z twierdzeniem Skolema--L\"owenheima
istnieje na przyk�ad model mocy $2^{\mathfrak{C}}$ dla takiej teorii $T$. Innymi
s�owy istnieje zbi�r mocy $2^{\mathfrak{C}}$ o w�asno�ciach liczb rzeczywistych.
\end{przyklad}

\begin{uwaga}
Z dowodu tw. G\"odla o pe�no�ci, wynika r�wnie� fakt na temat mocy modelu.
Model kt�ry si� tam pojawia jest co najwy�ej mocy j�zyka. Ma to du�e znaczenie,
gdy� zazwyczaj u�ywamy przeliczalnych j�zyk�w -- istniej� wi�c wtedy modele
przeliczalne. (Wi�cej znajdziesz w odpowiedniej uwadze po twierdzeniu o pe�no�ci.)
\end{uwaga}

%%%
\appendix
\section{Przyk�ady zada�}

\begin{zadanie}
Pokaza�, �e formu�a:
$$\exists_x\forall_y\exists_z [F(y,z)\to F(x,z)]\to[F(x,x)\to F(y,x)]$$
\begin{enumerate}[a)]
\item jest spe�niona w ka�dym modelu sko�czonym,
\item nie jest tautologi� -- wskaza� model niesko�czony, w kt�rym nie
jest spe�niona.
\end{enumerate}
\end{zadanie}

\begin{zadanie}
Niech w j�zyku b�d� dost�pna dwa symbole funkcyjne $\{+,\cdot\}$ oraz dwie
sta�e $\{0,1\}$. 
\begin{enumerate}[a)]
\item Podaj aksjomatyk� cia� o charakterystyce\footnote{Charakterystyka cia�a $\mathbb{K}$ oznaczana
symbolicznie $\chi(\mathbb{K})$ to najmniejsza liczba ,,jedynek'' z tego cia�a,
kt�ra po ,,dodaniu'' da w tym ciele ,,zero''. Je�li przez ,,dodawanie jedynek'' nie
da si� osi�gn�� zera, przyjmujemy, �e charakterystyka r�wna si� zero.} 0.
\item Udowodnij, i� teoria ta (z punktu poprzedniego) nie jest sko�czenie
aksjomatyzowana.
\item Pokaza�, �e je�li $\varphi$ jest zdaniem tego j�zyka, to: je�li zdanie
to jest spe�nione w ka�dym ciele $\mathbb{K}$ o charakterystyce $\chi(\mathbb{K})=0$,
to istnieje taka sta�a $k$, i� zdanie to jest spe�nione we wszystkich cia�ach
o charakterystyce wi�kszej od $k$.
\end{enumerate}
\end{zadanie}

\begin{zadanie}
Maj�c dowody $F\to G$ oraz $G\to H$, dowie�� $F\to H$, gdzie $F,G,H$ to pewne
formu�y.
\end{zadanie}

\begin{zadanie}
Dane s� struktury:
\begin{enumerate}
\item $\langle\mathbb{Z},+,0\rangle$, $\langle\mathbb{R},+,0\rangle$.
\item $\langle\mathbb{Z},+,0\rangle$, $\langle\mathbb{Q},+,0\rangle$.
\end{enumerate}
Rozstrzygn�� czy struktury te s�:
\begin{enumerate}[a)]
\item izomorficzne (je�li tak to poda� izomorfizm, je�li nie, to wykaza�, ze 
go nie ma),
\item maj� te same zbiory zda� w nich prawdziwych (je�li tak, to to wykaza�, 
je�li nie, to poda� zdanie rozr�niaj�ce).
\end{enumerate}
\end{zadanie}

\noindent\textbf{Rozwi�zanie:} Zaczniemy od pokazania, �e w $\langle\mathbb{Z},+,0\rangle$
nie s� spe�nione te same zdania co w $\langle\mathbb{R},+,0\rangle$ i $\langle\mathbb{Q},+,0\rangle$.
Rozwa�my bowiem zdanie:
$$\forall_x\exists_y y+y = x,$$
co s�ownie mo�na by zapisa�: ,,dla ka�dej liczby istnieje jej po�owa'', lub po 
prostu ,,dzielnie przez dwa jest wykonalne zawsze''. Oczywi�cie w zbiorze 
liczb ca�kowitych tak nie jest, bo na przyk�ad dla $x=3$ nie istnieje �aden $y$
nale��cy do $\mathbb{Z}$, kt�ry spe�nia�by $y+y=x$. Czyli punkt $b)$ mamy
w ten spos�b rozwi�zany. Okazuje si� jednak, �e to wystarcza r�wnie� na dow�d,
�e struktury te nie mog� by� izomorficzne, bo gdyby by�y to, zgodnie z udowodnionym
w tym opracowaniu twierdzeniem, musia�by by� w nich spe�nione te same zdania. 

Dla zestawu pierwszego mo�na poda� r�wnie� inne uzasadnienie, �e struktury nie s�
izomorficzne. Wiadomo bowiem, �e zbiory $\mathbb{Z}$ oraz $\mathbb{R}$ nie s�
r�wnoliczne, czyli nie istnieje �adna bijekcja $\mathbb{Z}\to\mathbb{R}$, a co
za tym idzie nie mo�e by� mowy o izomorfizmie (kt�ry musi by� bijekcj� w my�l
definicji).

\begin{zadanie}
Wykaza� niezale�no�� podanych zda� od aksjomat�w teorii porz�dk�w cz�ciowych ($TPC$).
Zdania do rozstrzygni�cia to:
\begin{enumerate}[a)]
\item $\exists_x\forall_y p(x,y)$
\item $\forall_x\exists_y p(x,y)\land \neg p(y,x)$
\end{enumerate}
\end{zadanie}

\noindent\textbf{Rozwi�zanie:} Dla ka�dego ze zda� wystarczy poda� dwa modele 
$TPC$: jeden w kt�rym dane zdanie jest spe�nione, a drugi w kt�rym nie jest spe�nione.

Dla punktu $a)$ mog� to by� $\langle\mathbb{N},\leq\rangle$, w kt�rym zdanie
jest prawdziwe (istnieje jeden $x$ taki, �e wszystkie inne elementa s� od niego
mniejsze b�d� r�wne - jest to oczywi�cie 0), oraz $\langle\mathbb{R},\leq\rangle$,
w kt�rym to zdanie jest fa�szywe (bo nie istnieje element najmniejszy).

Dla punktu $b)$ modelem w kt�rym zdanie jest prawdziwe mo�e by� r�wnie� $\langle\mathbb{N},\leq\rangle$,
poniewa� dla ka�dej liczby naturalnej, istnieje liczba kt�ra jest od niej wi�ksza i kt�ra
zarazem nie jest mniejsza r�wna od niej. Modelem w kt�rym zdanie to nie jest spe�nione
mo�e by� za to model $\langle P(\mathbb{N}),\subseteq\rangle$, czyli zbi�r wszystkich
podzbior�w liczb naturalnych z relacj� bycia podzbiorem. Zauwa�my bowiem, �e dla $x=\mathbb{N}$, 
kt�ry jest oczywi�cie elementem $P(\mathbb{N})$, nie istnieje taki zbi�r kt�ry 
jednoczenie zawiera�by si� w $P(\mathbb{N})$, zawiera� ca�e $\mathbb{N}$ i sam 
nie zawiera� si� w $\mathbb{N}$.

W obu przypadkach widzimy wi�c, �e zdania s� niezale�ne od aksjomat�w $TPC$. 
W niekt�rych modelach s� spe�nione, w innych nie, czyli zale�� od doboru modelu,
a nie od teorii jako takiej. 

%%%
\section{Klasyczny rachunek zda�}

W tym dodatku zawarto aksjomaty klasycznego rachunku oraz przyk�ady zada� wraz z
rozwi�zaniami.

\subsection{Oznaczenia i terminologia}

W klasycznym rachunku zda� wszystkie zmienne s� wolne, nie wyst�puje bowiem
poj�cie kwantyfikatora. St�d nie ma rozgraniczenia na zdania i formu�y. 
Teoretycznie, gdyby�my chcieli trzyma� si� poprzednich definicji (z rachunku
predykat�w) musieliby�my m�wi� tylko o formu�ach klasycznego rachunku zda�,
jednak przyj�o si�, �e mo�na o niech r�wnie� m�wi� zdania.

Definicje zbior�w zupe�nych, niesprzecznych, dowodu, spe�niania itp., s�
niemale�e identyczne jak w rachunku predykat�w, z t� r�nic�, �e formu�y
s� tutaj du�o prostszej postaci (nie ma predykat�w ani kwantyfikator�w, a jedynie
sp�jniki logiczne). Intuicyjny sens tych wszystkich poj�� pozostaje jednak
niezmieniony, tak wi�c pomijamy wszelkie definicje.

\subsection{Aksjomatyka klasycznego rachunku zda�}

Mo�liwe s� r�ne uk�ady systemu aksjomat�w. Prezentujemy tutaj jeden z mo�liwych,
nie koniecznie najlepszy, jednak na pewno poprawny. Poni�sze zapisy to schematy
aksjomat�w, kt�rych jest niesko�czenie wiele. Symbole $F,G,H$ oznaczaj� dowolne
formu�y klasycznego rachunku zda�.

\begin{enumerate}
\item Regu�a symplifikacji:
$$F\to(G\to F)$$
\item Regu�a Fregego:
$$[F\to(G\to H)]\to [(F\to G)\to(F\to H)]$$
\item Regu�a Claviusa:
$$(\neg F\to F) \to F$$
\item Regu�a Dunsa Scotusa:
$$\neg F \to (F\to G)$$
\end{enumerate}

Wszystkie tautologie klasycznego rachunku zda�, mo�na udowodni� w oparciu o ten
zestaw aksjomat�w i znan� ju� z rachunku predykat�w, regu�� odrywania.

\subsection{Przyk�ady zada�}

\begin{zadanie}
Niech zbi�r $A$ zawiera wszystkie te zdania klasycznego rachunku zda�, kt�re
s� prawdziwe przy pewnym, ustalonym, warto�ciowaniu (tj. podstawieniu) $w$.
Niech te� zbi�r $B$ zawiera wszystkie te zdania klasycznego rachunku zda�,
kt�re przy tym samym podstawieniu s� fa�szywe. Sprawdzi� czy zbiory $A$ i
$B$ s� zupe�ne i niesprzeczne.
\end{zadanie}

\noindent\textbf{Rozwi�zanie:} Zauwa�my najpierw, �e zbiory $A$ i $B$ na pewno s�
zupe�ne. Za��my bowiem, �e tak nie jest, tzn. na przyk�ad, �e zbi�r $A$ jest
niezupe�ny. Znaczy�o by to, �e istnieje jaka� formu�a $\varphi$ klasycznego
rachunku zda�, kt�ra nie nale�y do $A$, oraz $\neg\varphi$ nie nale�y do tego�
zbioru. Zauwa�my jednak, �e przy podstawieniu $w$ albo $\varphi$ jest prawidziwa,
albo $\neg\varphi$ jest prawidziwa, wobec czego albo pierwsza, albo druga musi
nale�e� do $A$. Dow�d, �e $B$ jest zupe�ny, jest identyczny. 

Zastan�wmy si�
teraz, czy zbiory te s� niesprzeczne. Zaczniemy od pokazania, �e zbi�r $B$ jest
sprzeczny. Zauwa�my, �e do zbioru $B$ nale�� w szczeg�lno�ci r�wnie�, wszystkie
zaprzecznia tautologii, czyli formu�y kt�re s� fa�szywe przy ka�dym podstawieniu.
No ale z drugiej strony tautologie s� uniwersalne. Tak wi�c, je�li $\varphi$ jest
tautologi� klasycznego rachunku zda�, to na pewno $B\vdash\varphi$ oraz $B\vdash\neg\varphi$.
No a to dok�adnie znaczy, �e zbi�r $B$ jest sprzeczny. Zajmijmy si� wi�c zbiorem $A$.

Zbi�r $A$ zawiera wszystkie formu�y, kt�re s� prawdziwe przy pewnym podstawieniu.
Udowodnimy indukcyjnie twierdzenie, �e je�li jaka� formu�a $\varphi$ daje si�
udowodni� w $A$, to na pewno $\neg\varphi$ nie da si� udowodni� w $A$, a dok�adniej
poka�emy, �e nie istnieje dow�d formu�y $\neg\varphi$ je�li istnieje dow�d $\varphi$
w oparciu o $A$. Na pocz�tku zauwa�my, �e je�li $\varphi$ jest prawdziwa przy podstawieniu
$w$ to nale�y po prostu do $A$, wi�c sama jest swoim dowodem. Je�li $\varphi$ jest
fa�szywa przy podstawieniu $w$, to za to $\neg\varphi$ jest prawidziwa i mo�emy
,,odwr�ci�'' sytuacj�. Zak�adamy wi�c, �e $\varphi$ jest prawdziwa przy podstawieniu
$w$ (co czynimy bez utraty og�lno�ci). Je�li istnia�by dow�d formu�y $\neg\varphi$
w oparciu o $A$ to przynajmniej raz musia�aby zosta� u�yta regu�a odrywania. 
Indukcj� przeprowadzimy wi�c po liczbie u�y� regu�y odrywania w dowodzie i poka�emy
�e mo�na u�ywa� jej niesko�czenie wiele razy, ale to i tak nie pomo�e. Pierwszy
krok indukcji mamy ju� w�a�ciwie za sob�, bo wiemy, �e dla zera jest dobrze.
Mo�emy jednak jeszcze pokaza�, �e jak zastosujemy tylko raz regu�� odrywania, to nic to
nie pomo�e. Gdyby $\neg\varphi$ da�o si� uzyska� stosuj�c raz regu�� odrywania,
to musia�aby istnie� jaka� formu�a $F$, taka, �e zar�wno $F$ jaki i $F\to\neg\varphi$
daj� si� wywie�� bez stosowania regu�y odrywania. No ale to znaczy, �e zar�wno
$F$ jak i $F\to\neg\varphi$ musia�by nale�e� do $A$, co jest niemo�liwe (gdyby $F\to\neg\varphi$
by�o prawdziwe przy podstawieniu $w$, to $F$ musia�oby by� fa�szywe, wi�c nie mog�oby
nale�e� do $A$ i odwrotnie, gdyby $A$ nale�a�o to, ta druga formu�a nie mog�aby nale�e�).
Za��my wi�c, �e przy u�yciu $n$ razy regu�y odrywania nie da si� otrzyma� $\neg\varphi$
z $A$. Poka�emy �e regu�a odrywania zastosowana jeszcze raz nic nie pomo�e.
Za��my, �e budujemy dow�d $\neg\varphi$ i u�yli�my w nim ju� $n$ razy regu�� odrywania.
Chcieliby�my u�y� j� ponownie. W dowodzie tym musia�aby istnie� formu�a $F$ oraz
$F\to\neg\varphi$, kt�re albo nale�� do $F$ albo powsta�y z regu�y odrywania
zastosowanej co najwy�ej $n$ razy (ale razem -- tzn. ��czna liczba regu� odrywania
musi wynosi� $n$ -- co szczerze m�wi� nie wiele zmienia). W zwi�zku z tym, zdania
$F$ oraz $F\to\neg\varphi$ nie mog� by� (zgodnie z za�o�eniem indukcyjnym) fa�szywe
przy podstawieniu $w$. Nie jest to jednak mo�liwe, bo przecie� $\neg\varphi$ jest
przy podstawianiu $w$ fa�szywe, czyli gdyby $F$ by�o prawdziwe, bo $F\to\neg\varphi$
by�oby fa�szywe i na odwr�t. Czyli dwie formu�y $F$ oraz $F\to\neg\varphi$ nie mog�
istnie�. Czyli zastosowanie regu�y odrywania po raz $n+1$ nic nie pomo�e. Tak wi�c
na mocy zasady indukcji matematycznej, mo�emy regu�� odrywania stosowa� bez
ko�ca, a i tak nie pomo�e nam to w uzyskaniu formu�y $\neg\varphi$. Co za tym idzie
zbi�r $A$ jest niesprzeczny. Co ciekawe, w ten spos�b pokazali�my te�, �e �w zbi�r
$A$ jest r�wny $A^\ast$, tzn. nie da si� z niego wywie�� nic wi�cej poza to co
sam zawiera.


\end{document}


