Die Mathe-Redaktion - 17.01.2018 19:11 - Registrieren/Login
Auswahl
ListenpunktHome
ListenpunktAktuell und Interessant ai
ListenpunktArtikelübersicht/-suche
ListenpunktAlle Links / Mathe-Links
ListenpunktFach- & Sachbücher
ListenpunktMitglieder / Karte
ListenpunktRegistrieren/Login
ListenpunktArbeitsgruppen
Listenpunkt1 im Schwätz / Top 15
ListenpunktWerde Mathe-Millionär!
ListenpunktZur Award-Abstimmung
ListenpunktFormeleditor fedgeo
Schwarzes Brett
Aktion im Forum
Suche
Stichwortsuche in Artikeln und Links von Matheplanet
Suchen im Forum
Suchtipps

Bücher
Englische Bücher
Software
Suchbegriffe:
Mathematik bei amazon
Naturwissenschaft & Technik
In Partnerschaft mit Amazon.de
Kontakt
Mail an Matroid
[Keine Übungsaufgaben!]
Impressum

Bitte beachten Sie unsere Nutzungsbedingungen, die Distanzierung, unsere Datenschutzerklärung und
die Forumregeln.

Sie können Mitglied werden oder den Newsletter bestellen.

Der Newsletter Okt. 2017

Für Mitglieder
Mathematisch für Anfänger
Wer ist Online
Aktuell sind 791 Gäste und 33 Mitglieder online.

Sie können Mitglied werden:
Klick hier.

Über Matheplanet
 
Zum letzten Themenfilter: Themenfilter:
Matroids Matheplanet Forum Index
Moderiert von mire2 StrgAltEntf
Logik, Mengen & Beweistechnik » Aussagenlogik » Intuitionistische Logik
Druckversion
Druckversion
Antworten
Antworten
Autor
Universität/Hochschule Intuitionistische Logik
Cek
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 26.11.2016
Mitteilungen: 115
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Themenstart: 2017-12-16


Hallo,

ich verstehe nicht ganz, wie ich in der Intuituionistischen Logik eine Formel folgender Art berechnen kann:

fed-Code einblenden



Wahlurne Für Cek bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.1, eingetragen 2017-12-16

\(\begingroup\)
Formeln "berechnet" man üblicherweise nicht, eher beweist man sie. Intuitionistische Logik ist klassische Logik ohne das Axiom $A\lor\neg A$. Der Junktor $\lor$ funktioniert in diesem Sinne also in intuitionistischer Logik eben nicht so wie in der klassischen Logik.

$A \implies B$ kannst du in intuitionistischer Logik nur so beweisen: Angenommen $A$. Dann ... Also $B$. In klassischer Logik kannst du Folgendes machen: Angenommen $\neg B$. Dann ... Also $\neg A$. Somit gilt $A\implies B$. Das geht in intuitionistischer Logik nicht.

Ich kann dir www.youtube.com/watch?v=Sij1jIL2gEg empfehlen.
\(\endgroup\)


Wahlurne Für Ehemaliges_Mitglied bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 778
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.2, eingetragen 2017-12-16

\(\begingroup\)
2017-12-16 15:38 - asdfusername in Beitrag No. 1 schreibt:
Formeln "berechnet" man üblicherweise nicht, eher beweist man sie. Intuitionistische Logik ist klassische Logik ohne das Axiom $A\lor\neg A$. Der Junktor $\lor$ funktioniert in diesem Sinne also in intuitionistischer Logik eben nicht so wie in der klassischen Logik.
Hallo zusammen,
1)
Weiß jemand eine Quelle, wo das Beweissystem (Ausdrücke, Axiome, Regeln, Syntax, Semantik, usw.) der intuitionistischer Logik exakt definiert
wird ?

2)
So was müßte es dann auch für den "mathematischen Konstruktivismus" geben.
Weiß jemand eine Quelle, wo das formal spezifiziert wird ?

mfg
cx

 
\(\endgroup\)


Wahlurne Für carlox bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
Buri
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 02.08.2003
Mitteilungen: 45110
Aus: Dresden
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.3, eingetragen 2017-12-16


