konstruktive-mathematik.txt

* Effektive Homotopietheorie:
  http://arxiv.org/pdf/1105.6257v3.pdf

* Berechenbare Mathematik = Realisierbarkeitsinterpretation konstruktiver Mathematik
  http://math.andrej.com/data/c2c.pdf

* Mal lesen: https://arxiv.org/pdf/1511.01113.pdf
  "Unreliability of the logical principles"


=== Lustige Situation in Ringen

Sei R ein Ring und seien a,b,c Ringelemente. Gelte a,b,c != 0.
Gelte ferner abc = 0.

Dann ist klar: R kann kein Integritätsbereich sein. Aber Nullteiler kann man
auch nicht explizit angeben:

* Sollte ab  = 0 sein, so ist (a,b)  ein Nullteiler.
* Sollte ab != 0 sein, so ist (ab,c) ein Nullteiler.

Welcher Fall vorliegt, kann man aber nicht entscheiden.


=== Faktorisierung ist schwer

* Sei E(n) eine entscheidbare Aussage. Wenn wir über Q(α₀, α₁, ...) mit
  α_n² = (if E(n) then p_n else -1) die Reduzibilität des Polynom X² + 1
  entscheiden können, können wir auch ∃n.E(n) entscheiden.

  (Hab ich aus Thierrys Vortrag am 12.4.2021 gelernt, Sheaf models and
  constructive mathematics.)


=== Ein Lemma über viele Aussagen

Seien Aussagen phi_ij mit i = 1, ..., n und j = 1, ..., m_i gegeben;
dabei n >= 1 und alle m_i >= 1.

Gelte: forall j_1. ... forall j_n. exists i. phi_{i, j_i}.

Dann: exists i. alle phi_{i, *} gelten.

Beweis durch Induktion über n; Induktionsanfang n = 1 klar. Der
Induktionsschritt n --> n + 1 geht so: Definiere Aussagen

    psi_ij := (phi_ij  oder  alle phi_{n+1, *} gelten)
        für i = 1, ..., n.

Diese Aussagen erfüllen die Voraussetzung:

    Seien j_1, ..., j_n beliebig. Nach Voraussetzung an die phi_ij
    erhalte dann für jeden Index j_{n+1} = 1, ..., m_{n+1} einen Index i
    mit phi_{i, j_i}. Falls dieser Index i immer n + 1 sein sollte, dann habe
    psi_{1, j_1}. Falls er auch nur einmal <= n sein sollte, dann habe psi_{i, j_i}.

Nach Induktionsvoraussetzung gibt es also ein i <= n sodass alle psi_{i, *}
gelten. Bin damit fertig.

Coquand beobachtete: Das ist einfach das Distributivgesetz!


=== Epimorphismen in der Kategorie der Gruppen

* https://golem.ph.utexas.edu/category/2015/08/wrangling_generators_for_subob.html#c049544
* http://ncatlab.org/nlab/show/epimorphisms+of+groups+are+surjective


=== Kompaktifizierung der natürlichen Zahlen

N* := { (x_n)_n | x_n in {0,1}, (x_n) monoton steigend }.

* N* ist die *finale Koalgebra* zum Funktor 1 + (__).

  Die Koalgebrenstruktur wird gegeben durch

      (x_n) |--> falls x_0 = 1: *, sonst: (x_(n+1)).

* Unendlich wird dargestellt durch

      (0,0,0,...),

  natürliche Zahlen durch

      (0,...,0, 1,...).

* Die Ordnung eines Elements in einem diskreten Monoid ist in natürlicher
  Weise ein Element dieser vervollständigten natürlichen Zahlen.

* Konsequenterweise ist auch die Charakteristik eines diskreten Rings
  eine solche Zahl.


=== Kohomologie

* http://homotopytypetheory.org/2013/07/24/cohomology/
  Andreas Blass (_Cohomology detects failures of the axiom of choice_)
  http://mathoverflow.net/questions/12119/reverse-mathematics-of-cohomology

* Bishop. Mathematics as a numerical language: H^1(S^1) = Z ist konstruktiv
  wohl eher nicht zeigbar.
  https://www.sciencedirect.com/science/article/pii/S0049237X08707407


=== Konstruktive reverse Mathematik

Tolle Übersicht im Fall von BISH (mit abhängiger Auswahl):
http://www.kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/1381-10.pdf


=== Eindeutigkeit impliziert Existenz

* Wenn eine Funktion näherungsweise Nullstellen hat (forall eps. exists x.
  |f(x)| < eps) und gleichförmig höchstens eine Nullstelle hat, so hat sie
  wirklich eine.

  Peter Schuster. Problems, Solutions, and Completions.
  http://www.sciencedirect.com/science/article/pii/S1567832609000137

