kategorielle-logik.txt

=== Quellen

* http://ljk.imag.fr/membres/Dominique.Duval/Slides/capp10.pdf
* A categorical semantics of quantum protocols: http://arxiv.org/abs/quant-ph/0402130

* Ein altes Paper:
  Michael Fourman, Continuous Truth I.

* http://www.dtc.ox.ac.uk/people/12/frot/CoherentTopoi.pdf
  Empfohlen von John Baez. Diskutiert den Zusammenhang zwischen Gödels
  Unvollständigkeitssatz und Delignes Theorem.

* http://www.cs.bham.ac.uk/~sjv/GeoAspects.pdf
  Ist eine schöne Einführung.

* https://ncatlab.org/toddtrimble/published/An+elementary+approach+to+elementary+topos+theory


=== Grafische Anschauung

* https://xorshammer.com/2016/07/24/the-cgp-grey-topos-of-continents/
  über die subendliche Garbe der Kontinente


=== Klassische Logik in kartesisch abgeschlossenen Kategorien

* Sei C eine kartesisch abgeschlossene Kategorie mit einem initialen Objekt 0.
  Falls 0^(0^A) isomorph zu A ist, für alle A [auch natürlich?], dann ist die
  Kategorie eine Quasiordnung. http://www.paultaylor.eu/stable/prot.pdf, Seite 151.


=== Bedeutung der Identität

"=" ist \exists längs der Diagonale. (Das kam eventuell in Jonas Freys Vortrag
im IHÉS vor.)


=== Zusammenhang zwischen [[.]] und |==

Siehe Shulmans Stack-Paper. Sei phi eine Aussage über einem Topos E mit einer
freien Variable x. Dann definiert die Kripke-Joyal-Interpretation von phi eine
Prägarbe auf E, nämlich

    A |--> { a : A --> X | A |== (a^* phi)[x/a] }.

Das ist eine Unterprägarbe von Hom(__, X). Diese nun wird dargestellt durch

    [[x:X. phi]].

NB: Diese Unterprägarbe ist sogar eine Garbe, also ein richtiges Unterobjekt in
Sh(E). Das klärt ein wenig die Bezeichnung "Stack-Semantik".


=== Schnitte von [[x:X. phi]] in einem Garbentopos Sh(Y)

Die U-Schnitte von [[x:X. phi]] gerade diejenigen U-Schnitte von X, die in der
Kripke-Joyal-Semantik die Aussage phi erfüllen. (Wende dazu den genannten
Zusammenhang auf A := Hom(__,U) an.)

* Die Formel "forall y. xy = 0 ==> x = 0" (d.h. "x ist regulär") ist nicht
  geometrisch. Trotzdem kann man einfach angeben, wie das Unterobjekt der
  regulären Elemente einer Ringgarbe R aussieht:

      Reg_R(U) = { x \in R(U) | U |== phi(x) }
               = { x \in R(U) | x regulär in allen R_p, p \in U }.

  Denn für festes x ist phi(x) eine geometrische Sequenz.


=== Schnitte von [[ { x:X | phi } ]] in einem Garbentopos Sh(Y)

Betrachte das Pullbackdiagramm

    [[ x:X. phi ]] --------> 1
         |                   |
         |                   |
         |                   |
         v                   v
         X --------------> Omega  (das ist, modulo Curryfizierung,
                 chi              die Interpretation [[ {x|phi} ]])

auf U-Schnitten; da Schnitte nehmen linksexakt ist, bleibt das ein
Pullbackdiagramm. Da aber Omega(U) nicht viel mit der externen Menge der
Wahrheitswerte zu tun hat, lässt sich chi_U nicht als klassifizierende
Abbildung einer Teilmenge von X(U) lesen.

Es gilt zumindest für alle s aus X(U): chi_U(s) = U <==> U |== phi[s/x].


=== Eindeutige Existenz impliziert externe Existenz

* Klar: Gelte E |== exists! x : X. phi(x). Dann gibt gibt es auch genau
  ein globales Element x von X mit E |== phi(x).

