logika.tex

\section{Nekonstruktivni principi}\label{sec:logika}

\subsection{Realna števila}\label{sec:logika-reals}

\begin{definicija}
  Podmnožica \(L ⊆ ℚ\) je
  \begin{itemize}
  \item \emph{naseljena}, ko obstaja element \(L\),
  \item \emph{dolnja}, ko za vsak \(q ∈ L\) in \(p < q\) velja \(p ∈ L\),
  \item \emph{navzgor odprta}, ko za vsak \(p ∈ L\) obstaja \(q > p\), da je \(q ∈ L\).
  \end{itemize}
  Pojme \emph{gornja} in \emph{navzdol odprta} definiramo simetrično.
\end{definicija}

\begin{definicija}[Dedekindova konstrukcija]\label{def:Rd}
  Par \(\p{L, U} ∈ 𝒫(ℚ)×𝒫(ℚ)\) je \emph{Dedekindov rez}, ko velja
  \begin{enumerate}
    \item \(L\) je naseljena, dolnja, in navzgor odprta
    \item \(U\) je naseljena, gornja, in navzdol odprta
    % \item \(L\) je dolnja
    % \item \(U\) je gornja
    % \item \(L\) je navzgor odprt
    % \item \(U\) je navzdol odprt
    \item za vsaka \(p\), \(q : ℚ\) velja \(p ∈ L ∧ q ∈ U ⇒ p < q\)
    \item za vsaka \(p < q\) velja \(p ∈ L ∨ q ∈ U\)
  \end{enumerate}
  Množica Dedekindovih rezov tvori \emph{Dedekindova realna števila}, ki jih
  označimo z \(\Rd\).
  Za \(x : \Rd\) naj \(Lₓ\) in \(Uₓ\) označujeta podmnožici \(ℚ\), ki tvorita
  Dedekindov rez \(x\).

  Za racionalno število \(p\) definiramo \(p < x\) kot \(p ∈ Lₓ\) in \(x < p\)
  kot \(p ∈ Uₓ\). Relacijo \(x < y\) za Dedekindovi realni števili potem
  definiramo kot ``obstaja racionalno število \(p\), da je \(x < p < y\)''.
  Z rezi to izrazimo kot \(U_x \between L_y\).

  Relacijo \(x ≤ y\) definiramo kot \(L_x ⊆ L_y ∧ U_y ⊆ U_x\).
  Vsebovanosti sta ekvivalentni, tako da zadošča pokazati zgolj eno.
\end{definicija}
\begin{opomba}
  Tretjemu pogoju zgoraj pravimo \emph{lociranost}. Izkaže se, da je ta pogoj
  ekvivalenten šibkejšemu pogoju "velja \(p ∈ L ∨ q ∈ U\)", kjer sta tu \(p\) in
  \(q\) neki \emph{izbrani} racionalni števili, za kateri velja \(p < q\).
\end{opomba}

\begin{definicija}[Cauchyjeva konstrukcija]\label{def:Rc}
  Zaporedje racionalnih števil \((xₙ)ₙ\) je \emph{Cauchyjevo}, ko za vsaka
  \(i,j : ℕ\) velja \(|xᵢ - xⱼ| ≤ 2⁻ⁱ+2⁻ʲ\).

  Cauchyjevi zaporedji \((xₙ)ₙ\) in \((yₙ)ₙ\) sta \emph{koincidenčni},
  ko za vse \(i : ℕ\) velja \(|xᵢ - yᵢ| ≤ 2⁻ⁱ⁺¹\).

  Kvocient množice Cauchyjevih zaporedij glede na relacijo koincidence tvori
  \emph{Cauchyjeva realna števila}, ki jih označimo z \(\Rc\).

  Relacijo \(x < y\) definiramo kot \(\exist{n:ℕ}{xₙ + 2⁻ⁿ < yₙ - 2⁻ⁿ}\),
  relacijo \(x ≤ y\) pa kot \(\exist{n:ℕ}{xₙ + 2⁻ⁿ ≤ yₙ - 2⁻ⁿ}\).
\end{definicija}
\begin{opomba}
  Zaporedjem iz definicije~\ref{def:Rc} ponavadi pravimo hitra
  Cauchyjeva zaporedja. Paziti je treba, da klasična \(ε\)-\(δ\) definicija
  Cauchyjevih zaporedij \emph{ni} ekvivalentna gornji. Več o različicah
  Cauchyjevih realnih števil si bralka lahko ogleda v~\cite{nlab-cauchy-real}.
\end{opomba}

\begin{lema}\label{th:real-order-lemma}
  Relaciji \(<\) in \(≤\) sta delni ureditvi v Dedekindovih in Cauchyjevih
  realnih številih. Poleg tega velja \(x < y ≤ z ⇒ x < z\) in
  \(x ≤ y < z ⇒ x < z\).
\end{lema}

\begin{trditev}
  Vsako Cauchyjevo realno število je tudi Dedekindovo.
\end{trditev}
\begin{dokaz}
  Naj bo \(x\) Cauchyjevo realno število in definirajmo
  \begin{align*}
    L ≔ \set{q : ℚ}{q < x}\text{ in}\\U ≔ \set{r : ℚ}{x < r}\text.
  \end{align*}
  Par \(\p{L, U}\) očitno zadošča prvim trem lastnostim Dedekindovih rezov, tako
  da se osredotočimo zgolj na zadnji pogoj. Pokazati moramo, da za vsako
  Cauchyjevo realno število \(x\) velja \(x > 0 ∨ x < 3\).
  Za racionalno število \(x₀\) velja \(x₀ > 1 ∨ x₀ < 2\), saj imajo racionalna
  števila odločljivo neenakost. Po definiciji za vse \(i : ℕ\) velja
  \(|x₀ - xᵢ| ≤ 1\), torej, če je \(x₀ > 1\), bodo vsi \(xᵢ > 0\), po drugi
  strani pa, če je \(x₀ < 2\), bodo vsi \(xᵢ < 3\), kar zaključi dokaz.
