Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Logik, Mengen & Beweistechnik » Mengenlehre » natural number game
Autor
Universität/Hochschule natural number game
OliverFuchs
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 25.03.2020
Mitteilungen: 162
Wohnort: Wien, Österreich
  Themenstart: 2020-07-08

Ich habe auf Anregung von Nuramon das natural number game begonnen. Ich habe ein Frage beim Schritt von Level 7 zu Level 8 der function world. Nach meiner Meinung, machen die Autoren da einen Fehler. In Level 7 ist eine Funkton der Form $(P\to Q)\to ((Q\to F)\to(P\to F))$ zu konstruieren. Naiv wie ich bin, habe ich das auch gemacht. proof completed ! war die Antwort. In Level 8 soll man eine Funktion der Form $(P\to Q)\to((Q\to \emptyset) \to (P\to \emptyset))$ konstruieren. Geht man wie in Level 7 vor, so kommt man darauf ein Element aus $\emptyset$ konstruieren zu müssen, was unmöglich ist. Nun wird behauptet, dass man aber in Level 7 einen korekten Beweis für alle Mengen geführt hat. Dann kommt ein Teil den ich, auch aus Mangel an Sprachkenntnissen, nicht verstanden habe. Ich habe mir aber bis dato die folgende Meinung gebildet. Ich betrachte den Level 8. Es gibt kein Element in $\emptyset$. Jetzt wird es haarig für mich. Wenn ich eine Funktion $f:X\to Y$ so definiert habe, dass ich jedem Elment $x\in X$ genau ein Element $y\in Y$ zuweise, dann ist das im Falle $X\not = \emptyset$ $Y=\emptyset$ und gültigem A.A. nicht möglich. Denn es gibt zumindest ein konkretes $x_0\in X$ aber zu diesem kann ich keinen Funktionswert $y_0:=f(x_0)$ definieren. Daher ist die Menge der Funktionen $Hom(X,Y)=\emptyset$ leer. Wenn also $P,Q$ nicht leere Mengen sind, so ist es nicht möglich eine Funktion wie in Level 8 gefordert, zu konstruieren. Wenn das in Lean doch geht, dann stimmt da was nicht. Betrachte ich Level 7 so gilt ähnliches. sind $P,Q$ nicht leer, so muss ich auch $F$ als nicht leer voraussetzen, weil ich sonst weder ein Element aus $Q\to F$ noch aus $P\to F$ wählen kann mein Bildraum $Hom((P\to F),(Q\to F))$, ist also leer. Da es aber der Definitonsraum mit $Hom(P,Q)$ nicht ist, kann ich keine Funktion finden und der Beweis geht in diesem Fall ins leere. (Im wörtlichen sinne). Also ist, entgegen der Behauptung im Text, der Beweis in Level 7 nicht für alle Mengen gültig. Sehen wir uns jetzt den Fall $P=Q=\emptyset$ an. Dann stehen wir vor der Aufgabe $Hom(\emptyset,\emptyset)$ zu bestimmen. Laut Definition ist ein Element $f\in Hom(\emptyset,\emptyset)$ eine Abbildung die jedem Element aus $\emptyset$ genau ein Element aus $\emptyset$ zuordnet. Wir habe schon gesehen, dass $Hom(X,\emptyset)=\emptyset$ (mit $X\neq\emptyset$) leer ist. Wie ist das aber wenn $X=\emptyset$ ist. Dann ist die Aussage $x\in X$ nie erfüllt. Damit kann aber der Satz, 'jedem Element $x\in X$ genau ein Elelement $y\in Y$ zuzuordnen ' nicht falsch sein. Dieser besagt ja, wenn ich ein Element aus $X$ habe, muss ich ihm genau ein Element aus $Y$ zuordnen. Nun habe ich aber kein Element in $X$. Die Foraussetzung der Aussage ist nicht erfüllt. Was ist aber der Wahrheitswert einer Aussage deren Voraussetzung nicht erfüllbar ist. Da kann ich zu wenig Logik, aber ich würde sagen, der ist unbestimmt. Damit ist aber nur gesagt, dass ich kein explizietes Verbot der Existenz so einer Funktion ableiten kann. Kann ich aber die Existenz einer solchen zeigen? Genau das wäre nötig. Gibt es also eine Funktion von $f:\emptyset\to\emptyset$ ? Die Intuition sagt nein. Was sagt die Überlegung ? Eine Funktion ist eben eine Zuordungsforschrift. Für unendliche Mengen kann man z.B. eine Rechenforschrit angeben. Für endliche Mengen kann man sogar eine Funktionstabelle angeben. Sofort kommt die nächste Frage, über die ich noch nie nachgedacht habe. Was ist eine endliche Menge und was eine undendliche? Abstrakt kann ich das gar nicht sagen. Daher folge ich zunächst meiner Intution und sage $\emptyset$ ist eine endliche Menge. Wenn ich also eine Funktion von $\emptyset$ nach $\emptyset$ angeben wollte, müsste ich eine Funktionstabelle hinschreiben können. Diese wäre aber Leer. Sie hätte keinen Eintrag. Wenn ich einmal die Menge aller Mengen und die damit verbunden Schwiergkeiten weg lasse, dann ist die Menge alle Funktionstabellen gleich die Menge aller Funktionen zwischen endlichen Mengen. Ist aber $\emptyset$ eine solche so könnte man auch die leere Tabelle zulassen und Ihr einen Namen geben. Etwa die leere-Funktion. Dann wäre aber $Hom(\emptyset,\emptyset)$ nicht leer !!!. Das könnte man nun wieder in die Diskussion von Level 7 zu Level 8 im Numbergame einfließen lassen. Wie weit liege ich mit diesen Überlegungen daneben? lg Oliver


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2282
  Beitrag No.1, eingetragen 2020-07-09

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) Die Menge $\mathsf{Hom}(\emptyset,\emptyset)$ ist tatsächlich nicht leer. Sie hat die Identität als Element. Etwas allgemeiner hat $\mathsf{Hom}(\emptyset, A)$ für beliebige $A$ ein Element $f$. Als Tabelle oder Graph betrachtet ist $f$ leer. Als Funktionsvorschrift betrachtet kann man Fallunterscheidungen hernehmen (das funktioniert jedenfalls bei induktiven Datentypen). Wie definiert man eine Funktion $\mathsf{bool} \to A$? Nun, man gibt an, was der Wert bei $\mathsf{ff}$ und was der Wert bei $\mathsf{tt}$ sein soll. Die Werte werden dabei als Terme vom Tyo $A$ angegeben. Beispiel mit $A = \IN$, in Lean: \sourceon Lean def f: bool → ℕ := λ b, match b with | ff := 7 | tt := 42 end \sourceoff Falls wir jetzt nicht $\mathsf{bool}$, sondern $\emptyset$ haben, sind es eben 0 statt 2 Fälle: \sourceon Lean def g: empty → A := λ e, match e with end \sourceoff Warum spreche ich hier von Funktionen, die $\emptyset$ *starten*? Nun, hier ist das interessante, dass man sich an einer Stelle in einem *absurden Kontext* befindet, wenn man sie in der Form $\lambda x.\ ???$ definiert. An der Stelle, wo das Funktionsresultat angegeben werden soll, haben wir eine Variable im Kontext, die für ein Element des leeren Typs steht. Und analoges (nur komplexeres) passiert passiert bei der Definition einer Funktion $(P \to Q) \to (Q \to \emptyset) \to (P \to A)$ -- egal, ob $A$ nun $\emptyset$ ist, oder etwas anderes. Man startet naheliegend mit $\lambda f\ g\ p.\ ???$. An der Stelle ???, wo wir nun einen Term vom Typ $A$ hinschreiben müssen, haben wir auch einen Term vom Typ $\emptyset$ zur Verfügung, nämlich $g(f\ p)$. Aber wenn man uns einen Term vom Typ $\emptyset$ gibt, können wir einen Term beliebigen Typs (natürlich auch von $\emptyset$) angeben.\(\endgroup\)


   Profil
