Wohlfundierte Relation

In der Mathematik heißt eine auf einer Menge definierte zweistellige Relation wohlfundiert, wenn es keine unendlichen Ketten in dieser Relation gibt, d. h. wenn es keine unendliche Folge von Elementen in mit für alle gibt. Insbesondere enthält eine wohlfundierte Relation keine Zyklen.

EigenschaftenBearbeiten

Wohlfundierte Relationen sind stets irreflexiv.

Unter Verwendung des Satzes vom ausgeschlossenen Dritten und dem Axiom der abhängigen Auswahl sind folgende Aussagen über   äquivalent:

  •   ist wohlfundiert.
  • Die transitive Hülle von   ist wohlfundiert.
  • Jede nichtleere Teilmenge   hat ein minimales Element, d. h. ein  , für das es kein   gibt mit  .
  • Wohlfundierte Induktion über   ist ein gültiges Prinzip, um Aussagen über alle Elemente von   zu beweisen.

BeispieleBearbeiten

  • Die Vorgängerrelation auf  , definiert durch  , ist wohlfundiert. Das zu   gehörige Induktionsprinzip ist das der Vollständigen Induktion. Ihre transitive Hülle ist die übliche  -Relation mit dem zugehörigen Induktionsprinzip der starken (Vollständigen) Induktion; mit klassischer Logik äquivalent zum unendlichen Abstieg.
  • Alle wohlfundierten Ordnungen und alle Wohlordnungen sind wohlfundierte Relationen, wenn man nur den irreflexiven Teil betrachtet. Die Umkehrungen gelten nicht, da wohlfundierte Relationen nicht transitiv sein müssen.
  • Ein Modell   der Zermelo-Fraenkel-Mengenlehre definiert eine Relation  , die aufgrund des Fundierungsaxioms wohlfundiert ist. Das dazugehörige Induktionsprinzip heißt Epsilon-Induktion.

Beziehungen zwischen den DefinitionenBearbeiten

Mit   sind folgende Definitionen dafür, dass   wohlfundiert ist, möglich:

  1.   ist klassisch wohlfundiert (bewohnte Teilmengen von   haben ein minimales Element):  .
  2.   ist wohlfundiert (wohlfundierte Induktion ist gültig):  .
  3. Bezüglich   gibt es keinen unendlichen Abstieg (relational formuliert):  .
  4. Bezüglich   gibt es keinen unendlichen Abstieg:  .

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

Konstruktiv kann man jedes Glied der Implikationskette   beweisen, die jeweils andere Richtung aber im Allgemeinen nicht.

  erfordert eine Instanz des Axioms der abhängigen Auswahl.

Für   wird klassische Logik benötigt, und zwar in einem sehr starken Sinn: Aus der Existenz einer klassisch wohlfundierten Relation   und Elementen   mit   folgt bereits der Satz vom ausgeschlossenen Dritten. 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   klassische Logik.

Siehe auchBearbeiten

LiteraturBearbeiten

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