uvod.tex

\section{Uvod}

Cilj našega dela je najti povezavo med topologijo in logiko. Specifično želimo
vsakemu prostoru na nek način dodeliti logični sistem, katerega lastnosti bodo
potem odražale (upamo da znane) lastnosti topološkega prostora.
Prva opazka, ki jo lahko naredimo je, da lahko gledamo ``logiko odprtih množic'',
kjer smatramo odprte množice kot trditve oziroma resničnostne vrednosti.
O tem si mislimo, kot da se resnica spreminja po prostoru. Poglejmo si na primer
trditev ``funkcija \(\id : ℝ → ℝ\) je pozitivna''. To seveda ni res, je pa res
če jo zožimo na pozitivna realna števila. Tako lahko tej trditvi priredimo
resničnostno vrednost \(\p{0, ∞}\). Presek torej igra vlogo konjunkcije,
unija disjunkcije, izrazimo lahko pa tudi implikacijo (čeprav jo v topologiji
redko vidimo).

Na ta način lahko prostoru priredili \emph{izjavni račun}. Kot bomo videli,
lahko že s tem izrazimo veliko, recimo karakteriziramo lahko diskretne prostore,
ekstremalno nepovezane prostore, in še kakšne.

Je pa izjavni račun vseeno zelo omejen, tako da bi ga radi razširili. Najprej
lahko dodamo univerzalni in eksistenčni kvantifikator, nato pa jih še razširimo
do logike višjega reda. To nam da več možnosti za karakterizacije topoloških
lastnosti. Recimo, da bi želeli dodati naravna števila v logiko prostora realnih
števil. Tako kot zgoraj, bi želeli, da se lahko ``vrednost'' naravnega števila
spreminja po prostoru. To je pa natanko (zvezna) funkcija \(ℝ → ℕ\). Zveznost
zahtevamo, da se ta naravna števila dovolj lepo obnašajo, konec koncev pa to
pomeni, da je ta funkcija konstantna. Zanimivo potem postane, da naravno število
ni nujno definirano povsod: res, obstajajo funkcije v naravna števila tudi iz
odprtih podmnožic \(ℝ\), ta pa niso nujno povezana, tako da te funkcije niso
nujno konstantne.

Taki logiki bomo potem pravili \emph{topološki model}. Zares smo do tega prišli
v napačnem vrstnem redu, saj imamo ponavadi najprej neko logiko, in potem
najdemo matematični objekt, ki se mu reče \emph{model}, ki tej logiki zadošča.
Tako je bolj korektno, da rečemo, da je cilj dela pokazati, da v logiki velja
določen logični princip natanko tedaj, ko za topološke modele te logike velja
neka topološka lastnost. Primer takega izreka je potem recimo, da izključena
tretja možnost velja natanko v diskretnih prostorih.



% V konstruktivni matematiki poznamo več tako imenovanih \quot{nekonstruktivnih}
% oziroma \quot{klasičnih} principov, najbolj znana sta recimo princip izključene
% tretje možnosti in aksiom izbire, obravnavamo pa lahko tudi šibkejše verzije
% obeh. V dvajsetem stoletju se je razvilo več različnih programov konstruktivne
% misli, na primer Brouwerjev intuicionizem, Bishopov konstruktivizem, Ruski
% konstruktivizem, in drugi. Ruski konstruktivisti so recimo priznavali princip
% Markova, ki pravi, da če zaporedje ničel in enk ni konstantno nič, mora potem
% nujno biti na nekem indeksu enka, pa čeprav ta princip ne velja
% \quot{konstruktivno}.

% Ruskemu konstruktivizmu (in ostalim programom) bi torej lahko pravili
% interpretacija ali celo \emph{implementacija} konstruktivne logike. Temu se bolj
% tehnično reče \emph{model}, se pa tudi uporablja fraza \emph{matematični svet},
% saj je model logike natanko svet, v katerem lahko delamo matematiko z uporabo te
% logike.

% Matematične svetove pa lahko pogrupiramo v neke večje kategorije, ki pa bodo
% matematikom malo bolj znani. Nekateri so motivirani s teorijo množic, drugi z
% izračunljivostjo, torej na primer s Turingovimi stroji (sem recimo spada Ruski
% konstruktivizem), tretji z algebro, četrti pa s topologijo. Ker raziskujemo
% povezavo med logiko in topologijo se v tem delu osredotočimo na topološke
% modele. Natančno to pomeni, da za vsak topološki prostor pogledamo model logike,
% ki pripada temu prostoru. Ideja sedaj je, da \quot{klasične} principe izrazimo v
% jeziku topološkega modela, to interpretiramo kot izjavo o topološkem prosoru
% samem, in tako dobimo slovar med \quot{klasičnimi} principi in topološkimi
% lastnostmi, kot na primer kompaktnost, separabilnost, \(Tₙ\) lastnostmi, in
% podobno.