OliverFuchs
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 25.03.2020
Mitteilungen: 162
Wohnort: Wien, Österreich
  Beitrag No.2, vom Themenstarter, eingetragen 2020-07-09

Ich weiss leider nicht welche Anrede in diesem Foumr üblich ist, also bleibe Ich heute beim Herzlichen weil ich das so hier gelernt habe und mir das das Forum sympathsich macht. Lieber TacTac! Hier scheinen etwas Verständigungsporbleme da zu sein. So wie Du die Antwort Fromutlierst kommst du von der Informatik oder der Computerorientierten Mathematik während ich eine klassiche Mathematikausbildung habe. Ich kann mit Datentypen nichts anfangen und bin solchen Argumentationen auch recht skeptisch gegenüber. Nur weil etwas mit DatenTypen Beweis bar ist muss das noch kein Beweis sein. Ich weiss dass heute auch angesehene Mathematiker solche Beweise anerkennen aber das ist immer mit Vorsicht zu genießen. Deine Behauptung ist also, dass $Hom(\emptyset,\emptyset)$ nicht leer ist. Rein von der Mathematischen Seite her ist das genau dann der Fall, wenn ich zumindest ein Element $f$ in $Hom(\emptyset, \emptyset)$ angeben kann. Dabei möchte ich jetzt nicht auf LEAN eingehen, denn LEAN kann irren. Nur weil etwas in LEAN geht muss es noch nicht wahr sein. Das berachte ich eher als Fingerübung um mal auch einen anderen Standpunkt für bekannte Eigene Gednaken zu überlegen. Wo wir aber einig waren ist, dass die leere Tabelle ein Kanditat ist. Ein seltsamer zwar aber immer hin. Das ist aber keine Zuordnungsvorschrift. Nun hast Du behauptet, dass die Identität $\id$ in $Hom(\emptyset,\emptyset)$ liegt. Weißt Du das genau. Ist das Mathamatisch gesichert oder nur eine Vermutung. Die Identität ist die eindeutige Zuordnungsvorschrift die jedem $x\in X$ ganau dieses $x\in X$ zuordent, die also $\in:X\to X$ erfüllt. Das ist natürlich ein Kandidat. So zu sagen die Einfachste Funtion zu nehmen. Ich werde mal ein Mail an meinen Prof. auf der Uni schreiben was ein Mathematiker dazu sagt. lg Oliver


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2282
  Beitrag No.3, eingetragen 2020-07-09

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2020-07-09 16:14 - OliverFuchs in Beitrag No. 2) Wo wir aber einig waren ist, dass die leere Tabelle ein Kanditat ist. Ein seltsamer zwar aber immer hin. Das ist aber keine Zuordnungsvorschrift. \quoteoff Ja, mag sein. \quoteon Nun hast Du behauptet, dass die Identität $\id$ in $Hom(\emptyset,\emptyset)$ liegt. Weißt Du das genau. Ist das Mathamatisch gesichert oder nur eine Vermutung. Die Identität ist die eindeutige Zuordnungsvorschrift die jedem $x\in X$ ganau dieses $x\in X$ zuordent, \quoteoff Genau das tut die Identität auf $\emptyset$. Auch dann, wenn man sie durch die Zuordnungsvorschrift $x \mapsto x$ definiert, die dir vielleicht im Fall $X=\emptyset$ komisch vorkommt. Sie ist es nicht. \quoteon die also $\in:X\to X$ erfüllt. \quoteoff Hä? \quoteon Das ist natürlich ein Kandidat. So zu sagen die Einfachste Funtion zu nehmen. Ich werde mal ein Mail an meinen Prof. auf der Uni schreiben was ein Mathematiker dazu sagt. \quoteoff Wenn er sich mit Kategorientheorie auskennt, wird er wissen, dass $\mathsf{Set}$, die Kategorie der Mengen und Funktionen, ziemlich kaputt wäre, wenn $\emptyset$ nicht das initiale Objekt wäre. (Das bedeutet, dass es für jede Menge $A$ *genau* eine Funktion $\emptyset \to A$ gibt.) In Typtheorien gibt man dem Term, der aus einem Term $t$ vom Typ $\emptyset$ einen Term vom Typ $A$ macht, oft den Namen $\mathsf{abort}_A(t)$ oder ähnlich. Du kannst dir ja mal überlegen, dass $(x\in\emptyset) \mapsto x$ und $(x\in\emptyset) \mapsto \mathsf{abort}_\emptyset(x)$ extensional dieselbe Funktion definieren. \(\endgroup\)


   Profil