* Gelte E |== exists X. phi(X) und

      E |== forall X,Y. phi(X) wedge phi(Y) ==> exists! f : X --> Y. f Iso.

  Dann gibt es in E ein Objekt X mit E |== phi(X).

  Das ist mir zumindest im Fall, dass E ein Garbentopos ist klar. Denn die
  Eindeutigkeitsbedingung liefert Isomorphismen der eingeschränkten Garben, die
  die Kozykelbedingung erfüllen.

  Im allgemeinen Fall heißt das "descent theorem for Grothendieck toposes"
  (Moerdijk) und gilt für geometrische Morphismen F --> E, welche offen (oder
  laut
  http://mathoverflow.net/questions/233219/descent-of-higher-categorical-structures-along-geometric-morphisms
  eigentlich) und surjektiv sind. Ich vermute, dass (klassisch) jeder Topos
  über Set offen ist. Dann muss er nur noch surjektiv sein.


=== Interne Sprache von Scheibentopoi

* Auch konstruktiv gilt, dass folgende Aussagen äquivalent sind:

  1. forall x in X. phi(x)
  2. Set |== forall x in X. phi(x)
  3. X |== phi
  4. Set/X |== phi

* Seien M und N Objekte aus Set/X. Dann ist die Aussage

      "M und N sind in Set/X isomorph"

  stärker als

      "Set/X |== M und N sind isomorph".

  Letzteres bedeutet nämlich nur, dass alle Fasern isomorph sind.
  Mit dem Auswahlaxiom kann man diese Aussage freilich verbessern.

  Wie sonst bei Garbentopoi auch bedeutet die zweite Aussage halt nur, dass die
  Garben M und N lokal isomorph sind. Daraus folgt nicht unbedingt globale
  Isomorphie.


=== Geometrische Formeln und Konstruktionen

* Geometrische Formeln vertragen sich gut mit dem Zurückziehen längs
  geometrischer Morphismen:

      f^* [[phi]] = [[f^*(phi)]].

* Mittels Induktion über den Formelaufbau kann man leicht folgendes zeigen:
  Sei phi eine geometrische Formel über eine Teilmenge U. Sei x in U.
  Dann gilt:

      Set |== x^* phi   <==>   ex. x \in V \subseteq U: V |== phi.

  Falls phi auch "==>" oder "forall" enthält, gilt nur "<==" -- allerdings nur
  dann, wenn man noch die volle Induktionsvoraussetzung für alle Teilaussagen
  zur Verfügung hat. Wegen der Charakterisierung der Gültigkeit geometrischer
  Sequenzen ist die Rückrichtung aber sowieso trivial.

  Die Äquivalenz gilt auch, wenn Teilaussagen der Form "x \in A" für
  Teil"mengen" A \subseteq M vorkommen. Die muss man allerdings richtig
  verstehen: Nicht die Menge A als globales Element von [M, Omega] auffassen,
  sondern als Untergarbe von M. Wenn A selbst über eine geometrische Formel
  definiert wurde, kann man auch gut angeben, wie die zurückgezogene Untergarbe
  x^* A aussieht.

* Damit ist es leicht, zu zeigen, dass eine geometrische Sequenz genau
  dann auf einer offenen Teilmenge U gilt, wenn sie an allen Halmen gilt.

* Eine *Konstruktion* heißt geometrisch, wenn sie sich nur aus Dingen
  zusammensetzt, die unter solchen Rückzügen erhalten bleiben, insbesondere
  sind das Produkt und Koprodukt, aber auch Interpretationen von geometrischen
  Formeln (nicht Sequenzen!).

* Etwa ist R^x := { x:R | exists y:R. xy = 1 } eine geometrische Konstruktion,
  Reg(R) := { x:R | forall y:R. xy = 0 ==> y = 0 } aber nicht.

* Objekte natürlicher Zahlen und Listenobjekte kommutieren mit Rückzug.

* Auch die Konstruktion der Menge der Kuratowski-endlichen Teilmengen
  ist geometrisch. Eine Möglichkeit, das einzusehen, besteht darin, K(X)
  als Kodifferenzkern zu realisieren:

      R ===> List(X) ---> K(X),

  wobei R <= List(X) x List(X) die Teilmenge bestehend aus folgenden Paaren ist:

      { (xs,ys) | bigwedge_i bigvee_j (xs[i] = ys[j]) & umgekehrt }.

