Formalisierung der Theorie endlicher Mengen in der Typentheorie

Die meisten Beweisassistenten haben eine Formalisierung des Konzepts der "endlichen Menge". Diese Formalisierungen unterscheiden sich jedoch stark (obwohl man hofft, dass sie alle im Wesentlichen gleichwertig sind!). Was ich derzeit nicht verstehe, ist der Designraum und die Vor- und Nachteile jeder Formalisierung.

Insbesondere möchte ich Folgendes verstehen:

• Kann ich endliche Mengen (dh Typen, die von einer endlichen Anzahl von Einwohnern bewohnt werden) in der einfachen Typentheorie axiomatisieren? System F? Was sind die Nachteile, wenn man es so macht?
• Ich weiß, dass es in einem abhängig typisierten System „elegant“ gemacht werden kann. Aus klassischer Sicht erscheinen die daraus resultierenden Definitionen jedoch äußerst fremd. [Ich sage nicht, dass sie falsch sind, weit davon entfernt!]. Aber ich verstehe auch nicht, warum sie "richtig" sind. Ich verstehe, dass sie das richtige Konzept auswählen , aber der tiefere Grund, es so zu sagen, ist das, was ich nicht vollständig verstehe.

Grundsätzlich möchte ich eine begründete Einführung in den Entwurfsraum von Formalisierungen des Konzepts der 'endlichen Menge' in der Typentheorie.

Ich weiß, dass es in einem abhängig typisierten System „elegant“ gemacht werden kann. Aus klassischer Sicht erscheinen die daraus resultierenden Definitionen jedoch äußerst fremd.

Können Sie erklären, was Sie mit "Alien" meinen? Es scheint mir, dass Sie das Konzept der endlichen Menge in der Typentheorie und in der Mengenlehre genauso formalisieren.

In der Mengenlehre definieren Sie die Menge als Dann definieren Sie das Prädikat der Endlichkeit als: Wobei Isomorphismus von Mengen bedeutet.$Fin(n)$F i n i t e ( X ) ≜ ∃ n ∈ N

$$\mathrm{Fin}(n) \triangleq \{ k \in \mathbb{N} \;|\; k < n \}$$ A ≃ $$\mathrm{Finite}(X) \triangleq \exists n\in\mathbb{N}.\; X \simeq \mathrm{Fin}(n)$$ $A \simeq B$

In der Typentheorie können Sie genau das Gleiche tun! Beachten Sie, dass ein Typ mit Elementen ist (da die zweite Komponente des Paares beweisunabhängig ist). Anschließend können Sie den Konstruktor für den Endlichkeitstyp wie folgt definieren: Wobei Isomorphismus von Typen bedeutet.F i n ( n ) n F i n i t e ( X ) ≜ & Sigma; n : N

$$\mathrm{Fin}(n) \triangleq \Sigma k:\mathbb{N}.\; \mathsf{if}\; k < n\,\mathsf{then}\; \mathsf{Unit} \;\mathsf{else}\; \mathsf{Void}$$ $\mathrm{Fin}(n)$$n$A ≃ $$\mathrm{Finite}(X) \triangleq \Sigma n:\mathbb{N}.\; X \simeq \mathrm{Fin}(n)$$ $A \simeq B$

Lassen Sie mich sehen, ob ich Neels Antwort etwas Nützliches hinzufügen kann. Der "Entwurfsraum" für endliche Mengen ist konstruktiv viel größer als klassisch, da verschiedene Definitionen von "endlich" nicht konstruktiv übereinstimmen müssen. Verschiedene Definitionen in der Typentheorie ergeben leicht unterschiedliche Konzepte. Hier sind einige Möglichkeiten.

Kuratowski-endliche Mengen ( endlich) können als freie Halbgitter charakterisiert werden: Bei gegebener Menge, Typ oder Objekt können die Elemente des freien Halbgitters als endliche Teilmengen von . In der Tat wird jedes dieser Elemente erzeugt durch:≤ X ≤ K ( X ) $K$$\lor$$X$$\lor$$K(X)$$X$

• das neutrale Element , das der leeren Menge entspricht, oder$0$
• ein Generator , der dem Singleton , oder{ x $x \in X$$\lbrace x \rbrace$
• eine Verbindung zweier Elemente, die einer Vereinigung entspricht.$S \lor T$

Eine äquivalente Formulierung von lautet: ist endlich, wenn und nur wenn und eine Surjektion .$K(X)$$S \subseteq X$$K$$n \in \mathbb{N}$ $e : \lbrace 1, \ldots, n \rbrace \to S$

Wenn wir dies mit Neel Definition vergleichen sehen wir , dass er erfordert bijection . Dies läuft darauf hinaus, die endlichen Teilmengen die eine entscheidbare Gleichheit haben: . Lassen Sie uns verwenden für die Sammlung von entscheidbar -finite Teilmengen von .$e : \lbrace 1, \ldots, n \rbrace \to S$$K$$S \subseteq X$$\forall x, y \in S . x = y \lor x \neq y$$D(X)$$K$$X$

Offensichtlich ist unter endlichen Vereinigungen geschlossen, aber es muss nicht unter endlichen Schnittpunkten geschlossen werden. Und ist unter keinen Operationen geschlossen. Da die Leute erwarten, dass sich endliche Mengen ein bisschen wie ein "Boolescher Aglebra ohne Spitze" verhalten, könnte man auch versuchen, sie als freie verallgemeinerte Boolesche Algebra ( , , und relative Komplemente ) zu definieren, aber ich eigentlich nie von einer solchen Anstrengung gehört.D ( X ) 0 ∨ ∧ $K(X)$$D(X)$$0$$\lor$$\land$$\setminus$

Bei der Entscheidung, was die "richtige" Definition ist, müssen Sie darauf achten, was Sie mit den endlichen Mengen tun möchten. Und es gibt keine einzige korrekte Definition. In welchem ​​Sinne von "endlich" ist beispielsweise die Menge der komplexen Wurzeln eines Polynoms endlich ?

Siehe Konstruktiv endlich? von Thierry Coquand und Arnaud Spiwack für eine detaillierte Diskussion der Endlichkeit. Die Lehre ist, dass Endlichkeit konstruktiv alles andere als offensichtlich ist.