\end{dokaz}

Obrat ne velja konstruktivno. To pomeni, da lahko na ``\(\Rd = \Rc\)''
gledamo kot nekakšen nekonstruktiven princip. Iz konstruktivne matematike
poznamo tudi druge konstrukcije realnih števil, na primer MacNeilleovo
konstrukcijo~\cite{nlab-macneille-reals}\cite[pogl.~D4.7]{Johnstone02}, ki jo
tudi lahko primerjamo z \(\Rd\) in \(\Rc\). Obstajajo še druge konstrukcije, a
se bomo v tem delu posvetili zgolj tem.

\begin{definicija}[MacNeilleova konstrukcija]\label{def:Rm}
  Par \(\p{L, U} ∈ 𝒫(ℚ)×𝒫(ℚ)\) je \emph{Dedekind-MacNeilleov rez}, ko velja
  \begin{enumerate}[(a)]
    \item \(L\) je naseljena, dolnja, in navzgor odprta
    \item \(U\) je naseljena, gornja, in navzdol odprta
    % \item \(L\) je dolnja
    % \item \(U\) je gornja
    % \item \(L\) je navzgor odprt
    % \item \(U\) je navzdol odprt
    \item \(p ∈ L ⇔ \exist{q>p}{q ∉ U}\)
    \item \(q ∈ U ⇔ \exist{p<q}{p ∉ L}\)
  \end{enumerate}
  Množica Dedekind-MacNeilleovih rezov tvori \emph{MacNeilleova realna števila},
  ki jih označimo z \(\Rm\).

  Ureditev na MacNeilleovih realnih številih definiramo enako kot na Dedekindovih
  realnih številih.
\end{definicija}

Lema~\ref{th:real-order-lemma} velja tudi za ureditve na MacNeilleovih realnih številih.

\begin{trditev}
  Vsako Dedekindovo realno število je tudi MacNeilleovo.
\end{trditev}
\begin{dokaz}
  Točki \((a)\) in \((b)\) sta enaki točkama \((1)\) in \((2)\) v Dedekindovi
  konstrukciji, tako da je treba pokazati zgolj zadnji dve. Ker sta
  simetrični, pokažimo zgolj zadnjo. Naj bo \(\p{L,U}\) Dedekindov rez.
  Če je \(p < q\) in \(p ∉ L\), po lociranosti vemo, da je \(q ∈ U\).
  Obratno naj bo \(q ∈ U\). Ker je \(U\) navzdol odprta, obstaja nek \(p ∈ U\),
  ki je manjši od \(q\). Potem je ta \(p\) tak, ki je manjši od \(q\) in ni v
  \(L\).
\end{dokaz}

V obratno smer lahko pokažemo zgolj, da sta \(L\) in \(U\) ločena.
\begin{lema}
  Za MacNeilleovo realno število \(\p{L,U}\) velja \(a∈L∧b∈U⇒a<b\).
\end{lema}
\begin{dokaz}
  Naj bo \(p∈L\) in \(q∈U\). Potem obstaja \(p' < q\), ki ni v \(L\). Ker je
  \(L\) dolnja to pomeni, da tudi \(q\) ni v \(L\). Prav tako ker je dolnja, je
  \(q\) zgornja meja za \(L\), torej je \(p < q\).
\end{dokaz}

Ostalo bi torej pokazati zgolj lociranost vsakega MacNeilleovega realnega
števila, a to žal ni mogoče.
Temu principu bomo torej pravili ``\(\Rm = \Rd\)''.

MacNeilleova realna števila so zanimiva, saj so \emph{polna} v smislu, da
ima vsaka naseljena omejena množica MacNeilleovih realnih števil supremum.
\begin{konstrukcija}\label{cons:Rm-sup}
  Za naseljeno omejeno množico MacNeilleovih realnih števil \(S\) množici
  \begin{gather*}
    U ≔ \set{q : ℚ}{\exist{p<q}{\for{x ∈ S}{p∈Uₓ}}}\text{ in}\\
    L ≔ \set{p : ℚ}{\exist{q>p}{q ∉ U}}
  \end{gather*}
  tvorita MacNeilleovo realno število \(\sup S ≔ \p{L, U}\), ki je supremum
  množice \(S\).
\end{konstrukcija}
\begin{dokaz}
  Prve tri lastnosti MacNeilleove konstrukcije~\ref{def:Rm} očitno
  veljajo, tako da pokažimo le zadnjo.

  Naj bo \(q ∈ U\). Potem obstaja \(p < q\), ki je prav tako element \(U\),
  torej ni element \(L\). Obratno, naj za \(q : ℚ\) obstaja \(p < q\), ki ni
  element \(L\). Definirajmo \(r ≔ \frac{2p+q}3\) in \(s ≔ \frac{p+2q}3\), tako
  da velja \(p < r < s < q\). Potem po definiciji \(L\) \(r ∉ U\) ne velja.
  Ampak, ker je \(U ⊆ Uₓ\) za vse \(x ∈ S\), je \(U⊥Lₓ\).
  Tako velja \(r ∉ Lₓ\), torej je \(s ∈ Uₓ\) in sledi \(q ∈ U\).

  Označimo \(u ≔ \p{L,U}\). Pokažimo najprej, da je gornja meja \(S\).
  Naj bo \(x ∈ S\) in \(p ∈ Lₓ\). Potem obstaja \(q > p\), da je \(q ∉ Uₓ\).
  Potem pa \(q\) ni element \(U\), torej je \(p\) element \(L\).

  Če je \(t : \Rm\) neka zgornja meja, torej velja \(Lₓ⊆Lₜ\) za vse \(x ∈ S\),
  mora veljati tudi \(Uₜ ⊆ Uₓ\). Naj bo torej \(q ∈ Uₜ\) in pokažimo, da je
  \(q ∈ U\). Ker je \(Uₜ\) navzdol odprta obstaja \(p < q\), ki je element
  \(Uₜ ⊆ Uₓ\). Sledi, da je \(p ∈ Uₓ\) za vse \(x ∈ S\), torej je \(q ∈ U\).
  To zaključi dokaz dejstva, da je \(u\) najmanjša gornja meja množice \(S\).
\end{dokaz}
\begin{posledica}
  Princip \(\Rm = \Rd\) je ekvivalenten polnosti Dedekindovih realnih števil.
\end{posledica}

Poglejmo si bolj podrobno ureditve \(<\) in \(≤\). Sedaj smo definirali vsako na
vsaki od množic realnih števil, vemo pa, da velja \(\Rc ⊆ \Rd ⊆ \Rm\). Izkaže
se, da so si relacije povezane.

\begin{lema}
  Za Cauchyjevi realni števili \(x\) in \(y\) velja \(x <_{\Rc} y ⇔ x <_{\Rd} y\)
  in \(x ≤_{\Rc} y ⇔ x ≤_{\Rd} y\).
  Za Dedekindovi realni števili \(x\) in \(y\) velja \(x <_{\Rd} y ⇔ x <_{\Rm} y\)
  in \(x ≤_{\Rd} y ⇔ x ≤_{\Rm} y\).
\end{lema}
Dokaz tega je očiten a zamuden, tako da ga raje izpustimo.

\begin{lema}\label{th:dedekind-real-≤-is-¬>}
  Za Dedekindovi realni števili \(x\) in \(y\) je \(x ≤ y ⇔ ¬(y < x)\).
\end{lema}
\begin{dokaz}
  Očitno \(x ≤ y < x\) vodi v protislovje, torej je smer \(⇒\) dokazana. Naj
  sedaj velja \(¬(y < x)\), torej za noben \(p : ℚ\) ne velja \(y < p < x\).
  To pomeni, da je \(U_y⊥L_x\). Če je sedaj \(p ∈ L_x\), mora po odprtosti
  obstajati \(q ∈ L_x\), ki je večji od \(p\). Potem pa po lociranosti \(y\)
  velja \(p ∈ L_y ∨ q ∈ U_y\). Ampak \(q\) ne more biti v \(L_x\) in \(U_y\),
  tako da je \(p ∈ L_y\).
\end{dokaz}

Lema~\ref{th:dedekind-real-≤-is-¬>} žal ne velja za MacNeilleova realna števila,
kljub temu, da se na \(\Rd\) ujemajo. Implikacija v desno velja, saj ta sledi iz
leme~\ref{th:real-order-lemma}, obratna implikacija pa ne drži. Vseeno pa velja
sledeče:
\begin{lema}
  Za realni števili \(x\) in \(y\) velja \(x < y ∨ x=y ⇒ x ≤ y\).
\end{lema}
Lemo je preprosto preveriti. V klasični logiki tu velja tudi obrat, a tega ne
moremo pokazati konstruktivno.


\subsection{Principi izbire}\label{sec:logika-izbire}

Princip izbire pravi, da za vsaki množici \(A\) in \(B\), in vsako celovito
relacijo \(R\), torej, za katero velja \(\for{x:A}{\exist{y:B}{R(x,y)}}\)
obstaja funkcija \(f : A → B\), tako da velja \(\for{x : A}{R(x, f(x))}\).

Princip izbire lahko ošibimo na tri načine: lahko omejimo množici \(A\) in \(B\),
lahko pa omejimo relacijo \(R\), tako da jemlje resničnostne vrednosti zgolj iz
določene množice \(Σ ⊆ Ω\).

\begin{definicija}
  \emph{Princip izbire nad \(Σ⊆Ω\)} je shema, ki za vsaka \(A\)
  in \(B\) pravi, da za vsako celovito relacijo \(R : A×B → Σ\), obstaja
  \emph{funkcija izbire} \(f : A → B\), tako da velja \(\for{x:A}{R(x,f(x))}\).
  Objektu \(A\) tako pravimo \emph{domena}, objektu \(B\) \emph{kodomena},
  objektu \(Σ\) pa \emph{Sierpinskijev objekt}.
  To označimo z \(\AC_Σ\). Če je \(Σ = Ω\), indeks opustimo in temu pravimo
  \emph{princip izbire}.
\end{definicija}
\begin{definicija}\label{pr:ac}
  Če v principu izbire fiksiramo domeno na \(A\), temu pravimo
  \emph{princip izbire nad \(Σ\) iz \(A\)}, in če fiksiramo še kodomeno na nek
  \(B\) temu pravimo \emph{princip izbire nad \(Σ\) iz \(A\) v \(B\)}. Ta potem
  označujemo \(\AC_Σ(A)\) in \(\AC_Σ(A, B)\). Podobno kot zgoraj opuščamo \(Σ\),
  ko je ta enaka \(Ω\).
\end{definicija}

Hitro lahko opazimo, da so principi izbire neobčutljivi za izomorfizme.
\begin{trditev}
  Naj bo \(φ : A ≅ A'\) in \(ψ : B ≅ B'\). Potem je \(\AC_Σ(A, B)\) ekvivalenten
  \(\AC_Σ(A', B')\).
\end{trditev}
\begin{dokaz}
  Situacija je očitno simetrična, tako da pokažimo zgolj eno implikacijo.
  Če je \({R : A'×B' → Σ}\) celovita, je potem tudi \({R∘\p{φ×ψ} : A×B → Σ}\)
  celovita. Za to relacijo obstaja funkcija izbire \(f : A → B\), da velja
  \(\for{x : A}{R∘\p{φ×ψ}{(x, f(x))}}\), kar je enako
  \(\for{x:A}{R(φ(x),ψ(f(x)))}\). Ker je \(φ\) izomorfizem, lahko
  kvantifikator reindeksiramo in dobimo \(\for{x:A'}{R(x,ψ∘f∘φ⁻¹(x))}\),
  torej je \(ψ∘f∘φ⁻¹\) funkcija izbire za \(R\).
\end{dokaz}
V teoriji množic to pomeni, da je aksiom izbire določen do kardinalnosti
natančno. To nam tudi utemelji zakaj lahko \(\AC(ℕ)\) pravimo princip
\emph{števne} izbire, saj deluje za poljubno števno (neskončno) množico.
Označimo ga torej \(\CC\), iz angleško \textenglish{countable choice}. Pomembno
vlogo bo igral tudi \emph{princip števne disjunktivne izbire} \(\AC(ℕ, 2)\), ki
ga označimo z \(\CCv\). Ime izhaja iz dejstva, da je
\(\exist{b:2}{R(n,b)}\) ekvivalentno \(R(n,0) ∨ R(n,1)\).

\begin{trditev}
  Če je \(Σ' ⊆ Σ\), \(\AC_Σ(A, B)\) implicira \(\AC_{Σ'}(A, B)\).
\end{trditev}
\begin{dokaz}
  Vsaka relacija nad \(Σ'\) je tudi relacija nad \(Σ\), tako da če imajo
  relacije nad \(Σ\) funkcije izbire jih imajo tudi relacije nad \(Σ'\).
\end{dokaz}

\begin{definicija}
  Množica \(A\) je \emph{končna}, ko obstaja naravno število, da je množica
  \(A\) izomorfna \emph{standardni končni množici} \(\cli n ≔ \{1,…,n\}\).
\end{definicija}
\begin{trditev}
  Princip \(\AC(\cli n)\) velja.
\end{trditev}
Dokaza z indukcijo, ki je standarden, na tem mestu ne bomo ponavljali.
% \begin{definicija}
%   \emph{Princip \[Σ\]-izbire iz \(A\) v \(B\)} pravi, da za vsako relacijo
%   \(R : A×B → Σ\) za katero velja \(\for{a:A}{\exist{b:B}{R(a,b)}}\), obstaja
%   funkcija izbire \(f : A → B\), tako da velja \(\for{a:A}{R(a,f(a))}\).

%   To bomo označili z \(\AC_Σ(A,B)\). Z \(\AC_Σ(A)\) bomo označevali shemo
%   \(\for{B}{\AC_Σ(A,B)}\), z \(\AC_Σ\) pa shemo \(\for{A}{\AC_Σ(A)}\).
%   Tem pravimo \emph{princip \(Σ\)-izbire iz \(A\)} in \emph{princip \(Σ\)-izbire}.
%   Kadar je \(Σ = Ω\) bomo \(Σ\) v indeksu opuščali, in ustrezno to poimenovali
%   kar samo \emph{princip izbire (iz \(A\) v \(B\))}.

%   Standardno se principu \(\AC(ℕ)\) pravi \emph{princip števne izbire} in
%   označuje \(\CC\).
%   Posebno pomemben bo princip \(\AC(ℕ, 2)\), ki ga bomo označevali \(\CCv\) in
%   mu pravili \emph{princip števne dvojiške(disjunktivne?) izbire}.
% \end{definicija}



% \begin{definicija}
%   \emph{Princip števne dvojiške izbire} pravi, da če velja
%   \(\for{n : ℕ}{P(n, 0) ∨ P(n, 1)}\) (torej, \(P\) je celovita relacija na
%   \(ℕ×2\)) obstaja funkcija izbire \(f : ℕ → 2\), da velja
%   \(\for{n : ℕ}{P(n,f(n))}\).
% \end{definicija}

Poznamo še princip odvisne izbire.
\begin{definicija}\label{pr:dc}
  \emph{Princip odvisne izbire nad \(Σ\) za \(A\)} pravi, da za vsako celovito
  relacijo \(R : A×A → Σ\) in \(a₀ : A\) obstaja zaporedje \((aᵢ)ᵢ\) začenši z
  \(a₀\), tako da za vsak \(n : ℕ\) velja \(R(aₙ, aₙ₊₁)\). Tega označimo z
  \(\DC_Σ(A)\). Če princip velja za vse \(A\) ga označimo \(\DC_Σ\).
\end{definicija}

\begin{trditev}
  Če je \(Σ⊆Ω\) zaprt za končne konjunkcije in števne disjunkcije, velja
  \(\DC_Σ ⇒ \CC_Σ\).
\end{trditev}
\begin{dokaz}
  Naj bo \(R : ℕ×B → Σ\) celovita.
  Definirajmo \(X ≔ \set{b:B}{\exist{n:ℕ}{R(n,b)}}\) in na \(X×X\) relacijo
  \(Q(x,y) ≔ \exist{n:ℕ}{R(n,x)∧R(n+1,y)}\).

  Ta je celovita, tako da lahko na njej uporabimo \(\DC_Σ\), torej dobimo
  zaporedje \(x : ℕ → X\). Ker je \(X⊑B\) je torej to preslikava \(ℕ → B\), ki
  ima želeno lastnost.
\end{dokaz}
S pogojem, da je \(Σ\) zaprt za navedeni operaciji, zagotovimo, da je \(Q\)
relacija na \(Σ\).

Poznamo tudi princip enolične izbire. Ta pravi, da vsaka funkcijska relacija
določa (enolično) funkcijo. Ker smo v topoloških modelih funkcije definirali
kot funkcijske relacije, v topoloških modelih ta princip vedno velja, tako da ga
ne bomo posebej obravnavali.


\subsection{Principi odločitve}\label{sec:logika-odločitve}

\begin{definicija}[Izključena tretja možnost]\label{pr:lem}
  \emph{Princip izključene tretje možnosti} pravi, da za vsako resničnostno
  vrednost \(p\) velja \(p∨¬p\). Formulo \(p∨¬p\) označimo \(\lem(p)\), formulo
  \(\for{p:Ω}{p∨¬p}\) pa z \(\lem*\).
\end{definicija}

\begin{definicija}[Šibka izključena tretja možnost]\label{pr:wlem}
  \emph{Princip šibke izključene tretje možnosti} pravi, da za vsako
  resničnostno vrednost \(p\) velja \(¬p∨¬¬p\). Formulo \(¬p∨¬¬p\) označimo
  \(\wlem(p)\), formulo \(\for{p:Ω}{¬p∨¬¬p}\) pa z \(\wlem*\).
\end{definicija}
\begin{trditev}\label{th:lem-impl-wlem}
  Velja implikacija \(\lem* ⇒ \wlem*\).
\end{trditev}
\begin{dokaz}
  Formula \(\wlem(p)\) je natanko \(\lem(¬p)\), tako da trditev očitno velja.
\end{dokaz}

\begin{definicija}
  Naj bodo \(x\), \(y : ℝ\) in \(α\), \(β : 2^ℕ\). Relacija \(\apart\) je
  definirana kot
  \[ x \apart y ⇔ x > y ∨ x < y\text{ in} \]
  \[ α \apart β ⇔ \exist{n : ℕ}{α(n) ≠ β(n)}\text.\]
\end{definicija}
To je konstruktivno strožja verzija neenakosti, zato jo pišemo kot dvakrat
prečrtano enakost.

\begin{definicija}\label{pr:lpo}
  \emph{Princip števne odločitve} pravi, da za vsako števno zaporedje ničel in enic
  lahko odločimo, ali je celo nič, ali pa vsebuje enico.
  Formulo \(α = 0∨α\apart 0\) označimo \(\lpo(α)\), formulo
  \(\for{α : 2^ℕ}{\lpo(α)}\) pa z \(\lpo*\).
\end{definicija}

%TODO: tega verjetno ne rabim?
% \begin{definicija}\label{pr:wlpo}
%   \emph{Princip šibke števne odločitve} pravi, da za vsako števno zaporedje
%   ničel in enic lahko odločimo, ali je celo nič, ali ni.
%   Formulo \(α = 0∨α ≠ 0\) označimo \(\wlpo(α)\), formulo
%   \(\for{a:2^ℕ}{\wlpo(α)}\) pa z \(\wlpo*\)
% \end{definicija}

\begin{definicija}\label{pr:alpo}
  Naj bo \(ℝ\) ena od različic realnih števil.
  \emph{Analitični princip števne odločitve za \(ℝ\)} pravi, da za vsako realno
  število lahko odločimo, ali je pozitivno ali nenegativno. Formulo
  \(x > 0 ∨ x ≤ 0\) označimo \(\alpo_ℝ(x)\), formulo \(\for{x : ℝ}{\alpo_ℝ(x)}\) pa
  z \(\alpo*_ℝ\).

  Če je \(ℝ = \Rd\), indeks opustimo in pravimo le \emph{analitični princip
    števne odločitve}.

  Podobno definiramo \emph{analitični princip šibke števne odločitve za \(ℝ\)},
  ki ga označimo \(\awlpo*_ℝ\), s formulo \(\awlpo_ℝ(x) = x≤0 ∨ ¬(x≤0)\).
\end{definicija}

\begin{trditev}\label{th:alpo-equiv}
  Princip \(\alpo*_ℝ\) je ekvivalenten \(\for{x:ℝ}{x = 0 ∨ x \apart 0}\) in
  \(\awlpo*_ℝ\) je ekvivalenten \(\for{x:ℝ}{x = 0 ∨ ¬(x=0)}\).
\end{trditev}
\begin{dokaz}
  Če uporabimo \(\alpo*_ℝ\) na \(x\) in \(-x\) dobimo želeno formulo. Obratno pa
  \({x = 0 ∨ x < 0}\) implicira \(x ≤ 0\). Podobno pokažemo tudi drugi del.
\end{dokaz}
Tako bomo prosto od tu naprej menjali med ekvivalentnima pogojema. Seveda pa se
v posameznem dokazu omejimo na zgolj enega.

\begin{trditev}\label{th:alpoc-is-lpo}\label{th:implications}
  Velja veriga implikacij \(\lem* ⇒ \alpo* ⇒ \alpo*_{\Rc} ⇔ \lpo*\).
\end{trditev}
\begin{dokaz}
  Ker je \(¬(x > 0)\) natanko \(x ≤ 0\), je \(\alpo*\) očitno posledica
  \(\lem*\). Prav tako je vsako Cauchyjevo realno število tudi Dedekindovo, tako
  da druga implikacija tudi velja.

  Za zadnjo ekvivalenco pa potrebujemo malo dela. Pri \(\lpo*\) odločamo, ali
  imamo povsod nič, ali pa obstaja enica. Naj bo \(α\) zaporedje, za
  katerega odločamo \(\lpo*\). Definiramo Cauchyjevo realno število
  \[ x ≔ \lim_{n → ∞}2^{-\min\set{k : ℕ}{α(k) = 1 ∨ k = n}}\text. \]
  Uporabimo \(\alpo(x)\). Če velja \(x ≤ 0\), mora zaporedje limitirati proti
  \(0\), kar pomeni, da \(α(k) = 1\) ni nikoli zadoščeno, torej je \(α = 0\).
  Po drugi strani, če je \(x > 0\), obstaja nek \(k : ℕ\), tako da je
  \(x > 2⁻ᵏ\). To pomeni, da ima \(α\) enico na enem izmed prvih \(k\)
  mest, kar pomeni, da želeni indeks obstaja.

  Preostanek dokaza izvira iz~\cite{Gro-Tsen24}.
  Naj bo \(x = (xᵢ)ᵢ\) Cauchyjevo zaporedje, za katerega odločamo \(\alpo_{\Rc}*\).
  Definiramo lahko zaporedje
  \[ β(k,n) ≔
    \begin{cases}
      1 &; \for  {m≥n}{xₘ ≤ 2⁻ᵏ}\\
      0 &; \exist{m≥n}{xₘ > 2⁻ⁿ}\text.
    \end{cases} \]
  Vse te odločitve lahko naredimo, saj velja \(\lpo*\) in je neenakost med
  racionalnimi števili odločljiva. Sedaj uporabimo \(\lpo*\) na \(n↦β(k,n)\).

  Podobno definiramo
  \[ α(k) ≔
    \begin{cases}
      1 &; \for  {n:ℕ}{β(k,n) = 0}\\
      0 &; \exist{n:ℕ}{β(k,n) = 1}\text.
    \end{cases} \]
  Nazadnje uporabimo \(\lpo*\) na \(α\). Če je \(α = 0\), imamo za vsak
  \(k\) nek \(n\), da je za vsak \(m≥n\) \(xₘ ≤ 2⁻ᵏ\), kar pomeni, da je
  \(x = 0\). Po drugi strani, če je \(α(k) = 1\) za nek \(k\), pa velja, da za
  vsak \(n\) obstaja \(m≥n\), da je \(xₘ > 2⁻ᵏ\), torej je \(x > 2⁻ᵏ\) in je
  \(x > 0\).
\end{dokaz}

To pomeni, da analitični princip števne odločitve za Cauchyjeva realna števila
ni zanimiv, tako od tu naprej prosto menjamo med \(\alpo*_{\Rc}\) in
\(\lpo*\) po potrebi, kjer to ne povzroči zmede.


\subsection{Ostali principi}\label{sec:logika-ostalo}

Seveda se principi ne delijo popolnoma zgolj na principe izbire in odločitve.
Nekaj takih imamo zgoraj o realnih številih, nekaj jih bomo pa še definirali.


\subsubsection{Redukcija instanc}

Oglejmo si najprej razne Sierpinskijeve objekte, ki smo jih do sedaj definirali.
\begin{align*}
  Ω   &= \set{p}{p : Ω}\\
  Σ_ℝ &= \set{x > 0}{x : ℝ}\\
  Σ⁰₁ &= \set{α \apart 0}{α : 2^ℕ}\\
  Δ   &= \set{p : Ω}{p ∨ ¬p}\\
  R   &= \set{p : Ω}{¬¬p ⇒ p}
\end{align*}
Objektom \(Σ_ℝ\), \(Σ⁰₁\), \(Δ\), in \(R\) pravimo \emph{realne},
\emph{semiodločljive}, \emph{odločljive}, in \emph{regularne} resničnostne vrednosti.
% Tu nam \(Δ\) predstavlja Sierpinskijev objekt \emph{odločljivih} resničnostnih
% vrednosti, \(R\) pa \emph{regularnih}.

\begin{trditev}
  Naj bo \(ℝ\) objekt realnih števil. Potem je Sierpinskijev objekt \(Σ_ℝ\) enak
  \(\set{x \apart 0}{x : ℝ}\).
\end{trditev}
\begin{dokaz}
  Če je \(x : ℝ\), je \(x \apart 0 ⇔ \abs x > 0\).
  Obratno je \(x > 0 ⇔ \max\{x,0\} \apart 0\).
\end{dokaz}

\begin{definicija}\label{pr:res}
  Vse logične principe, kvantificirane po \(Ω\), lahko omejimo tako, da domeno
  kvantifikacije omejimo na nek Sierpinskijev objekt. Specifično je torej
  \(\lem*{\res Σ} ≔ \for{p∈Σ}{\lem(p)}\), itd.
\end{definicija}

\begin{trditev}
  Princip \(\lem*{\res Δ}\) velja.
\end{trditev}

Izkaže se, da lahko principe odločitve izrazimo kot princip izključene tretje
možnosti, omejene na te Sierpinskijeve objekte.
\begin{trditev}
  Imamo \(\alpo* = \lem*{\res{Σ_{\Rd}}}\), \(\alpo*_{\Rc} = \lem*{\res{Σ_{\Rc}}}\), in
  \(\lpo* = \lem*{\res{Σ⁰₁}}\).
\end{trditev}
\begin{dokaz}
  Ker je \(¬(x > 0) ⇔ x ≤ 0\), in \(¬(α\apart 0) ⇔ α = 0\), enakosti sledijo.
\end{dokaz}
Podobno lahko šibke verzije gornjih principov dobimo kot zožitve \(\wlem*\) na
vsakega od teh objektov. To je tudi razlog, zakaj tej skupini principov pravimo
``principi odločitve''.

Pokazali smo tudi, da je \(\alpo*_{\Rc} ⇔ \lpo*\). Ali to pomeni, da
je \(Σ_{\Rc} = Σ⁰₁\)? Namreč, v dokazu~\ref{th:alpoc-is-lpo} skonstruiramo taka
\(x : \Rc\) in \(α : 2^ℕ\), da je \(x > 0\) natanko tedaj, ko je \(α \apart 0\).

A vendar se izkaže, da velja zgolj \(Σ⁰₁ ⊆ Σ_{\Rc}\). Če pogledamo dokaz, v to
smer brez predpostavk skonstruiramo \(x : \Rc\), v obratni smeri pa bistveno
uporabimo več (celo neskončno) \emph{instanc} \(\lpo*\) v konstrukciji zaporedja
\(α\).

Izkaže se, da lahko matematično natančno opišemo gornji pojav~\cite{Bauer22}.
Ideja pride iz teorije izračunljivosti, specifično iz Weihrauchovih redukcij.
Tam skrbno pazimo, kolikokrat se uporabi posamezne predpostavke.

\begin{definicija}
  Predikat \(φ ⊑ A\) je \emph{reducibilen} na predikat \(ψ ⊑ B\), ko velja
  \[ \for{x:A}{\exist{y:B}{ψ(y) ⇒ φ(x)}}\text. \label{eq:inst-red} \]
  To označimo z \(\p{φ, A} ≤ \p{ψ, B}\), ali kar z \(φ ≤ ψ\), ko so domene
  predikatov razvidne iz konteksta.
\end{definicija}

Reducibilnost nam torej pove, da lahko vsako instanco \(\for{x:A}{φ(x)}\)
(torej, vsak \(φ(a)\)) dokažemo tako, da poiščemo nek \(b:B\), da bo \(ψ(b)\)
dovolj močen, da lahko pokaže \(φ(a)\). Pomembno tu je, da lahko poiščemo samo
en \(b\), torej lahko uporabimo samo eno instanco \(\for{y:b}{ψ(b)}\).

Tako vsi principi odločitve in izbire postanejo instance, saj so vsi univerzalno
kvantificirani. Prav tako, če pogledamo dokaze trditev~\ref{th:lem-impl-wlem}
in~\ref{th:implications} vidimo, da dobimo redukcije
\(\lpo* ≤ \alpo*_{\Rc} ≤ \alpo* ≤ \lem*\) in \(\wlem* ≤ \lem*\). 

Redukcije \(\p{φ, A} ≤ \p{φ, B}\), ko je \(A ⊆ B\), so očitne, tako da poglejmo
le ta zanimivo redukcijo \(\lpo* ≤ \alpo*_{\Rc}\).

\begin{trditev}
  Velja redukcija \(\lpo* ≤ \alpo*_{\Rc}\).
\end{trditev}
\begin{dokaz}
  Naj bo \(α:2^ℕ\). Definirajmo realno število
  \[ x ≔ \lim_{n → ∞}2^{-\min\set{k : ℕ}{α(k) = 1 ∨ k = n}}\text. \]

  Kot smo zgoraj pokazali velja \(x \apart 0 ⇔ α \apart 0\), torej redukcija
  velja.
\end{dokaz}

Reducibilnost nam torej definira refleksivno in tranzitivno relacijo. To lahko
dopolnimo do ekvivalenčne relacije \(≡\), ki ji pravimo \emph{ekvivalenca instanc}.
Ekvivalenčnim razredom po tej relaciji pravimo \emph{stopnje instance}, ali na
kratko \emph{stopnje}.
Izkaže se, da ima ta ureditev zelo lepo strukturo. Več o njej si lahko pogledate
v~\cite{Bauer22}, mi bomo pa definirali le produkt stopenj.

\begin{definicija}
  \emph{Produkt \(φ⊑A\) in \(ψ⊑B\)} je predikat \(φ×ψ⊑A×B\) definiran s
  predpisom \(φ×ψ(a,b) ≔ φ(a)∧ψ(b)\).
  Na očiten način lahko definiramo končne potence \(φⁿ\) predikata \(φ\).
  Prav tako lahko definiramo števno potenco \(φ^ℕ\) predikata \(φ\) s predpisom
  \(φ^ℕ((aᵢ)ᵢ) ≔ \for{i:I}{φ(aᵢ)}\).
\end{definicija}

\begin{definicija}
  Pravimo, da je \(φ⊑A\) \emph{idempotenten}, ko velja \(φ²≤φ\).
\end{definicija}
Idempotentnost pomeni, da lahko odločitev \(φ\) za dve vrednosti \(a₀\) in
\(a₁ ∈ A\) odločimo zgolj z eno ``poizvedbo'' \(φ\) na nekem \(a ∈ A\).

Poglejmo si recimo \(\lem*\). Na prvi pogled je videti, kot da se moramo
odločiti med štirimi alternativami, \(p∧q\), \(p∧¬q\), \(¬p∧q\), in \(¬p∧¬q\),
medtem ko nam ena instanca \(\lem*\) da zgolj dve možnosti. Čeprav se zdi
nemogoče, idempotenco \(\lem*\) lahko dokažemo.

\begin{lema}
  Za vse \(p:Ω\) velja \(¬¬\lem(p)\).
\end{lema}
\begin{dokaz}
  Formula \(¬\lem(p)\) je ekvivalentna \(¬p∧¬¬p\), kar ne drži.
\end{dokaz}

\begin{trditev}
  Princip \(\lem*\) je idempotenten.
\end{trditev}
\begin{dokaz}
  Naj bosta \(p\) in \(q\) resničnostni vrednosti.
  Iz \(\lem{\p{\lem²(p,q)}}\) sledi \(\lem²(p,q)\), saj \(¬\lem²(p,q)\) ne
  velja, torej je \(\lem²(p,q)\) želena vrednost.
\end{dokaz}
Reducibilnost izhaja iz teorije izračunljivosti. Tam se idempotenca ne pojavi
pogosto, saj tam pomeni, da lahko dve izvedbi algoritma izvedemo že z eno
izvedbo, na posebej izbranem vhodu. Recimo \(\lpo*\) ni idempotenten.
Hipotetični algoritem, ki bi odločal \(\lpo(α)\), najprej reče, da je odločil
\(α=0\). Nato bere zaporedje, in ko naleti na enico, potuje skozi čas in
spremeni svoj odgovor. Če iščemo enico v dveh zaporedjih, mora za vsakega od
njih potovati skozi čas, tako da gotovo ne moremo tega izračunati z eno izvedbo
algoritma. Se pa izkaže, da v topoloških modelih temu ni nujno tako, a k temu se
vrnemo kasneje.

V~\ref{th:alpoc-is-lpo} smo pokazali, da so principi, ki govorijo o \(Σ⁰₁\) in
\(Σ_{\Rc}\) ekvivalentni. Ampak vseeno ta Sierpinskijeva objekta nista nujno
enaka. Na kratko se lahko o tem prepričamo tako, da opazimo, da je dokaz tega
dejstva zahteval neskončno instanc \(Σ⁰₁\), torej so elementi \(Σ_{\Rc}\)
ekvivalentni števnim konjunkcijam elementov \(Σ⁰₁\). Velja torej naslednja
redukcija.
\begin{trditev}
  Velja redukcija \(\alpo*_{\Rc} ≤ \lpo*^ℕ\).
\end{trditev}
\begin{dokaz}
  To smo pravzaprav pokazali že zgoraj. Uporabimo \(ω⋅ω + ω + 1\) instanc \(\lpo*\),
  kar je števno mnogo, torej je števno mnogo instanc \(\lpo*\) dovolj za gornjo
  redukcijo.
\end{dokaz}


\subsubsection{Kripkejeve sheme}

Oglejmo si sedaj malce strožjo reducibilnost, namreč, ko v~\ref{eq:inst-red} zamenjamo
\(⇒\) z \(⇔\). Specifično nas to zanima, saj si želimo ogledati principe
\(Σ = Ω\), za razne Sierpinskijeve objekte, kajti to velja natanko tedaj, ko
velja \(\for{p:Ω}{\exist{s∈Σ}{s ⇔ p}}\). Kot vidimo, je to enaka formula
kot~\ref{eq:inst-red}, le da smo \(⇒\) zamenjali z \(⇔\).

\begin{definicija}\label{pr:ks}
  \emph{Kripkejeva shema za \(Σ ⊆ Ω\)} pravi, da je \(Σ = Ω\). Formulo
  \(\for{p : Ω}{\exist{s : Σ}{s = p}}\) označimo s \(\ks*(Σ)\).
  Navadna \emph{Kripkejeva shema} je Kripkejeva shema za
  \(Σ⁰₁ ≔ \set{α \apart 0}{α : 2^ℕ} ⊆ Ω\) in jo označimo \(\ks*\).

  \emph{Analitična Kripkejeva shema za \(ℝ\)} je Kripkejeva shema za \(Σ_ℝ\),
  kjer je \(ℝ\) nek objekt realnih števil. Označimo jo z \(\aks*_ℝ\)
  Posebej \(\ks*(Σ_{\Rd})\) pravimo \emph{analitična Kripkejeva shema}.
\end{definicija}

\begin{trditev}
  Kripkejeva shema za \(Δ\) je ekvivalentna \(\lem*\).
\end{trditev}

\begin{trditev}\label{th:aks-impl-lem≤alpo}
  Če velja \(\ks*(Σ)\), velja \(\lem* ≤ \lem*{\res{Σ}}\).
\end{trditev}
\begin{dokaz}
  Naj bo \(p:Ω\). Po predpostavki je \(Σ = Ω\), torej je \(p∈Σ\). Potem
  lahko na \(p\) uporabimo \(\lem*{\res{Σ}}\) in \(\lem(p)\) velja.
\end{dokaz}
\begin{posledica}
  Če velja \(\ks*(Σ)\), je \(\lem*{\res{Σ}}\) idempotenten.
\end{posledica}


\subsubsection{Princip Markova}

\begin{definicija}\label{pr:mp}
  \emph{Princip Markova} je \(\for{α:2^ℕ}{¬(α=0) ⇒ α \apart 0}\). Kot ponavadi
  označimo z \(\mp(α)\) notranjo formulo in z \(\mp*\) kvantificiran izraz.

  Podobno kot v~\ref{pr:alpo} definiramo analitične različice principa.
\end{definicija}
Ta je zožitev principa eliminacije dvojne negacije, \(\for{p:Ω}{¬¬p ⇒ p}\), na
Sierpinskijev objekt \(Σ⁰₁\). Za tega vemo, da je ekvivalenten izključeni tretji
možnosti, a je \(\mp*\) vseeno šibkejši od \(\lpo*\).
% \begin{dokaz}
%   Če velja \(α = 0 ∨ α \apart 0\), in ne velja \(α=0\), potem velja \(α \apart 0\).
% \end{dokaz}

Kot na začetku tega podrazdelka lahko zožimo še Kripkejevo shemo. Tu moramo
paziti, da ko zožimo \(\ks*(Σ)\) na \(Σ' ⊆ Ω\), mora veljati \(Σ ⊆ Σ'\).
\begin{trditev}
  Kripkejeva shema za \(Σ⁰₁∩R ⊆ Σ⁰₁\) je natanko princip Markova in je
  ekvivalenten trditvi \(Σ⁰₁ ⊆ R\). Podobno velja za analitične različice
  principa.
\end{trditev}

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