* "Idealerweiterung bilden" ist eine geometrische Konstruktion:

      J B = { b:B | bigvee_n exists b_1,...,b_n:B. exists j_1,...,j_n:J.
                        b = sum_i phi(j_i) b_i }.

* Die Konstruktion "freier R-Modul auf" kommutiert ebenfalls. Das ist NICHT
  klar, wenn man dazu die feinste Äquivalenzrelation mit ... verwendet,
  aber SCHON, wenn man ihn einfach als Koequalizer definiert:

      Rel ==> L(R x X) --> coeq,

  wobei Rel = { (v,w) | v,w sind mit einer elementaren Umformung miteinander
  verbunden }. Die beiden Morphismen aus Rel sind die beiden
  Projektionsmorphismen. Denn Koequalizer, Rel und L sind alle geometrisch.

* Auch die Konstruktion "Menge der (Kuratowski-)endlichen Teilmengen"
  ist geometrisch. Siehe http://www.cs.bham.ac.uk/~sjv/GLiCS.pdf, Seite 10.

* Auch die Konstruktion "Kählerdifferentiale" ist geometrisch.

* Rückzug von Örtlichkeiten funktioniert, ist aber nicht ganz trivial:
  Siehe Spitters/Vickers/Wolters, Gelfand spectra in Grothendieck toposes using
  geometric mathematics, http://arxiv.org/pdf/1310.0705.pdf.

* Die Hom-Konstruktion ist im Allgemeinen nicht geometrisch, aber schon, wenn
  der vordere Modul von endlicher Präsentation ist. Siehe meine Antwort auf
  StackExchange: http://math.stackexchange.com/questions/16203/why-doesnt-hom-commute-with-taking-stalks/645385#645385

* Die Aussage "der Ringhomo phi : A --> B ist eine Lokalisierung" ist eine
  geometrische Implikation, denn sie ist äquivalent zu "der kanonische Homo
  A[S^(-1)] --> B ist bijektiv (wobei S = phi^{-1}[B^x])" und das wiederum
  bedeutet ausgeschrieben:

      forall y : B. exists x, s : A. phi(s) invertierbar und phi(s) y = b.
          wedge
      forall x : A. phi(x) = 0 ==> exists s : A. phi(s) invertierbar und sx = 0.

* Für zwei endlich präsentierte Moduln/Algebren ist die Eigenschaft,
  zueinander isomorph zu sein, geometrisch.


=== Generischer Halm

Sei xi ein generischer Punkt eines topologischen Raums X. Das soll heißen, dass
der Abschluss von {xi} ganz X ist. Dann gilt: Jede nichtleere offene Teilmenge
enthält xi. Daher folgt für eine geometrische Formel phi über X:

    phi gilt am generischen Halm  <==>
    phi gilt auf einer dichten offenen Teilmenge von X.

In diesem Sinn ist zu einem lokal geringten Raum (X,O_X) die "Keim-Umgebung"
(pt,O_{X,x}) also nicht nur in einem geometrischen Sinn keimartig, sondern auch
in einem logischen.

Verallgemeinerung: Sei xi ein Punkt, sodass der Abschluss von {xi} eine Menge A
ist. Dann gilt: Jede nichtleere offene Teilmenge von A enthält xi. Somit gilt
für geometrische Formeln phi über X:

    phi gilt am Halm xi  <==>
    phi gilt auf einer offenen Menge, die xi enthält  <==>
    phi gilt auf einer dichten offenen Teilmenge von A
        (ziehe hier phi längs A ^--> X zurück und rede
        dann in der internen Sprache von Sh(A))


=== Sh_j(E) vs. Sh(E) mit j-Übersetzung

