Matroids Matheplanet Forum Index
Moderiert von matroid
Mathematik » Notationen, Zeichen, Begriffe » Notation der komplexen Zahlen nicht gerechtfertigt
Thema eröffnet 2021-08-20 11:25 von carlox
Seite 2   [1 2]   2 Seiten
Autor
Universität/Hochschule Notation der komplexen Zahlen nicht gerechtfertigt
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2194
  Beitrag No.40, eingetragen 2021-08-28

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) Ich meine: Die Elemente von $\IC$ können einfach Paare von reellen Zahlen sein. Und dann kann man sagen, dass die Notation "$x + \mathrm i y$", wenn $x$ und $y$ Terme sind, die für reelle Zahlen stehen, als Bedeutung das Paar $(x,y)$ erhält. Die Aussage aus #38 ist dann trivialerweise wahr.\(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1252
  Beitrag No.41, vom Themenstarter, eingetragen 2021-08-29

\quoteon(2021-08-28 21:16 - tactac in Beitrag No. 40) Ich meine: Die Elemente von $\IC$ können einfach Paare von reellen Zahlen sein. Und dann kann man sagen, dass die Notation "$x + \mathrm i y$", wenn $x$ und $y$ Terme sind, die für reelle Zahlen stehen, als Bedeutung das Paar $(x,y)$ erhält. Die Aussage aus #38 ist dann trivialerweise wahr. \quoteoff 1) "trivialerweise wahr". Du meinst damit wie man die Notationsfrage rechtfertigen kann? Man muss eigentlich beweisen, dass die Notation widerspruchsfrei ist. Wenn man Notationen "ungeschickt" wählt kann man sich Widersprüche einfangen. Triviales Beispiel: c = 300000 und c = 1 ergibt einen Widerspruch. 2) "Bedeutung" Ich verstehe, was du anschaulich damit meinst. Kann man das auch formalisieren ? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2194
  Beitrag No.42, eingetragen 2021-09-04

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-08-29 08:43 - carlox in Beitrag No. 41) \quoteon(2021-08-28 21:16 - tactac in Beitrag No. 40) Ich meine: Die Elemente von $\IC$ können einfach Paare von reellen Zahlen sein. Und dann kann man sagen, dass die Notation "$x + \mathrm i y$", wenn $x$ und $y$ Terme sind, die für reelle Zahlen stehen, als Bedeutung das Paar $(x,y)$ erhält. Die Aussage aus #38 ist dann trivialerweise wahr. \quoteoff 1) "trivialerweise wahr". Du meinst damit wie man die Notationsfrage rechtfertigen kann? Man muss eigentlich beweisen, dass die Notation widerspruchsfrei ist. Wenn man Notationen "ungeschickt" wählt kann man sich Widersprüche einfangen. Triviales Beispiel: c = 300000 und c = 1 ergibt einen Widerspruch. \quoteoff Klar. Wobei es in dem Beispiel ja so sein dürfte, dass es entweder von vorn herein als illegal erkannt wird, oder bei der Benutzung der Notation "c" bemerkt wird, dass eine Mehrdeutigkeit vorliegt, oder einfach eine der Definitionen benutzt wird. \quoteon 2) "Bedeutung" Ich verstehe, was du anschaulich damit meinst. Kann man das auch formalisieren ? mfg cx \quoteoff Sicherlich. In Coq und Lean zum Beispiel kann man recht komplexe Notationen definieren. Die Dokumentation dieser Mechanismen (oder deren Quellcode) kann man als Formalisierung sehen. Beide legen übrigens keinen großen Wert darauf, alle Arten von Schindluder zu unterbinden. Und hier mal etwas Lean-Code; da kommt allerdings nicht die in #40 vorgeschlagene Notation vor, aber mehr oder weniger die Aussage aus #0 samt Beweis (foo). Da wird eine implizite Konversion benutzt, und die Möglichkeit dazu durch die has_coe-Typklasseninstanz festgelegt: \sourceon Lean import .Ring structure Complex(R : Type) := mk :: (re : R) (im : R) @[reducible] def i{R : Type}[Ring R]: Complex R := Complex.mk 0 1 @[reducible] instance(R : Type)[Ring R]: Ring (Complex R) := { add := λ p q, Complex.mk (p.re + q.re) (p.im + q.im), zero := Complex.mk 0 0, neg := λ p, Complex.mk (-p.re) (-p.im), mul := λ p q, Complex.mk (p.re*q.re - p.im*q.im) (p.re*q.im + p.im*q.re), one := Complex.mk 1 0, add_zero := λ x, by { cases x, simp }, add_assoc := λ x y z, by { cases x, cases y, cases z, simp }, add_neg := λ x, by { cases x, simp }, add_comm := λ x y, by { cases x, cases y, simp, split; apply Ab.add_comm }, one_mul := λ x, by { cases x, simp }, mul_one := λ x, by { cases x, simp }, mul_assoc := λ x y z, by { cases x, cases y, cases z, simp [Ring.mul_assoc], split; ac_refl }, add_mul_distr_l := λ x y z, by { cases x, cases y, cases z, simp, split; ac_refl }, add_mul_distr_r := λ x y z, by { cases x, cases y, cases z, simp, split; ac_refl }, } @[reducible] instance(R : Type)[Ring R]: has_coe R (Complex R) := ⟨λ r, Complex.mk r 0⟩ theorem foo(R : Type)[Ring R](x y : R): (⟨x,y⟩: Complex R) = x + i*y := begin simp, split, calc x = x + -0 : by simp ... = (x:Complex R).re + -(y:Complex R).im : by refl, calc y = 0 + y : by simp ... = (x:Complex R).im + (y:Complex R).re : by refl end \sourceoff \(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1252
  Beitrag No.43, vom Themenstarter, eingetragen 2021-09-06

