Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Logik, Mengen & Beweistechnik » Mengenlehre » natural number game
Druckversion
Druckversion
Antworten
Antworten
Autor
Universität/Hochschule natural number game
OliverFuchs
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 25.03.2020
Mitteilungen: 28
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  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

 




Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 1754
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  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:
Lean
def f: bool   := λ b, match b with
    | ff := 7
    | tt := 42
end

Falls wir jetzt nicht $\mathsf{bool}$, sondern $\emptyset$ haben, sind es eben 0 statt 2 Fälle:
Lean
def g: empty  A := λ e, match e with 
end

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\)


Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
OliverFuchs
Aktiv Letzter Besuch: im letzten Monat
Dabei seit: 25.03.2020
Mitteilungen: 28
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  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




Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
Folgende Antworten hat der Fragesteller vermutlich noch nicht gesehen.
Er/sie war noch nicht wieder auf dem Matheplaneten
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 1754
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.3, eingetragen 2020-07-09

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\)
2020-07-09 16:14 - OliverFuchs in Beitrag No. 2 schreibt:
Wo wir aber einig waren ist, dass die leere Tabelle ein Kanditat ist.
Ein seltsamer zwar aber immer hin. Das ist aber keine Zuordnungsvorschrift.
Ja, mag sein.

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,
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.

die  also $\in:X\to X$ erfüllt.
Hä?

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.
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\)


Eine Notiz zu diese Forumbeitrag schreiben Notiz   Profil  Quote  Link auf diesen Beitrag Link
OliverFuchs wird per Mail über neue Antworten informiert.
Neues Thema [Neues Thema] Antworten [Antworten]    Druckversion [Druckversion]

 


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-2020 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]