* Gelte für einen modalen Operator Box:

      (Box phi)^Box = Box(phi^Box).

  Dabei bezeichnet (__)^Box die Box-Übersetzung (nur auf Formeln, ohne Änderung
  der Objekte).

  Das ist erfüllt für folgende Operatoren:

  * Box = negneg.
  * Box = (__ --> alpha) --> alpha.
  * Box = alpha --> __.
  * Box = __ v alpha.

  Wenn diese Bedingung erfüllt ist, so fühlt sich Box unter die Box-Übersetzung
  wie die Identität an:

      (Box phi ==> phi)^Box

    = (Box phi)^Box ==> phi^Box

    = Box(phi^Box) ==> phi^Box, das ist stets richtig.

  Das ist wohl einer der Gründe, wieso man bei der Box-Übersetzung nicht die
  Objekte vergarbifizieren muss: Sie fühlen sich schon garbifiziert an!

* Im Allgemeinen ist der Vergissfunktor Sh_j(E) --> Sh(E) ja nur linksexakt.
  Was bringt die Ableitung dieses Funktors (etwa auf abelschen Gruppen)?
  Etwa im Fall Set_negneg --> Set?
  Wie sieht die aus?
  Was bringt das im Fall j = ((__ --> !x) --> !x)?

  Ein explizites Modell sieht so aus, über Ext^1(ZZ, __),
  wobei ZZ die konstante Garbe ZZ bezeichnet:

  Zu einer kurzen exakten Sequenz 0 --> X --> Y --> Z --> 0 in Sh_j(E)
  (also j-gibt es zu jedem z:Z ein Urbild) gehört die Sequenz

      0 --> X -f-> Y -g-> Z --> Ext^1(ZZ,X)

  in E, mit Ext^1(ZZ,X) = { [0 --> X --> ? --> ZZ --> 0 j-exakt] }.
  Die Dimensionsshiftabbildung sieht so aus:

      z |--> [0 --> X --> { (y,r) | g(y) = rz } --> ZZ --> 0].

  Diese Sequenz ist tatsächlich j-exakt.

* Welche Bedeutung hat es, mit (__)^j zu arbeiten, aber über Objekte
  von E zu sprechen? Klingt erstmal so, als ob man Garbensprache verwenden
  würde, um über Prägarben zu sprechen. Das wäre ja nicht sound.
  Aber vielleicht arbeitet man tatsächlich automatisch mit den assoziierten
  Garben.

* http://www.pps.univ-paris-diderot.fr/~mellies/mpri/mpri-ens/articles/hyland-effective-topos.pdf
  Evtl. ist meine j-Erkenntnis nicht neu.


=== Modale Logik

* Sei J intuitionistische Logik ergänzt um einen modalen Operator (der
  dieselben Axiome erfüllt wie eine Lawvere--Tierney-Topologie). Dann gilt:

      J |== phi  genau dann, wenn  E_j |== phi für alle Topoi E und LT j.

  Das steht in Goldblatt, Grothendieck Topology and Geometric Modality, Seite 164, (7.14).
  (Danke an Tadeusz Litak von PSSL 99.)


=== Bemerkungen, die konsolidiert werden müssen

* "Set |== x^* phi   <==>   ex. x \in V subseteq U: V |== phi."

  Das gilt nicht für das "große E", also unbeschränkte Quantifikation.
  Die Hinrichtung passt noch. Aber nicht die Rückrichtung.

  Es sei denn, man schränkt sich auf lokal konstante Garben ein.

  XXX: Weiß nicht mehr, was ich damit gemeint habe. Zum einen muss man sich
  sicher auf geometrische Formeln phi einschränken. Zum anderen passt es doch
  auf für das "große E": In der Hinrichtung kann man die konstante Garbe
  nehmen, in der Rückrichtung den Halm.

* "X |== forall A. (phi --> psi)  <==>  f.a. x \in X, Mengen A: phi_x --> psi_x."

  Das stimmt, für geometrische phi, psi.

* Sei X mit folgender Eigenschaft: Jede offene Teilmenge lässt sich durch
  kompakte offene Teilmengen überdecken. Das ist etwa für Schemata erfüllt!

  Sei phi eine solche Aussage, sodass für jede kompaktoffene Teilmenge U
  gilt: U cap [phi] ist wieder kompakt.

  Das ist etwa für phi = "f invertierbar" auf einem Schema erfüllt!

  Dann gilt folgendes logisches Prinzip:

      X |== (phi --> bigvee_i psi_i) --> bigvee_i (phi --> psi_i),

  wobei (psi_i) eine monotone Familie über eine gerichtete Indexmenge ist.