Hallo tactac, \quoteon In Coq und Lean zum Beispiel kann man recht komplexe Notationen definieren. \quoteoff Also könnte man (z.B. in Lean oder Coq) Mengen definieren: (wobei: $\{-n \mid n \in \mathbb{N} \} $ $\{\frac{p}{q} \mid p \in \mathbb{Z} \land q \in \mathbb{Z} \setminus \{ 0 \} \} $ $\{x+iy : x,y \in \mathbb{R} \} $ Symbolmengen (Mengen von selbst gebastelten Symbolen) sind. ) 1) $ \mathbb{Z} = \mathbb{N} \quad \cup \quad \{-n \mid n \in \mathbb{N} \} $ mit 0 = -0 und noch zu definierender Addition auf $ \mathbb{Z} $ 2) $ \mathbb{Q} = \mathbb{Z} \quad \cup \quad \{\frac{p}{q} \mid p \in \mathbb{Z} \land q \in \mathbb{Z} \setminus \{ 0 \} \} $ mit: $ \frac{p}{1} = p $ $ \frac{0}{p} = 0 $ für $p \neq 0 $ $ \frac{p}{q} = \frac{p \oplus c}{q \oplus c} $ für $q \oplus c \ \neq 0 $ und $ \oplus $ ist Addition auf $ \mathbb{Z} $ und noch zu definierender Addition auf $ \mathbb{Q} $ 3) $ \mathbb{C} = \mathbb{R} \quad \cup \quad i \mathbb{R} \quad \cup \quad \{x+iy : x,y \in \mathbb{R} \} \quad \cup \quad \{i\} $ mit: x := x + i0 iy := 0 + iy und noch zu definierender Addition und Multiplikation auf $ \mathbb{C} $ Ist das richtig? Erlaubt ZFC, daß man diese Mengen bilden kann ? Wenn das erlaubt ist, verstehe ich nicht warum du schreibst: \quoteon Vor allem sollte man auch nicht versuchen, C als Menge von Notationsinstanzen zu definieren. \quoteoff mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2194
  Beitrag No.44, eingetragen 2021-09-17

