church.tex

\section{Neizračunljive funkcije}

Intuitivni pojam izračunljivog kao onog za što postoji algoritam, zajedno s Church--\!Turingovom tezom, napokon daju mogućnost da dokažemo da za neke probleme ne postoje algoritmi. To ćemo učiniti dokazom da neka funkcija $g$ nije parcijalno rekurzivna --- tada po teoremu ekvivalencije $\beta g$ nije Turing-izračunljiva, po definiciji~\ref{def:izr} $g$ nije izračunljiva, pa možemo reći da za nju ne postoji algoritam.

Najčešće će $g$ biti karakteristična funkcija, jer obično se postojanje algoritma ispituje za \emph{probleme odluke}: za dani skup $A$ i njegov podskup $D$, postoji li algoritam koji za proizvoljni $x\in A$ odlučuje je li $x\in D$? Jednom kada imamo kodiranje $\N A$ skupa $A$, to gledamo kao pitanje izračunljivosti skupa (jednomjesne relacije) $\N A[D]\subseteq\N$, odnosno funkcije $\chi_{\N A[D]}$. Sve te ideje smo već vidjeli, za $A:=\Sigma^*$, kad smo promatrali odlučive jezike u točki~\ref{sec:Todl}.

\begin{definicija}[{name=[odlučivost problema]}]
Za brojevni problem $D$ kažemo da je \emph{odlučiv} ako je njegova karakteristična funkcija $\chi_D$ rekurzivna. Za problem $D\subseteq A$ takav da postoji prirodno kodiranje $\N A:A\to\N$, kažemo da je \emph{odlučiv} ako je brojevni problem $\N A[D]$ odlučiv\!.
\end{definicija}

"Brojevni problemi" nisu ništa drugo nego relacije, ali postavljeni u obliku pitanja, odnosno ispitivanja nekog svojstva. Recimo, $Halt_2=\dom{\f{comp}_2}^3$ možemo promatrati kao problem "za zadane $x,y,e\in\N$, (postoji li i) stane li program koda $e$ s ulazom $(x,y)$?", odnosno "ima li izraz $\kf{e}(x,y)$ vrijednost?". Već smo nagovijestili da taj problem nije odlučiv\!.
Kako bismo to dokazali? Uzmimo za početak nešto lakše. U napomeni~\ref{nap:diagtot} smo već spomenuli paradoks sličan Russellovu, koji nastaje ako pretpostavimo da su svi algoritmi totalni: poredali smo sve jednomjesne algoritme u niz $(\mathcal A_n)_{n\in\N}$, pa smo za ulaz $n$ primijenili $\mathcal A_n$ na $n$, i vratili sljedbenik izlaznog podatka. Pomoću indeks\=a možemo to doslovno napraviti (zovemo ih indeksima jer je niz $(\kf e^1)_{e\in\N}$ popis svih jednomjesnih parcijalno rekurzivnih funkcija, i "indeks funkcije $\f f$" je upravo njen indeks u tom nizu).

\begin{definicija}[{name=[Russellova funkcija i Kleenejev skup]}]
\emph{Russellova funkcija} je jednomjesna funkcija $\f{Russell}^1$ zadana s
\begin{equation}\label{eq:Russelldef}
    \f{Russell}(n):\simeq\f{comp}_1(n,n)+1\text.
\end{equation}
\emph{Kleenejev skup} je domena Russellove funkcije: $K^1:=\dom{\f{Russell}}$.
\end{definicija}

\begin{korolar}[{name=[parcijalna rekurzivnost Russellove funkcije]}]\label{kor:Russellprek}
Russellova funkcija je parcijalno rekurzivna.
\end{korolar}
\begin{proof}
	Iz propozicije~\ref{prop:compspec}, jer je $\f{Russell}$ kompozicija $\f{Sc}$, $\f{comp}_1$ i $\f I_1^1$.
%Definicija~\eqref{eq:Russelldef} u simboličkom obliku glasi $\f{Russell}=\f{Sc}\circ\f{comp}_1\circ(\f I_1^1,\f I_1^1)$, pa tvrdnja slijedi iz propozicije~\ref{prop:compspec}.
\end{proof}

Paradoks iz uvoda sada se može iskazati ovako: imamo algoritam za $\f{Russell}$, ali nijedan algoritam koji računa vrijednosti od $\f{Russell}$ nije totalan. Drugim riječima, Russellova funkcija je izračunljiva, ali ne postoji njeno izračunljivo totalno proširenje.