Hi carlox,
das Axiomensystem H von Arend Heyting (1898-1980) ist hier angegeben, es besteht aus den 11 Axiomen
fed-Code einblenden
zusammen mit der Schlußregel Modus ponens A,A⇒B ⊧ B, die auch als Axiom (6) vorkommt.
Interessant scheint mir die Feststellung, dass es Aussageformen gibt, die zwar in der klassischen (und sogar in einer dreiwertigen) Logik gelten, also Tautologien sind, aber in dem intutionistischen System nicht bewiesen werden können. Solch eine Aussageform ist zum Beispiel
fed-Code einblenden
Das kann auf n+1 Aussagen und n-wertige Logik verallgemeinert werden, die intutionistische Logik lässt sich also nicht durch Wahrheitswerttabellen in einer mehrwertigen Logik entscheiden.
Gruß Buri



Wahlurne Für Buri bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.4, eingetragen 2017-12-16


Ich bin Fan des sogenannten Kalkül des natürlichen Schließens. In seiner natürlichen Form ist dieser intuitionistisch. Auch dazu siehe die Vorlesung von Ingo Blechschmidt.



Wahlurne Für Ehemaliges_Mitglied bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 954
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.5, eingetragen 2017-12-16


2017-12-16 16:18 - carlox in Beitrag No. 2 schreibt:
1)
Weiß jemand eine Quelle, wo das Beweissystem (Ausdrücke, Axiome, Regeln, Syntax, Semantik, usw.) der intuitionistischer Logik exakt definiert
wird ?
z.B.
Sørensen, Urzyczyn: Lectures on the Curry-Howard Isomorphism, Kapitel 2 und 9,
Streicher: Introduction to Constructive Logic and Mathematics, Kapitel 2 bis 4.



Wahlurne Für tactac bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 778
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.6, eingetragen 2017-12-17


Erst mal Dank an alle für die vielen Infos.
2017-12-16 17:41 - Buri in Beitrag No. 3 schreibt:
Interessant scheint mir die Feststellung, dass es Aussageformen gibt, die zwar in der klassischen (und sogar in einer dreiwertigen) Logik gelten, also Tautologien sind, aber in dem intutionistischen System nicht bewiesen werden können. Solch eine Aussageform ist zum Beispiel
fed-Code einblenden
Das kann auf n+1 Aussagen und n-wertige Logik verallgemeinert werden, die intutionistische Logik lässt sich also nicht durch Wahrheitswerttabellen in einer mehrwertigen Logik entscheiden.
Gruß Buri
Gilt der der Vollständigkeitssatz also nicht in der intuitionistischen bzw. konstruktivistischen Mathematik ?

mfg
cx




Wahlurne Für carlox bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
Buri
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 02.08.2003
Mitteilungen: 45110
Aus: Dresden
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.7, eingetragen 2017-12-17


2017-12-17 08:20 - carlox in Beitrag No. 6 schreibt:
... Gilt der der Vollständigkeitssatz also nicht in der intuitionistischen bzw. konstruktivistischen Mathematik ?
Hi carlox,
ich weiß es nicht. Vielleicht sagt uns jemand, was dieser Satz genau besagt, wahrscheinlich hängt es mit dem Begriff Tautologie zusammen.
Ich weiß auch nicht, ob die Formeln a ∨ ¬a und ¬¬a ⇒ a, die in der intuitionistischen Logik nicht beweisbar sind, als Tautologien anzusehen sind. Oder wird der Begriff der Tautologie in der intutionistischen Logik gar nicht verwendet?
Gruß Buri



Wahlurne Für Buri bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.8, eingetragen 2017-12-17


"Tautologie" ist ein Begriff aus der klassischen Logik. Meines Erachtens gibt es kein Analogon aus der intuitionistischen Logik. EDIT: Nicht ganz richtig. Im folgenden Beitrag erklärt tactac, wie sich die Semantik von aussagenlogischer intuitionistischer Aussagenlogik definieren lässt.
Der Vollständigkeitssatz gilt mit üblichen Definitionen nicht für einen intuitionistischen Kalkül.

Mit ein bisschen abuse of language ist die Semantik intuitionistischer Logik in einem gewissen Sinn gerade die Syntax intuitionistischer Logik. en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation



Wahlurne Für Ehemaliges_Mitglied bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 954
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.9, eingetragen 2017-12-17