* Es stimmt nicht: Wenn eine Menge höchstens ein Element enthält
  und nicht nicht ein Element enthält, dann enthält sie ein Element.

* Anders sieht es aus, wenn wir nicht mit "nicht nicht" die Aussage
  abschwächen, sondern mit der propositionalen Abschneidung ("merely",
  "anonymously")! Siehe Seite 2 von https://arxiv.org/pdf/1610.03346.pdf:

      On the other hand, should A have only one inhabitant up to the internal
      equality, this inhabitant can be constructed from an inhabitant of ||A||.
      This is a crucial difference between propositional truncation and double
      negation.

* Dann gibt es natürlich noch: Eindeutige lokale Existenz impliziert
  (eindeutige) globale Existenz.


=== Nullstellensatz konstruktiv

* Es geht um folgende Behauptung: Sei k ein algebraisch abgeschlossener
  geometrischer Körper. Seien f_1, ..., f_m Polynome über k. Dann besitzen die
  f_j eine gemeinsame Nullstelle oder 1 in (f_1, ..., f_m).

  Ich glaube, dass man diesen Satz wie folgt konstruktiv zeigen kann.
  Zunächst zeigt Theorem VII.1.8 (Seite 386) von Lombardi/Quitté, dass
  1 in (f_1, ..., f_m) oder dass es eine gemeinsame Nullstelle in einer
  reduzierten endlichen k-Algebra A mit 1 != 0 gibt.

  Da k ein algebraisch abgeschlossener geometrischer Körper ist, ist k
  auch fppf-lokal. Trivialerweise ist A flach über k. Ich denke, man kann auch
  zeigen, dass A treuflach über k ist. Somit liftet die Nullstelle in A zu
  einer in k.

  Allerdings nutzt das jetzt aus, dass k in einem starken Sinn fppf-lokal ist.
  Klassisch auf jeden Fall okay. Konstruktiv weiß ich's nicht.

* Theorem VII.1.9 nutzt Gröbnerbasen. Braucht man dann nicht sowas wie LPO
  oder Markov oder das abhängige Auswahlaxiom? Lombardi/Quitté haben keine
  Angst vor ihm!

* Jedenfalls muss es einen konstruktiven Beweis geben. Weil die Behauptung
  eine geometrische Implikation ist.


=== Type-2 Theory of Effectivity

* Ziegler, Brattka: A computable spectral theorem.
  https://pdfs.semanticscholar.org/a669/d482836f92827fd98d4c266489b54b9f0183.pdf

  Hier wird wiederholt, welche Operationen aus der linearen Algebra alle
  berechenbar (oder zumindest von unten oder oben approximierbar) sind:
  Kern, Spann, ...

* Die stetige Familie exp(-1/eps^2) [cos(2/eps), sin(2/eps); sin(2/eps), -cos(2/eps)]
  von reellen symmetrischen Matrizen (mit der Nullmatrix im Fall eps = 0)
  zeigt, dass die Berechnung von Eigenbasen nicht stetig ist.

  Für eps != 0 erhält man nämlich die Basen

      (cos(1/eps), sin(1/eps)), (sin(1/eps), -cos(1/eps))

  (bis auf Reihenfolge und Orientierung).

  Das Beispiel stammt von Rellich. Siehe Proposition 12 in Ziegler/Brattka für
  Details.

* Weihrauch, Computable Analysis.


=== Reelle Zahlen

* Was ich im Softwareprojekt gemacht habe, steht teilweise auch in (aber mit
  Cauchyfolgen statt Cauchyprozessen): Real Numbers, Generalizations of the
  Reals, and Theories of Continua herausgegeben von P. Ehrlich

* In Garbentopoi über lokal zusammenhängenden topologischen Räumen gilt
  (in klassischer Metalogik):

      Es gibt keine Surjektion NN --> RR.
      Es gibt keine Surjektion NN --> C.

  Dabei meint RR die Garbe der lokal konstanten reellwertigen Funktionen
  und C die Garbe der stetigen reellwertigen Funktionen. (Diese sind aus
  interner Sicht einfach die Mengen der Cauchy- bzw. Dedekind-Zahlen.)

  Sogar über beliebigen Garbentopoi über topologischen Räumen gilt, dass es
  keine Surjektion NN --> RR gibt (betrachte Halme!).

* Ich kann glaub ich zeigen, dass die Aussage "Es gibt eine Surjektion NN ->
  R_Cauchy" in Topoi von Garben über Örtlichkeiten, die mindestens einen Punkt
  besitzen, nicht stimmt.

