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:

• Der Allabschluss ∀(F) einer Formel F lautet

1. F, falls F geschlossen ist (d. h. nicht über freie Variablen verfügt)
2. ∀x₁...x_n F falls x₁,...,x_n freie Variablen in F sind.

Der Allabschluss kann auch für Formelmengen definiert werden:

• Sei S eine Menge von Formeln. Dann ist der Allabschluss ∀S die Menge ∀S := {∀(F) | F∈S}.

Die zum Allabschluss analoge Operation mit dem Existenzquantor ∃ heißt Existenzabschluss.

Der Allabschluss ist im Allgemeinen nicht logisch äquivalent zur Ursprungsformel, d. h.

• F ∀(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.