=== Sh(X) boolsch

* Sh(X) ist genau dann boolsch, wenn für jede offene Teilmenge U gilt:
  U ist die einzige offene dichte Teilmenge von U. (Damit meine ich mit
  "offen": "schwach offen", d.h. ist der Schnitt mit einer offenen Menge leer,
  so ist schon diese Menge leer.)

  Das ist genau dann der Fall, wenn für jede offene Teilmenge U
  eine offene Teilmenge V mit U cup V = X und U cap V = empty existiert.

  Das wiederum ist genau dann der Fall, wenn für jede offene Teilmenge U gilt,
  dass U cup int(U^c) = X.

  In klassischer Logik ist das genau dann der Fall, wenn jede offene Teilmenge
  abgeschlossen ist.

* Übrigens: Genau dann hat X die Eigenschaft, dass die einzige offene Teilmenge
  ganz X ist, wenn jeder offener Teilraum von X die hat.

  Die Rückrichtung ist klar. Für die Hinrichtung:

  Sei W ein offener Teilraum von X.

  Sei U dicht in W. Zeige, dass U = W.
  Betrachte dazu (int(W^c) cup U).
  Das könnte dicht in X liegen.
  Dann wäre (int(W^c) cup U) = X. Also U cap W = U = W. :-)

  Bleibt zu zeigen, dass (int(W^c) cup U) dicht in X liegt.
  Gelte (int(W^c) cup U) cap Z = empty.
  Dann int(W^c) cap Z = empty und U cap Z = empty.
  Da U cap (Z cap W) = empty, folgt Z cap W = empty.
  int(W^c) = bigcup { Q | Q cap W = empty } umfasst also Z.
  Also Z <= int(W^c). Also Z = empty. :-)

* Sei X ein T1-Raum, d.h. für je zwei verschiedene Punkte existiert eine
  offene Menge U, die den einen, aber nicht den anderen Punkt enthält.
  (Das ist äquivalent dazu, dass alle Punkte abgeschlossen sind. Schemata sind
  also im Allgemeinen nicht T1! Ein Spektrum eines Rings ist genau dann T1,
  wenn der Ring <=null-dimensional ist.)

  Dann gilt: Sh(X) ist boolsch <==> X ist diskret.

  "<==": Sei V in U offen, dicht. Sei x in U. Dann {x} \subseteq U offen,
  nichtleer. Also V cap {x} != {}. Also x in V.

  "==>": Sei x in X. Angenommen, {x} ist nicht offen.
  Setze U := bigcup { V | V offen mit x nicht in V } = int(X \ {x}).
  Dann ist U dicht in X: Sei W offen, nichtleer. Dann muss ein y in W
  existieren, das nicht gleich x ist. (Denn enthielte W nur x, so wäre {x}
  offen.) Nach T1-Voraussetzung existiert dann eine offene Menge V, die y aber
  nicht x enthält. Daher ist der Schnitt U cap W nicht leer: Er umfasst V cap W,
  und diese Menge enthält y.
  Somit ist U = X. Das ist ein Widerspruch.


=== Besondere Interpretationen

* Für eine Formel phi über X gilt genau dann, dass [[phi]] (nicht nur offen,
  sondern auch) abgeschlossen ist, wenn intern "phi oder neg phi".

  Die Hinrichtung ist klar: X = [[phi]] cup [[phi]]^c ist dann eine offene
  Überdeckung. Die Rückrichtung ist auch nicht schwer.

* Die Untergarbe [[ { x : 1 | phi } ]] der terminalen Garbe ist genau dann
  lokal konstant, wenn [[phi]] clopen ist, wenn also intern "phi oder neg phi"
  gilt.

  (Zeige als Lemma: [[ { x : 1 | phi } ]] ist genau dann konstant, wenn [[phi]]
  leer oder ganz X ist. Nutze, dass man Abgeschlossenheit lokal testen kann.)