\begin{lema}[{name=[neproširivost Russellove funkcije do rekurzivne]}]\label{lm:Russellnrek}
Ne postoji rekurzivna funkcija $\f r$ takva da je $\f r|_{K}=\f{Russell}$.
\end{lema}
\begin{proof}
Pretpostavimo da takva funkcija postoji. Tada je ona parcijalno rekurzivna, pa po teoremu ekvivalencije ima indeks, označimo jedan njen indeks s $e$ (pogledajte napomenu~\ref{nap:>1ind'}); i totalna je, pa postoji $q:=\f r(e)\in\N$. Sada je sljedbenik tog broja jednak
\begin{equation}
    1+q=1+\f r(e)=1+\kf e(e)=1+\f{comp}(e,e)\text,
\end{equation}
iz čega slijedi $e\in K$ i $\f{Russell}(e)=1+q$. No $\f r(e)=q\ne 1+q$, pa $\f r$ ne može biti proširenje od $\f{Russell}$, kontradikcija.
\end{proof}

\begin{teorem}[{name=[nerekurzivnost Kleenejeva skupa]}]\label{tm:DRnrek}
Kleenejev skup $K$ nije rekurzivan.
\end{teorem}
\begin{proof}
Pretpostavimo suprotno, i označimo s $\rus:=\IF{K:\f{Russell},\f Z}$ proširenje Russellove funkcije nulom.
%Točkovno, imamo
%\begin{equation}
    %\rus(n):\simeq
%\begin{cases}
%\f{Russell}(n),&n\in K\\
%0,&\text{inače}
%\end{cases}\text.
%\end{equation}
Po korolaru~\ref{kor:Russellprek} $\f{Russell}$ je parcijalno rekurzivna, po pretpostavci suprotnog je $K$ rekurzivna relacija, a $\f Z$ je inicijalna. Prema teoremu~\ref{tm:gprek}, iz toga bi slijedilo da je $\rus$ parcijalno rekurzivna funkcija.

S druge strane, po definiciji~\ref{def:gr} je $R_0:=K\kompl$, pa je
\begin{equation}
    \dom{\rus}=(\dom{\f Z}\cap R_0)\cup(\dom{\f{Russell}}\cap K)=(\N\cap K\kompl)\cup(K\cap K)=K\kompl\cup K=\N\text,
\end{equation}
dakle $\rus$ je totalna funkcija. Sveukupno bismo dobili da je $\rus$ rekurzivna funkcija, što je u kontradikciji s lemom~\ref{lm:Russellnrek}.% (jer je $\rus|_{K}=\f{Russell}$).
\end{proof}

Time smo napokon dokazali da postoji izračunljiva funkcija s neizračunljivom domenom, i vidimo u čemu je problem s našom dosadašnjom intuicijom: iako proširenje nulom doživljavamo kao trivijalnu operaciju na brojevnoj funkciji, za izračunljivost $\tilde{\f f}$ je potrebno ustanoviti kad ulazni podatak $x$ \emph{nije} u domeni $\dom{\f f}$ (da bismo ga preslikali u~$0$) --- a to zapravo zahtijeva da ustanovimo da \emph{nijedna} konfiguracija stroja koji računa $\f f$ s ulazom $x$ nije završna.

To je temeljna nesimetrija u definiciji algoritma: dok je zaustavljanje algoritma moguće karakterizirati neograničenom egzistencijalnom kvantifikacijom (projekcijom), što jest domena izračunljive funkcije (dobivene minimizacijom), njegovo \emph{nezaustavljanje} nije moguće tako karakterizirati. Ukratko, prirodni brojevi imaju lijepo svojstvo \emph{početne konačnosti}: od svakog prirodnog broja ima konačno mnogo manjih, i ako postoji prirodni broj s nekim svojstvom, prateći sljedbenike od nule stići ćemo do njega u konačno mnogo koraka. S druge strane (doslovno!), prirodnih brojeva ima beskonačno mnogo: od svakog broja ima beskonačno mnogo većih, i ako trebamo ustanoviti da neko svojstvo vrijedi za sve prirodne brojeve, to nikako ne možemo učiniti provjeravajući ih pojedinačno. Čak i da ih ne provjeravamo redom, do svakog trenutka smo provjerili samo konačno mnogo njih, među njima postoji najveći, a većih od njega ima jednako mnogo kao i svih prirodnih brojeva.

Naravno, to nije \emph{dokaz} da ne postoji možda neka druga metoda kojom bismo ustanovili da $x\notin\dom{\f f}$ --- samo pokazuje da stvari nisu tako jednostavne.

\subsection{Svođenje i problemi zaustavljanja}

Problem kojim smo se bavili --- za zadani $n$, je li $n$ u domeni od $\kf n^1$ --- čini se vrlo umjetnim: nije da bismo ikad bili doista zainteresirani za općeniti odgovor na to pitanje. Ipak, jednom kad imamo neki neodlučiv problem, možemo se dočepati i ostalih.

Metoda je ista ona pomoću koje iz već poznatih odlučivih problema (izračunljivih funkcija) dobivamo nove: \emph{svođenje} (redukcija). Ako možemo neku funkciju $f$ svesti na neku drugu $g$ --- napisati $f$ pomoću kompozicije, i eventualno primitivne rekurzije, funkcije $g$ s nekim izračunljivim funcijama, tada znamo da ako je $g$ izračunljiva, tada je i $f$ takva. To smo koristili mnogo puta u funkcijskom programiranju --- recimo, pogledajte primjer~\ref{pr:m-v}. Tamo nam je bila bitna primitivna rekurzivnost, pa smo govorili samo o totalnim funkcijama, i primitivna rekurzija je igrala bitnu ulogu. Kad govorimo o (ne)odlučivim problemima, primitivna rekurzivnost gubi na korisnosti, pa ćemo zapravo promatrati samo kompoziciju. Kako se radi o problemima, dakle karakterističnim funkcijama relacija koje su totalne, zbog marljive evaluacije proizlazi da sve funkcije u kompoziciji moraju također biti totalne.

Napomenimo, u literaturi postoje razne vrste svođenja problema, pa i općenitih funkcija. Odabiremo najjednostavniju prikladnu našim potrebama.

\begin{definicija}[{name=[svedivost brojevnih relacija]}]\label{def:svod}
Neka su $k,l\in\N_+$ te $R^k$ i $P^l$ relacije. Kažemo da je $R$ \emph{svediva} na $P$, i pišemo $R\preceq P$, ako postoje rekurzivne funkcije $\f G_1^k$, $\f G_2^k$,~\ldots, $\f G_l^k$ takve da vrijedi $\chi_R=\chi_P\circ(\f G_1,\f G_2,\dotsc,\f G_l)$.
\end{definicija}

Jednakost iz definicije se može točkovno zapisati kao $R(\vec x)\Leftrightarrow P\bigl(\f G_1(\vec x),\dotsc,\f G_l(\vec x)\bigr)$. To je zapravo obična kompozicija $\chi_R=\chi_P\circ G$, samo uzevši u obzir da $G$ ima kodomenu $\N^l$, pa je prikazujemo kroz $l$ koordinatnih funkcija u skladu s napomenom~\ref{nap:brip}.

Također naglasimo da nismo ništa dokomponirali na $\chi_P$ slijeva: ne dozvoljavamo \emph{post-processing} povratne vrijednosti od $\chi_P$, već samo \emph{pre-processing} njenih ulaznih podataka. Kako se radi o karakterističnim funkcijama kodomene $bool=\{0,1\}$, jedini netrivijalni \emph{post-processing} je negiranje, ali upravo smo vidjeli da komplement nije baš jednostavna operacija na problemima (npr.\ na %domenama izračunljivih funkcija, odnosno 
problemima zaustavljanja), pa ga s razlogom ne želimo u ovom kontekstu.

\begin{propozicija}[{name=[refleksivnost i tranzitivnost svedivosti]}]\label{pp:preceqrt}
Relacija $\preceq$ (na skupu %$\bigcup_{k\in\N_+}\!\mathcal P(\N^k)$
	svih brojevnih relacija) je refleksivna i tranzitivna.
\end{propozicija}
\begin{proof}
	Za refleksivnost, stavimo $\f G_1:=\f I_1^l$, $\f G_2:=\f I_2^l$,~\ldots, $\f G_l:=\f I_l^l$ (koordinatne funkcije identitete $id_{\N^l}$). Očito je $\chi_P\circ(\f I_1^l,\dotsc,\f I_l^l)=\chi_P\circ id_{\N^l}=\chi_P$, pa je $P\preceq P$.

	Tranzitivnost je kompliciranija, ali samo zbog napomene~\ref{nap:brip}. Neka su $k,l,m\in\N_+$ te neka su $R^k$, $Q^m$ i $P^l$ relacije takve da je $R\preceq Q\preceq P$. Dakle, postoje rekurzivne funkcije $\f G_1^k$,~\ldots, $\f G_m^k$ takve da je $\chi_R=\chi_Q\circ(\f G_1,\dotsc,\f G_m)$, i rekurzivne funkcije $\f H_1^m$,~\ldots, $\f H_l^m$ takve da je $\chi_Q=\chi_P\circ(\f H_1,\dotsc,\f H_l)$. Sada je (možemo svuda pisati jednakosti jer su sve funkcije ili karakteristične ili rekurzivne, dakle totalne, a kompozicija totalnih je totalna po propoziciji~\ref{prop:comptot})
\begin{multline}\label{eq:tranzpreceq}
    \chi_R(\vec x)=\chi_Q\bigl(\f G_1(\vec x),\dotsc,\f G_m(\vec x)\bigr)=\bigl(\chi_P\circ(\f H_1,\dotsc,\f H_l)\bigr)\bigl(\f G_1(\vec x),\dotsc,\f G_m(\vec x)\bigr)=\\
    =\chi_P\bigl(
    \f H_1\bigl(\f G_1(\vec x),\dotsc,\f G_m(\vec x)\bigr),\dotsc,
    \f H_l\bigl(\f G_1(\vec x),\dotsc,\f G_m(\vec x)\bigr)
    \bigr)=\\
    =\chi_P\bigl(
    \bigl(\f H_1\circ(\f G_1,\dotsc,\f G_m)\bigr)(\vec x),\dotsc,
    \bigl(\f H_l\circ(\f G_1,\dotsc,\f G_m)\bigr)(\vec x)\bigr)=\\
    =\bigl(\chi_P\circ\bigl(\f H_1\circ(\f G_1,\dotsc,\f G_m),\dotsc,\f H_l\circ(\f G_1,\dotsc,\f G_m)\bigr)\bigr)(\vec x)\text,
\end{multline}
	pa ako definiramo $\f F_i:=\f H_i\circ(\f G_1,\dotsc,\f G_m)$ za sve $i\in[1\mspace{-1mu}\dd l]$, sve te funkcije su rekurzivne po lemi~\ref{lm:comprek}. Sada~\eqref{eq:tranzpreceq} postaje $\chi_R=\chi_P\circ(\f F_1,\dotsc,\f F_l)$, odakle slijedi $R\preceq P$.
\end{proof}

$R\preceq P$ znači da ako imamo algoritam za rješavanje problema $P$, pomoću njega možemo riješiti i problem $R$. Intuitivno, $R$ je "barem toliko odlučiv" koliko i $P$.

\begin{propozicija}[{name=[svedivost čuva rekurzivnost]}]\label{pp:rek<rek}
Relacija svediva na rekurzivnu relaciju je i sama rekurzivna.
\end{propozicija}
\begin{proof}
Neka su $k,l\in\N_+$ te $\f R^k$ relacija i $\f P^l$ rekurzivna relacija takve da je $\f R\preceq\f P$.\\
	To znači $\chi_{\f R}=\chi_{\f P}\circ(\f G_1,\dotsc,\f G_l)$, pa je $\f R$ rekurzivna po lemi~\ref{lm:comprek}.
\end{proof}

\begin{korolar}[{name=[inverz svedivosti čuva neodlučivost]}]\label{kor:nrek<nrek}
Ako su $R$ i $P$ problemi takvi da $R$ nije odlučiv i $R\preceq P$, tada ni $P$ nije odlučiv\!.
\end{korolar}
\begin{proof}
Ovo je samo kontrapozicija propozicije~\ref{pp:rek<rek}, iskazana jezikom problema.
\end{proof}

% \section{Problemi zaustavljanja}

Korolar~\ref{kor:nrek<nrek}, kao što smo već nagovijestili, omogućuje nam da pomoću jednog neodlučivog problema dođemo do ostalih.

\begin{propozicija}[{name=[neodlučivost problema zaustavljanja za RAM-strojeve]}]\label{pp:Haltnodl}
Problemi $Halt_1$ i $HALT$ nisu odlučivi.
\end{propozicija}
\begin{proof}
Tvrdimo da vrijedi $K(n)\Leftrightarrow Halt_1(n,n)$. Doista,
\begin{equation*}
    K=\dom{\f{Russell}}\!=\dom{\f{Sc}\,\circ\,\f{comp}_1\circ\,(\f I_1^1,\f I_1^1)}\!=\dom{\f{comp}_1\circ\,(\f I_1^1,\f I_1^1)}\!
    =\left\{n\;\middle\vert\;\bigl(\f I_1^1(n),\f I_1^1(n)\bigr)\in\dom{\f{comp}_1}\right\}
    =\{n\mid(n,n)\in Halt_1\}\text,
\end{equation*}
gdje smo koristili korolar~\ref{kor:comptot} da se riješimo sljedbenika.\newline Iz toga slijedi $K\preceq Halt_1$, pa je $Halt_1$ neodlučiv po korolaru~\ref{kor:nrek<nrek} i teoremu~\ref{tm:DRnrek}.

	Slično, po definiciji iz korolara~\ref{kor:funHaltTk}, vrijedi $Halt_1(x,e)\Leftrightarrow HALT(\kr x,e)$, a funkcija $\f{Code}^1$ je primitivno rekurzivna po propoziciji~\ref{prop:Codekprn}, pa je $Halt_1\!\preceq HALT$, iz čega je i $HALT$ neodlučiv\!.
\end{proof}

U literaturi se $Halt_1$ odnosno $HALT$ (kako gdje) zove \emph{halting problem} (problem zaustavljanja), jer postavlja pitanje stane li određeno izračunavanje (zadano pomoću RAM-programa i ulaza za njega). Mogli bismo dokazati i neodlučivost problema $Halt_k$ za $k\ge 2$ (pokušajte formalno dokazati svođenje $Halt_1(x,e)\Leftrightarrow Halt_k(x,0,0,\dotsc,0,e)$), ali to će slijediti jednom kad dokažemo teorem o parametru.

Po Church--\!Turingovoj tezi, ne postoji algoritam koji bi za svaki par $(P,u)$ RAM-programa $P$ i njegovog ulaza $u$ odlučivao stane li $P$-izračunavanje s $u$ --- odnosno, za svaki algoritam $\mathcal A$ postoje $P\in\mathscr Prog$ i $u\in\N$ takvi da $\mathcal A$ ne daje ispravan odgovor na pitanje stane li $P$-izračunavanje s $u$. Ali vrijedi i više: možemo postići da $P$ ne ovisi o~$\mathcal A$. To je u skladu s univerzalnošću: postoji "najkompliciraniji" RAM-stroj, čiji je problem zaustavljanja najteži.

\begin{korolar}[{name=[neodlučivost problema zaustavljanja za jedan fiksni RAM-stroj]}]\label{kor:RAMhaltnodl}
Postoji RAM-program $P_0$, takav da nijedan algoritam ne može točno odrediti,\\ za svaki $u\in\N$, stane li $P_0$-izračunavanje s $u$.
\end{korolar}
\begin{proof}
%Kompiliramo (teorem~\ref{tm:pir}) simboličku definiciju funkcije $\f{Russell}$ koju smo dobili u dokazu korolara~\ref{kor:Russellprek}. Tako dobijemo RAM-program $P_0$, za koji po definiciji~\ref{def:compute} vrijedi: za svaki $t\in\N$, $P_0$-izračunavanje s $t$ stane ako i samo ako je $t\in K$.
Po korolaru~\ref{kor:Russellprek}, Russellova funkcija je parcijalno rekurzivna. Po teoremu~\ref{tm:pir}, ona je i RAM-izračunljiva. Označimo s $P_0$ jedan RAM-program koji je računa. Po definiciji~\ref{def:compute}, za svaki $u\in\N$, $P_0$-izračunavanje s $u$ stane ako i samo ako je $u\in K$.

Kad bi postojao algoritam za odlučivanje problema zaustavljanja $P_0$-izračunavanja s proizvoljnim $u$, po Church--\!Turingovoj tezi $K$ bi bio odlučiv problem, što je u kontradikciji s teoremom~\ref{tm:DRnrek}.
\end{proof}

\begin{lema}[{name=[neodlučivost problema zaustavljanja za jedan fiksni Turingov stroj]}]\label{lm:THaltnodl}
Postoji Turingov stroj $\mathcal T_0$ nad unarnom abecedom $\Sigma_{\t\textbullet}=\{\t\textbullet\}$, takav da nijedan algoritam ne može točno odrediti, za svaku riječ $w\in\t\textbullet^*$\!, stane li $\mathcal T_0$-izračunavanje s $w$.
\end{lema}
\begin{proof}
Jezična funkcija $\rho:=\t\textbullet\f{Russell}$ je Turing-izračunljiva po korolaru~\ref{kor:peuf}, a po definiciji unarne reprezentacije vrijedi
\begin{equation}\label{eq:rhoRussell}
    \rho(\t\textbullet^t)\simeq\t\textbullet^{\f{Russell}(t)}\text.
\end{equation}
To znači da za $\mathcal T_0$ možemo uzeti Turingov stroj koji računa $\rho$ --- koji jest nad unarnom abecedom, i stane točno za riječi oblika $\t\textbullet^t,t\in K$.

Sad, kada bi postojao algoritam koji bi za svaku riječ nad $\Sigma_{\t\textbullet}$ odlučivao hoće li $\mathcal T_0$-izračunavanje s njome stati, pomoću njega bismo mogli odlučiti $K$, sljedećim algoritmom: za ulaz $u\in\N$, konstruiramo riječ $\t\textbullet^u$, i vratimo stane li $\mathcal T_0$-izračunavanje s njom. Po definiciji~\ref{def:Tcomputefi}, to će biti ako i samo ako je $\t\textbullet^u\in\dom\rho$, što će prema definiciji unarne reprezentacije biti ako i samo ako je $u\in K$. Po Church--\!Turingovoj tezi, to bi značilo da je $K$ rekurzivna, što je u kontradikciji s teoremom~\ref{tm:DRnrek}.
\end{proof}

\begin{propozicija}[Neodlučivost problema zaustavljanja za Turingove strojeve]\ \\
Za svaku abecedu $\Sigma$ postoji Turingov stroj nad njom, čiji je problem zaustavljanja neodlučiv\!.
\end{propozicija}
\begin{proof}
Ako je $\t\textbullet\;\raisebox{1.1pt}{$\in$}\;\Sigma$, možemo primijeniti lemu~\ref{lm:THaltnodl} na Turingov stroj $\mathcal T_0$ nad abecedom $\Sigma$. Kad bi postojao algoritam koji za svaku riječ $w\in\Sigma^*$ točno određuje stane li $\mathcal T_0$-izračunavanje s $w$, to bi posebno moralo vrijediti za sve $w\in\t\textbullet^*\subseteq\Sigma^*$, što je u kontradikciji s lemom~\ref{lm:THaltnodl}.

Ako pak $\t\textbullet\notin\Sigma$, uzmimo neki konkretni znak $\alpha\in\Sigma$ (po definiciji abecede je $\Sigma\ne\emptyset$, pa $\alpha$ postoji), i \emph{zamijenimo} ga s \t\textbullet: gledamo Turingov stroj $\mathcal T_0'$ koji izgleda kao $\mathcal T_0$ iz prethodnog odlomka, osim što umjesto \t\textbullet\ ima $\alpha$ --- kako u $\Sigma$, tako i u $\Gamma$ i u svim prijelazima od $\delta$. S obzirom na to da znakovi radne abecede nemaju nikakvu imanentnu semantiku (osim praznine, ali za to pogledajte sljedeći odlomak), $\mathcal T_0'$-izračunavanje s $\alpha^u$ stane ako i samo ako $\mathcal T_0$-izračunavanje s $\t\textbullet^u$ stane --- pa kad bi neki algoritam za svaku $w\in\Sigma^*$ točno određivao stane li $\mathcal T_0'$-izračunavanje s $w$, tada bi to posebno vrijedilo i za sve riječi oblika $\alpha^u,u\in\N$, pa bismo opet imali kontradikciju s neodlučivošću od $K$ kao u prethodnom odlomku.

Postoji još samo jedan slučaj koji nismo uzeli u obzir: što ako je praznina stroja $\mathcal T_0$ upravo~\t\textbullet? Tada ona po definiciji nije u $\Sigma$, ali je ne možemo samo zamijeniti s $\alpha$ jer $\alpha$ jest u $\Sigma$. U tom slučaju odaberemo neki novi znak $\beta\notin\Gamma$, proglasimo ga prazninom, i \t\textbullet\ zamijenimo s $\beta$ u $\Gamma$ i $\delta$. Nakon toga primijenimo postupak iz prethodnog odlomka.
\end{proof}

\section{Neodlučivost logike prvog reda}

%Jedan od najvažnijih rezultata o neodlučivosti je svakako Churchov teorem o neodlučivosti logike prvog reda.
U uvodnom kursu matematičke logike obično se za logiku sudova dokažu teoremi adekvatnosti i potpunosti (koji povezuju sintaksni pojam dokazivosti sa semantičkim pojmom valjanosti) te se navedu neki sustavi (npr.\ glavni test) koji u potpunosti određuju je li neka formula valjana ili nije. Drugim riječima, postoji algoritam za utvrđivanje valjanosti. Postoji li \emph{polinomni} algoritam za to, zanimljivije je pitanje koje vodi na slavni milijun dolara vrijedan problem $P\stackrel?=NP$ --- ali barem znamo da je valjanost odlučiva. Štoviše, dobra je vježba, koristeći kodiranje opisano u primjeru~\ref{pr:lskod}, formalno dokazati da je skup $\f{PValid}\subset\f{PF}$, svih kodova valjanih formula logike sudova, primitivno rekurzivan. Praktički jedino na što treba misliti je da je ne možemo kodirati (totalne) interpretacije jer ih ima neprebrojivo mnogo, ali parcijalne interpretacije (s konačnom domenom) možemo.

Za logiku prvog reda također vrijede teoremi adekvatnosti i potpunosti (dakle, postoji dokaz za formulu $\phi$ koji koristi samo aksiome i pravila zaključivanja logike prvog reda, ako i samo ako je $\phi$ istinita u svim $\sigma$-strukturama prvog reda, gdje je $\sigma$ signatura koja sadrži sve nelogičke simbole u $\phi$), i također imamo glavni test, i znamo da je korektan (odgovor koji dade je uvijek točan), ali nije totalan --- mogu postojati beskonačne grane, u kojima algoritam ne daje odgovor. I to nije nedostatak specifičnog algoritma: jedan od prvih i najvažnijih rezultata o neodlučivosti je Churchov teorem da \textbf{problem valjanosti za logiku prvog reda nije odlučiv}. Skraćeno kažemo "logika prvog reda nije odlučiva", jer zapravo nije bitno da se radi o problemu valjanosti. Ekvivalentno možemo promatrati probleme ispunjivosti, oborivosti, proturječnosti, ili zaključivanja (logičke posljedice konačnog skupa formula), i svi su oni međusobno svedivi. Ovdje ćemo se baviti problemom koji prirodno ima oblik problema zaključivanja, pa se prvo usredotočimo na njegovu vezu s problemom valjanosti.

\begin{definicija}[{name=[problem valjanosti i problem zaključivanja]}]
    Označimo s $F1$ skup svih formula logike prvog reda,\newline
	\hspace*{6.1em}
	a s $\Valid\subset F1$ skup svih valjanih formula među njima.

	\emph{Problem valjanosti} pita: za zadanu formulu $\phi\in F1$, je li $\phi\in\Valid\mspace{2mu}$?

\emph{Problem zaključivanja} pita: za zadane $\phi_1,\phi_2,\dotsc,\phi_k,\phi\in F1$,\newline
	\hspace*{14.1em}je li $\phi$ logička posljedica skupa $\{\phi_1,\dotsc,\phi_k\}$?
\end{definicija}

\begin{propozicija}[{name=[međusobna svedivost valjanosti i zaključivanja]}]\label{pp:valj<>zaklj}
Problemi valjanosti i zaključivanja svedivi su jedan na drugi.
\end{propozicija}
\begin{proof}[Skica dokaza]
Možemo samo neformalno govoriti o svođenju, jer još nismo precizirali abecedu i jezik logike prvog reda. Taj jezik jest detaljno prikazan u~\cite{skr:VukML}, ali nad beskonačnom abecedom, što nije dovoljno dobro za naše potrebe (pokušajte otkriti na kojim smo sve mjestima dosad koristili konačnost abecede). Uz nekoliko modifikacija prilagodit ćemo taj jezik teoriji formalnih jezika, ali zasad samo opišimo ideje.

U jednom smjeru, zamislimo da imamo instancu problema valjanosti, i algoritam ("crnu kutiju") za odluku problema zaključivanja. Pitamo se što uvrstiti u taj algoritam, da dobijemo odgovor na pitanje valjanosti. Ako zadana instanca pita je li $\phi$ valjana, odgovor na to pitanje je isti kao i na pitanje je li $\phi$ posljedica praznog skupa formula --- dakle stavimo $k=0$ (i ne moramo zadavati formule $\phi_i$ jer ih nema).

U drugom smjeru je zanimljivije. Pretpostavimo da imamo algoritam za utvrđivanje valjanosti, a zadane su nam formule $\phi_1$, $\phi_2$,~\ldots, $\phi_k$ i $\phi$, s pitanjem je li $\phi$ logička posljedica ovih prethodnih. Svođenje možemo opisati indukcijom po $k\in\N$. Baza je ista kao gore: za $k=0$, zapravo se pitamo je li $\phi$ valjana. Pretpostavimo da je problem zaključivanja za $k=l$ svediv na problem valjanosti, i pogledajmo problem zaključivanja za $k=l+1$. Također, zbog jakog teorema potpunosti svejedno je koristimo li relaciju logičke posljedice $\models$ ili izvedivosti $\vdash$.

Ako je zadnja premisa $\phi_{l+1}$ \emph{rečenica} (zatvorena formula, bez slobodnih varijabli), možemo primijeniti teorem dedukcije (za jedan smjer --- drugi smjer je trivijalan pomoću pravila zaključivanja \emph{modus ponens}):
\begin{equation}\label{eq:prebaci}
\phi_1,\dotsc,\phi_l,\phi_{l+1}\vdash\phi\text{\quad ako i samo ako\quad}
\phi_1,\dotsc,\phi_l\vdash(\phi_{l+1}\to\phi)\text,
\end{equation}
zbog kojeg je problem zaključivanja s $l+1$ premisom svediv na problem zaključivanja s $l$ premisa, a onda po pretpostavci indukcije i po tranzitivnosti na problem valjanosti.

Ako formula $\phi_{l+1}$ nije rečenica, umjesto nje možemo promotriti njeno \emph{univerzalno zatvorenje} $\overline{\phi_{l+1}}$, dobiveno univerzalnim kvantificiranjem svih slobodnih varijabli u $\phi_{l+1}$. Iz logike znamo da $\mathfrak N\models\phi_{l+1}$ ako i samo ako $\mathfrak N\models\overline{\phi_{l+1}}$, dakle odgovor na problem zaključivanja neće se promijeniti, a $\overline{\phi_{l+1}}$ jest rečenica, pa možemo primijeniti teorem dedukcije kao u prethodnom odlomku.
\end{proof}
Za dovršetak odnosno formalizaciju dokaza još bi trebalo vidjeti da je funkcija koja preslikava $\bigl(\phi_1,\dotsc,\phi_l,\phi_{l+1},\phi\bigr)$ u $\bigl(\phi_1,\dotsc,\phi_l,(\overline{\phi_{l+1}}\to\phi)\bigr)$ rekurzivna (zadana s $l+1$ koordinatnih funkcija na kodovima, prvih $l$ od kojih su inicijalne), što zasad ne možemo jer nemamo kodiranje skupa~$F1$ --- ali je intuitivno jasno da to možemo učiniti samo mehaničkim manipulacijama simbolima od kojih se formule sastoje.

\subsection{Reprezentacija RAM-konfiguracija formulama prvog reda}

Osnovna ideja dokaza Churchova teorema je svesti problem zaustavljanja za RAM-strojeve na problem zaključivanja. Iz toga će onda Churchov teorem odmah slijediti po propoziciji~\ref{pp:Haltnodl} i korolaru~\ref{kor:nrek<nrek}.

Dakle, neka su $k\in\N_+$, $P\in\mathscr Pr\mspace{-1mu}o\mspace{-2mu}g$ te $\vec u\in\N^k$ (u logici prvog reda obično individualne varijable označavamo s $x_i$, pa ćemo ovdje koristiti $u_i$ kao uobičajenu oznaku za ulazne podatke). Trebamo konstruirati skup formula $\Gamma$ i formulu $\zeta$, koji ovise o $P$ i $\vec u$, tako da $P$-izračunavanje s $\vec u$ stane ako i samo ako vrijedi $\Gamma\models\zeta$. Štoviše, zbog korolara~\ref{kor:RAMhaltnodl}, zapravo možemo cijelu konstrukciju provesti za fiksni $P$ (i za $k=1$), pa ga nećemo pisati (iako smo svjesni da će $\Gamma$ i $\zeta$ ovisiti o $P$).

Logičko zaključivanje je, u osnovi, traženje "puta" od premisa do zaključka, i osnovni razlog zašto je to težak problem je što znamo da put (\hspace{-1pt}\emph{izvod}) postoji kad ga nađemo, ali dok ga nismo našli, ne znamo je li to zato što ne postoji, ili samo nismo tražili dovoljno dugo. To vrlo podsjeća na traženje "puta" od početne do završne konfiguracije pri rješavanju problema zaustavljanja --- možemo li nekako formalizirati tu vezu?

U $\Gamma$ bi se trebala nalaziti neka formula $\pi_{\vec u}$ koja opisuje početnu konfiguraciju s ulazom $\vec u$, a $\zeta$ bi trebala biti formula koja opisuje završnu konfiguraciju --- ne zanima nas rezultat izračunavanja, nego samo zaustavljanje, pa $\zeta$ može biti egzistencijalno kvantificirana po stanju registara, i samo fiksirati vrijednost programskog brojača, a onda ne mora ovisiti o $\vec u$.

Instrukcije programa $P$ mogli bismo shvatiti kao pravila zaključivanja --- recimo, $3.\;\incr1$ kaže da iz formule koja predstavlja konfiguraciju $(x,y,\vec z,0,\dotsc,3)$ možemo izvesti formulu koja predstavlja konfiguraciju $(x,y\!+\!1,\vec z,0,\dotsc,4)$, za sve $x$, $y$ i $\vec z$. Nažalost, standardni račun logike prvog reda (\emph{račun predikata}) ne dopušta nam imati vlastita (nelogička) pravila zaključivanja; "osuđeni" smo na \emph{modus ponens} i generalizaciju. Srećom, \emph{modus ponens} je vrlo općenito pravilo, koje može simulirati ostala pravila pomoću odgovarajućih nelogičkih aksioma --- primjerice, ako bismo htjeli imati pravilo kojim iz $\phi$ i $\eta$ izvodimo $\theta$, dovoljno je u nelogičke aksiome dodati formulu $\bigl(\phi\to(\eta\to\theta)\bigr)$. Tada možemo iz tog aksioma i $\phi$ izvesti $(\eta\to\theta)$, pa onda iz te formule i $\eta$ izvesti $\theta$, koristeći samo \emph{modus ponens}.

Taj pristup ćemo koristiti ovdje, odnosno u $\Gamma$ ćemo imati po jednu formulu $\iota_i$ za svaku instrukciju programa $P$ (s rednim brojem $i$). Još je preostalo objasniti što ćemo s ovim trotočkama u konfiguracijama (odnosno kako reprezentirati konačni nosač), i što s aritmetičkim operacijama ($+$ za \inc, $-$ za \dec).

Konfiguracije prikazujemo određenim atomarnim formulama. Sadržaj programskog brojača, budući da je jedan od konačno mnogo njih (za fiksni RAM-program $P$), kodirat ćemo statički, kroz supskript relacijskog simbola odgovarajuće atomarne formule --- a sadržaj pojedinih registara preko terma u toj formuli. Ipak, kako svaka formula može sadržavati samo konačno mnogo terma, morat ćemo se ograničiti na relevantne registre.

Aritmetiku bismo mogli prikazati nekom
varijantom Peanove aritmetike, ali zapravo možemo i lakše: budući da je sve što nam treba sljedbenik i prethodnik, dovoljno je imati jedan konstantski simbol ("nulu") i jedan jednomjesni funkcijski simbol ("sljedbenik"). Zatvoreni termi na očit način predstavljaju prirodne brojeve: broj $u$ predstavljamo termom dobivenim $u$-strukom primjenom tog funkcijskog simbola na taj konstantski simbol.

Naglasimo da \emph{ne} promatramo logiku prvog reda s jednakošću --- nećemo imati potrebu promatrati jednakost kao relacijski simbol s nekim posebnim svojstvima. Usporedba s nulom za instrukcije tipa \dec\ bit će sintaksna.

Formalnije: krenimo od RAM-algoritma $P^k$, duljine $n:=n_P$ i širine $m:=m_{P^k}$.\\ Signatura $\sigma$, nad kojom ćemo graditi naše formule, imat će:
\begin{itemize}
    \item jedan konstantski simbol $\mathsf o$;
    \item jedan jednomjesni funkcijski simbol $\mathsf s$;
    \item $n+1$ $m$-mjesnih relacijskih simbola $R_0^m$,~$R_1^m$,~\ldots,~$R_n^m$.
\end{itemize}

Za svaki $u\in\N$, $\overline u$ označava zatvoreni term $\mathsf s(\mathsf s(\dotsb(\mathsf s(\mathsf o))\dotsb\mspace{-2mu}))$ s $u$ pojava funkcijskog simbola $\mathsf s$: $\overline 0=\mathsf o$, $\overline 1=\mathsf s(\mathsf o)$, $\overline 2=\mathsf s\bigl(\mathsf s(\mathsf o)\bigr)$ i tako dalje. Za sve $\vec u=(u_1,u_2,\dotsc,u_k)\in\N^k$ definiramo formulu
\begin{equation}\label{eq:defpiu}
    \pi_{\vec u}:=R_0(\mathsf o,\overline{u_1},\overline{u_2},\dotsc,\overline{u_k},\mathsf o,\mathsf o,\dotsc,\mathsf o)\text,
\end{equation}
gdje nakon $\overline{u_k}$ ima još $m-k-1$ simbola $\mathsf o$ (po definiciji je $m=m_{P^k}=\max\,\{m_P,k+1\}\ge k+1$, pa je $m-k-1=m-(k+1)\in\N$).

Za svaki $i\in[0\dd n\rangle$, definiramo formulu $\iota_i$ ovisno o tipu instrukcije $I_i$ programa $P$:
\smallskip

$\rhd$ Ako je to $i.\;\incr j$, definiramo
    \begin{equation}\label{eq:formINC}
        \iota_i:=\bigl(R_i(x_0,\dotsc,x_{m-1})\to R_{i+1}(x_0,\dotsc,x_{j-1},\mathsf s(x_j),x_{j+1},\dotsc,x_{m-1})\bigr)\text.
    \end{equation}

$\rhd$ Ako je to $i.\;\decr jl$, definiramo
    \begin{multline}\label{eq:formDEC}
        \iota_i:=\bigl(
        \bigl(
        R_i(x_0,\dotsc,x_{j-1},\mathsf o,x_{j+1},\dotsc,x_{m-1})\to R_l(x_0,\dotsc,x_{j-1},\mathsf o,x_{j+1},\dotsc,x_{m-1})
        \bigr)
        \land{}\\
        {}\land
        \bigl(
        R_i(x_0,\dotsc,x_{j-1},\mathsf s(x_j),x_{j+1},\dotsc,x_{m-1})\to R_{i+1}(x_0,\dotsc,x_{m-1})
        \bigr)
        \bigr)\text.
    \end{multline}

$\rhd$ Ako je to $i.\;\goto\;l$, definiramo
    \begin{equation}\label{eq:formGOTO}
        \iota_i:=\bigl(R_i(x_0,\dotsc,x_{m-1})\to R_l(x_0,\dotsc,x_{m-1})\bigr)\text.
    \end{equation}

\noindent Definiramo skup i formulu
\begin{align}
\SwapAboveDisplaySkip
    \Gamma_{\vec u}&:=\{\pi_{\vec u}\}\cup\{\iota_i\mid i\in[0\dd n\rangle\}\text,\\
%\shortintertext{i formulu}
\label{eq:defzeta}
    \zeta&:=\exists\,x_0\,\dotsm\,\exists\, x_{m-1}R_n(x_0,\dotsc,x_{m-1})\text.
\end{align}

\subsection{Zaključivanje kao zaustavljanje}

Neka je $P^k$ RAM-algoritam, $\vec u$ ulaz za njega, i pomoću njih konstruirajmo $\Gamma_{\vec u}$ i $\zeta$ kako je opisano u prethodnoj točki.
%\begin{lema}
%Ako vrijedi $\Gamma_{\vec u}\models\zeta$, tada $P$-izračunavanje s $\vec u$ stane.
%\end{lema}
%\begin{proof}
Također, neka je $(c_t)_{t\in\N}$ $P$-izračunavanje s $\vec u$. Promotrimo $\sigma$-strukturu $\mathfrak N$ s nosačem $\N$ i interpretacijom nelogičkih simbola zadanom s:
\begin{itemize}
	\item $\mathsf o^{\mathfrak N}:=0$,
	\item $\mathsf s^{\mathfrak N}:=\f{Sc}$ te
    \item za svaki $i\in[0\dd n]$,
    $
		R_i^{\mathfrak N}:=\bigl\{
        \bigl(c_t(\reg0),\dotsc,c_t(\reg{m-1})\bigr)
        \bigm|
        t\in\N\land c_t(\textsc{pc})=i
		\,\bigr\}
    $.
\end{itemize}
	Indukcijom po $r$ se dokaže $\overline r^{\mathfrak N}=r$ za sve $r\in\N$, pa $\mathfrak N\models R_{pc}(\overline{r_0},\overline{r_1},\dotsc,\overline{r_{m-1}})$ --- odnosno $\mathfrak N\models_v R_{pc}(x_0,x_1,\dotsc,x_{m-1})$, gdje je $v$ valuacija takva da je $v(x_j)=r_j$ za sve $j\in[0\dd m\rangle$ --- neformalno znači da RAM-stroj s programom $P$ i ulazom $\vec u$ može doći u konfiguraciju $(r_0,r_1,\dotsc,r_{m-1},0,0,\dotsc,pc)$ (nakon $t$ koraka izračunavanja).

\begin{lema}[{name=[istinitost početne formule u $\mathfrak N$]}]\label{lm:Npiu}
Vrijedi $\mathfrak N\models\pi_{\vec u}$.
\end{lema}
\begin{proof}
Gledajući~\eqref{eq:defpiu}, tražimo $t\in\N$ takav da je $c_t(\textsc{pc})=0$ i $c_t(\reg j)=\begin{smallcases}
	u_j,&j\in[1\mspace{-1mu}\dd k]\\
0,&\text{inače}
\end{smallcases}\!$; drugim riječima, $c_t$ treba biti početna konfiguracija s ulazom $\vec u$, a ona se sigurno postiže za $t=0$. % (možda i za neke druge $t$, ali jedan nam je dovoljan).
\end{proof}

\begin{lema}[{name=[istinitost instrukcijskih formula u $\mathfrak N$]}]\label{lm:Niotai}
Za svaki $i\in[0\dd n\rangle$ vrijedi $\mathfrak N\models\iota_i$.
\end{lema}
\begin{proof}
Očekivano, imat ćemo slučajeve ovisno o tipu $i$-te instrukcije programa $P$.

Ako je to \inc, dakle $i.\;\incr j$ za neki $j$, tada mora biti $j<m_P\le m$, i trebamo vidjeti da u $\mathfrak N$ vrijedi formula~\eqref{eq:formINC}. Ta formula je kondicional, pa uzmimo proizvoljnu valuaciju $v$ i pretpostavimo da u $\mathfrak N$ uz valuaciju $v$ vrijedi njen antecedens: $\mathfrak N\models_v R_i(x_0,\dotsc,x_{m-1})$. To znači da postoji $t$ takav da je $c_t=\bigl(v(x_0),\dotsc,v(x_{m-1}),0,\dotsc,i\bigr)$, no takva konfiguracija po definiciji~\ref{def:RAMconf}\eqref{stav:leadINC} prelazi u
\begin{equation}\label{eq:nextINC}
	\bigl(v(x_0),\dotsc,v(x_{j-1}),v(x_j)+1,v(x_{j+1}),\dotsc,v(x_{m-1}),0,\dotsc,i+1\bigr)\text.
\end{equation}
	S druge strane, $c_t\leadsto c_{t+1}$ po definiciji~\ref{def:compute}, pa po lemi~\ref{lema:ramdet} imamo da je~\eqref{eq:nextINC} upravo $c_{t+1}$ (to ćemo koristiti i kasnije). Drugim riječima, stroj može postići konfiguraciju~\eqref{eq:nextINC}, iz čega slijedi (jer je $v(x_j)+1=\f{Sc}\bigl(v(x_j)\bigr)=\mathsf s^{\mathfrak N}\bigl(v(x_j)\bigr)=\bigl(\mathsf s(x_j)\bigr){}^{\mathfrak N}[v]$)
\begin{equation}
    \mathfrak N\models_v R_{i+1}\bigl(x_0,\dotsc,x_{j-1},\mathsf s(x_j),x_{j+1},\dotsc,x_{m-1}\bigr)\text,
\end{equation}
odnosno u $\mathfrak N$ uz valuaciju $v$ vrijedi i konzekvens formule~\eqref{eq:formINC}, što smo trebali.

	Ako je instrukcija $i.\;\decr jl$ za neke $j<m$ i $l\le n$, tada trebamo dokazati da u $\mathfrak N$ (uz proizvoljnu valuaciju $v$) vrijedi formula~\eqref{eq:formDEC}. Ta formula je konjunkcija dva kondicionala, pa trebamo dokazati da vrijede oba, sličnom metodom kao u prethodnom odlomku. Za prvi, pretpostavimo da vrijedi $\mathfrak N\models_v R_i(x_0,\dotsc,x_{j-1},\mathsf o,x_{j+1},\dotsc,x_{m-1})$. To znači da postoji $t$ takav da je $c_t=\bigl(v(x_0),\dotsc,v(x_{j-1}),0,v(x_{j+1}),\dotsc,v(x_{m-1}),0,\dotsc,i\bigr)$ (jer je $\mathsf o^{\mathfrak N}[v]=\mathsf o^{\mathfrak N}=0$), no takva konfiguracija po definiciji~\ref{def:RAMconf}\eqref{stav:leadDEC0} prelazi u konfiguraciju
\begin{equation}
    c_{t+1}=\bigl(v(x_0),\dotsc,v(x_{j-1}),0,v(x_{j+1}),\dotsc,v(x_{m-1}),0,\dotsc,l\bigr)\text,
\end{equation}
dostižnu u $t+1$ koraka, pa vrijedi $\mathfrak N\models_v R_l(x_0,\dotsc,x_{j-1},\mathsf o,x_{j+1},\dotsc,x_{m-1})$.

	Za drugi, pretpostavimo $\mathfrak N\models_v R_i(x_0,\dotsc,x_{j-1},\mathsf s(x_j),x_{j+1},\dotsc,x_{m-1})$. Kao u \inc-slučaju, $\bigl(\mathsf s(x_j)\bigr){}^{\mathfrak N}[v]=v(x_j)+1$, što je pozitivno zbog $v(x_j)\in\dulj{\mathfrak N}=\N$, pa to znači da postoji $t$ takav da je $c_t=\bigl(v(x_0),\dotsc,v(x_{j-1}),v(x_j)+1,v(x_{j+1}),\dotsc,v(x_{m-1}),0,\dotsc,i\bigr)$. Po definiciji~\ref{def:RAMconf}\eqref{stav:leadDEC-} ta konfiguracija prelazi u $c_{t+1}=\bigl(v(x_0),\dotsc,v(x_{m-1}),0,\dotsc,i+1\bigr)$ te vrijedi $\mathfrak N\models_v R_{i+1}(x_0,\dotsc,x_{m-1})$, čime smo dokazali i drugi kondicional.

Ako je instrukcija $i.\;\goto\;l$ za neki $l\le n$, tada opet uzmemo proizvoljnu valuaciju $v$, i trebamo dokazati da uz nju u $\mathfrak N$ vrijedi formula~\eqref{eq:formGOTO}. To slijedi iz definicije~\ref{def:RAMconf}\eqref{stav:leadGOTO}, jer se stanje registara u ovom slučaju uopće ne mijenja, samo se vrijednost programskog brojača promijeni iz $i$ u $l$.
\end{proof}

\begin{propozicija}[{name=[zaključivanje povlači zaustavljanje]}]\label{pp:models>stop}
Za svaki $\vec u\in\N^k$, ako $\Gamma_{\vec u}\models\zeta$, tada $P$-izračunavanje s $\vec u$ stane.
\end{propozicija}
\begin{proof}
Pretpostavka $\Gamma_{\vec u}\models\zeta$ znači da u svakoj strukturi u kojoj vrijede sve formule iz $\Gamma_{\vec u}$, vrijedi i formula $\zeta$. Leme~\ref{lm:Npiu} i~\ref{lm:Niotai} pokazuju da je $\mathfrak N$ takva struktura, pa vrijedi $\mathfrak N\models\zeta$. Čitajući~\eqref{eq:defzeta}, vidimo da to znači da za svaku valuaciju $v$ (pa posebno, recimo, za onu koja sve varijable preslika u $0$) postoji valuacija $v'$, koja se podudara s $v$ na svim individualnim varijablama $x_i,i\ge m$, takva da vrijedi
\begin{equation}
	\bigl(v'(x_0),\dotsc,v'(x_{m-1})\bigr)\in R_n^{\mathfrak N}\text.
\end{equation}
	Valuacije nam zapravo ovdje uopće nisu bitne --- jedino što je bitno je da iz toga slijedi $R_n^{\mathfrak N}\ne\emptyset$, pa postoji $t\in\N$ takav da je $c_t(\textsc{pc})=n$. No to znači da je $c_t$ završna konfiguracija, pa $P$-izračunavanje s $\vec u$ stane nakon najviše $t$ koraka.
\end{proof}

%\subsection{Zaustavljanje povlači zaključivanje}

Sada nam je cilj dokazati obrat propozicije~\ref{pp:models>stop}. Bitna razlika je u tome što sad moramo \emph{dokazati} da je $\zeta$ logička posljedica od $\Gamma_{\vec u}$, pa više ne možemo koristiti "intendiranu interpretaciju" s prirodnim brojevima, nego moramo provesti argumentaciju za proizvoljnu $\sigma$-strukturu $\mathfrak M$ u kojoj vrijedi $\Gamma_{\vec u}$. Ta struktura ne mora biti izomorfna s $\mathfrak N$, ne mora čak ni zadovoljavati jednostavne aksiome poput injektivnosti sljedbenika (zapravo, ne možemo ih ni \emph{iskazati} jer nemamo simbol za jednakost u teoriji), ali svejedno ćemo moći pokazati da u njoj vrijedi $\zeta$.

Pa neka je $\mathfrak M=(M,\Theta,g,S_0,S_1,\dotsc,S_n)$ proizvoljna $\sigma$-struktura (redom imamo $\mathsf o^{\mathfrak M}=:\Theta\in M$, $\mathsf s^{\mathfrak M}=:g:M\to M$, a za svaki $i\in[0\dd n]$, $R_i^{\mathfrak M}=:S_i\subseteq M^m$), i neka vrijedi $\mathfrak M\models\Gamma_{\vec u}$.

Neka je $(c_t)_{t\in\N}$ $P$-izračunavanje s $\vec u$. Za proizvoljne $t\in\N$ i $j\in[0\dd m\rangle$, označimo\\ $a_j^t:=\overline{c_t(\reg j)}^{\mathfrak M}\!=g\bigl(g(\dotsb g(\Theta)\dotsb\mspace{-1mu})\bigr)$, gdje ima $c_t(\reg j)$ poziva funkcije $g$.

\begin{lema}[{name=[izračunavanje čuva istinitost formula pojedinih konfiguracija]}]\label{lm:formcomputesteps}
Za svaki $t\in\N$ vrijedi $\mathfrak M\models R_{c_t(\textsc{pc})}\bigl(\overline{c_t(\reg0)},\dotsc,\overline{c_t(\reg{m-1})}\bigr)$,\newline odnosno $(a_0^t,a_1^t,\dotsc,a_{m-1}^t)\in S_{c_t(\textsc{pc})}$.
\end{lema}
\begin{proof}
Indukcijom po $t$. Za $t=0$, tražena formula je upravo $\pi_{\vec u}$, koja se nalazi u $\Gamma_{\vec u}$ pa po pretpostavci vrijedi u $\mathfrak M$. Pretpostavimo da tvrdnja vrijedi za $t=b$, i pogledajmo tvrdnju za $t=b+1$. Ako je $c_b$ završna konfiguracija, tada je $c_{b+1}=c_b$ jer završne konfiguracije prelaze (jedino) u same sebe, pa je formula za $c_{b+1}$ ista kao formula za $c_b$, i vrijedi u $\mathfrak M$ po pretpostavci indukcije. Inače, $i:=c_b(\textsc{pc})<n$, pa postoji instrukcija programa $P$ s rednim brojem $i$, i također je $\iota_i\in\Gamma_{\vec u}$, dakle $\mathfrak M\models\iota_i$.

Ako je ta instrukcija tipa \inc, recimo $i.\;\incr j$ za neki $j<m$, tada u $\mathfrak M$ vrijedi~\eqref{eq:formINC}, odnosno uz valuaciju $v(x_j):=a_j^b$, vrijedi
\begin{equation}
\label{eq:korakINC}
	\bigl(a_0^b,\dotsc,a_{j-1}^b,g(a_j^b),a_{j+1}^b,\dotsc,a_{m-1}^b\bigr)\in S_{i+1}\text,
\end{equation} uz pretpostavku $(a_0^b,\dotsc,a_{m-1}^b)\in S_i=S_{c_b(\textsc{pc})}$. No ta pretpostavka je upravo pretpostavka indukcije, pa onda vrijedi i~\eqref{eq:korakINC}. A formula~\eqref{eq:korakINC} je upravo formula koja odgovara konfiguraciji $c_{b+1}$, jer je $i+1=c_b(\textsc{pc})+1=c_{b+1}(\textsc{pc})$, i
\begin{equation}
	a_j^{b+1}=\overline{c_{b+1}(\reg j)}^{\mathfrak M}\!=\overline{1+c_b(\reg j)}^{\mathfrak M}\!=\bigl(\mathsf s\bigl(\overline{c_b(\reg j)}\bigr)\bigr)^{\mathfrak M}\!=\mathsf s^{\mathfrak M}\bigl(\overline{c_b(\reg j)}^{\mathfrak M}\bigr)=g(a_j^b)\text.
\end{equation}
	Ako je ta instrukcija tipa \goto, s odredištem $l\le n$, uz istu valuaciju imamo da $\vec a\in S_i$ povlači $\vec a\in S_l$. Tvrdnja $\vec a\in S_i$ je pretpostavka indukcije, dok je $\vec a\in S_l$ upravo tvrdnja koja nam je potrebna za korak (stanje registara ostaje isto, odnosno $a_j^b=a_j^{b+1}$ za svaki $j\in[0\dd m\rangle$).

	Ako je ta instrukcija tipa \dec, recimo $\decr jl$, promotrimo slučajeve s obzirom na to je li $c_b(\reg j)=0$ (pogrešno je reći "s obzirom na to je li $a_j^b=\Theta$", jer nitko ne brani da bude npr.\ $g(\Theta)=\Theta$, odnosno $\overline1^{\mathfrak M}=\overline0^{\mathfrak M}$). Ako jest, imamo istu argumentaciju kao u prethodnom odlomku, jer se stanje registara tada ne mijenja: $\vec a\in S_i$ povlači $\vec a\in S_l$ po prvom konjuktu u~\eqref{eq:formDEC}. Ako nije, tada je sigurno $c_b(\reg j)\ge1$, pa promotrimo~\eqref{eq:formDEC} (odnosno njen drugi konjunkt) uz valuaciju
$v'(x_h):=\begin{smallcases}
	a_h^b=\overline{c_b(\reg h)}^{\mathfrak M},&h\ne j\\
	\overline{c_b(\reg j)-1}^{\mathfrak M},&h=j
\end{smallcases}$.
	Uz tu valuaciju vrijedi antecedens, jer je $\bigl(\mathsf s(x_j)\bigr){}^{\mathfrak M}[v']=a_j^b$ --- pa onda vrijedi i konzekvens, odnosno formula s istim sadržajem registara, osim što je $c_{b+1}(\reg j)$ za jedan manji, i $c_{b+1}(\textsc{pc})$ za jedan veći, kao što i treba biti.
\end{proof}

\begin{propozicija}[{name=[zaustavljanje povlači zaključivanje]}]\label{pp:stop>models}
Ako $P$-izračunavanje s $\vec u$ stane, tada $\Gamma_{\vec u}\models\zeta$.
\end{propozicija}
\begin{proof}
	Pretpostavimo da izračunavanje $(c_t)_{t\in\N}$ stane, odnosno postoji $t_0$ takav da je $c_{t_0}(\textsc{pc})=n$. Da bismo dokazali $\Gamma_{\vec u}\models\zeta$, uzmimo proizvoljnu $\sigma$-strukturu $\mathfrak M$ u kojoj vrijedi $\Gamma_{\vec u}$. Za tu strukturu vrijedi lema~\ref{lm:formcomputesteps}, pa posebno za $t=t_0$ vrijedi $(a_0^{t_0},\dotsc,a_{m-1}^{t_0})\in S_n$. To znači da za svaku valuaciju $v$ možemo naći $v'$ koja se podudara s $v$ u svim varijablama $x_j$ za $j\ge m$, a $v'(x_j)=a_j^{t_0}$ za $j<m$, takvu da vrijedi $\mathfrak M\models_{v'}R_n(x_0,\dotsc,x_{m-1})$. No to upravo znači $\mathfrak M\models\zeta$.
\end{proof}

%\subsection{Neformalna izreka Churchova teorema}

\begin{teorem}[Churchov teorem o neodlučivosti logike prvog reda]\label{tm:Church}\ \\
Ne postoji algoritam koji za proizvoljnu formulu logike prvog reda odlučuje je li valjana.
\end{teorem}
\begin{proof}
Pretpostavimo da imamo takav algoritam $\mathcal A$,\\ i opišimo sljedeći neformalni algoritam za odluku Kleenejeva skupa:
\begin{quote}
Kao u dokazu korolara~\ref{kor:RAMhaltnodl} (kompiliranjem), dobijemo RAM-program $P_0$ koji računa Russellovu funkciju. Za taj program uvedimo oznake $m$ i $n$ te formule $\iota_i,i<n$ i $\zeta$ nad signaturom $\sigma$ (koja također ovisi o $P_0$ preko $m$).

Za ulaz $u\in\N$ (koji dalje promatramo kao $(u)\in\N^1$):
\begin{enumerate}
    \item Konstruiramo formulu $\pi_u$.
    \item Konstruiramo konačan skup $\Gamma_u$.
    \item Konstruiramo instancu problema zaključivanja $\Gamma_u%\mathrel{\begin{array}[b]{@{}c@{}}
    %\renewcommand\arraystretch{0.1}
    %\vphantom{{\scriptstyle?}}\\[-9pt]
    \models^?
    %\end{array}}
    \zeta$.
    \item\label{step:varphi_u} Pretvorimo je (koristeći dokaz propozicije~\ref{pp:valj<>zaklj})\\ u instancu problema valjanosti neke formule $\varphi_u$.
    \item Provjerimo (koristeći $\mathcal A$) je li tako dobivena formula valjana.
\end{enumerate}
\end{quote}
Taj algoritam odlučuje Kleenejev skup, jer za svaki $u\in\N$ vrijedi:% sljedeći lanac ekvivalencija:
\begin{equation}\label{eq:lanaceqv}
    u\in K\Longleftrightarrow\text{$P_0$-izračunavanje s $u$ stane}\Longleftrightarrow(\Gamma_u\models\zeta)\Longleftrightarrow{}(\models\varphi_u)\text.
\end{equation}
Prva ekvivalencija je definicija~\ref{def:compute}, jer je $K=\dom{\f{Russell}}$, a $P_0$ računa $\f{Russell}$. Druga ekvivalencija je u jednom smjeru propozicija~\ref{pp:stop>models}, a u drugom smjeru propozicija~\ref{pp:models>stop}. Treća ekvivalencija je dobivena primjenom propozicije~\ref{pp:valj<>zaklj}.

Dakle, pod pretpostavkom da $\mathcal A$ ispravno odlučuje koje su formule prvog reda valjane a koje nisu, upravo opisani neformalni algoritam ispravno odlučuje koji su brojevi elementi Kleenejeva skupa a koji nisu. Po Church--\!Turingovoj tezi, to bi značilo da je relacija $K$ rekurzivna, što je u kontradikciji s teoremom~\ref{tm:DRnrek}.
\end{proof}

%\subsection{Formule prvog reda kao formalni jezik}

Time je dokazan Churchov teorem, ali na neformalnoj razini --- "dokazali" smo da ne postoji neformalni algoritam, pozivanjem na Church--\!Turingovu tezu. Možemo li bez toga?

\subsection{Formule prvog reda kao formalni jezik}

Rekli smo da probleme obično shvaćamo kao jezike: odlučivost problema je tu rekurzivnost (karakteristične funkcije kodiranja) jezika čiji elementi su riječi koje predstavljaju instance problema na koje je odgovor potvrdan. U ovom slučaju, promotrili bismo jezik $\Valid$ (nad nekom abecedom $\Sigma_{\log}$, dovoljno bogatom da može izraziti svaku formulu logike prvog reda) u kojem bi se nalazile samo valjane formule. Ako uspijemo dokazati da $\Valid$ nije rekurzivan, "odgurat" ćemo primjenu Church--\!Turingove teze na sam kraj dokaza, i pseudokod u dokazu teorema~\ref{tm:Church} moći ćemo zamijeniti pravom rekurzivnom funkcijom koja svodi $K$ na $\Valid$ (preciznije $\kr{\Valid}$).

Hoćemo li time dobiti išta vrednije nego u prethodnoj točki? Da, jer imamo garanciju da smo barem svođenje napisali egzaktno --- a ako prihvatimo definiciju~\ref{def:izr}, argument postaje sasvim matematički bez pozivanja na intuiciju pojma algoritma.

Za početak uvedimo abecedu $\Sigma_{\log}$. Koristimo pristup blizak standardnom, samo s konačnom abecedom. (To je važan uvjet: bez njega, na primjer, funkcija prijelaza ne bi bila konačna, pa bi dokaz leme~\ref{lm:newssdprn} bio bitno kompliciraniji.) Recimo, uobičajeni alfabet logike prvog reda ima beskonačno mnogo individualnih varijabli $x_0$, $x_1$, $x_2$,~\ldots\ --- ali kad pogledamo kako ih doista pišemo, posebno kasnije ($x_{38}$, $x_{904}$,~\ldots), vidimo da su sve one zapravo riječi nad $11$-članom abecedom $\{x,{}_0,{}_1,{}_2,{}_3,{}_4,{}_5,{}_6,{}_7,{}_8,{}_9\}$. Drugim riječima, tradicionalni alfabet našeg jezika je beskonačan jer nije atomaran: s\=am se može shvatiti kao (regularni) jezik nad elementarnijom abecedom, koja jest konačna.

Taj fenomen je uobičajen u modernim programskim jezicima: imaju hijerarhiju jezičnih "slojeva", koji im omogućuju da njihova teorija ostane utemeljena u teoriji formalnih jezika, a da ipak budu dovoljno izražajni. Recimo, po analogiji s prethodnim odlomkom, najčešće imaju prebrojivo mnogo varijabli (imena za podatke), no sve su one jednostavnim pravilima sastavljene od konačno mnogo mogućih znakova. Konkretno, u programskom jeziku C imena varijabli čine jezik nad $63$-članom abecedom $\{\t\_,\t a,\t b,\t c,\dotsc,\t z,\t A,\t B,\t C,\dotsc,\t Z,\t 0,\t 1,\t 2,\dotsc,\t 9\}$, zadan pravilom da prvi znak ne smije biti znamenka, a čitavo ime ne smije biti nijedna od konačno mnogo ključnih riječi.

Ta \emph{leksička} struktura prirodno se nalazi "ispod" sintaksne strukture programskog jezika, u smislu da se leksički analizator izvršava prije sintaksnog, i predaje mu samo tipove \emph{tokena} pronađenih u izvornom kodu. Recimo, iako su \t{abc} i \t{xy} dvije različite varijable, u sintaksno ispravnom programu možemo zamijeniti jednu drugom i sigurno nećemo uvesti sintaksnu grešku --- iako ćemo vjerojatno uvesti neke semantičke greške poput nedeklariranih varijabli.

Vrlo je slična stvar i u logici prvog reda: $x_2$ i $x_{58}$ su različite individualne varijable, ali ako sintaksa kaže da na nekom mjestu (recimo neposredno iza kvantifikatora) mora doći varijabla, tada može doći bilo koja varijabla, i formula će ostati sintaksno ispravna. Ili, na početku atomarne formule mora stajati relacijski simbol, ali možemo staviti bilo koji relacijski simbol $R_i$ --- mora biti odgovarajuće mjesnosti, ali to samo znači da se mjesnost može zaključiti iz ostatka atomarne formule, pa je ne treba pisati. Recimo, \t{(R(x)\textrightarrow R(x,x))} je formula u kojoj postoje dva relacijska simbola: $R_0^1$ i $R_0^2$.

Mogli bismo dakle tako raditi, ali je dekadski zapis supskripta nespretan. Već smo prikazivali prirodne brojeve u unarnom zapisu, zašto ne i ovdje? Tradicionalna matematika poznaje zapise $x$, $x'$, $x''$,~\ldots\ --- što je upravo naš prebrojiv skup individualnih varijabli, samo nad manjom abecedom $\{x,'\!\}$. Isti pristup upotrijebit ćemo za konstantske ($c$, $c'$, $c''$,~\ldots), funkcijske ($f$, $f'$,~\ldots) i relacijske ($R$, $R'$,~\ldots) simbole.

Ostatak alfabeta logike prvog reda je konačan i možemo ga ubaciti u našu abecedu, ali radi jednostavnosti uzet ćemo minimalni skup veznika i kvantifikatora $\{\lnot,\to,\forall\}$ (tzv\!.\ \emph{osnovni jezik} --- pogledajte~\cite[str.\ 124]{skr:VukML} za obrazloženje). Još moramo imati zarez i zagrade za konstrukciju složenih terma i atomarnih formula, a (vanjske) zagrade ćemo koristiti i pri pisanju kondicionala. Negacija i univerzalna kvantifikacija su prefiksni operatori, višeg prioriteta od kondicionala, pa im ne trebamo pisati zagrade.

U abecedu ćemo dodati i separator \t\#, koji ćemo koristiti u radu s konačnim nizovima formula --- najvažniji primjer bit će \emph{dokazi}, odnosno izvodi iz nekog konačnog (ili barem odlučivog) skupa aksioma.

%\subsection{Kodiranje formula prvog reda}

\begin{definicija}[{name=[logička abeceda i njeno kodiranje]}]
\emph{Logička abeceda} je zadana prvim retkom tablice
\begin{equation}
    \begin{array}{r|cccccccccccc}
        \Sigma_{\log}& \t x & \t c & \t f & \t R & \t, & \t' & \t( & \t) & \t{$\lnot$} & \t\textrightarrow & \t{$\forall$} & \t\# \\\hline
         \N\Sigma_{\log}& 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 & 11 & 12
    \end{array}\text.
\end{equation}
Njeno kodiranje zadano je drugim retkom te tablice. Njena pomaknuta baza je $12$. \end{definicija}

\begin{primjer}[{name=[kodiranje formule "ne postoji najveći element"]}]
Pogledajmo formulu $\varphi:=\forall x\exists y(x<y)$. Kao što znamo, ona je ljepši zapis za nešto poput $\forall x_0\exists x_1 R_1^2(x_0,x_1)$ (ako postoji jednakost --- a ovdje vjerojatno postoji ako teorija govori o uređaju $<$ --- obično se simbol $R_0^2$ rezervira za nju), a ona se može u osnovnom jeziku napisati kao \t{$\forall$x$\lnot\forall$x'$\lnot$R'(x,x')}, pa je njen kod $\kr{\varphi}=(B19\,B169\,4671\,5168)_{12}=14\,318\,611\,220\,424\,608$.
\end{primjer}

\begin{primjer}[{name=[kodiranje jednostavne aritmetičke formule]}]
Kodirajmo formulu $1+1=2$. Prikladna teorija je recimo Peanova aritmetika, čija je formalna reprezentacija u alfabetu teorije prvog reda dana tablicom
\begin{equation}
    \begin{array}{c|c|c|c}
        \text{naziv}&\text{neformalno}&\text{simbol}&\text{nad }\Sigma_{\log}\\\hline
        \text{nula} & 0 & c_0 & \t c\\
        \text{sljedbenik} & x' & f_0^1 & \t{f(x)} \\
        \text{zbrajanje} & x+y & f_0^2 & \t{f(x,x')}\\
        \text{množenje} & xy & f_1^2 & \t{f'(x,x')}\\
        \text{jednakost} & x=y & R_0^2 & \t{R(x,x')}\\
        \text{uređaj} & x<y & R_1^2 & \t{R'(x,x')}
    \end{array}
\end{equation}
Time formula u osnovnom jeziku postaje \t{R(f(f(c),f(c)),f(f(c)))}, s kodom\\ $\kr{1+1=2}=(473\,7372\,8537\,2885\,3737\,2888)_{12}=2\,544\,115\,135\,095\,560\,147\,164\,520$.
\end{primjer}

%\begin{definicija}[{name=[jezici svih i valjanih formula prvog reda]}]
%Nad logičkom abecedom promotrimo sljedeće jezike:
%\begin{quote}
%\begin{labeling}{$\Valid$}
%\item[$F1$] Skup svih formula prvog reda.
%\item[$\Valid$] Skup svih valjanih formula prvog reda.\qedhere
%\end{labeling}
%\end{quote}
%\end{definicija}

\begin{propozicija}[{name=[odlučivost jezika svih formula prvog reda]}]\label{pp:F1odl}
    Jezik $F1$ nad abecedom $\Sigma_{\log}$ je odlučiv\!.
\end{propozicija}
\begin{proof}[Skica dokaza] Puni dokaz ovoga odveo bi nas predaleko u teoriju formalnih jezika. Tamo se promatraju razne klase jezika (koje čine tzv\!.\ \emph{Chomskyjevu hijerarhiju}) te \emph{gramatike} i \emph{automati} za njih. Turingovi odlučitelji iz točke~\ref{sec:Todl} vrsta su takvih automata, no postoje i jednostavniji automati, koji prepoznaju jednostavnije jezike.

Specijalno, u sintaksnoj analizi vrlo je bitna klasa \emph{beskontekstnih} jezika, koje generiraju beskontekstne gramatike, a prepoznaju ih potisni automati. Potisni automat je specijalni slučaj (nedeterminističnog višetračnog) Turingova stroja, a beskontekstna gramatika se može zapisati u \emph{Chomskyjevoj normalnoj formi}, osiguravajući da njegovo izračunavanje uvijek stane --- pa se može smatrati Turingovim odlučiteljem.

Jedna beskontekstna gramatika za jezik $F1$ zadana je pravilima
\begin{align}
    Form&\to Rel\t(Terms\t)\mid\t{$\lnot$} Form\mid\t(Form\t\textrightarrow Form\t)\mid\t{$\forall$}\,Var\,Form\\
    Terms&\to Term\mid Terms\t,Term\\
    Term&\to Var\mid Const\mid Func\t(Terms\t)
\end{align}
uz tipove tokena
    \begin{align}
	    \SwapAboveDisplaySkip
    Var&\to\t x\mid Var\t'\\
    Const&\to\t c\mid Const\t'\\
    Func&\to\t f\mid Func\t'\\
    Rel&\to\t R\mid Rel\t'
\end{align}
($Var$, $Const$, $Func$ i $Rel$ su leksičke varijable, dok su $Form$, $Term$ i $Terms$ sintaksne varijable; $Form$ je početna varijabla). Objašnjenje pojmova i dokaze tvrdnji koje smo naveli zainteresirani čitatelj može pronaći u~\cite{sipser}.
\end{proof}

Iz prethodne propozicije slijedi (po teoremu~\ref{tm:oikr}) da je $\kr{F1}$ rekurzivan skup. Drugim riječima, ako restringiramo $\N\Sigma_{\log}^*$ na formule prvog reda zapisane u osnovnom jeziku, imamo kodiranje formula. Za konstruktore tog skupa moramo prvo napraviti leksičke konstruktore za pojedine tokene. U nastavku često koristimo konkatenaciju u pomaknutoj bazi $12$ koju zovemo jednostavno \emph{konkatenacijom} i u skladu s tim umjesto $\conc{1\!2}$ pišemo samo $\conc{}$. Još nam treba jedan jednostavni rezultat.

\begin{korolar}[{name=[(prava) podriječ ima (strogo) manji kod]}]\label{kor:krvw}
Ako je riječ $v$ prava podriječ od $w$, tada je $\kr v<\kr w$.
\end{korolar}
\begin{proof}
    Nejednakost~\eqref{eq:injNSz} kaže da manji broj ne može imati dulji zapis u pomaknutoj bazi. Dakle, kraća riječ mora imati manji kod, a očito je $\dulj v<\dulj w$.
\end{proof}

\subsection{Formalna izreka Churchova teorema}

\begin{lema}[{name=[primitivna rekurzivnost leksičke strukture formula prvog reda]}]\label{lm:lexF1}
Funkcije $\f{Var}$, $\f{Const}$, $\f{Func}$ i $\f{Rel}$, koje preslikavaju $i\in\N$\\ redom u $\kr{x_i}$, $\kr{c_i}$, $\kr{f_i}$ i $\kr{R_i}$, primitivno su rekurzivne.
\end{lema}
\begin{proof}
Zapravo je jedini zanimljivi dio vidjeti da je "potenciranje" (uzastopna konkatenacija) znaka odnosno riječi, $Repeat(w,n):=w^n$, primitivno rekurzivno. Prateća funkcija te operacije može se napisati primitivnom rekurzijom i konkatenacijom:
\begin{align}
    \f{Repeat}(x,0)&=\kr{\varepsilon}=0\text,\\
    \f{Repeat}(x,n+1)&=\f{Repeat}(x,n)\conc{}x\text.
\end{align}
    Sada, uz pokratu $t:=\f{Repeat}(6,i)=\kr{\t{'{}'{}'}\dotsm\t'}$, imamo $\f{Var}(i):=\kr{\t{\,x{}'{}'}\dotsm\t'}=1\conc{}t$ --- i analogno $\f{Const}(i):=2\conc{}t$, $\f{Func}(i):=3\conc{}t$ te $\f{Rel}(i):=4\conc{}t$.
\end{proof}

Introdukciju logičkih veznika mogli bismo obavljati na sličan način, samo ih treba izraziti u osnovnom jeziku. Recimo, primitivno rekurzivna funkcija
\begin{equation}\label{eq:Conjunction}
    \f{Conjunction}(x,y):=
    \kr{\t{$\lnot$(\,}}\conc{}
    x\conc{}
    \kr{\t{\textrightarrow$\,\lnot$}}\conc{}
    y\conc{}
    \kr{\,\t)}=
    115\conc{}
    x\conc{}
    129\conc{}
    y\conc{}
    8
\end{equation}
ima svojstvo da je $\f{Conjunction}(\kr{\varphi},\kr{\psi})=\kr{\varphi\land\psi}$ (preciznije $\kr{\t{$\lnot$(}\varphi\,\t{\textrightarrow\,$\lnot$}\psi\t)}$ u osnovnom jeziku) za sve formule $\varphi$ i $\psi$, pa se može shvatiti kao introdukcija konjunkcije na kodovima. Za eliminaciju možemo iskoristiti pristup grubom silom (\emph{brute force}):
\begin{align}
    \f{IsConjunction}(x,y,z)&:\Longleftrightarrow y\in\kr{F1}\land z\in\kr{F1}\land x=\f{Conjunction}(y,z)\text,
\\\label{eq:lconj}
    \f{LeftConjunct}(x)&:=(\mu y<x)(\exists z<x)\f{IsConjunction}(x,y,z)\text,
\\\label{eq:rconj}
    \f{RightConjunct}(x)&:=(\mu z<x)(\exists y<x)\f{IsConjunction}(x,y,z)\text.
\end{align}

Koristili smo propoziciju~\ref{pp:F1odl}, teorem~\ref{tm:oikr} te korolar~\ref{kor:krvw} za ograničavanje kvantifikacije i minimizacije. Brojni drugi trikovi takvog tipa, uključujući i sasvim netrivijalne stvari poput supstitucije terma za varijablu u formuli, mogu se vidjeti u~\cite{smullyan}.

Za univerzalno zatvorenje zapravo ne moramo nalaziti slobodne varijable u formuli --- s obzirom na to da je $\forall x\varphi$ ekvivalentna s $\varphi$ ako $x$ nije slobodna u $\varphi$, dovoljno je naći neki konačni \emph{nadskup} skupa slobodnih varijabli. A kako za svaku varijablu $x_n$ koja se pojavljuje (slobodno ili vezano) u $\varphi$ vrijedi da je odgovarajuća riječ $\t{x{}'{}'}\dotsm\t'$ podriječ duljine $n+1$ od $\varphi$, slijedi da mora biti $n<n+1\le\dulj\varphi=\f{slh}(\kr{\varphi},12)$. Dakle, ako nam je zadan kod $c$ formule $\varphi$, dovoljno je ispred "nalijepiti" samo one kvantifikatore $\forall x_i$ za $i<\f{slh}(c,12)$, i možemo biti sigurni da smo dobili univerzalno zatvorenje.

\noindent\begin{align}
    \f{UnivQuant}(i)&:=\kr{\forall x_i}=\kr{\forall}\conc{}\kr{x_i}=11\conc{}\f{Var}(i)\\
    \f{UnivQuants}(0)&:=\kr{\varepsilon}=0\\
    \f{UnivQuants}(i+1)&:=\kr{\forall x_0\forall x_1\forall x_2\dotsm\forall x_i}=\f{UnivQuants}(i)\conc{}\f{UnivQuant}(i)\\
    \f{UnivClosure}(c)&:=\f{UnivQuants}\bigl(\f{slh}(c,12)\bigr)\conc{}\,c
\end{align}
Sada je funkcija $\f{UnivQuant}$ primitivno rekurzivna po lemi~\ref{lm:lexF1} i propoziciji~\ref{pp:concprn}, zatim $\f{UnivQuants}$ po propoziciji~\ref{prop:F1prn}, a onda i $\f{UnivClosure}$ po propoziciji~\ref{pp:concprn} i lemi~\ref{lm:ldcpprn}.

Zapravo, kako u našem slučaju --- reprezentacija problema zaustavljanja RAM-stroja preko valjanosti formula prvog reda --- koristimo samo prvih $m$ varijabli ($m$ je konstanta), dovoljna će nam biti funkcija $c\mapsto\f{UnivQuants}(m)\conc{}c$.

Pogledajmo kako u osnovnom jeziku izgleda formula $\varphi_u$ iz dokaza teorema~\ref{tm:Church}\eqref{step:varphi_u}. To ovisi o instrukcijama programa $P_0$ koji računa Russellovu funkciju, ali dio koji nam je jedini bitan za svođenje je prilično malen i odnosi se samo na formulu $\pi_u$.

Preciznije, neka je $P_0=\begin{prog}t.&I_t\end{prog}_{t<n}$. U $\Gamma_u$ imamo formule $\iota_t,t<n$, čija se univerzalna zatvorenja obrnutim redom prebacuju na desnu stranu~\eqref{eq:prebaci}, gdje na početku stoji samo formula $\zeta$. Na kraju nam na lijevoj strani ostane samo $\pi_u$ (formulu na desnoj stani tada označimo s $\psi$), koju ne trebamo univerzalno zatvarati jer je rečenica. Formula $\psi$, iako ogromna, ne ovisi o $u$ --- ako konstruiramo funkciju argumenta $u$, njen kod će biti (vrlo velika) konstanta.

    Dakle, $\varphi_u:=(\pi_u\to\psi)$, gdje je $\psi$ oblika $\bigl(\overline{\iota_0}\to\bigl(\overline{\iota_1}\to(\overline{\iota_2}\to\dotsb(\overline{\iota_{n-1}}\to\zeta)\dotsm)\bigr)\bigr)$\text.
Uz standardne reprezentacije ($\mathsf o$ kao $c_0$ odnosno \t c, $\mathsf s$ kao $f_0^1$ odnosno \t f, a $R_i$ kao $R_i^m$ odnosno riječ koda $\f{Rel}(i)$), možemo svaku pojedinu atomarnu formulu koja se pojavljuje u $\psi$ zapisati u osnovnom jeziku. Od veznika su nam potrebni kondicionali (koje imamo u osnovnom jeziku, samo moramo pisati vanjske zagrade), i konjunkcije za formule oblika~\eqref{eq:formDEC} --- koje se mogu reprezentirati kako smo to objasnili u~\eqref{eq:Conjunction}, ili proširujući $\Gamma_u$ tako da za svaku instrukciju $I_t$ tipa \dec\ ubacimo \emph{dva} kondicionala (zvat ćemo ih $\iota_t^0$ i $\iota_t^+$) unutra. Obično je lakše koristiti ovaj drugi pristup.

\begin{primjer}[{name=[zaustavljanje RAM-izračunavanja kao valjanost jedne formule]}]
Promotrimo problem zaustavljanja $P$-izračunavanja s $\vec u$, gdje je
\begin{equation}
    P:=\begin{prog}
    0.&\decr11\\
    1.&\decr11
    \end{prog}\text,
\end{equation}
    a $\vec u=(1,2)$ (dakle, $m=3$, a $n=2$). Vidimo da $P$-izračunavanje s $\vec u$ ne stane:
\begin{equation}
    (0,1,2,0,\dotsc,0)\leadsto(0,0,2,0,\dotsc,1)\leadsto(0,0,2,0,\dotsc,1)\leadsto\dotsb\text.
\end{equation}
Jezikom logike prvog reda:
\begin{align}
%\SwapAboveDisplaySkip
	\iota_0^0&=\bigl(R_0(x_0,\mathsf o,x_2)\to R_1(x_0,\mathsf o,x_2)\bigr)&
    \iota_0^+&=\bigl(R_0\bigl(x_0,\mathsf s(x_1),x_2\bigr)\to R_1(x_0,x_1,x_2)\bigr)\\
	\iota_1^0&=\bigl(R_1(x_0,\mathsf o,x_2)\to R_1(x_0,\mathsf o,x_2)\bigr)&
    \iota_1^+&=\bigl(R_1\bigl(x_0,\mathsf s(x_1),x_2\bigr)\to R_2(x_0,x_1,x_2)\bigr)\\
	\zeta&=\exists x_0\exists x_1\exists x_2 R_2(x_0,x_1,x_2)&
    \psi&=\bigl(\iota_0^0\to\bigl(\iota_0^+\to(\iota_1^0\to(\iota_1^+\to\zeta))\bigl)\bigl)\\
	&\pi_{(1,2)}=R_0\bigl(\mathsf o,\mathsf s(\mathsf o),\mathsf s\bigl(\mathsf s(\mathsf o)\bigr)\bigr)&
	&\varphi_{(1,2)}=(\pi_{(1,2)}\to\psi)
\end{align}
    odnosno znamo da nije valjana formula (zapisana u osnovnom jeziku)
\begin{multline}
    \varphi_{(1,2)}=\t{(R(c,f(c),f(f(c)))\textrightarrow}\\
    \t{($\forall$x$\forall$x'$\forall$x'{}'(R(x,c,x'{}')\textrightarrow R'(x,c,x'{}'))\textrightarrow}\\
    \t{($\forall$x$\forall$x'$\forall$x'{}'(R(x,f(x'),x'{}')\textrightarrow R'(x,x',x'{}'))\textrightarrow}\\
    \t{($\forall$x$\forall$x'$\forall$x'{}'(R'(x,c,x'{}')\textrightarrow R'(x,c,x'{}'))\textrightarrow}\\
    \t{($\forall$x$\forall$x'$\forall$x'{}'(R'(x,f(x'),x'{}')\textrightarrow R'{}'(x,x',x'{}'))\textrightarrow}\\
    \t{$\lnot\forall$x$\forall$x'$\forall$x'{}'$\lnot$R'{}'(x,x',x'{}'))))))}\text,
\end{multline}
čiji kod ima dvjestotinjak znamenaka --- ali o $\vec u$ ovisi samo prvi red;\\ sve ostalo je konstanta za fiksni RAM-algoritam $P^k$.
\end{primjer}

\begin{lema}[{name=[primitivna rekurzivnost svođenja $K$ na $\Valid$]}]\label{lm:K<Valid}
Funkcija $\f{Phi}$, koja svakom prirodnom broju $u$ pridružuje \\ kod formule $\varphi_u$ iz dokaza teorema~\ref{tm:Church}\,\eqref{step:varphi_u}, primitivno je rekurzivna.
\end{lema}
\begin{proof}
    Prvo, označimo s $psi:=\kr{\psi}$ kod formule $\psi$ koja nastane prebacivanjem svih $\overline{\iota_i}$ na desnu stranu relacije $\models$. Taj broj ne ovisi o $u$.

Drugo, označimo s $\f{Pi}$ funkciju koja preslikava $u\mapsto\kr{\pi_u}$. Ta funkcija je primitivno rekurzivna, jer je funkcija $\f{Numeral}$, koja preslikava $u\mapsto\kr{\overline u}$, primitivno rekurzivna.
\begin{align}
	\f{Numeral}(u)&:=\kr{\t{f(f(}\dotsb\mspace{1mu}\t{f(c)}\dotsm\t{))}}=\f{Repeat}(43,u)\conc{}2\conc{}\f{Repeat}(8,u)\\
    \f{Pi}(u)&:=\kr{\pi_u}=\kr{R_0(\mathsf o,\overline u,\mathsf o,\dotsc,\mathsf o)}=
    \kr{\,\t{R(c,}}\conc{}\kr{\overline u}\conc{}\kr{(\t{,c})^{m-2}}\conc{}\kr{\t)}=\notag\\
    &=7949\conc{}\f{Numeral}(u)\conc{}\f{Repeat}(62,m-2)\conc{}8\\
    \f{Phi}(u)&:=\kr{\varphi_u}=\kr{\t(\pi_u\!\,\t\textrightarrow\,\psi\t)}=7\conc{}\f{Pi}(u)\conc{}10\conc{}psi\conc{}8
\end{align}
    $\f{Repeat}$ nam treba da bismo formalno zapisali ovo označeno trotočkom u $\pi_u$: preostalih $m-2$ (konstanta; znamo da je $m\ge2$) registara su resetirani. Treba nam i za $\f{Numeral}$ iz istog razloga: trotočke prije i nakon \t{f(c)}.
\end{proof}

\begin{propozicija}[Churchov teorem formalno]
Jezik $\Valid$ nije odlučiv\!.
\end{propozicija}
\begin{proof}
Lanac ekvivalencija~\eqref{eq:lanaceqv} sada možemo proširiti još trima karikama:
\begin{multline}\label{eq:K<Valid}
    u\in K
    \Longleftrightarrow
    \text{$P_0$-izračunavanje s $u$ stane}
    \Longleftrightarrow
    (\Gamma_u\models\zeta)
    \Longleftrightarrow{}
    (\models\varphi_u)
    \Longleftrightarrow\\
    \Longleftrightarrow
    \varphi_u\in\Valid
    \Longleftrightarrow
    \kr{\varphi_u}\in\kr{\Valid}
    \Longleftrightarrow
    \f{Phi}(u)\in\kr{\Valid}
    \text.
\end{multline}
Predpredzadnja ekvivalencija je definicija skupa $\Valid$ (u donjem redu je $\varphi_u$ zapisana u osnovnom jeziku). Predzadnja ekvivalencija je u jednom smjeru definicija~\eqref{eq:kodLdef}, a u drugom injektivnost kodiranja (propozicija~\ref{pp:bijkr}): ako je $\kr{\varphi_u}=\kr{\varphi'}$ za neku $\varphi'\in\Valid$, tada je $\varphi_u=\varphi'\in\Valid$. Zadnja ekvivalencija je definicija funkcije $\f{Phi}$.

	Čitav se lanac~\eqref{eq:K<Valid} može sažeti u $\chi_{K}=\chi_{\kr{\Valid}}\circ\f{Phi}$, gdje je $\f{Phi}$ (čak primitivno, po lemi~\ref{lm:K<Valid}) rekurzivna, pa vrijedi $K\preceq\kr{\Valid}$.
Kada bi $\Valid$ bio odlučiv\!, po teoremu~\ref{tm:oikr} bi jednomjesna relacija $\kr{\Valid}$ bila rekurzivna. Prema propoziciji~\ref{pp:rek<rek}, tada bi i Kleenejev skup bio rekurzivan, što je kontradikcija s teoremom~\ref{tm:DRnrek}.
\end{proof}

\section{Prema Gödelovu prvom teoremu nepotpunosti}

Argumentima potrebnim za dokaz Churchova teorema već smo se poprilično približili dokazu Gödelova prvog teorema, u formulaciji Tarskog: \textbf{Postoji istinita rečenica na prirodnim brojevima, nedokaziva u PA\@}. Za potpuni dokaz trebalo bi razraditi još mnogo tehničkih detalja, ali pogledajmo samo osnovnu ideju.

U prethodnoj točki uveli smo, za svaki prirodni broj $u$, rečenicu $\varphi_u$ koja je valjana ako i samo ako je $u$ element Kleenejeva skupa. Također smo uveli strukturu $\mathfrak N=(\N,0,\f{Sc},\dotsc)$, čiji konstantsko-funkcijski fragment se podudara sa standardnim modelom od PA (prirodni brojevi, nula i sljedbenik).

\begin{definicija}[{name=[Gödelov skup]}]
\emph{Gödelov skup} je skup rečenic\=a
%\begin{equation}
    $\mathscr G\ddot o:=\{\lnot\varphi_u\mid u\in K\kompl\}$.
%\end{equation}
\end{definicija}
%Kako je negacija rečenice ponovo rečenica, Gödelov skup je skup rečenica.

\begin{propozicija}[{name=[istinitost Gödelova skupa rečenica u $\mathfrak N$]}]\label{pp:NvdGo}
Vrijedi $\mathfrak N\models\mathscr G\ddot o$.
\end{propozicija}
\begin{proof}
Po kontrapoziciji propozicije~\ref{pp:models>stop}, za svaki $u\in K\kompl$ formula $\varphi_u$ nije valjana, a iz dokaza te propozicije slijedi da ne vrijedi upravo na strukturi $\mathfrak N$ (jer tamo vrijedi $\pi_u$ i sve $\iota_i$, ali ne vrijedi $\zeta$). Iz logike znamo da $\mathfrak N\nvDash\varphi_u$ povlači $\mathfrak N\models\lnot\varphi_u$, jer je $\varphi_u$ rečenica. Drugim riječima, za svaki $u\in K\kompl$ vrijedi $\mathfrak N\models\lnot\varphi_u$, što smo trebali dokazati.
\end{proof}

\begin{teorem}[{name=[Gödelov prvi teorem nepotpunosti]}]\label{tm:goedel}
Postoji rečenica $\gamma\in\mathscr G\ddot o$ (\emph{Gödelova rečenica}) koja nije dokaziva u PA\@.
\end{teorem}
\begin{proof}[Skica dokaza]
Ključno je vidjeti da je jezik nad $\Sigma_{\log}$,
\begin{equation}
    %Proof\bigl((\psi_i)_{i=0}^n,\psi\bigr):\Longleftrightarrow\text{$(\psi_i)_{i=0}^n$ je dokaz za formulu $\psi$,}
    Proof:=\{\,\psi_0\t\#\,\psi_1\t\#\,\dotsb\,\t\#\,\psi_n\mid (\psi_0,\psi_1,\dots,\psi_n)\text{ je dokaz u logici prvog reda}\,\}\text,
\end{equation}
	odlučiv\!. To sigurno nećemo napraviti u potpunosti, ali sve osnovne ideje već imamo. Prvo, slično kao u točki~\ref{sec:stdstring}, možemo napraviti funkcije $\f{arg}'_i$, koje iz kodiranog \t\#-separiranog niza formula ekstrahiraju pojedinu formulu (zapravo njen kod). Dinamizacijom možemo napraviti i $(\f{arg}')^2$, pomoću koje onda možemo govoriti o svim formulama u dokazu (i osigurati da su dijelovi između separatora doista formule). Sad je jasno da, kako bi takav niz bio u $Proof$, svaka formula u njemu mora biti ili instanca sheme aksioma (A1), (A2), (A3), (A4) ili (A5) (iz Hilbertova računa predikata), ili pak mora biti dobivena modus ponensom ili generalizacijom iz neke prethodne formule. Uz pokrate $\varphi_i$ za $\f{arg}'(p,i)$ te analogno $\varphi_j$ i $\varphi_k$ imamo
\begin{multline*}
	p\in\langle Proof\rangle\Longleftrightarrow\bigl(\forall i<2+\bigl(\num j<\f{slh}(p,12)\bigr)\bigl(\f{sdigit}(p,j,12)=12\bigr)\bigr)\bigl(\varphi_i\in\kr{F1}\land{}\\{}\land\bigl(
	\varphi_i\in\bigcup\nolimits_{j=1}^{\,5}\kr{Axiom_j}\lor(\exists j<i)(\exists k<i)\f{ModPon}(\varphi_i,\varphi_j,\varphi_k)\lor(\exists j<i)\f{Gen}(\varphi_i,\varphi_j)\bigr)\bigr)
\end{multline*}
	Sheme (A1), (A2) i (A3) možemo opisati konkatenacijom, uz ograničavanje kvantifikacije pomoću korolara~\ref{kor:krvw}. Opisat ćemo (A1) --- (A2) i (A3) su dulje ali ne bitno kompliciranije.
\begin{equation*}
	f\in\kr{Axiom_1}:\Longleftrightarrow(\exists a<f)\,(\exists b<f)\,\bigl(a\in\kr{F1}\land b\in\kr{F1}\land f=\langle\t(\,\rangle\conc{}a\conc{}\langle\t{\,\textrightarrow(\,}\rangle\conc{}b\conc{}\langle\,\t\textrightarrow\,\rangle\conc{}a\conc{}\langle\t{\,))}\rangle\bigr)
\end{equation*}

	Za sheme (A4) i (A5) moramo još voditi računa o reprezentaciji terma, i uvjetima za supstituciju --- što uvodi određene tehničke poteškoće, ali sve su one rješive našim alatima razvijenima u točki~\ref{sec:ogrprog}. Za alternativnu aksiomatizaciju logike prvog reda koja izbjegava brojne tehničke poteškoće pogledajte~\cite{smullyan}.

Modus ponens i generalizaciju je jednostavno zapisati.
\begin{align}
    \f{ModPon}(a,b,c)&:\Longleftrightarrow b=
    \kr{\t(}\conc{}
    c\conc{}
    \kr{\t\textrightarrow}\conc{}
    a\conc{}\kr{\t)}\\
    \f{Gen}(a,b)&:\Longleftrightarrow
    (\exists k<a)(a=\f{UnivQuant}(k)\conc{}b)
\end{align}

	Odnosno, $\alpha$ je dobivena modus ponensom iz $\beta$ i $\gamma$ ako i samo ako je $\beta=(\gamma\to\alpha)$. Također, $\alpha$ je dobivena generalizacijom iz $\beta$ ako postoji $k$ takav da je $\alpha=\forall x_k\beta$. Pri tome je $k<k+1=\dulj{x_k}<\dulj{\forall x_k}<\dulj{\forall x_k\beta}=\dulj{\alpha}\le\kr\alpha=a$ po lemi~\ref{lm:dulj<=kr}, pa možemo ograničiti kvantifikaciju po $k$.

    Kad smo se koliko-toliko uvjerili da je $Proof$ odlučiv\!, trebamo isto provesti za $Proof_{\text{PA}}$, jezik koji sadrži dokaze u Peanovoj aritmetici. Nije tako strašno: među aksiome treba dodati i nelogičke, Peanove aksiome, i još provjeriti za svaku formulu u dokazu je li instanca sheme aksioma matematičke indukcije. Ovo posljednje je također petljavo, ali iz istog razloga kao (A4): supstitucija je komplicirana, i to je jedna od spomenutih tehničkih poteškoća elegantno izbjegnutih u~\cite{smullyan}.

Promotrimo sada sljedeći \emph{paralelni} algoritam:
\begin{quote}
    Za ulaz $u\in\N$, prvo zapišemo $\neg\varphi_u$ tako da, osim nule i sljedbenika, koristi samo zbrajanje i množenje (nazovimo taj zapis $\neg\varphi_u'$). Zatim pokrenemo dvije dretve.

    U prvoj simuliramo $P_0$-izračunavanje s $u$, odnosno računanje funkcije $\f{Russell}$ u točki $u$. Ako ova dretva stane, prekidamo program i vraćamo $\mathit{true}$ ($1$).

    U drugoj dretvi, generiramo sve elemente od $Proof_{\text{PA}}$ redom po kodovima. Za svaki $p\in Proof_{\text{PA}}$, nađemo zadnju pojavu znaka \t\# u $p$, i dio $p$ od te pojave (isključivo) do kraja usporedimo s formulom $\neg\varphi_u'$ dobivenom na početku. Ako su jednake, prekidamo program i vraćamo $\mathit{false}$ ($0$).
\end{quote}

Ako je $u\in K$, prva dretva će stati, pa će i cijeli algoritam stati i vratiti $1$ --- pod pretpostavkom da druga dretva ne zaustavi algoritam prije. No PA je konzistentna teorija, pa ne dokazuje ono što nije istina. Kako $\neg\varphi_u$ nije istinita u $\mathfrak N$, tako niti $\neg\varphi_u'$ nije istinita u $\N$, dakle ne može se dogoditi da neki $p\in Proof_{\text{PA}}$ završi njome.

	S druge strane, ako $u\notin K$, prva dretva po definiciji neće stati, no hoće li druga? Ako bi PA bila i \emph{potpuna} teorija, odnosno dokazivala sve što je istina u strukturi $\N$, tada bi s vremenom na red došao i dokaz za $\neg\varphi_u'$ (koja jest istinita po propoziciji~\ref{pp:NvdGo}). To bi značilo da za sve $u\notin K$, naš algoritam također stane i vraća $0$.

Sve u svemu, vidimo da neformalni algoritam koji smo napisali računa $\chi_{K}$, što je po Church--\!Turingovoj tezi u kontradikciji s teoremom~\ref{tm:DRnrek}.

Jedina pretpostavka koja može biti pogrešna je da PA dokazuje sve formule oblika $\neg\varphi_u', u\in K\kompl$ --- drugim riječima, postoji formula iz $\mathscr G\ddot o$ koja nije dokaziva u PA\@.
\end{proof}

\subsection{Problemi u skici dokaza Gödelova teorema}

U dokazu teorema~\ref{tm:goedel} mnogo je toga napravljeno neformalno. Idejno smo veoma blizu, ali tehnička zahtjevnost takvog rezultata je ogromna. Samo navedimo neke najočitije rupe, i ukratko opišimo kako ih možemo "zakrpati".

\begin{itemize}
    \item Možemo li doista relacije $R_n$ izraziti pomoću nule, sljedbenika, zbrajanja i mno\-že\-nja? Koristeći funkciju $\f{Reg}$ svaku od njih možemo izraziti kao projekciju primitivno rekurzivne relacije, ali kodiranje potrebno za $\f{Reg}$ bitno koristi potenciranje. Pokazuje se~\cite{smullyan} da je Gödelov teorem mnogo lakše dokazati ako u strukturi $\N$ shvatimo i potenciranje kao osnovnu operaciju. Zapisati potenciranje \emph{logički} pomoću zbrajanja i množenja (ne koristeći primitivnu rekurziju, jer ona ide preko teorije skupova, Dedekindovim teoremom rekurzije), ili alternativno, razviti kodiranje konačnih nizova koje umjesto množenja i potenciranja koristi zbrajanje i množenje, vrlo je teško. Gödelov originalni pristup (funkcija $\beta$ i kineski teorem o ostacima) je zapetljan, ali do danas nismo otkrili ništa bolje. %TODO: navesti Quineove dinamičke zareze
    \item Kako iz činjenice da je skup $\kr{Proof_{\text{PA}}}$ rekurzivan možemo dobiti njegovu iz\-ra\-čun\-lji\-vu enumeraciju? Ovo možete riješiti za vježbu. Dakle, zadatak je dokazati: ako je $\f S$ beskonačan rekurzivan skup, tada je enumeracija od $\f S$ (funkcija koja broju $i$ pridružuje $i$-ti po veličini element od $\f S$) rekurzivna. Potrebnu ideju vidjeli ste kod enumeracije skupa $\mathbb P$~\eqref{eq:primerek}. $Proof_{\text{PA}}$ je očito beskonačan skup.
    \item Pokriva li Church--\!Turingova teza i paralelne algoritme? Svakako, iako će proći još neko vrijeme do trenutka kad ćemo to dokazati u poglavlju~\ref{ch:re}. Usprkos nemogućnosti dokaza same teze, dokazat ćemo da se paralelni algoritmi mogu izvršavati na RAM-stroju (odnosno opisati parcijalno rekurzivnim funkcijama) te se imaju jednako pravo zvati algoritmima kao i oni slijedni (neparalelni). Konkretno, tvrdnja koja nam ovdje treba formalizirana je kao Postov teorem, dokazan u točki~\ref{sec:Post}.
    \item Možemo li potpuno izbjeći Church--\!Turingovu tezu? Kako teorem govori o dokazivanju a ne o algoritmima, čini se da možemo --- ili je barem možemo zamijeniti "Hilbertovom tezom" da je intuitivni pojam dokazivanja u nekoj teoriji točno opisan preciznom definicijom formalnog dokaza. Taj pristup je naravno potpuno izvan opsega ove knjige, kojoj su centralna tema algoritmi.
    \item Nekonstruktivnost dokaza svakako upada u oči. Dokazali smo da Gödelova rečenica postoji tako što smo zapravo dokazali da pretpostavka da su u nekom beskonačnom skupu sve rečenice dokazive vodi na kontradikciju. Tada nedokaziva rečenica u tom skupu postoji u klasično-logičkom smislu, ali svejedno o njoj ne znamo skoro ništa. Možemo li \emph{konstruirati} Gödelovu rečenicu? Odgovor je potvrdan, iako konstrukcija uopće nije jednostavna. Ključna je ideja \textbf{samoreferiranja}: moguće je u Peanovoj aritmetici konstruirati formulu koja na određeni način govori o samoj sebi --- konkretno, kaže da ona sama nije dokaziva. Mi ćemo sličan fenomen samoreferiranja vidjeti u teoremu rekurzije: algoritmi u svojoj definiciji mogu koristiti (najčešće \emph{pozivati} pomoću funkcije $\f{comp}_k$, gdje je $k$ mjesnost algoritma --- ali mogući su i drugi oblici korištenja) same sebe. Osnovna ideja --- specijalizacija\slash supstitucija i dijagonalna funkcija --- je ista kao i za samoreferirajuće formule. To je tema sljedećeg poglavlja.
\end{itemize}
% govor o PRA: F1 je prejaka, mnogo toga se može napraviti primitivno rekurzivno!