OliverFuchs
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 25.03.2020
Mitteilungen: 162
Wohnort: Wien, Österreich
  Beitrag No.4, vom Themenstarter, eingetragen 2020-09-01

Diesen Tread will ich noch nicht schließen, da ich das Spiel noch nicht fertig gespielt habe. lg Oliver


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2282
  Beitrag No.5, eingetragen 2020-09-02

Es besteht keine Pflicht, Threads zu schließen. Viel Erfolg! Bei Fragen fragen.


   Profil
OliverFuchs hat die Antworten auf ihre/seine Frage gesehen.
OliverFuchs wird per Mail über neue Antworten informiert.

Wechsel in ein anderes Forum:
 Suchen    
 
All logos and trademarks in this site are property of their respective owner. The comments are property of their posters, all the rest © 2001-2021 by Matroids Matheplanet
This web site was originally made with PHP-Nuke, a former web portal system written in PHP that seems no longer to be maintained nor supported. PHP-Nuke is Free Software released under the GNU/GPL license.
Ich distanziere mich von rechtswidrigen oder anstößigen Inhalten, die sich trotz aufmerksamer Prüfung hinter hier verwendeten Links verbergen mögen.
Lesen Sie die Nutzungsbedingungen, die Distanzierung, die Datenschutzerklärung und das Impressum.
[Seitenanfang]