=== Reelle Zahlen

* Dedekindsche reelle Zahlen: Garbe der stetigen reellwertigen Funktionen.

* Cauchy-Zahlen: Garbe der lokal konstanten reellwertigen Funktionen.
  (Wenn der zugrundeliegende Raum lokal zusammenhängend ist -- siehe Elephant
  D4.7.12.)

* ???: Garbe der differenzierbaren/glatten Funktionen.

* ???: Garbe der holomorphen Funktionen. Aus interner Sicht diskret!

* Mehr zu den glatten Funktionen:
  http://www.numdam.org/article/CTGDC_1975__16_3_217_0.pdf
  Fourman, Comparaison des reels d'un topos structures lisses sur un topos
  elementaire

  Mike: Die Garbe der glatten Funktionen lässt sich eher nicht intern
  charakterisieren. Da auf demselben topologischen Raum viele glatte Strukturen
  geben kann.
  https://nforum.ncatlab.org/discussion/6315/internal-definitions-of-cohesion/?Focus=50466#Comment_50466


=== Eigenschaften konstanter Garben

* Sei phi eine Formel, in der nur konstante Garben vorkommen. Dann gilt
  (konstruktiv!):

      U |== phi  genau dann, wenn  U <= sup { T | phi }.

  (Wenn das auch für solche Formeln gelten soll, in denen unendliche
  Konjunktion oder Allquantifikation über unendliche Mengen vorkommen, dann
  muss U overt sein. U könnte also zum Beispiel einfach die Örtlichkeit zu
  einem topologischen Raum sein.)

  Beweis durch Induktion; klar für top, bot. Für wedge wegen der
  in Rahmen geforderten Distributivität.

* Es gilt: U <= sup { T | phi }  <==>  U = sup { U | phi }.

* Ist die Örtlichkeit overt, so ist das ferner äquivalent zu:

      (U > 0  ==>  phi).

* Sei phi eine Formel, in der nur konstante Garben vorkommen, und sei psi
  eine beliebige Formel. Dann ist U |== (phi ==> psi) äquivalent zu:

      U = sup { U | phi }  ==>  U |== psi.

  Das kann man noch vereinfachen zu:

      phi  ==>  U |== psi.

  (Das heißt aber nicht, dass U = sup { U | phi } zu phi äquivalent ist!)

* Speziell im Rahmen der Radikalideale gilt:

      sqrt(f) = sup { sqrt(f) | phi }  <==>  f nilpotent oder phi.

* Sei phi eine Formel mit einem freien Parameter und in der nur Mengen
  vorkommen. Dann gilt:

      [| { x : XX | phi(x) } |] = konstante Garbe zu { x in X | phi(x) }.

  Dabei ist XX die konstante Garbe zur Menge X.

* Das heißt jetzt nicht, dass der Funktor "konstante Garbe bilden" stets
  beliebige Limiten bewahrt. Denn [| ... |] bewahrt nicht beliebige Limiten.
  Das bräuchte man aber, damit das aus der vorherigen Beobachtung folgen würde.


=== Lokal konstante Garben

Im effektiven Topos ist der Untertopos der Mengen gerade der Untertopos der
negneg-Garben. Ich wollte das für lokal konstante Garben nachbauen; das
funktioniert aber nicht:

* Angenommen, es existiert ein modaler Operator Box, sodass eine Garbe E
  auf X genau dann lokal konstant ist, wenn sie eine Box-Garbe ist.

* Dann folgt, dass eine Aussage phi genau dann Box-stabil ist, wenn
  ihre Interpretation clopen ist, wenn also phi oder neg phi.

* Wegen der Tautologie

      Box alpha  <==>  forall beta. (beta Box-stabil und alpha=>beta) ==> beta

  erhält man so einen Ausdruck für Box alpha. Vereinfachung zeigt aber, dass
  dann

      Box alpha  <==>  neg neg alpha

  gilt. Und bekanntlich gibt es Garben, die nicht lokal konstant, aber trotzdem
  negneg-Garben sind. (Beispiel?)

