Allabschluss
# Allabschluss

Als Allabschluss bezeichnet man eine syntaktische Operation in der Prädikatenlogik, durch welche für alle sogenannten freien Variablen einer Formel F eine Allquantifizierung, d. h. eine Quantifizierung mittels des Allquantors ∀ vorgenommen wird. Formal:
* F, falls F geschlossen ist (d. h. nicht über freie Variablen verfügt)
* ∀x$_1$...x$_n$ F falls x$_1$,...,x$_n$ freie Variablen in F sind.
Der Allabschluss kann auch für Formelmengen definiert werden:
Die zum Allabschluss analoge Operation mit dem Existenzquantor ∃ heißt Existenzabschluss.

## Äquivalenz und Allgemeingültigkeit des Allabschlusses

Der Allabschluss ist im Allgemeinen nicht logisch äquivalent zur Ursprungsformel, d. h.
* F $\equiv$ ∀(F) gilt nicht für alle F.
Er bewahrt jedoch die Allgemeingültigkeit einer Formel, d. h.
* Wenn F allgemeingültig, dann ist auch ∀(F) allgemeingültig.