* Jeder Grothendiecktopos besitzt einen zusammenhängenden und lokal
  zusammenhängenden geometrischen Morphismus aus einem Topos von Garben über
  einer Örtlichkeit. Wenn daher f : NN --> R_Cauchy ein Epimorphismus in E ist,
  so gibt es einen solchen Epi auch in einem lokalischen Topos. Es folgt, dass
  dieser keine Punkte hat. Aber ich glaube leider, dass das nicht einmal etwas
  über das Fehlen von Punkten von E aussagt.

* Für jeden Rampenparameter eps > 0 können wir eine Intervallschachtelung
  definieren, bei der wir in jedem Schritt versuchen, als nächstes diejenige
  Zahl auszuschließen, die als erstes in dem momentanen offenen Intervall
  liegt. Dies wird im Allgemeinen nicht gelingen.

  Wenn wie darüber diagonalisieren, also als n-tes Intervall das n-te Intervall
  zum Rampenparameter 1/n nehmen, so entsteht keine Schachtelung. Daher ist
  Konvergenz (etwa der linken Ränder) völlig unklar. Aber zumindest können wir
  zeigen, dass keine Konvergenz vorliegt. Und dass für jedes eps > 0
  nicht nicht eine Schranke N existiert, sodass die linken Ränder ab N
  sich alle um höchstens eps unterscheiden.

* Eine schnelle Möglichkeit, eine Form von Überabzählbarkeit der
  MacNeille-Zahlen einzusehen: Habe für die eine Injektion P(N) --> R, indem
  eine Menge X auf sup { sum_{n in A} 2^(-n) | A <= X endlich } geschickt wird.
  Komponiert mit einer angeblichen Injektion R --> N haben wir damit eine
  Injektion P(N) --> N. Oder anders: Eine angebliche Surjektion N --> R
  liefert eine Injektion P(R) --> P(N) --> R.


=== Noetherianität

