intuitionistische-logik.txt

=== Disjunktion durch existenzielle Quantifikation

  phi v psi <==>
    exists x : { 0, 1 }.
      (x = 0 ==> phi) wedge (x != 0 ==> psi).


=== Ein paar Tautologien

Schreibe -phi := (phi -> r).

* Sei phi entscheidbar. Dann:
  phi -> psi   <==>   nicht phi oder psi.

  Die Rückrichtung benötigt das Explosionsprinzip für psi!

* Falls man Explosionsprinzip für psi hat, sind in minimaler Logik
  äquivalent:
  1) --(phi ==> psi)
  2) phi ==> --psi
  3) --phi ==> --psi
  Dabei sind 2) und 3) sogar stets äquivalent, und 1) ==> 2)/3) folgt auch
  immer.

* -(phi ==> psi)  <==>  --phi & -psi.

  Für "==>" benötigt man dabei das Explosionsprinzip für phi.
  "<==" gilt stets.

* r ==> --phi.

* --r <==> r.

* ---phi <==> -phi.

* --(phi v psi) <==> --(--phi v --psi).

* -(phi v psi) <==> -phi & -psi.

* --(phi & psi) <==> --phi & --psi.


=== Doppelnegationsübersetzungen (in minimale Logik)

Habe mindestens folgende Varianten:

* Vor jedem Operator/Quantor jeweils nichtnicht einfügen.
* Nur vor jedem "oder", jedem "es gibt" und natürlichen den atomaren Formeln
  jeweils nichtnicht einfügen.
* "bot" durch "r" ersetzen, direkt nach jedem "forall x" ein nichtnicht
  einfügen und dann die gesamte Aussage doppelt negieren.

Die ersten beiden sind immer äquivalent. Die dritte ist zu den ersten
äquivalent, falls ich für atomare Formeln das Explosionsprinzip habe und ich
für jeden in Existenzquantoren vorkommenden Typ einen Term habe.

Fundamentale Aussage: Gilt phi |- psi klassisch, so gilt phi^0 |- psi^0 in
minimaler Logik. Insbesondere gilt phi^negneg |- psi^negneg, falls ich "bot"
habe. In klassischer Logik ist phi^r äquivalent zu (phi v r).

In folgendem Artikel steht, welche übersetzten Aussagen von ihren
Originalfassungen intuitionistisch impliziert werden:

    Hajime Ishihara. A note on the Gödel-Gentzen translation.
    Math. Log. Quart. 46 (2000) 1, 135--137.

Angeblich gilt: --phi <==> phi^r, falls in phi nicht forall, ==> vorkommen.

* Im PPL-Artikel von Fairtlough und Mendler wird auf Johannson "Der
  Minimalkalkül, ein reduzierter intuitionistischer Formalismus" (1936) für den
  "oder f"-Trick verwiesen.


=== Friedmans Trick

Definiere top^A = T, bot^A = A, phi^A = phi v A für phi atomar und durch naive
Rekursion für &,v,-->,forall,exists.

Dann habe: Falls phi |- psi intuitionistisch, dann phi^A |- psi^A
intuitionistisch; brauche dazu A |- phi^A als Lemma, und dazu muss es für alle
unter Existenzquantoren vorkommenden Typen Terme geben. Es gibt dann mitunter
unendlich viele verschiedene Beweise!

Habe phi^A <==> phi v A für (zumindest) all solche Formeln, die sich nur aus
top, bot, wedge, vee, forall_{<= n}, exists zusammensetzen. Also quasi für
geometrische Formeln! Es muss wieder Terme für alle existenzquantifizierten
Typen geben.

Habe (nicht nicht exists x. phi(x))^A ==> exists x. phi(x), falls
phi(x)^A ==> phi(x) v A und A := (exists y. phi(x)).


=== AxC ==> LEM

Sei phi eine Aussage.

Definiere die Mengen

    A := { x \in {0,1} | x = 0 oder phi },
    B := { x \in {0,1} | x = 1 oder phi }.

Beide Mengen sind bewohnt, daher gibt es nach AxC eine Auswahlfunktion s
mit

    [s(A) = 0 oder phi] und [s(B) = 1 oder phi].

Somit folgt

    s(A) != s(B) oder phi.

Die Behauptung folgt, da wegen Extensionalität gilt:

    phi <==> A = B <==> s(A) = s(B).

Bemerkung: the axiom of choice is a local-global statement (although I had
never thought of it this way before this problem), namely that if f:X->Y is a
surjection you can find a way to glue the preimages f^(-1)[{y}] of a surjection
together to form a section of the map f.
http://mathoverflow.net/questions/12119/reverse-mathematics-of-cohomology


=== Minima von Mengen natürlicher Zahlen

Behauptung: Für alle m >= 0 und alle aufwärts-abgeschlossenen Teilmengen U von
N, die m enthalten gilt: Nicht nicht besitzt U ein Minimum.

Beweis durch Induktion: Induktionsanfang m = 0 klar. Jetzt der Schritt m --> m + 1.
Kann zeigen: Falls m in U, dann enthält U nicht nicht ein Minimum nach
Induktionsvoraussetzung. Falls m nicht in U, dann ist m + 1 das Minimum: Sei u
in U beliebig. Dann u >= m + 1 oder u <= m. Letzteres kann nicht sein.
In beiden Fällen folgt also, dass U nicht nicht ein Minimum besitzt.
Da nicht nicht (m in U oder m nicht in U), folgt die Behauptung! (Wenn man vier
nichts zu zweien kürzt.)


=== Basen endlich erzeugter Vektorräume