\(\begingroup\) \(\newcommand{\sem}[1]{[\![#1]\!]}\)
2017-12-17 11:33 - Buri in Beitrag No. 7 schreibt:
Ich weiß auch nicht, ob die Formeln a ∨ ¬a und ¬¬a ⇒ a, die in der intuitionistischen Logik nicht beweisbar sind, als Tautologien anzusehen sind. Oder wird der Begriff der Tautologie in der intutionistischen Logik gar nicht verwendet?
Gruß Buri
Intuitionistische Aussagenlogik: $V$ sei die Menge der Aussagenvariablen, die in den Formeln vorkommen.
Für jede Heyting-Algebra $H$ ist $\mathcal I_H := |H|^V$ die Menge der $H$-Interpretationen. Die Semantik einer Formel $\phi$ bzgl. einer $H$-Interpretation $I$, $\sem\phi_I$, wird auf naheliegende Weise rekursiv über den Aufbau der Formel und unter Verwendung der Operationen der Heytingalgebra definiert.
Ein $\phi$ ist nun Tautologie, wenn für alle Heytingalgebren $H$ und alle $I\in \mathcal I_H$ gilt: $\sem\phi_I=1$.

Hasse-Diagramm einer Heytingalgebra, mit der sich zeigen lässt, dass $A\lor\lnot A$ und $\lnot\lnot A \to A$ keine Tautologien sind:
    1
    |
    M
   / \
  L   R
   \ /
    0
Wir haben hier $\lnot M = 0, \lnot\lnot M=1$, aber $1 \not\leq M$ ($1=x\to y$ ist immer äquivalent zu $x\leq y$), sowie
$\lnot L = R, \lnot R = L$ (also $\lnot\lnot L = L$), aber trotzdem $L\lor\lnot L = M \neq 1$.
\(\endgroup\)


Wahlurne Für tactac bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
Folgende Antworten hat der Fragesteller vermutlich noch nicht gesehen.
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 778
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.10, eingetragen 2017-12-18


@all
habe vor einiger Zeit irgendwo gelesen, daß konstruktive Mathematik in der Informatik eine Anwendung hat.
Leider weiß ich nicht mehr die Quelle und worum es genau ging.
Weiß jemand von euch mehr davon ?

mfg
cx
 



Wahlurne Für carlox bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.11, eingetragen 2017-12-18


Wenn eine Aussage konstruktiv berechenbar EDIT: natürlich meine ich "beweisbar" EDIT END ist, dann hat sie einen Realsierer, einen Algorithmus der sie realisiert. Siehe die Vorlesung von Ingo Blechschmidt.



Wahlurne Für Ehemaliges_Mitglied bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 778
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.12, eingetragen 2017-12-18


2017-12-18 09:44 - asdfusername in Beitrag No. 11 schreibt:
Siehe die Vorlesung von Ingo Blechschmidt.
Gibt es die auch als digitales Skript ?
Habe bis jetzt nur Filme von ihm gefunden wie z.B:
www.youtube.com/watch?v=Sij1jIL2gEg

mfg
cx




Wahlurne Für carlox bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
Ehemaliges_Mitglied
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.13, eingetragen 2017-12-18


iblech.gitlab.io/garben-und-logik/notes.pdf



Wahlurne Für Ehemaliges_Mitglied bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
tactac
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 15.10.2014
Mitteilungen: 954
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.14, eingetragen 2017-12-20

\(\begingroup\) \(\newcommand{\sem}[1]{[\![#1]\!]}\)
2017-12-17 14:52 - tactac in Beitrag No. 9 schreibt:
Ein $\phi$ ist nun Tautologie, wenn für alle Heytingalgebren $H$ und alle $I\in \mathcal I_H$ gilt: $\sem\phi_I=1$.
Vielleicht noch eine Ergänzung hierzu. Das analoge für klassische Aussagenlogik wäre ja: "Ein $\phi$ ist nun Tautologie, wenn für alle Booleschen Algebren $B$ und alle $I\in \mathcal I_B$ gilt: $\sem\phi_I=1$."
Wenn $\mathbf 2$ die zweielementige Boolesche Algebra ist, ist aber leicht zu zeigen:
$(\forall I\in\mathcal I_\mathbf 2.\ \sem\phi_I=1) \implies (\forall A\in\mathbf{Set}.\ \forall I \in\mathcal I_{\mathbf 2^A}.\ \sem\phi_I=1)$.
Zusammen damit, dass jede Boolesche Algebra isomorph zu einer Unteralgebra von einem $\mathbf 2^A$ ist (ob man das ohne LEM oder stärkere Geschütze beweisen kann, weiß ich aber jetzt nicht), wird deutlich, warum man bei Betrachtung klassischer Logik zwecks Semantik selten mal über etwas anderes als $\mathbf 2$ spricht (was eigentlich aus didaktischer Sicht eher schlecht ist).
\(\endgroup\)


Wahlurne Für tactac bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
KidinK
Senior Letzter Besuch: in der letzten Woche
Dabei seit: 10.06.2013
Mitteilungen: 1073
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.15, eingetragen 2017-12-20

\(\begingroup\)
2017-12-20 01:05 - tactac in Beitrag No. 14 schreibt:
...dass jede Boolesche Algebra isomorph zu einer Unteralgebra von einem $\mathbf 2^A$ ist (ob man das ohne LEM oder stärkere Geschütze beweisen kann, weiß ich aber jetzt nicht)...

Das ist äquivalent zum Primidealsatz (genauso wie die Aussage, dass $b=1\iff \varphi(b)=1\text{ für alle Homomorphismen }\varphi\colon B\to\mathbf{2}$ (in Logik-Sprache nennt man Homomorphismen nach $\mathbf{2}$ wohl Interpretationen?)).

Liebe Grüße,
KidinK
\(\endgroup\)


Wahlurne Für KidinK bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
Zwerg_Allwissend
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 02.12.2013
Mitteilungen: 125
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.16, eingetragen 2017-12-20 23:29


2017-12-18 07:13 - carlox in Beitrag No. 10 schreibt:
@all
habe vor einiger Zeit irgendwo gelesen, daß konstruktive Mathematik in der Informatik eine Anwendung hat.
Leider weiß ich nicht mehr die Quelle und worum es genau ging.
Weiß jemand von euch mehr davon ?

mfg
cx
 
Na ja, kommt drauf an was man unter "Anwendung" genau versteht. Jedenfalls war das in den 1980er Jahren ein Hype in der Forschung. Die Grundidee war folgende: Anstatt einen Algorithmus zur Lösung eines Problems zu entwerfen und dann zu beweisen, dass der Algorithmus das Problem löst (also den Algorithmus zu verifizieren), beweist man konstruktiv, dass eine Lösung für das Problem existiert. Aus dem konstruktiven Beweis kann dann automatisch (!) ein (korrekter!) Algorithmus extrahiert werden.

Das ist von der Theorie her eine nette Idee und man kann viele Papiere darüber schreiben, aber für die praktische Anwendung hat die Sache einen Haken: Notwendigerweise muss ein Algorithmus korrekt sein, aber das reicht in der Praxis noch nicht. Man möchte auch möglichst effiziente Algorithmen verwenden. Nun ist der Entwurf effizienter Algorithmen eine durchaus nicht-triviale und kreative Tätigkeit. Beispielsweise entwickelt man geeignete Datenstrukturen oder macht sich bestimmte mathematische Prinzipien zu Nutze. Bei der konstruktiven Methoden müssen jedoch  Effizienzkriterien schon  während (!) der Beweisentwicklung  betrachtet werden, und das klappt dann nicht.

Die "traditionelle" Methode ist erfolgreicher, da die beiden kreativen Leistungen "Algorithmenentwurf" und "Verifikation" getrennt voneinander erbracht werden und nicht gleichzeitig, wie bei der konstruktiven Methode.

Siehe z.B. das NUPRL System von R. L. Constable für eine Implentierung.



Wahlurne Für Zwerg_Allwissend bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
carlox
Aktiv Letzter Besuch: in der letzten Woche
Dabei seit: 22.02.2007
Mitteilungen: 778
Aus:
Zum letzten BeitragZum nächsten BeitragZum vorigen BeitragZum erstem Beitrag  Beitrag No.17, eingetragen 2017-12-22 20:52


2017-12-16 18:48 - asdfusername in Beitrag No. 4 schreibt:
Auch dazu siehe die Vorlesung von Ingo Blechschmidt.
Daß jemand seine Vorlesungen Online stellt, mit "seinen" Studenten auf Augenhöhe kommuniziert, diskutiert, ein gutes Lernklima schafft und außerdem den Stoff hochinteressant vermittelt... das habe ich so noch nicht erlebt.
Dafür könnt ihr Ingo Blechschmidt dankbar sein.
Schade, daß Augsburg von mir weit weg ist ...

PS:
Wie sieht es eigentlich mit dem Angebot an Logik-Vorlesungen an anderen Unis aus - im Vergleich zu Augsburg ?


mfg
cx



Wahlurne Für carlox bei den Matheplanet-Awards stimmen
  Profil  Quote  Link auf diesen Beitrag Link
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-2017 by Matroids Matheplanet
This web site was made with PHP-Nuke, a web portal system written in PHP. 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]