* Coquand und Lombardi (Foliensatz /Krull's Principal Ideal Theorem/)
  definieren die Noetherianität eines Rings wie folgt.
  http://www.mittag-leffler.se/sites/default/files/IML-0001-30.pdf

  Bedeute G(x_0,...,x_{n-1}), dass ein i < n mit x_i in (x_0,...,x_{i-1})
  existiert. G() ist falsch.

  Ein Ring ist genau dann noethersch, wenn für jedes Prädikat P über endliche
  Folgen von Ringelementen mit

      1. G(sigma) ==> P(sigma)
      2. P(sigma) ==> P(sigma,x)
      3. (forall x. P(sigma,x)) ==> P(sigma)

  gilt: P(sigma) für alle sigma.

  (Das ist äquivalent dazu, dass G | [], wobei P | σ der induktiv erzeugte Typ
  mit den Konstruktoren Here : P(σ) → P|σ und Later : ((x) → P|σ,x) → P|σ
  ist. Für die Hinrichtung betrachte das Prädikat P gegeben durch P(σ) ≡ (G|σ).
  Für die Rückrichtung Induktion.)

* Wenn (x_1,...,x_n) = (1), so gilt P(x_1,...,x_n) für solch ein Prädikat.

* G(x_1,...,x_n) bedeutet, dass (x_1) <= (x_1,x_2) <= ... <= (x_1,...,x_n)
  *keine* echt aufsteigende Kette von Idealen ist.

* In diesem Sinn ist Z noethersch. Es genügt, P(x) für alle x in Z
  nachzuweisen. Der Fall P(0) ist klar, da G(0). Sei N die Gesamtzahl
  Primfaktoren (mit Vielfachheiten gezählt) in x. Dann gilt für alle
  k <= N und alle a_1,...,a_k: G(x,a_1,...,a_k) oder (x,a_1,...,a_k) = (1).
  Somit folgt P(x).

* Angeblich ist mit dieser Definition R[X] noethersch, falls R noethersch ist.

* Oft definiert man P(sigma) als (G(sigma) vee phi).

* In klassischer Logik kann man wie folgt einsehen, dass CL-Noetherianität
  dasselbe wie die übliche Bedingung ist.

  "==>": Definiere P(a_0,...,a_{n-1}) als "jede aufsteigende Kette von endlich
  erzeugten Idealen, die mit (a_0) <= (a_0,a_1) <= ... <= (a_0,...,a_{n-1})
  beginnt, hält".

  "<==": Wenn P() nicht gilt, kann man sukzessive eine Folge (a_0,...)
  konstruieren, sodass für kein n P(a_0,...,a_{n-1}) gilt. Aber irgendwann ist
  G(a_0,...,a_{n-1}) erfüllt.

* Die CL-Bedingung impliziert meine Prozessbedingung -- allerdings nicht für
  Prozesse, die Ideale ausgeben, sondern für Prozesse, die Folgen von
  Ringelementen ausgeben. Wobei die Folge im nächsten Schritt immer eine um
  genau ein Element ergänzte Folge sein muss.

  Definiere dafür P(a_0,...,a_{n-1}) als "jeder Prozess in diesem Sinn,
  für den es einen initialen Ablauf der Form () <= (a_0) <= ... <=
  (a_0,...,a_{n-1}) gibt, hält".

  Man kann die CL-Bedingung auch abändern, sodass die sigma's nicht mehr Folgen
  von Elementen, sondern Folgen von endlich erzeugten Idealen sind. Das
  Prädikat G definiert man dann als

      G(I_0,...,I_{n-1}) :<==> exists i < n. I_0 + ... + I_{i-1} = I_0 + ... + I_i.

  Die veränderte CL-Bedingung impliziert meine Prozessbedingung in ihrer
  unveränderten Form.

  Man kann die CL-Bedingung auch durch eine negative Variante ersetzen:

      1. Q(sigma) ==> neg G(sigma)
      2. Q(sigma a) ==> Q(sigma)
      3. Q(sigma) ==> exists a. Q(sigma a)

      Ring noethersch genau dann, wenn für all solchen Prädikat gilt: neg Q().

  Ein Ring, der diese Bedingung erfüllt, hat dann die Eigenschaft, dass kein
  Prozess nicht hält. (Definiere Q(sigma) :<=> "es gibt einen Prozess, für den
  ein Anfangsablauf wie von sigma vorgeschrieben existiert, der nicht hält".)
  (Bis auf Ideal/Element-Unterschied.)

* Es gibt auch die Noether-Bedingung von Richman und Seidenberg:
  aufsteigende Folgen von endlich erzeugten Idealen stoppen.

  Hervé Perdry schreibt in /Strongly Noetherian rings and constructive ideal
  theory/: Ist R kohärent und RS-noethersch, so ist auch R[X] kohärent und
  RS-noethersch. Außerdem hat R[X] herauslösbare Ideale, falls R sie hat.

* Meine alte Definition von "processly Noetherian" war Quatsch. Zur Erinnerung:
  Ein Prozess in einer partiell geordneten Menge X war eine Funktion f : N --> P(X)
  sodass f(0) bewohnt ist und sodass für alle n und x aus f(n) ein y aus f(n+1)
  mit x <= y existiert. So ein Prozess heißt haltend, wenn es ein n und ein x
  gibt, sodass x in f(n) und in f(n+1) liegt.

  Das Problem dabei ist, dass die Zugehörigkeit von x zu f(n) und f(n+1) nicht
  ausdrückt, dass x ist ein möglicher Fixpunkt des f zugrundeliegenden
  (gedachten) iterativen Entstehungsprozesses ist.

* Richman spricht ja in http://math.fau.edu/richman/Docs/new-acc.pdf über die
  ascending tree condition. Die ist super! Und identisch mit der Bedingung, die
  ich eigentlich im Sinn hatte. Nämlich:

  Ein Prozess in X ist ein Tupel (x0, phi) mit x0 in X und phi : X --> P(X).
  Dabei muss phi erfüllen:

      0. Für alle y aus phi(x) ist x <= y.
      1. phi(x0) ist bewohnt.
      2. Für alle x1 aus phi(x0) ist phi(x1) bewohnt.
      3. Für alle x1 aus phi(x0) und x2 aus phi(x1) ist phi(x2) bewohnt.
      4. Und so weiter.

  Dabei könnte oder sollte man 0. so abschwächen, dass es nur noch über die
  von x0 aus erreichbaren Ergebnisse spricht.

  Ein solcher Prozess hält, wenn es eine Abfolge x1, x2, ..., xn mit

      x_(i+1) in f(x_i) für i = 0, ..., n-1  und  x_n in f(x_n)

  gibt.

  Die Äquivalenz zu Richmans Definition sieht wie folgt aus.

  Sei (x0, phi) ein Prozess. Betrachte die durch Erweiterung geordnete
  Partialordnung aller endlichen Abläufe dieses Prozesses. Diese Partialordnung
  ist ein Baum. Definiere eine Familie J auf diesem Baum durch J_[x0,...,xn] := xn.
  Nach Voraussetzung hält J. Also gibt es [x0,...,xn] < [y0,...,ym] mit xn = ym.
  Nach Definition der Ordnung ist [y0,...,ym] = [x0,...,xn,x_(n+1),...,x_m].
  Also xn = x_(n+1).

  Sei J ein auf einem Baum I definierte Familie. Definiere den Prozess
  (bot in I, phi) mit

      phi(x) := { y | exists i < j: x = J_i, y = J_j }.

  Der so definierte Prozess hält. Also gibt es i < j mit J_i = J_j. Also hält J.

* Die alte komische Prozessbedingung wird von der neuen guten impliziert.
  Aber umgekehrt nicht. Komisches Halten aller komischen Prozesse impliziert
  nicht richtiges Halten aller richtigen Prozesse.

* Man könnte sich bei Richmans und der neuen Prozessdefinition fragen:
  Ist es nicht komisch, dass man nur fordert, dass *irgendein* Ablauf hält?
  Sollte man das nicht für Abläufe tun?

  Tatsächlich aber halten auch alle Abläufe. Schließlich ist ein Teilbaum eines
  Baums wieder ein Baum, der ebenfalls halten muss.

  Bisschen komisch ist es trotzdem.

* Wie sieht's im Computer aus? Soll ein Zeuge der Noetherianität alle möglichen
  Abläufe eines Algorithmus durchgehen? Natürlich nicht. Er beschränkt sich auf
  irgendeinen. Dieser muss ja ebenfalls halten. Hat wohl damit etwas zu tun,
  dass "im Computer das abhängige Auswahlaxiom gilt".

* Ist X ein lokal noethersches Schema, so ist O_X kohärent. Denn:

  1. Klassisch folgt aus Noetherianität Kohärenz.
  2. Ist M kohärent, so auch M~.

  Als Korollar hat man auf lokal noetherschen Schemata: Endlich erzeugte
  Untermoduln von O_X sind schon quasikohärent. Denn da O_X kohärent ist, sind
  endlich erzeugte Untermoduln von O_X schon endlich präsentiert. Und endlich
  präsentierte Moduln sind quasikohärent. (Hier geht der einfache Fakt ein,
  dass endlich erzeugte Untermoduln von kohärenten Moduln kohärent sind.)

  Dieses Korollar gilt auch völlig allgemein. Ein endlich erzeugter Untermodul
  von O_X ist das Bild eines Morphismus der Form O_X^n --> O_X.

* "Witzig": O_X erfüllt genau dann eine "schlechte Noetherianitätsbedingung",
  wenn es eine "gute Noetherianitätsbedingung" erfüllt. Denn man hat Äquivalenz
  zur klassischen Welt und dort sind alle Bedingungen gleich.

  Intern hat man auch: Ist O_X noethersch, so ist O_X kohärent. Obwohl diese
  Folgerung konstruktiv nicht zulässig ist.

  Was gilt in einer konstruktiven Meta-Theorie? Vielleicht sowas: Ist A
  kohärent und noethersch so ist O_{Spec A} kohärent und noethersch. Wobei der
  Verzicht auf Kohärenz jeweils nicht möglich ist.

* Noethersche Mengen:
  https://hal.inria.fr/inria-00503917/file/Coquand_Spiwack_-_2010_-_Constructively_Finite.pdf

  Noethersche Mengen sind stets streamless; die Umkehrung gilt nicht:
  https://cs.ioc.ee/~tarmo/tsem11/bezem2012-slides.pdf

* A~ in Spec(A) ist genau dann ind-noethersch (Good | [], wobei sich Good auf
  endliche Listen endlich erzeugter Ideale bezieht), wenn A lokind-noethersch
  ist. Dabei kommt als ein weiterer Konstruktor Local dazu, wenn auf einer
  Überdeckung jeweils P||σ gilt, so auch direkt P||σ.

  Es gilt: Good || σ gdw. Good_loc || σ gdw. Good_loc | σ, wobei Good_loc(σ)
  bedeutet, dass es eine Zerlegung der Eins gibt, sodass σ jeweils
  weglokalisiert stockt.

  Good || σ ⇒ Good_loc || σ: trivial, da nur Abschwächung.
  Good || σ ⇐ Good_loc || σ: zum Schluss extra Anwendung von Local.
  Good_loc || σ ⇒ Good_loc | σ: Da Good_loc lokal ist.
  Good_loc || σ ⇐ Good_loc | σ: trivial.

* Warnung: ind-noethersch zu sein ist keine geometrische Formel wegen der
  unendlichen Verzweigung. Verhält sich in Teilen dennoch so ähnlich (in
  klassischer Metatheorie intern wahr genau dann wenn halmweise wahr).

* https://www.andrew.cmu.edu/user/avigad/Students/hertz.pdf:
  Dialectica-Interpretation von Dickson und Basissatz

* Noethersche Mengen: coole Anwendung von Thierry und Vincent Siles
  für reguläre Sprache und reguläre Ausdrücke (regexps),
  https://link.springer.com/chapter/10.1007/978-3-642-25379-9_11

* Siehe auch: https://www.cse.chalmers.se/~coquand/base.ps

  Die induktive Noether-Definition wird reflektiert von positiven ouverten
  Räumen (und vermutlich auch von positiven ouverten Grothendieck-Topoi).


=== Dickson & Co

* Wenn jede Folge spezifierte guten Paaren hat, ist es ganz leicht, die
  Existenz von guten Tripeln zu zeigen. Betrachte einfach die Unterfolge der
  hinteren Komponenten guter Paare.


=== Analysis

http://www.phil.pku.edu.cn/cllc/people/fengye/finitismAndTheLogicOfMathematicalApplications.pdf

Hochgelobt von David Roberts auf MO.


=== Generische Freiheit

* Generische Freiheit für Moduln:

  Let R be a reduced ring. Let A be a finitely generated R-module. Assume
  that the only f in R such that A[f^(−1)] is a finitely free R[f^(−1)]-module
  is f = 0. Then R = 0.

  http://mathoverflow.net/questions/250040/constructive-proof-that-a-kernel-consists-of-nilpotent-elements

* Und für Algebren:

  Lemma 1: Sei R ein Ring. Sei M ein R-Modul mit Erzeugendensystem
  (x_i)_{i in I}. Sei I total geordnet. Gelte für alle g in R:
  Ist in M[g^{-1}] einer der Erzeuger R[g^{-1}]-Linearkombination von
  anderen Erzeugern mit kleinerem Index, so ist g = 0. Dann ist M frei mit
  (x_i)_i als Basis.

  Beweis: Sukzessive von höheren zu niedrigeren Indizes den Beweis von
  Lemma 1 in der MO-Antwort anwenden.

  Lemma 2:
      Sei R ein reduzierter Ring. Sei S eine R-Algebra von endlichem Typ.
      Sei M ein endlich erzeugter S-Modul.

      Gelte für alle f aus R: Sollte M[f^{-1}] (nicht notwendigerweise
      endlich) frei über R[f^{-1}] sein, so ist f = 0.

      Dann ist R = 0.

  Beweis: Sei S als R-Algebra durch x_1, ..., x_m erzeugt. Sei M als S-Modul
  durch v_1, ..., v_l erzeugt. Dann ist das System aller Vektoren der Form
  x_1^{i_1} ... x_m^{i_m} v_j ein Erzeugendensystem von M als R-Modul. Wir ordnen
  die Menge aller Indizes (j, i_1,...,i_m) lexikographisch.

  Wir führen nun eine Induktion über die Struktur eines "schönen
  Erzeugendensystems" von M als R-Modul. Wir möchten sukzessive
  überflüssige Elemente aus einem solchen System entfernen, bis wir bei
  einer Basis landen.

  Ein schönes Erzeugendensystem soll ein Untersystem des trivialen
  Erzeugendensystems bestehend aus allen Vektoren der Form
  x_1^{i_1} ... x_m^{i_m} v_j sein, das folgende kritische Eigenschaften hat:

  a) Wenn einer dieser Vektoren nicht Teil des Systems ist, dann sind
     auch alle Vektoren mit noch größeren x_i-Potenzen nicht Teil des
     Systems.

  b) Jeder Vektor der Form x_1^{i_1} ... x_m^{i_m} v_j ist
     Linearkombination von Vektoren aus dem System, deren Index jeweils
     kleiner als (j, i_1,...,i_m) ist.

  Eigenschaft a) stellt sicher, dass ein Induktionsbeweis zulässig ist.
  Wenn man beliebige Erzeugendensysteme erlaubt, kann es nämlich sein,
  dass man unendlich oft überflüssige Vektoren aus dem System entfernen
  muss und danach immer noch nicht bei einer Basis landet. Dagegen gibt es
  keine unendlichen absteigenden Ketten in der Menge aller schönen
  Erzeugendensysteme.

  Eigenschaft b) ist nötig, damit der Induktionsschritt durchgeht.

  Der Induktionsanfang, bei dem das gegebene schöne Erzeugendensystem das
  leere System ist, ist schnell erledigt: Dann ist M = 0. Indem wir die
  Voraussetzung für f := 1 verwenden, sind wir fertig.

  Im Induktionsschritt sei ein schönes Erzeugendensystem gegeben.
  Wir möchten die Voraussetzungen von Lemma 1 überprüfen (dann können wir,
  indem wir die Voraussetzung für f := 1 verwenden, den Beweis
  abschließen).

  Sei also ein beliebiges Element g in R gegeben, sodass über R[g^{-1}]
  einer der Vektoren aus dem gegebenen schönen Erzeugendensystem
  Linearkombination von Vektoren mit kleinerem Index ist. Dann lässt sich
  M[g^{-1}] über R[g^{-1}] durch ein echt kleineres schönes
  Erzeugendensystem erzeugen (einfach den überflüssigen Vektor sowie all
  seine x_i-Vielfache streichen und nachprüfen, dass das entstehende
  Erzeugendensystem wieder schön ist). Nach Induktionsvoraussetzung ist
  R[g^{-1}] = 0. Also ist g = 0.

