Wohlfundierte Relation

In der Mathematik heißt eine auf einer Menge M definierte zweistellige Relation \prec wohlfundiert, wenn es keine unendlichen Ketten in dieser Relation gibt, d.h., wenn es keine unendliche Folge {\displaystyle a_{0},a_{1},a_{2},a_{3},\dots } von Elementen in M mit {\displaystyle a_{i+1}\prec a_{i}} für alle i gibt. Insbesondere enthält eine wohlfundierte Relation keine Zyklen.

Eigenschaften

Wohlfundierte Relationen sind stets irreflexiv.

Unter Verwendung des Satzes vom ausgeschlossenen Dritten und dem Axiom der abhängigen Auswahl sind folgende Aussagen über {\displaystyle {\mathord {\prec }}\subseteq M\times M} äquivalent:

Beispiele

Beziehungen zwischen den Definitionen

Mit {\displaystyle {\mathord {\prec }}\subseteq M\times M} sind folgende Definitionen dafür möglich, dass \prec wohlfundiert ist:

  1. \prec ist klassisch wohlfundiert (bewohnte Teilmengen von M haben ein \prec-minimales Element): {\displaystyle \forall X\subseteq M.\,\forall x_{0}\in X.\,\exists x\in X.\,\forall y\in X.\,y\not \prec x}.
  2. \prec ist wohlfundiert (wohlfundierte Induktion ist gültig): {\displaystyle \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}.
  3. Bezüglich \prec gibt es keinen unendlichen Abstieg (relational formuliert): {\displaystyle \lnot \exists X\subseteq M.\,\exists x_{0}\in X.\,\forall x\in X.\,\exists y\in X.\,y\prec x}.
  4. Bezüglich \prec gibt es keinen unendlichen Abstieg: {\displaystyle \lnot \exists f\in M^{\mathbb {N} }.\,\forall n\in \mathbb {N} .\,f(n+1)\prec f(n)}.

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

Konstruktiv kann man jedes Glied der Implikationskette {\displaystyle (1)\implies (2)\implies (3)\implies (4)} beweisen, die jeweils andere Richtung aber im Allgemeinen nicht.

{\displaystyle (4)\implies (3)} erfordert eine Instanz des Axioms der abhängigen Auswahl.

Für {\displaystyle (3)\implies (1)} wird klassische Logik benötigt, und zwar in einem sehr starken Sinn: Aus der Existenz einer klassisch wohlfundierten Relation \prec und Elementen x,y mit {\displaystyle x\prec y} 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 {\displaystyle (3)\implies (1)} klassische Logik.

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 M eine Menge, {\displaystyle {\mathord {\prec }}\subseteq M\times M} eine klassisch wohlfundierte Relation darauf, {\displaystyle y,z\in M} und {\displaystyle y\prec z}. Zu zeigen ist, dass für beliebige Aussagen P gilt: {\displaystyle P\lor \lnot P}. Dafür sei P beliebig. Die Menge {\displaystyle X:=\{x\in M\mid P\lor x=z\}} ist nun eine Teilmenge von M und bewohnt, da sie z enthält. Es gibt also ein x\in X mit {\displaystyle \forall y\in X.\,y\not \prec x}. Aus x\in X ergeben sich zwei Fälle:

  1. P. In dem Fall gilt P.
  2. {\displaystyle x=z}. In dem Fall gilt {\displaystyle \lnot P}, denn angenommen, P gelte, ist y\in X und somit {\displaystyle y\not \prec x=z}, was {\displaystyle y\prec z} widerspricht.

In beiden Fällen folgt {\displaystyle P\lor \lnot P}. \square

Siehe auch

Trenner
Basierend auf einem Artikel in: Extern Wikipedia.de
Seitenende
Seite zurück
© biancahoegel.de
Datum der letzten Änderung: Jena, den: 03.04. 2023