* Die ausgeschriebene Tautologie führt übrigens zu folgender Interpretation von Box:

  V |== Box W genau dann, wenn

      für alle offenen U <= V, beta <= U gilt:

          W cap U <= beta  und  beta <= U abgeschlossen  ==>  U <= beta.

Vermutlich war das ganze sowieso zum Scheitern verurteilt, denn Kerne von
Morphismen zwischen lokal konstanten Garben müssen nicht wieder lokal konstant
sein. (Beispiel?)

Ein Vorschlag, der zumindest auch für Garben der Form {x:1|phi} funktioniert,
ist

    "E lokal konstant  <==>  E diskret und (E bewohnt oder E nicht bewohnt)".

Aber auch hier stimmt die Rückrichtung nicht. Vielleicht klappt folgendes, aber
das ist nicht so schön:

    "E lokal konstant  <==>  bigwedge phi",

wobei das bigwedge über alle Aussagen phi läuft, die für klassische Mengen
erfüllt sind. (Wenn man das allgemein genug interpretiert, stimmt die
Äquivalenz trivialerweise: Wähle phi := "bigvee_{Mengen I} (E = \ul{I})".)

Mike erinnert in https://mathoverflow.net/a/277844/31233 daran, dass die
interne Sprache, wenn man nur ihr endliches Fragment betrachtet, keine Chance
haben kann, Konstanz zu erkennen. Denn das Konzept von Konstanz hängt vom
gewählten geometrischen Morphismus nach Set ab. Dabei kann man sich Set
aussuchen!


=== Konstruktion von modalen Operatoren

Unter welchen Voraussetzungen definiert die Setzung

  Box alpha := forall beta. (phi(beta) und alpha => beta) => beta

einen modalen Operator?

Hinreichend dafür ist, dass für phi gilt:

    phi(beta)  ==>  phi(delta => beta).


=== Kohärente Topoi

* Kohärente Topoi haben genügend Punkte. (Deligne)
* Big_et(X) ist kohärent, da definierbar als Topos über dem Situs Aff/X,
  Affine quasikompakt sind und daher Überdeckungssiebe endlich erzeugt sind.
  (Was heißt das genau?)
  http://mathoverflow.net/questions/145821/interaction-petit-topos-gros-topos


=== Interne Sprache eines klassifizierenden Topos

* Die interne Sprache von Set[T] ist lustig, denn die Stages, die man
  für die Kripke--Joyal-Semantik verwendet, sind einfach die Objekte der
  syntaktischen Kategorie zu T, also Formeln-in-Kontexten {vec x. phi}.
  Zu Beginn arbeitet man mit {x. top}, dem völlig generischen Modell, das sich
  noch in alle Richtungen entfalten kann. Durch Stagewechsel spezialisiert es
  sich dann.

* Hat sich auch Coquand gedacht: http://www.cse.chalmers.se/~coquand/site.pdf


=== Platonismus vs. Formalismus

Lambek, Scott. Reflections on a categorical foundations of mathematics.

Für eine Intuitionistin ist Platonismus wunderbar mit Formalismus vereinbar:
durch Arbeit im initialen (Elementar-)Topos. Denn:

* Eine Aussage besitzt genau dann einen intuitionistischen Beweis, wenn
  sie im initialen Topos gilt.

* Der initiale Topos befriedigt Platonistinnen, denn als ein initiales Objekt
  ist er eindeutig (in der Kategorie der Elementartopoi mit logischen
  Morphismen).

* Er befriedigt Formalistinnen, da er rein syntaktisch/linguistisch konstruiert
  werden kann.

Außerdem:

* Er befriedigt Logizistinnen, weil die interne Sprache des initialen Topos
  eine Form von Logik höherer Ordnung ist.

* Er befriedigt Konstruktivistinnen, da der initiale Topos die
  Disjunktionseigenschaft und die Existenzeigenschaft hat.

Dieser Standpunkt heißt wohl "constructive nominalism".