* Aus interner Sicht ist das alles etwas einfacher. Im kleinen Zariskitopos
  von Spec(R) gilt für alle Elemente f der Strukturgarbe:

      neg neg (f = 0  vee  f invertierbar).

  Dann eine Induktion über die Struktur eines "schönes Erzeugendensystems",
  um nachzuweisen, dass M~ nicht nicht frei ist. Wir haben:

      neg neg (ein Erzeuger ist Linearkombination von kleineren  oder  nicht).

  Da wir eine doppelt negierte Aussage beweisen möchten, können wir davon
  ausgehen, dass die Aussage in Klammern stimmt. Im zweiten Fall ist das
  Erzeugendensystem linear unabhängig. Im zweiten Fall können wir die
  Induktionsvoraussetzung auf das verkleinerte System anwenden.

  Genauer geht es hier immer um "Freiheit über einer endlichen Menge oder einer,
  die bijektiv zu N ist". Das ist auch wichtig, denn sonst können wir nicht
  folgern, dass die Modulgarbe lokal frei ist.


=== Algebraische Abgeschlossenheit

* Die dedekindschen komplexen Zahlen sind im Allgemeinen nicht algebraisch
  abgeschlossen. Etwa nicht im Garbentopos über [0,1]. Dort sind sie gegeben
  durch die Garbe der stetigen komplexwertigen Funktionen. Aber das Polynom
  X^2 - w, wobei w die Funktion ist, die immer schneller und immer kleiner um 0
  herum kreist, hat in der internen Sprache keine Nullstelle.

  Oder auch einfach X^2 - w über C, wobei w die generische komplexe Zahl ist.

