##  [Teiltyp](/de/node/60072) 

 Definition

Ein partieller Typ (partieller n-Typ) ist eine konsistente Menge von Erster-Ordnung-Formeln mit Parametern in einem gewählten Variablen-Tupel, die einige Eigenschaften beschreibt, die ein potentielles Tupel erfüllen kann, aber nicht notwendigerweise jede Formel in diesen Variablen entscheidet; er besitzt mindestens eine realisierende Erweiterung und kann zu einem vollständigen Typ erweitert werden.

 

 

 

 

 

 





## Prinzip

Prinzip

Nicht-maximale Konsistenz: Ein partieller Typ ist jede konsistente, aber nicht notwendigerweise maximale Sammlung von Formeln; seine Funktion besteht darin, partielle Informationen oder Einschränkungen zu erfassen, die bei Bedarf zu einer vollständigen Beschreibung erweitert werden können.

 

 

 

 

 





## Demonstration

Demonstration

In der Theorie dichter linearer Ordnungen ohne Endpunkte ist die Menge von Formeln { x > a_n für jedes Element a_n einer streng zunehmenden Folge } ein partieller 1-Typ über den Parametern {a_n}, der einen oberen Schnitt beschreibt; er entscheidet nicht jede Formel und lässt verschiedene vollständige Erweiterungen offen, je nachdem, wie der Schnitt gefüllt wird.

 

 

 

 

## Fehlanwendung

Fehlanwendung

Anzunehmen, ein partieller Typ bestimme eindeutig einen vollständigen Typ oder jeder partielle Typ müsse in jeder Erweiterung realisiert werden; partielle Typen mit quantorenfreien oder endlichen Beschreibungen zu verwechseln, die in manchen Kontexten inkonsistent sein können.

 

 

 

 

 





## Konsequenz

Konsequenz

Partielle Typen dienen als Bausteine beim Aufbau von Modellen, zum Nachweis der Konsistenz von Eigenschafts-Sammlungen und zur Untersuchung von Definierbarkeit und Forking; sie sind die syntaktischen Objekte, deren maximale Erweiterungen vollständige Typen sind und deren Realisierbarkeit Auskunft über Gesättigtheit gibt.

 

 

 

 

## Umkehrung

Umkehrung

Ein vollständiger Typ ist die maximale konsistente Erweiterung eines partiellen Typs; die Umkehrung der Partialität ergibt eine eindeutige, entscheidende Beschreibung ohne offene Formeln.

 

 

 

 

 





## Abgrenzung

Abgrenzung

Gilt nur für Erster-Ordnung-Formeln in einer festgelegten Sprache und dem gewählten Variablen-Tupel; partielle Typen bleiben über nichtentschiedene Formeln stumm und garantieren nicht automatisch die Realisierbarkeit, sofern nicht Konsistenz und ggf. Kompaktheit oder Gesättigtheit angewandt werden.

 

 

 

 

 





## Semantische Spannung

Semantische Spannung

Spannung zwischen Flexibilität (mehrere mögliche Erweiterungen) und Präzision (fehlende Entscheidungen über bestimmte Formeln); partielle Typen sind nützlich bei offen gehaltenen Möglichkeiten, problematisch bei Forderung nach Eindeutigkeit oder Isolierung.

 

 

 

 

 





## Synthese

Synthese

Ein partieller Typ ist eine konsistente, bewusst unvollständige syntaktische Spezifikation von Eigenschaften eines potentiellen Tupels: er dokumentiert Einschränkungen und erlaubt Erweiterungen, wobei lokale Bedingungen mit globalen Realisierungen über die Erweiterung zu vollständigen Typen verbunden werden.