Nur Achtung: Der Beweis, dass der initiale Topos wirklich ein Modell mit den
gewünschten Eigenschaften ist, setzt die metamathematische Annahme, dass es
eine geeignete Kategorie von Mengen gibt. (Letzter Satz des Artikels)

Siehe auch: http://www.math.mcgill.ca/barr/lambek/pdffiles/WorldMath.pdf

Marc: Der initiale Topos sollte der Topos der Garben über dem Situs der Topoi
sein. Stimmt das?

* Lambek und Scott sprechen auch über T(L_1)/LEM. Dieser Topos ist initial
  in der Kategorie der boolschen Elementartopoi mit logischen Morphismen. Wegen
  Gödels Unvollständigkeitssatz wissen wir aber, dass er kein lokaler Topos
  ist.


=== Kommutative Theorien

http://www.wra1th.plus.com/gcw/rants/math/MathPhant.html

Suppose we have two operations huey and dewey in an algebraic theory. We say
that they commute if for any rectangular array of elements, with rows the right
size for huey and columns the right size for dewey, the application of huey to
each row and dewey to the resulting column yields the same as applying dewey to
each column and then huey to the resulting row. This can be expressed in a way
that makes no mention of elements. An algebraic theory is commutative if any
pair of its operations commute. This generalizes the notion of a commutative
ring.

Commutative algebraic theories have very nice properties. Every operation is a
homomorphism. So the set of homorphisms from one model to another has a
canonical structure as a model itself. This makes the category of models
closed. Furthermore, the resulting internal Hom functor has a left adjoint
which generalizes the tensor-product construction for modules. A free model on
one generator is a unit for this tensor-product.

Beispiele:

* Theorie der R-Moduln, wobei R ein kommutativer Ring ist
* Theorie von F_1
* Theorie der vollständigen Verbände (mit Suprema bewahrenden Morphismen)
* Theorie, die für jedes n-Tupel von nichtnegativen reellen Zahlen mit Summe 1
  eine n-stellige Operation haben. Modelle sind unter anderem konvexe Mengen in
  euklidischen Räumen.


=== Gleichheit von Beweisen

Von Peter Arndt empfohlen: Lambek.


=== Adjunktive Behandlung von Existenz- und Allquantifikation

* Klar: exists -| Pullback -| forall.

* Im Kontext von Teilmengen und einer Abbildung f : X --> Y:

      exists_f : (M <= X) |--> f[M] = { y | exists x. y = f(x) und x in M }

          ist linksadjungiert zu

      f^{-1} : (N <= Y) |--> f^{-1}[N] = { x | f(x) in N }

          ist linksadjungiert zu

      forall_f : (M <= X) |--> { y | forall x. y = f(x) ==> x in M } =
                               { y | f^{-1}[y] <= M }

* Beispiel: forall_f(Menge der regulären Punkte) = Menge der regulären Werte.

* Wieso gibt es bei der Produkt-/Hom-Adjunktion keinen dritten beteiligten
  Funktor, hier aber schon? Das wird in /A bifibrational reconstruction of
  Lawvere’s presheaf hyperdoctrine/ von Paul-André Melliès und Noam Zeilberger
  aufgelöst.

  Mike formuliert es so: (A x __) und (__)^A sind Kompositionen von
  adjungierten Funktoren:

      (A x __) = p_! . p^{-1}
      (__)^A   = p_* . p^{-1}

  https://nforum.ncatlab.org/discussion/7026/focusing/?Focus=56775#Comment_56775


=== Produkt von Topoi

Sei E = Set[T] der klassifizierende Topos einer geometrischen Theorie T.
Dann erscheint es mir plausibel, dass E x E der klassifizierende Topos der
Theorie T + T ist, und außerdem dass aus E-Sicht E x E der klassifizierende
Topos von T ist.


=== Nächste Schritte

* Für den Rückzug mit f^* statt f^(-1) auf Spec k(x)
  geeignete Transferprinzipien herleiten.

* Halm vs. kleine Umgebung kategoriell verstehen.

* Assoziierte Punkte?

* Wie konstruiert man eigentlich den freien Topos?

* https://arxiv.org/abs/1603.03374 Über Missverständnisse von Barrs Theorem