* Die cauchyschen komplexen Zahlen sind algebraisch abgeschlossen.
  Wim Ruitenburg. Constructing roots of polynomials over the complex numbers.
  http://www.mscs.mu.edu/~wimr/publica/roots_new.pdf

* Mehr zu algebraischen Zahlen:
  https://projecteuclid.org/download/pdf_1/euclid.pjm/1102810439
  Algebraic numbers, a constructive development

* Von abzählbaren Körpern K (gemeint ist: ¬inv ⇒ 0) können wir wie folgt einen
  algebraischen Abschluss konstruieren. Wir nehmen die Zerfällungsalgebra aller
  normierten Polynome positiven Grads und teilen das über die
  Krivine-Konstruktion erhaltene maximale Ideal heraus. Das Ergebnis, K₁, ist
  wieder ein Körper, die normierten Polynome über K positiven Grads zerfallen
  alle und K₁ ist auch algebraisch über K.

  Leider sehe ich nicht, wie man konstruktiv zeigen könnte, dass auch die neuen
  Polynome zerfallen würden.

  Ich kann nur zeigen: Für jedes normierte Polynom positiven Grads aus K₁[X]
  gilt, dass es nicht nicht der Fall ist, dass es eine Nullstelle in K₁ hat.

  Aber nicht verzagen! Wir wiederholen einfach die Konstruktion für die neuen
  Polynome, um K₂ zu erhalten, und so weiter. K∞ ist dann der Kolimes (in der
  Kategorie der Ringe) dieser K_n. Und darüber zerfallen dann sicher alle
  Polynome. :-)

  K∞ ist wieder ein Körper (im selben Sinne); jedes normierte Polynom zerfällt;
  jedes Element ist algebraisch über K; und der Unterring K[x ∈ K∞ | f(x) = 0
  für ein f ∈ K[X]] ist ganz K∞. (Das ist was anderes, größeres, als K[die
  synthetischen Nullstellen der Polynome von K[X]].)

  Dank der generischen Surjektion geht das alles auch für beliebige Ringe, der
  Abschluss lebt dann in einem anderen Topos.