\(\begingroup\)\(\newcommand{\sem}[1]{[\![#1]\!]} \newcommand{\name}[1]{\ulcorner#1\urcorner} \newcommand{\upamp}{\mathbin {⅋}}\) \quoteon(2021-09-06 14:50 - carlox in Beitrag No. 43) Hallo tactac, \quoteon In Coq und Lean zum Beispiel kann man recht komplexe Notationen definieren. \quoteoff Also könnte man (z.B. in Lean oder Coq) Mengen definieren: (wobei: $\{-n \mid n \in \mathbb{N} \} $ $\{\frac{p}{q} \mid p \in \mathbb{Z} \land q \in \mathbb{Z} \setminus \{ 0 \} \} $ $\{x+iy : x,y \in \mathbb{R} \} $ Symbolmengen (Mengen von selbst gebastelten Symbolen) sind. ) 1) $ \mathbb{Z} = \mathbb{N} \quad \cup \quad \{-n \mid n \in \mathbb{N} \} $ mit 0 = -0 und noch zu definierender Addition auf $ \mathbb{Z} $ 2) $ \mathbb{Q} = \mathbb{Z} \quad \cup \quad \{\frac{p}{q} \mid p \in \mathbb{Z} \land q \in \mathbb{Z} \setminus \{ 0 \} \} $ mit: $ \frac{p}{1} = p $ $ \frac{0}{p} = 0 $ für $p \neq 0 $ $ \frac{p}{q} = \frac{p \oplus c}{q \oplus c} $ für $q \oplus c \ \neq 0 $ und $ \oplus $ ist Addition auf $ \mathbb{Z} $ und noch zu definierender Addition auf $ \mathbb{Q} $ 3) $ \mathbb{C} = \mathbb{R} \quad \cup \quad i \mathbb{R} \quad \cup \quad \{x+iy : x,y \in \mathbb{R} \} \quad \cup \quad \{i\} $ mit: x := x + i0 iy := 0 + iy und noch zu definierender Addition und Multiplikation auf $ \mathbb{C} $ Ist das richtig? Erlaubt ZFC, daß man diese Mengen bilden kann ? \quoteoff Wenn man soetwas wie ZFC benutzt, gibt es die Frage, ob man etwas "bilden kann", eigentlich nicht. ZFC gibt Axiome vor, die u.a. behaupten, dass unter gewissen Voraussetzungen irgendwelche Mengen existieren (die dann meist extensional spezifiziert werden). Aber ich verstehe in etwa, was du meinst, und ja, man kann die angedeuteten Dinge in sowas wie Coq oder Lean nachbauen. Es ist nur in speziell dieser Form (zumindest für $\IC$) recht aufwendig und unsinnig. \quoteon Wenn das erlaubt ist, verstehe ich nicht warum du schreibst: \quoteon Vor allem sollte man auch nicht versuchen, C als Menge von Notationsinstanzen zu definieren. \quoteoff \quoteoff Eine Orientierung an einer möglichen Semantik ist besser. Ein notationsorientiertes Vorgehen (so mit "prä"-komplexen Zahlen $R\times R + R + R + 1$ und einer hinterher dafür definierten Äquivalenzrelation, die in einem Setoid der komplexen Zahlen für die Gleichheit stehen soll) ist zwar möglich, bringt aber zu viele Fallunterscheindungen mit sich und anderen Kram. Wenn man das ganze allgemein für $R \to R[i]$ machen will statt nur für $\IR \to \IC$, merkt man zum Beispiel recht schnell, dass allein für eine uniforme Definition der richtigen Äquivalenzrelation auf der Syntax erforderlich ist, dass in beliebigen Ringen entweder $0=1$ oder $0\neq 1$ gilt. \(\endgroup\)


   Profil
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 1252
  Beitrag No.45, vom Themenstarter, eingetragen 2021-09-18

\quoteon In Coq und Lean zum Beispiel kann man recht komplexe Notationen definieren. \quoteoff Hallo tactac, Danke für dein Feedback. Dein Umgang mit Lean haben mein Interesse geweckt, mich damit mal zu beschäftigen, wenn ich Zeit habe. Wie lange hast du gebraucht, um mit Lean umzugehen bzw. dies einigermaßen zu erlernen? Wie lange braucht man als "Normalsterblicher" dazu? Was meinst du ? mfg cx


   Profil
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 2194
  Beitrag No.46, eingetragen 2021-09-18

\quoteon(2021-09-18 11:43 - carlox in Beitrag No. 45) \quoteon In Coq und Lean zum Beispiel kann man recht komplexe Notationen definieren. \quoteoff Hallo tactac, Danke für dein Feedback. Dein Umgang mit Lean haben mein Interesse geweckt, mich damit mal zu beschäftigen, wenn ich Zeit habe. Wie lange hast du gebraucht, um mit Lean umzugehen bzw. dies einigermaßen zu erlernen? \quoteoff Viele der Konzepte kannte ich schon von Haskell und Coq. Ich musste also zum Losspielen nur ein neues Vokabular (bzw. Teile davon) und ein paar neue Syntax-Bits lernen. Das ging recht schnell: Tage bis wenige Wochen, bis ich komfortabel damit umgehen konnte. Aber natürlich weiß ich auch nach Jahren nicht „alles“ und lerne immer wieder etwas hinzu. Die Standardbibliothek und etwa mathlib sollte man wohl auch einigermaßen kennen — das ist aber ein Fass ohne Boden. 😄 \quoteon Wie lange braucht man als "Normalsterblicher" dazu? Was meinst du ? \quoteoff Auch bei Null beginnend dürfte es nicht viel länger als in paar Wochen dauern, bis man nichttriviale Dinge basteln kann. Natürlich nicht auf einem Niveau, das erfahrene Benutzer davon abhält, die Hände über dem Kopf zusammenzuschlagen und/oder sehr hilfreiche Tipps zu geben, wenn sie deinen Code lesen.


   Profil
carlox hat die Antworten auf ihre/seine Frage gesehen.
carlox wird per Mail über neue Antworten informiert.
Seite 2Gehe zur Seite: 1 | 2  

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]