Močno se zgledujemo po delu Inga
Blechschmidta~\cite{Blechschmidt17,Blechschmidt22}, ki zgradi slovar med
algebraično geometrijo in komutativno algebro v (Zariskijevem) modelu. Bolj
standardna literatura na to temo je pa~\cite{MM92,Johnstone02}.

To delo predpostavlja nekaj znanja teorije kategorij, se pa bo avtorica
potrudila navesti točne citate na vse naprednejše kategorične definicije in
izreke. Znanje teorije modelov ali teorije toposov ni nujno, je pa za globlje
razumevanje celostne slike verjetno potrebno. Zaželeno je osnovno poznavanje
konstruktivne matematike, za kar priporočamo~\cite{Bauer16, Bishop85}.

Razdelek~\ref{sec:modeli} je namenjen uvodu pojma topološkega modela,
razdelek~\ref{sec:logika} definira različne logične principe, ki jih v tem delu
obravnavamo. Razdelki~\ref{sec:izbire},~\ref{sec:reals}, in~\ref{sec:inst-red}
so namenjeni karakterizaciji topoloških lastnosti prek interpretacije logičnih principov iz
razdelka~\ref{sec:logika} v topoloških modelih.

Kolikor je avtorici znano, so naslednji rezultati originalni prispevki:
\ref{th:psp-is-pgt}, \ref{th:psp-has-cc}, \ref{th:psp-is-not-pgt},
\ref{th:t1-pgt-is-psp}, \ref{th:ac-is-lem}, \ref{th:lpov-lpo},
\ref{th:amp-is-almost-psp}, \ref{th:alpo-is-awlpo-and-amp}, in
\ref{th:Rc=R-is-lpo}.
Prav tako je originalna ločitev \(\Rd = \Rc\) od \(\CCv\) in \(\alpo*\)
iz podrazdelka~\ref{sec:reals-Rd=Rc}. Rezultati iz razdelka~\ref{sec:inst-red}
so vsi originalni, le lema~\ref{th:cantor-real-is-semidec} je bila razvita s
pomočjo mentorja.

Vse primere prostorov, ki ločijo kakšne principe, sem našla s
pomočjo matematične zbirke podatkov~\cite{pibase}.

\subsection{Oznake}

V delu uporabljamo več nestandardnih oznak, ki so navedene in razložene v
spodnji tabeli.

% TODO: alignment
\begin{tabularx}{0.9\linewidth}{lX}
  % \(よ\) & vložitev Yonede\\
  \(f{\res U}\) & zožitev \(f\) na \(U\)\\
  \(\Rm\) & realna števila konstruirana z MacNeilleovimi rezi\\
  \(\Rd\) & realna števila konstruirana z Dedekindovimi rezi\\
  \(\Rc\) & realna števila konstruirana kot kvocient Cauchyjevih zaporedij\\
  %\(\lem\) & princip izključene tretje možnosti, \\
  % \(\cov{U}{i}\) & pokritje \(\{Uᵢ\}_{i∈I}\) monžice \(U\), kjer je
  %                  \(I\) neka indeksna množica\\
  \(𝒫A\) & potenčna množica \(A\)\\
  \(𝒪X\) & odprte množice prostora \(X\)\\
  \(𝒜X\) & zaprte množice prostora \(X\)\\
  %\(U \op X\) & \(U\) odprta podmnožica \(X\)\\
  \(U ⊥ V\) & presek \(U\) in \(V\) je prazen\\
  \(U \between V\) & presek \(U\) in \(V\) ni prazen\\
  \(\eventually{V ⊆ U}{P(V)}\) & obstaja pokritje množice \(U\), in za vsak
                                 element pokritja \(V\) velja \(P(V)\)
\end{tabularx}

V delu tudi uvedem novo vrsto definicije oziroma izreka, namreč
\emph{konstrukcijo}. Ta igra vlogo izrekov, ki konstruirajo točno določen
objekt. Primer takega je recimo prvi izrek o izomorfizmu.
\begin{izrek}
  Naj bosta \(G\) in \(H\) grupi in \(φ : G → H\) homomorfizem.
  Potem je \(\im φ ≅ \quot{G}{\ker φ}\).
\end{izrek}
\begin{dokaz}
  Definirajmo \(\hat φ(g\ker φ) ≔ φ(g)\)...
\end{dokaz}
Torej ko govorimo o prvem izreku o izomorfizmu ne mislimo o kar nekem
izomorfizmu, ampak imamo v mislih nek določen izomorfizem. Tako se pogosto
sklicuje na ``dokaz izreka X.XX'', ki je izvedel neko tako konstrukcijo. Veliko
bolje bi bilo, če se lahko skličemo kar neposredno na specifično konstrukcijo.
\begin{konstrukcija}
  Za grupi \(G\) in \(H\) in homomorfizem \(φ : G → H\) je preslikava
  \(\hat φ(g\ker φ) ≔ φ(g)\) izomorfizem \(\quot{G}{\ker φ} ≅ \im φ\).
\end{konstrukcija}
Tako ne rabimo podrobno brati dokaza, da iz njega izluščimo ključne definicije
in oznake.


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "main"
%%% End: