effektiver-topos.txt

=== Assemblies

* Sei A eine PCA. Eine A-Assembly ist dann eine Menge X zusammen mit je einer
  bewohnten Teilmenge R_x <= A für jedes Element x aus X. Wir schreiben genau
  dann

      a |== x,  wenn  a in R_x.

* Ein Morphismus von Assemblies ist eine Abbildung der zugrundeliegenden
  Mengen für den es einen Realisierer e gibt: ein Element aus A mit der
  Eigenschaft, dass

      für alle x aus X und alle a mit a |== x gilt:
          ea |== f(x).

* Eine Assembly heißt genau dann modest (anständig), wenn:

      e |== x  und  e |== y   ===>   x = y.

  Eine anständige Assembly ist also dasselbe wie eine Menge X zusammen mit
  einer partiellen Surjektion A --> X.

* Die volle Unterkategorie der anständigen Assemblies ist reflektiv.

* Ebenso ist Set eine reflektive volle Unterkategorie. (Dabei nehmen wir
  als Realisierer einfach alle Elemente aus A.)

* Die Kategorie der Assemblies ist kartesisch abgeschlossen und regulär.
  Außerdem besitzt sie (wie auch die Kategorie der anständigen Assemblies)
  endliche Kolimiten. Die Einbettung Mod --> Asm bewahrt diese. Auch Mod ist
  regulär.

  Das Exponential Y^X ist als Menge gegeben durch die Menge der
  Assembly-Morphismen X --> Y. Genau dann schreiben wir e |== f,
  falls e ein Realisierer für f wie in der Definition eines Assembly-Morphismus
  ist.

  Ist Y anständig, so ist es auch Y^X.

* Ein Morphismus in Asm oder Mod ist genau dann ein Mono/Epi, wenn die
  zugrundeliegende Abbildung injektiv/surjektiv ist.

* Ein Morphismus in Asm oder Mod ist genau dann ein regulärer Epi,
  wenn es auch einen Realisierer für die Urbilder gibt, wenn also die interne
  Aussage "die Abbildung ist surjektiv" wahr ist.

* Ein Morphismus f in Asm ist genau dann ein regulärer Mono, wenn
  er ein Mono ist und wenn es einen Realisierer e gibt sodass,
  falls a |== f(x), dann ea |== x.

  Letzteres ist genau dann der Fall, wenn in der internen Sprache Zugehörigkeit
  zum Unterobjekt negneg-stabil ist. (Stimmt die Äquivalenz?)

* Schon in Asm (und Mod?) kann man Logik erster Ordnung interpretieren.
  Details stehen in Streicher.


=== Konstruktion des effektiven Topos

Nach https://webdpmms.maths.cam.ac.uk/~martin/Research/Oldpapers/hyland-effectivetopos.pdf.

* Objekte: Paare (X,=), wobei X eine Menge ist und (=) ein
  "Nichtstandardprädikat" auf X x X ist, also eine Relation r |== (x=y)
  zwischen Zahlen und Elementen von X x X. Dabei muss gelten:

  * Es gibt eine Maschine, die die Symmetrie von (=) bezeugt,
    die also Realisierer von (x=y) in Realisierer von (y=x) umwandelt.

  * Es gibt eine Maschine, die die Transitivität von (=) bezeugt.

  (Reflexivität fordert man nicht. Wir schreiben "Ex" für (x=x).)

  Das ist also nicht ganz dasselbe wie eine Assembly, da wir keinen Begriff von
  Realisierern für die Elemente von X haben.

  Ein solches Paar (X,=) gibt aber Anlass zu einer Assembly. Nämlich die, die
  als Trägermenge X' := { x in X | ex. r |== (x=x) } und als
  Realisierbarkeitsrelation r |== x <==> r |== (x=x) hat. Die Relation (=) gibt
  dann ein Unterobjekt von X' x X': Trägermenge { (x,y) in X' x X' | ex. r |== (x=y) },
  Realisierbarkeitsrelation NICHT "r |== (x,y) <==> r |== (x=y)", sondern
  "r |== (x,y) <==> pi_1(r) |== x und pi_2(r) |== y und pi_3(r) |== (x=y)",
  Inklusion offensichtlich. Aus Realisierbarkeitssicht ist diese Relation dann
  reflexiv, symmetrisch und transitiv.

* Morphismen (X,=) --> (Y,=) sind Äquivalenzklassen funktionaler Relationen G
  (Nichtstandardprädikate auf X x Y):

      |== G(x,y) wedge x = x' wedge y = y' --> G(x',y')
      |== G(x,y) --> Ex wedge Ey
      |== G(x,y) wedge G(x,y') --> y = y'
      |== Ex -> exists y. G(x,y)

  Mit "|==" ist hier etwa gemeint: Es gibt eine Maschine, die Paare (r,s,t) mit
  r in G(x,y), s |== (x=x'), t |== (y=y') nimmt und eine Zahl u mit u in
  G(x',y') ausgibt.

  Zwei solche Relationen G und H sind genau dann äquivalent, wenn

      |== G(x,y) <--> H(x,y).

* Der Unterobjektklassifizierer ist folgendes Objekt: (Sigma,<->),
  wobei Sigma = P(N) und r |== M <-> N genau dann, wenn r eine Maschine ist,
  die Elemente aus M auf Elemente aus N abbildet.

  Hm. Diese Relation ist reflexiv, Sigma ist also wirklich groß (hat viele
  globale Elemente).

* Achtung: Die zugrundeliegende Menge eines Objekts (X,=) ist *keine*
  Isomorphieinvariante. Dagegen ist Γ(X,=) es natürlich schon.

* Ein Objekt (X,=) ist genau dann separiert, wenn es isomorph ist zu
  einem, für das aus Bewohntheit von [[ x = x' ]] schon folgt, dass x = x'.
  (Zumindest in einer klassischen Metatheorie.)

* Lass jetzt mal in einer konstruktiven Metatheorie arbeiten. Stimmt folgendes?
  Der kanonische Morphismus X --> ΔΓX ist genau dann ein Mono, wenn für alle x, x'
  aus |X| aus der Bewohntheit von [[ x = x' ]] folgt, dass x = x'.
  Nein, glaube nicht, dass das stimmt. Weil ich oben "isomorph zu" überlesen
  habe.

  Zur Erinnerung: ΔY hat als zugrundeliegende Menge Y und als
  Gleichheitsprädikat [[ y = y' ]] = { n | y = y' }. Und ΓX ist die Menge
  derjenigen x aus |X|, für die [[ x = x ]] bewohnt ist, "modulo [[ x = y ]]".

  "==>": Seien x, x' aus |X| mit r in [[ x = x' ]]. Dann gibt es auch e in
  [[ x = x ]], e' in [[ x' = x' ]]. In ΓX sind damit x und x' gleich.
  Und weiter?


=== Realisierbarkeitslogik

* r |== neg(phi) bedeutet: Es gibt keinen Realisierer für phi.
  Dabei geht r auf der rechten Seite gar nicht ein!

* r |== neg(neg(phi)) bedeutet: Es gibt nicht nicht einen Realisierer
  für phi. In klassischer Logik ist das natürlich äquivalent dazu, dass es
  einen Realisierer für phi gibt. Wieder geht r gar nicht ein.

* Ein Realisierer a realisiert genau dann (neg neg phi --> phi),
  wenn aus der (nicht nicht) Realisierbarkeit von phi folgt, dass für alle
  Realisierer r gilt, dass ar |== phi.


=== Beispiele für Realisierbarkeitsübersetzungen

* "Es gibt eine Injektion phi : N^N --> N" bedeutet, dass es eine Injektion
  (Menge der berechenbaren Funktionen N --> N) --> N gibt, welche berechenbar
  ist: Gegeben ein Realisierer einer berechenbaren Funktion f : N --> N, soll
  die natürliche Zahl phi(f) produzieren.

  Das ist nicht möglich bei gewöhnlichen Turingmaschinen, wohl aber bei ITTMs.
  Definiere dabei phi(f) := min { n | die n-te ITTM berechnet f }.

* Genau dann gibt es einen Realisierer für "Jede Funktion N --> N ist entweder
  konstant Null oder an einer Stelle ungleich Null", wenn es ein Halteorakel
  gibt (genauer: ein Orakel, welches entscheidet, ob eine gegebene Maschine in
  endlich vielen Schritten hält). Die Aussage ist also nicht realisierbar im
  Fall gewöhnlicher Turingmaschinen, aber durchaus realisierbar bei ITTMs.

  Denn sei ein solcher Realisierer gegeben. Ist eine Maschine gegeben, welche
  auf Terminierung untersucht werden soll, dann befragen wir den Realisierer
  nach dem Konstantheitsstatus derjenigen Funktion, welche n schickt auf den
  Wahrheitswert, ob die Maschine nach n Schritten bereits angehalten hat.

  Umgekehrt können wir mit einem Halteorakel den Realisierer für die gegebene
  Funktion einfach nacheinander auf allen Eingaben laufen lassen.

* "Jede 0/1-Folge, welche nicht nur aus Nullen besteht, enthält eine Eins."
  (Markov) Das stimmt bei gewöhnlichen Turingmaschinen und bei ITTMs. Der
  Realisierer führt einfach eine unbeschränkte Suche durch.

* Auswahlaxiom: Man kann recht einfach zeigen, dass eine Assembly X genau
  dann projektiv ist, wenn es einen Realisierer r gibt, der kanonische
  Realisierer für die Elemente aus X berechnet: Ist a ein Realisierer eines
  Elements von X, so soll auch ra einer sein; und sind a und b Realisierer
  desselben Elements, so soll ra = rb sein.

* Die formale Church--Turing-These besagt: Jede Funktion N --> N ist
  durch eine Turingmaschine (äquivalent: einen λ-Term) gegeben. Im
  Realisierbarkeitsmodell durch Turingmaschinen ist sie trivialerweise erfüllt.
  Im Modell durchs λ-Kalkül dagegen nicht, da ein Realisierer nicht in gegebene
  λ-Terme hineinschauen kann.

  Als Konsequenz ist die Funktion N^N --> N/~, welche einer Funktion die
  Äquivalenzklasse von sie berechnenden Turingmaschinen zuordnet, nicht
  realisierbar im λ-Kalkül-Modell, wohl aber im TM-Modell.

* Was sind Beispiele für Aussagen, die im λ-Kalkül-Modell, aber nicht im
  TM-Modell realisierbar sind?

* TM können übrigens parallel-or, Lambda-Kalkül nicht. Das besagt wohl
  das Berry sequentiality theorem.
  http://lama.univ-savoie.fr/~hyvernat/Realisabilite2011/Files/JohnLongley1.pdf#page=26

* Vermutung von Longley und Phoa: Jedes Element einfachen Typs in PER(λC) ist
  PCF-definierbar.

* Es gibt Beispiele für propositionale Aussagen, die realisiert werden,
  aber nicht in Heyting-Arithmetik ableitbar sind: Rose 1953,
  https://www.ams.org/journals/tran/1953-075-01/S0002-9947-1953-0055952-4/S0002-9947-1953-0055952-4.pdf,
  Thm. 6.1. Ich verstehe aber die Notation nicht.

  Lässt man die Beschränkung auf propositionale Aussagen fallen, gibt es viele
  Beispiele: etwa die Negation der Aussage, jede Turingmaschine halte oder
  halte nicht.

* In Eff gibt es eine Folge rationaler Intervalle, die R überdecken
  und von beliebig kleinem Gesamtmaß sind.
  (https://webdpmms.maths.cam.ac.uk/~martin/Research/Oldpapers/hyland-effectivetopos.pdf)

* Aufgrund von paralleler Simulierung gelten (MP und de Morgan in der Metatheorie
  vorausgesetzt) paar interessante nicht-konstruktive propositionale
  Behauptungen:

  https://mathoverflow.net/questions/300362/how-is-this-ha-unprovable-formula-recursive-realizable


=== In schwachen Metatheorien

* PRA zeigt:

      Falls HA die Sequenz (phi |- psi) im Kontext x_1, ..., x_n ableitet, so
      gibt es eine Zahl r mit

          HA |- (r ||= (forall x_1. ... forall x_n. (phi ==> psi))).

* PRA + "Turingmaschinen, die HA-beweisbar terminieren, terminieren" zeigt
  auch:

      Falls HA |- phi, so gibt es r mit HA |- (r ||= phi).

* PRA zeigt:

      Falls HA |- phi, so HA |- (exists r. r ||= phi).

* Update: Es hängt wohl davon ab, wie die Klauseln für ∃ und ∨ aussehen.
  Fordern die direkt die Existenz von Zeugen oder nur die Existenz von
  Turingmaschinen, die Zeugen berechnen könnten?

  Ich denke, dass, falls letzteres, schon PRA zeigt: Falls HA |- phi,
  so gibt es r mit HA |- (r ||= phi).

  Aber wieso betont das niemand?

* Mit der neuen Konvention geht der falsche Beweisversuch des
  Reflektionsprinzips nicht durch, wie es sollte:

  Gelte HA |- (HA |- phi). Dann gibt es r mit HA |- (r ||= (HA |- phi)).
  Also HA |- (r ist eine Turingmaschine, die mit einem HA-Beweis von phi
  terminiert). Daraus folgt aber nicht (in einer schwachen Metatheorie), dass
  HA |- phi.

* Ich denke, die "neue Konvention" folgt allgemein wie folgt.
  Man verwendet ja, wenn man gut drauf ist, eine PCA als Grundlage.
  Dort ist die Paarung <x,y> definiert als \f -> f x y. Also als Funktion! Als
  Maschine, die bereit ist, x und y zu produzieren. Nicht als direkt
  zugängliches Pärchen.

* https://mathoverflow.net/questions/323964/kleene-realizability-in-peano-arithmetic
  Antwort auf die Frage, welche Formeln aus PA-Sicht realisierbar sind:
  Diejenigen, die in HA + ECT₀ + MP + SLEM beweisbar sind.


=== Realisierung von IZF

* Man kann sogar eine Realisierbarkeitssemantik für IZF, inklusive
  nichtklassischer Prinzipien aber großer Kardinalzahlen (!) angeben.
  http://lama.univ-savoie.fr/~hyvernat/Realisabilite2011/Files/JohnLongley1.pdf,
  Seite 13.

* Krivine's philosophy is that new programming concepts should be motivated by
  their need to realize important axioms. (Seite 18)


=== Idempotenz von Realisierbarkeit

* Für jede HA-Formel phi gilt: HA + ECT_0 |- (phi <--> (|== phi)).

  Dabei ist ECT_0, für beliebige Formeln B(x,y) und "fast negativen" Formeln
  A(x) (aus "t = s", "exists x. t = s", top, bot, wedge, implies, forall
  zusammengesetzt):

      forall x. (A(x) --> exists y. B(x,y))
          --> exists e. forall x. (A(x) --> M_e(x) terminiert und B(x, M_e(x)))

  (Für "fast negative" Formeln A gilt: Es gibt eine Turingmaschine, die einen
  Realisierer für A findet, sofern es einen solchen gibt (ganz ohne Markovs
  Prinzip, diese Behauptung ist in HA beweisbar).)

  (Einer der Fälle des Beweises dieser Behauptung: Ang. (A --> A') hat einen
  Realisierer. Dann gibt es also e mit forall r. (r |- A ==> er! & er |- A').
  Eine solche Maschine e können wir aber auch selbst bauen: Lese ein r als
  Eingabe ein und setze voraus, dass r |- A. Dann hat ja A einen Realisierer.
  Also finden wir, da A' fast negativ ist, einen Realisierer für A'. Den nennen
  wir er.)

  (Hm, ich kann diese Behauptung doch ausdehnen auf "vee", oder: Seien e und e'
  Maschinen, die Realisierer von A bzw. A' finden. Lasse diese in verzahnter
  Art und Weise ablaufen, bis eine terminiert. Dann gib den entsprechenden
  Realisierer aus. Tja, gute Idee, aber funktioniert nicht: Das Verhalten von
  e und e' ist ja nicht spezifiziert, falls A bzw. A' keine Realisierer haben.
  Insbesondere könnten sie mit falschen Ergebnissen terminieren. Das kann ich
  auch nicht durch cleverere Konstruktion verhindern, zumindest nicht mit
  gewöhnlichen Maschinen im Vergleich zu ITTMs.)

  (Für jede Aussage A ist "r |- A" äquivalent (über HA) zu einer fast
  negativen. Behauptet Seite 245 von Oosten (Realizability: its categorical
  side). Müsste auch passen.)

  (Für jede fast negative Formeln A gilt: A <--> (exists r. r |- A).)
  top bottom = wedge vee implies forall exists
  (A --> B). Zeige: Gibt r mit: Ist x mit x |- A, so rx! mit rx |- B.
  (forall x. A(x)). Zeige: Gibt r mit: rx! mit rx |- A(x).

  (Mit MP gilt für alle fast negativen Formeln A: Genau dann A, wenn A^negneg.)

* Daraus folgt: HA |- (|== phi) genau dann, wenn HA + ECT_0 |- phi.

  Die Rückrichtung ist klar, denn HA |- (|== ECT_0).

* Das hängt wohl eng mit einer Form von Idempotenz zusammen:

      |== (phi --> (|== phi)).

* Siehe /Extensional realizability/ von Jaap van Oosten, Seite 2.
  https://www.sciencedirect.com/science/article/pii/S0168007296000504


=== Krivine-Realisierbarkeit

* Krivine-Realisierbarkeit interpretiert klassische Logik und sogar ZF.
  Ziel (von wem?): Das auf ZFC ausdehnen.

* Krivines Philosophie ist: Neue Programmierkonzepte sollten dadurch motiviert
  werden, dass sie wichtige Axiome realisieren.
  http://lama.univ-savoie.fr/~hyvernat/Realisabilite2011/Files/JohnLongley1.pdf#page=18

* A Guide to Krivine Realizability for Set Theory, https://arxiv.org/pdf/2307.13563


=== Referenz über viele Realisierbarkeitsarten

https://staff.fnwi.uva.nl/d.h.j.dejongh/teaching/il/real0new.pdf
Seite 19


=== Gleichmäßige Stetigkeit

In folgenden Topoi gilt, dass alle Funktionen vom Typ 2^N --> N gleichmäßig
stetig sind:

* Der Realisierbarkeitstopos zu Kleenes modifizierter Algebra.
  Zum Nachweis benötigt man aber ein Stückchen klassische Prinzipien in
  der Metatheorie.

* Der Topos der C-Räume von Chuangjie Xu (einem Schüler von Escardó):
  https://cj-xu.github.io/talks/xu-tlca2013.pdf
  https://cj-xu.github.io/talks/xu-kleene-kreisel.pdf


=== Stetigkeit ℝ → ℝ

Sei e eine Maschine, die eine Funktion f : ℝ → ℝ berechnet. Sei a eine Maschine,
die eine Zahl x : ℝ berechnet. Wir wollen zeigen, dass f in x stetig ist. Sei
dazu ε > 0 gegeben. Finde j mit 2^{-j} ≤ ε/2. Wir bauen folgende Maschine r:

    Lese eine Zahl n ein.

    Prüfe, ob e(r)(j) innerhalb von n Schritten anhält. Wenn nein, gib a(n) aus.
    Sei im Folgenden K die Anzahl Schritte, die die Berechnung e(r)(j) zum
    Halten brauchte.

    Prüfe, ob e(r)(j) kompatibel mit e(a)(j) ist, im Sinne von
    |e(r)(j) - e(a)(j)| ≤ 2^{-j} + 2^{-j}. Wenn nein, gib a(n) aus.

    Suche nun nach einer rationalen Zahl q mit |a(i) - q| ≤ 2^{-i} + 2^{-K}
    für alle i < K sodass |e(q) - e(a)| zertifiziert größer als ε ist
    (damit meine ich, dass ein l existiert mit x(l) - 2^{-l} - 2^{-l} > ε,
    wobei x(l) = |e(q)(l+1) - e(a)(l+1)|). (Die Suche ist dann also verzahnt
    über q und l.) Wenn eine solche Zahl gefunden wurde, gib diese aus.

Dann haben wir:

1. Es ist unmöglich, dass e(r)(j) nicht anhält. Denn wäre das so, so wäre r ≃ a
   und damit e(r)(j) terminierend mit Ergebnis e(a)(j).

2. Mit MP folgt, dass e(r)(j) anhält. Sei K die Anzahl Rechenschritte.

   Das Ergebnis muss dann auch kompatibel mit e(a)(j) sein, sonst wäre wieder
   r ≃ a und damit eben doch e(r)(j) = e(a)(j).

3. Sei nun q eine beliebige rationale Zahl mit |a(i) - q| ≤ 2^{-i} ...+ 2^{-K}...
   für alle i < K. Angenommen |e(q) - e(a)| > ε. Dann wird die Suche
   erfolgreich sein und eine gewisse rationale Zahl q' mit den gleichen
   Eigenschaften finden. Dann wird zwar nicht r ≃ q' gelten. Aber es wird
   gelten: r(i) = a(i) für i < K und r(i) = q' für i ≥ K. Definiert dies eine
   reelle Zahl, und zwar genauer die Zahl q'?

      |r(i) - r(i')| ≤ 2^{-i} + 2^{-i'}?
      falls i,i' < K:      ja nach Voraussetzung an a.
      falls i,i' ≥ K:      ja, da Differenz Null.
      falls i < K, i' ≥ K: ja, denn |a(i) - q'| ≤ 2^{-i} ≤ 2^{-i} + 2^{-i'}.
      falls i ≥ K, i' < K: ja, analog.

      |r(i) - q'| = 0 für i ≥ K und ≤ 2^{-i} für i < K.

   Somit muss e(r) eine reelle Zahl darstellen, und zwar dieselbe wie e(q').
   Insbesondere wird e(r)(j) kompatibel zu e(q')(j) sein. Auf der anderen Seite
   gilt aber |e(q') - e(a)| > ε, d.h. es gibt l mit |e(q')(l+1) - e(a)(l+1)| >
   ε + 2^{-l} + 2^{-l}. Widerspruch:

      |e(r)(l+1) - e(a)(l+1)| ≥ |e(a)(l+1) - e(q')(l+1)| - |e(q')(l+1) -
      e(r)(l+1)| > ε + 2^{-l} + 2^{-l} - 2^{-(l+1)} - 2^{-(l+1)} = ε + 2^{-l}.

      |e(r)(l+1) - e(a)(l+1)| ≤ |e(r)(l+1) - e(r)(j)| + |e(r)(j) - e(a)(l+1)| ≤
      2^{-j} + 2^{-(l+1)} + 2^{-(l+1)} + 2^{-j} = 2^{-l} + 2 2^{-j} ≤ ε +
      2^{-l}.

3. Sei nun y eine beliebige reelle Zahl mit |x - y| ≤ 2^{-K}.

   Dann finde eine rationale Zahl q...


=== Effektiver Topos

* Muss aus Asm(A) noch einen Tripos machen und daraus einen Topos.
  Dabei wird Gleichheit dann nicht mehr trivial realisiert.

* Die interne Sprache des effektiven Topos ist im Wesentlichen
  die Realisierbarkeitssemantik. Eine genaue Formulierung findet sich auf Seite 41
  von Jaap van Oostens Doktorarbeit (http://www.illc.uva.nl/Research/Publications/Dissertations/HDS-26-Jaap-van-Oosten.text.pdf).


=== Untertopoi des effektiven Topos

* Sei A <= N. Sei k_A der kleinste modale Operator im effektiven Topos,
  der Entscheidbarkeit von A erzwingt.

  Dann ist k_A <= k_B genau dann, wenn A Turing-reduzierbar zu B ist.

  https://webdpmms.maths.cam.ac.uk/~martin/Research/Oldpapers/hyland-effectivetopos.pdf,
  Seite 36.


=== Kleine vollständige Kategorien

* Der effektive Topos enthält eine kleine vollständige Kategorie:
  https://webdpmms.maths.cam.ac.uk/~martin/Research/Oldpapers/smallcomplete88.pdf


=== Berechenbarkeit von Lösungen von Differentialgleichungen

* Pour-el, Richards. A computable ordinary differential equation which
  possesses no computable solution.
  http://www.sciencedirect.com/science/article/pii/0003484379900214


=== 2-kategorielle Aspekte der Tripos-zur-Topos-Konstruktion

* https://www.lama.univ-savoie.fr/~hyvernat/Realisabilite2009/Files/Jonas_Frey.pdf
  https://arxiv.org/abs/1104.2776

* https://arxiv.org/abs/1401.7867


=== Ein Realisierbarkeitstopos über beweisbar haltende Turingmaschinen?

* Man könnte denken, dass es eine PCA gibt, in der wir definieren: e * n
  ist genau dann definiert, wenn e von der Form <r,p> ist, wobei p ein
  ZFC-Beweis ist, dass r eine stets terminierende Turingmaschine ist; in diesem
  Fall sei e * n = r(n).

* Aber den Kombinator S kann man nicht bauen. Der wäre in etwa so:

    Lese <f,p> ein.
    Prüfe, dass p ein Terminierungsbeweis von f ist. (Andernfalls halte.)
    Gib folgende TM (zusammen mit einem Terminierungsbeweis) aus:

        Lese <g,q> ein.
        Prüfe, dass q ein Terminierungsbeweis von g ist. (Andernfalls halte.)

        Gib folgende TM (zusammen mit ...) aus:

            Lese x ein.
            Berechne g(x).
            Berechne f(x).
            Berechne f(x)(g(x)).

                  Für den letzten Schritt brauche ich eine UTM!
                  Aber da ZFC ZFC-Beweisen misstraut, kann ich keinen
                  ZFC-Terminierungsbeweis der UTM angeben.


=== Mengen als Programme

* In https://www1.maths.leeds.ac.uk/~rathjen/ober.pdf gibt Rathjen
  eine Art Realisierbarkeitssemantik an, in der Realisierer aber nicht
  natürliche Zahlen, sondern beliebige Mengen sind.


=== Verallgemeinerung von ITTMs, die Wahrheit in V berechnen können

https://arxiv.org/pdf/1806.08747.pdf


=== Verschachtelter effektiver Topos

* Für jede Formel α von HA^ω (auf jeden Fall HA) gilt:

      Eff |== α   genau dann, wenn   Eff |== (Eff |== α).

  exists r. r |- α   gdw.  exists s. s |- exists r. α

  (Auch für HA^ω, falls ich die Aussage "e hält auf Eingabe n" als fast
  negative Aussage schreiben kann.)

* Es stimmt aber nicht, dass [[Eff]]_Eff = Eff ist. Das ist Seite 247 von
  Oosten. (Also auch nicht, dass Eff glaubt, dass Eff gleich Set ist.)

* Es gibt aber eine verwandte Konstruktion Eff'. Mit LEM gilt Eff = Eff'.
  Und [[Eff']]_Eff = Eff, wenn ich Seite 250 richtig lese. Also (weiterhin LEM
  in der Metatheorie angenommen) glaubt Eff', dass Eff' gleich Set ist.

* Wie man Eff und Set schnell auseinanderhalten kann (wenn man klassische Logik
  zur Verfügung hat):

  In Eff gibt es kein abzählbares Koprodukt von 1. Angenommen das gäbe es, K.
  Dann gäbe es 2^{aleph_0} viele Morphismen K → N. (Genauer: So viele, wie es
  Funktionen N → N gibt.) Aber es gibt nur abzählbar viele Morphismen von
  irgendeinem Objekt nach N hinein.


=== Mangelnde Quotienten in Asm, der Kategorie der Assemblies

* Oosten schreibt: Die Kategorie der Assemblies ist regulär, kartesisch
  abgeschlossen und besitzt endliche Kolimiten.

* Insbesondere gibt es Kodifferenzkerne von Äquivalenzrelationen.
  (Zu konstruieren wie man es erwarten würde.)

* Aber die Aussage "forall x,y. x ~ y ⇐ pi(x) = pi(y)" ist im Allgemeinen
  falsch. Okay im Allgemeinen nur, falls die Äquivalenzrelation ¬¬-stabil ist.


=== Zum Unterobjektklassifizierer im effektiven Topos

* Oosten Seite 131:

      forall p : Ω. exists A : P_¬¬(ℕ).
          (p ↔ (A bewohnt)).


=== Church-Numerale im effektiven Topos

https://nforum.ncatlab.org/discussion/8622/church-numerals-are-realizers/


=== Interne modest Mengen

* IM, die Kategorie der internal modest sets in Eff, ist eine interne Kategorie
  in Eff. Sie ist vollständig(!).

* Ergebnis: Jeder Funktor IM → IM hat einen Fixpunkt.

* Damit kann man etwa schnell ein Modell des untypisierten Lambdakalküls bauen,
  einfach Fixpunkt von D ⊢→ D^D finden.

Steht alles auf Seite 236 von /Elementary Categories, Elementary Toposes/
von Colin McLarty.


=== Gluing

* Wirklich mal Artin-Gluing verstehen. Das verarztet diese Slash-Relationen und
  so. Oostens Buch.


=== De Jong's Theorem

* HA ist konservativ über Prädikatenkalkül im Sinne von Seite 123 Oosten.


=== Kategorizität von HA

* Klar, Bennos Paper

* https://arxiv.org/pdf/2302.14699


=== Lambda-Kalkül als PCA

* Alle Lambda-Terme nehmen, bis auf α- und β-Äquivalenz (auch η?).
  Verknüpfung ist Juxtaposition und ist total.

* Nun die "stark normalisierenden" Lambda-Terme nehmen (bis auf α-Äquivalenz).
  Verknüpfung ist Normalform nach Juxtaposition und ist partiell.
  (Quelle: Buch von Oosten, "term models")


=== Doppelnegations-PCA?

Sei A eine PCA. Dann können wir folgende neue Verknüpfung definieren:

- e * x ↓ genau dann, wenn für alle totalen r gilt, dass e x r ↓.

- In diesem Fall sind alle e x r Ergebnisse von e * x.

Mit "total" meine ich dabei: Hält auf allen natürlichen Zahlen als Eingaben.

Ist A eine typisierte PCA, kann das sicher noch besser ausgedrückt werden.

Ist A mit der neuen Verknüpfung eine (nicht-deterministische) PCA? Die LEM
realisiert?


=== Quellen

* http://math.andrej.com/data/c2c.pdf
* http://www.mathematik.tu-darmstadt.de/~streicher/REAL/REAL.pdf
* http://math.andrej.com/wp-content/uploads/2014/03/real-world-realizability.pdf
* https://arxiv.org/abs/1401.7867
* http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/ von Wesley Phoa
  (sehr empfohlen von Michael O'Connor, Todd Trimble und Tom Leinster)
* https://webdpmms.maths.cam.ac.uk/~martin/Research/Oldpapers/hyland-effectivetopos.pdf

* https://www.cs.bham.ac.uk/~axj/ccc2021/abstracts/CCC_2021_paper_4.pdf
  Mathematik mit Irrtumswahrscheinlichkeit ε!

* https://pages.cpsc.ucalgary.ca/~robin/FMCS/FMCS_04/material/hofstra.pdf
  gut!