imported>Daniel5Ko: /* Beispiele */ Konkrete Syntax einheitlich über den Artikel.

2026-04-17T22:31:21Z

Beispiele: Konkrete Syntax einheitlich über den Artikel.

Neue Seite

In der [[Mathematik]] heißt eine auf einer [[Menge (Mathematik)|Menge]] <math>M</math> definierte [[zweistellige Relation]] <math>\prec</math> '''wohlfundiert''', wenn es keine unendlichen absteigenden [[Ordnungsrelation#Totalordnung|Ketten]] in dieser Relation gibt, d. h., wenn es keine unendliche [[Folge (Mathematik)|Folge]] <math>a_0, a_1, a_2, a_3, \dots</math> von Elementen in <math>M</math> mit <math>a_{i+1} \prec a_i</math> für alle <math>i</math> gibt. Insbesondere enthält eine wohlfundierte Relation keine Zyklen.

== Eigenschaften ==
* Wohlfundierte Relationen sind stets [[Irreflexive Relation|irreflexiv]].
* Wohlfundierte Relationen sind [[azyklisch]].
* Ist <math>R\subseteq M \times M</math> wohlfundiert und <math>S \subseteq R</math>, so ist <math>S</math> wohlfundiert.

Unter Verwendung des [[Satz vom ausgeschlossenen Dritten|Satzes vom ausgeschlossenen Dritten]] und dem [[Axiom der abhängigen Auswahl]] sind folgende Aussagen über <math>\mathord{\prec} \subseteq M\times M</math> äquivalent:
* <math>\prec</math> ist wohlfundiert.
* Die [[Transitive Hülle (Relation)|transitive Hülle]] von <math>\prec</math> ist wohlfundiert.
* Jede nichtleere Teilmenge <math>X\subseteq M</math> hat ein <math>\prec</math>-minimales Element, d. h. ein <math>a \in X</math>, für das es kein <math>a' \in X</math> gibt mit <math>a'\prec a</math>.
* [[Wohlfundierte Induktion]] über <math>\prec</math> ist ein gültiges Prinzip, um Aussagen über alle Elemente von <math>M</math> zu beweisen.

== Beispiele ==
* Die Vorgängerrelation auf <math>\mathbb N</math>, definiert durch <math>n \prec m :\Longleftrightarrow n+1=m</math>, ist wohlfundiert. Das zu <math>\prec </math> gehörige Induktionsprinzip ist das der [[Vollständige Induktion|vollständigen Induktion]]. Ihre transitive Hülle ist die übliche {{nowrap|<math><</math>-Relation}} mit dem zugehörigen Induktionsprinzip der [[Vollständige Induktion#Starke Induktion|''starken'' (vollständigen) Induktion]], mit klassischer Logik äquivalent zum [[Unendlicher Abstieg|unendlichen Abstieg]].
* Die Relation <math>{\prec} \subseteq \mathbb N \times \mathbb N</math>, definiert durch <math>n \prec m :\Longleftrightarrow n\neq 0 \land (m = 0 \lor \exists p\text{ prim}.\, p\cdot n=m)</math>, ist wohlfundiert, ebenso dieselbe Relation eingeschränkt auf <math>\mathbb N\setminus\{1\}</math>, welche viele minimale Elemente hat. Die transitive Hülle von <math>\prec</math> ist die (echte) [[Teilerrelation]] auf <math>\mathbb N</math>.
* Alle [[Wohlfundierte Ordnung|wohlfundierten Ordnungen]] und alle [[Wohlordnung]]en sind wohlfundierte Relationen, wenn man nur den irreflexiven Teil betrachtet. Die Umkehrungen gelten nicht, da wohlfundierte Relationen nicht transitiv sein müssen.
* Ein Modell <math>V</math> der [[Zermelo-Fraenkel-Mengenlehre]] definiert eine Relation <math>\epsilon\subseteq V\times V</math>, die aufgrund des [[Fundierungsaxiom]]s wohlfundiert ist. Das dazugehörige Induktionsprinzip heißt [[Epsilon-Induktion]].
* Die [[Adjazenz]]relation eines endlichen [[Graph (Graphentheorie) #Teilgraphen, Wege und Zyklen|gerichteten azyklischen Graphen]] ist wohlfundiert.

== Beziehungen zwischen den Definitionen ==

Mit <math>\mathord{\prec} \subseteq M \times M</math> sind folgende Definitionen dafür möglich, dass <math>\prec</math> wohlfundiert ist:
# <math>\prec</math> ist '''klassisch wohlfundiert''' ([[Bewohnte Menge|bewohnte]] Teilmengen von <math>M</math> haben ein <math>\prec</math>-minimales Element): <math>\forall X \subseteq M.\, \forall x_0 \in X.\, \exists x\in X.\, \forall y\in X.\, y \not\prec x</math>.
# <math>\prec</math> ist '''wohlfundiert''' (wohlfundierte Induktion ist gültig): <math>\forall X\subseteq M.\, (\forall x \in M.\, (\forall y \in M.\, y \prec x \to y \in X) \to x \in X) \to \forall x \in M.\, x \in X</math>.
# Bezüglich <math>\prec</math> gibt es '''keinen unendlichen Abstieg (relational formuliert)''': <math>\lnot\exists X \subseteq M.\, \exists x_0\in X.\, \forall x\in X.\, \exists y\in X.\, y \prec x</math>.
# Bezüglich <math>\prec</math> gibt es '''keinen unendlichen Abstieg''': <math>\lnot\exists f\in M^\N.\, \forall n\in\N.\, f(n+1)\prec f(n)</math>.

(1) und (3) sind offenkundig äquivalent zueinander, wenn klassische Logik verwendet wird.

[[Konstruktive Mathematik|Konstruktiv]] kann man jedes Glied der Implikationskette <math>(1)\implies(2)\implies(3)\implies(4)</math> beweisen, die jeweils andere Richtung aber im Allgemeinen nicht.

<math>(4)\implies(3)</math> erfordert eine Instanz des [[Axiom der abhängigen Auswahl|Axioms der abhängigen Auswahl]].

Für <math>(3)\implies(1)</math> wird klassische Logik benötigt, und zwar in einem sehr starken Sinn: Aus der Existenz einer klassisch wohlfundierten Relation <math>\prec</math> und Elementen <math>x,y</math> mit <math>x\prec y</math> folgt bereits der [[Satz vom ausgeschlossenen Dritten]] (siehe unten). In diesem Sinn ist die klassische Wohlfundiertheit (1) zu stark für konstruktive Mathematik. Da es aber bewohnte, nach (2) wohlfundierte Relationen üblicherweise gibt, impliziert <math>(3)\implies(1)</math> klassische Logik.

Oft anzutreffen ist eine Variante von (2), die sich folgendermaßen ergibt: Offensichtlich ist die Formel in (2) äquivalent zu
: <math>\forall x \in M.\, \forall X\subseteq M.\, (\forall x \in M.\, (\forall y \in M.\, y \prec x \to y \in X) \to x \in X) \to x \in X,</math>
und dies wiederum offensichtlich äquivalent zu
: <math>\forall x \in M.\, x \in \bigcap \{X\subseteq M \mid \forall x \in M.\, (\forall y \in M.\, y \prec x \to y \in X) \to x \in X\}.</math>
Mit der Abkürzung <math>\mathrm{Acc}_\prec</math> (“accessible”) für den Mengendurchschnitt, dessen Elemente „<math>\prec</math>-zugänglich“ heißen, hat man dann: <math>{\prec}\subseteq M \times M</math> ist wohlfundiert genau dann, wenn alle Elemente von <math>M</math> <math>\prec</math>-zugänglich sind, also <ref>
{{Internetquelle |url=https://rocq-prover.org/doc/v9.0/corelib/Corelib.Init.Wf.html#well_founded |titel=Rocq Core Library, Library Corelib.Init.Wf |abruf=2025-08-01}}
</ref>
: <math>\forall x \in M.\, x \in \mathrm{Acc}_\prec</math>.

== Klassische Wohlfundiertheit impliziert den Satz von ausgeschlossenen Dritten ==
Es wird gezeigt, dass aus der Existenz einer bewohnten, klassisch wohlfundierten Relation der Satz vom ausgeschlossenen Dritten folgt.
Es seien <math>M</math> eine Menge, <math>\mathord{\prec} \subseteq M \times M</math> eine klassisch wohlfundierte Relation darauf, <math>y,z \in M</math> und <math>y \prec z</math>.
Zu zeigen ist, dass für beliebige Aussagen <math>P</math> gilt: <math>P \lor \lnot P</math>. Dafür sei <math>P</math> beliebig.
Die Menge <math>X := \{ x \in M \mid P \lor x = z\}</math> ist nun eine Teilmenge von <math>M</math> und bewohnt, da sie <math>z</math> enthält. Es gibt also ein <math>x \in X</math> mit <math>\forall y\in X.\, y \not \prec x</math>.
Aus <math>x \in X</math> ergeben sich zwei Fälle:
# <math>P</math>. In dem Fall gilt <math>P</math>.
# <math>x = z</math>. In dem Fall gilt <math>\lnot P</math>, denn angenommen, <math>P</math> gelte, dann ist <math>y \in X</math> und somit <math>y \not\prec x = z</math>, was <math>y \prec z</math> widerspricht.
In beiden Fällen folgt <math>P \lor \lnot P</math>. <math>\square</math>

== Siehe auch ==
* [[Abstiegsfunktion]]
* [[Fundierte Menge]]

== Literatur ==
* Paul Taylor: ''Practical Foundations of Mathematics'', Cambridge University Press, 1999, ISBN 0-521-63107-6, Seiten 97ff

== Einzelnachweise ==
<references />

[[Kategorie:Mathematische Logik]]

Wohlfundierte Relation - Versionsgeschichte

imported>Daniel5Ko: /* Beispiele */ Konkrete Syntax einheitlich über den Artikel.