Sei U := { x \in Q | x = 0 oder phi }. Betrachte den Q-Vektorraum V := Q / U.
Dieser ist endlich erzeugt. Wenn er eine (endliche) Basis besäße, hätte diese entweder
Länge 0 oder eine positive Länge. Im ersten Fall würde phi folgen, im zweiten
nicht phi.


=== Diagonalisierbarkeit von Matrizen

http://www.sciencedirect.com/science/article/pii/0168007286900060
Andre Scedrov. Diagonalization of continuous matrices as a representation of intuitionistic
reals.


=== Limit Computable Mathematics

* Michael Toftdal, Calibration of Ineffective Theorems of Analysis
  in a Constructive Context. http://www.shayashi.jp/PALCM/toftdal.pdf
* http://www.shayashi.jp/PALCM/
* Oleg


=== "Injektive Objekte" in Set

Potenzmengen sind "injektiv" bezüglich beliebiger injektiver Abbildungen: Ist
f : A --> B eine beliebige Injektion, so lässt sich jede Abbildung A --> P(M)
auf B fortsetzen.

Ferner sind die Mengen, die injektiv bezüglich herauslösbarer Injektionen sind,
gerade die bewohnten Mengen.


=== Zerfällungen von Injektionen

Sei iota : A --> B mit pi . iota = id. Wenn B diskret ist, ist A herauslösbar
in B. Denn "b in A" ist äquivalent zu "iota(pi(b)) = b".


=== Körperbedingungen

Schreibe in diesem Abschnitt "-" für "neg".

* Gelte -(s inv.) ==> s nilpotent.

  Dann ist -(1 = 0) äquivalent dazu, dass auch die Rückrichtung gilt.

* Gelte -(s inv.) ==> s nilpotent und -(1 = 0).

  Dann gilt auch: --(s nilpotent) ==> s nilpotent.

* Gelte -(s inv.) ==> s nilpotent und -(1 = 0) und ferner s^2 = 0 ==> s = 0.

  Dann gilt: --(s = 0) ==> s = 0.

* Unter diesen Voraussetzungen gilt auch: s regulär <==> --(s invertierbar).


=== Intuitionistische epistemische Logik

Sergei Artemov, Tudor Protopopescu.
Intuitionistic Epistemic Logic.
http://arxiv.org/abs/1406.1582


=== Dialoge für Beweissuche

Jesse Alama.
Dialogues for proof search.
http://arxiv.org/abs/1405.1864


=== Seemingly impossible programs

Sei f : Omega --> 2 eine beliebige Abbildung. Dann gibt es ein Element phi : Omega
mit

    f(phi)  <==>  exists psi. f(psi).

Und zwar gilt doch f(bot) oder neg f(bot).

Im ersten Fall können wir phi := bot wählen.

Im zweiten Fall können wir phi := top wählen. Damit ist "==>" klar und "<=="
geht so: Sei psi mit f(psi) gegeben. Wir wollen f(top) nachweisen. Das können
wir mit Widerspruch. Gelte also neg f(top). Sollte psi gelten, dann gilt auch
f(top), das kann nicht sein. Also gilt neg psi. Damit ist aber f(psi)
äquivalent zu f(bot), was nicht gilt. Das ist ein Widerspruch dazu, dass f(psi)
schon gilt.

(Post von Martin Escardo an constructivenews@googlegroups.com, 2015-11-19
23:52.)


=== Intuitionistische Logik für Kinder

Eduardo Ochs
http://angg.twu.net/math-b.html#zhas-for-children
http://angg.twu.net/dednat6/tests/4.pdf


=== Modale Operatoren

Äquivalent sind:

    1. phi ==> Box phi
    2. Box Box phi ==> Box phi
    3. Box phi  wedge  Box psi  <==>  Box (phi wedge psi)

und:

    (phi ==> Box psi)  <==>  (Box phi ==> Box psi).

"<==": 1. und 2. sind klar. Die Rückrichtung von 3. ebenfalls.
Zur Hinrichtung überlege zunächst, dass

    Box phi  wedge  Box psi  ==>  Box (phi wedge Box psi).
          ????

"==>": Klar. Sogar ohne die 3.?


=== Nabla-Übersetzung (ehemals Box-Übersetzung)

* Vermutlich stimmt folgendes in Minimallogik:

  Falls phi |- psi in A-Logik und die Nabla-Übersetzungen aller über
  Minimallogik hinausgehenden Axiome von A-Logik in B-Logik ableitbar sind, so
  folgt phi^Nabla |- psi^Nabla in B-Logik.


=== Überabzählbare diskrete Mengen

* Konstruktiv können wir nicht die Existenz überabzählbarer diskreter Mengen
  nachweisen. Andrej Bauer und Andrew Swan in https://arxiv.org/pdf/1804.00427.pdf

* Damit können wir auch nicht die Existenz überabzählbarer geometrischer Körper
  nachweisen.


=== Literatur

* The Age of Alternative Logics.
  Assessing Philosophy of Logic and Mathematics Today.

* Von Andrej Bauer empfohlen:
  http://www.cs.cmu.edu/~fp/courses/15317-f09/index.html

* Bishop. Schizophrenia in contemporary mathematics.
  https://prl.ccs.neu.edu/img/sicm.pdf


=== Nächste Schritte

* Verstehen, wie Olegs Sum-Vorschlag die Doppelnegationsübersetzung
  ersetzen kann

* CPS von Typen wie "Integer" verstehen

* Zusammenhang zur nicht-nicht-Topologie erkennen

* Vermutung zu Geschichte: Früher haben die Leute durchaus LEM
  benutzt, aber nur über relativ harmlose Aussagen.
  Prüfe diese Vermutung, indem du z.B. in Cauchy nachsiehst, wie er den
  Tigersatz bewiesen hat!

* Bishop lesen! Ist die Bibel, laut Andrej.