=== Fan-Theorem & Co.

* FAN: Für jeden herauslösbaren Baum (herauslösbare Teilmenge von {0,1}^*
  die unter Verkürzung von Wörtern abgeschlossen ist), aus dem jede 0/1-Folge
  herausläuft, ist endlich.

* WKL: Jeder unendliche herauslösbare Baum hat einen unendlichen Pfad
  (0/1-Folge, sodass jede Abschneidung im Baum enthalten ist).

* Kontraposition von WKL:

  Sei T ein herauslösbarer Baum. Falls T keinen unendlichen Pfad besitzt,
  so ist T nicht unendlich.

  Jede 0/1-Folge läuft heraus ==> T besitzt keinen unendlichen Pfad.

  T nicht unendlich <== T endlich.

  Kontraposition-von-WKL =/=> FAN.

  FAN =/=> Kontraposition-von-WKL.

* Kontraposition von FAN:

  Sei T ein herauslösbarer Baum. Falls T unendlich ist, so ist es nicht der
  Fall, dass jede 0/1-Folge herausläuft.

  Kontraposition-von-FAN =/=> WKL (auch nicht mit Markov).
  WKL ==> Kontraposition-von-FAN.

* Mit Markovs Prinzip gilt: FAN <==> Kontraposition-von-WKL.

* LEM ==> FAN (ohne Auswahlprinzipien).


=== Zum Auswahlaxiom äquivalente Aussagen

* Jeder nichttriviale Ring enthält ein maximales Ideal:
  Von Hodges (1979). Siehe auch Banaschweski: A new proof that "Krull implies
  Zorn".


=== Lokale und globale Lipschitzstetigkeit

* Der Beweis, dass lokale Lipschitzstetigkeit auf Kompakta globale impliziert,
  ist nicht völlig uninteressant. Was sagt proof mining dazu?


=== Diskretheit und Abzählbarkeit

* Es gibt das Gerücht, dass sich konstruktive Mathematik und Überabzählbarkeit
  nicht vertragen würden. Das ist natürlich falsch. Aber eine gewisse
  Präzisierung davon stimmt: In function realizability, jede diskrete Menge ist
  abzählbar. https://mathoverflow.net/a/296882/31233


=== Potenzmengen & Co.

* Die Inklusion P_{≤1}(X) → P(X) besitzt eine Retraktion:

  Eine Teilmenge K ⊆ X können wir auf { x ∈ X | K = {x} } schicken.


=== Approximative Maxima

(1) The statement "for any ε > 0, for any uniformly continuous function
f : [0,1] → ℝ, there is a point x₀ ∈ [0,1] such that f(x) ≤ f(x₀) + ε
for all x ∈ [0,1]" is constructively provable (without any form of
choice). [Proof idea: Find an appropriate δ using uniform continuity.
Subdivide [0,1] in overlapping intervals of length at most δ. Take the
maximum of the (finitely many) values of f at the interval boundaries.
Then find a point x₀ such that f(x₀) is close to this maximum.]

(2) The statement "for any ε > 0, for any pointwise continuous function
f : [0,1] → ℝ, there is a point x₀ ∈ [0,1] such that f(x) ≤ f(x₀) + ε
for all x ∈ [0,1]" is not constructively provable. It would entail that
any continuous function on [0,1] is bounded. However, this fails in
RUSS. (However, it does hold in toposes of sheaves over locally compact
spaces, at least assuming a classical metatheory.)


=== Exakte Brechnungen

https://dl.acm.org/doi/pdf/10.1145/3341703

Beschreibt eine Sprache, MarshallB, in der alle Funktionen stetig sind und
Maxima von kompakten Mengen bestimmt werden können.


=== Integrationstheorie

https://drops.dagstuhl.de/opus/volltexte/2006/290/pdf/05021.SpittersBas1.Paper.290.pdf


=== Schematheorie

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


=== Ordinalzahlen

https://arxiv.org/abs/2208.03844

Wir müssen uns bei Brouwer-artigen Baumordinalzahlen auf Limiten von strikt
anwachsenden Sequenzen beschränken, andernfalls funktioniert Exponentiation
nicht:

    0 ^ lim(0,1,1,1,...) = 0 ^ 1 = 0

        aber

    lim(0^0, 0^1, 0^1, 0^1, ...) = lim(1,0,0,0,...) = 1.

Dank der strikten Monotonie können wir dagegen eine entsprechende
Fallunterscheidung machen.

Siehe den Absatz direkt vor Abschnitt 7 des zitierten Aufsatzes.


=== Ultrafilter in Kombinatorik

* Wie geht Hindman's Theorem konstruktiv? Wenn ich die Theoreme nicht
  verwechsele, wurde mir diese Aufgabe von Christian Sattler gestellt.