Alleinführung im Antezedens/Konjunktion der Gruppenaxiome/Beispiel

Nehmen wir an, wir möchten die Aussage beweisen, dass in einer jeden Gruppe das neutrale Element eindeutig bestimmt ist. Wir formalisieren diese Aussage als

$\beta \rightarrow \forall x\alpha ,$

wobei ${}\beta$ die Konjunktion der drei Gruppenaxiome und ${}\alpha =\forall z(xz=z)\rightarrow x=e$ ist. In ${}\alpha$ ist ${}x$ nicht gebunden, in ${}\forall x\alpha$ schon. In einem mathematischen Beweis wird man sich dann eine „feste, aber beliebige“ Gruppe ${}G$ „denken“, und darin ein „festes, aber beliebiges“ ${}x\in G$. Für dieses ${}x$ beweist man dann die Aussage, dass wenn ${}xz=z$ für alle ${}z\in G$ gilt, dass dann ${}x=e$ sein muss. Im Beweis selbst wird nicht über ${}x$ quantifiziert, dies steckt gewissermaßen in der gewählten Beliebigkeit drin. Man beweist also eher die Aussage

$\beta \rightarrow \alpha ,$

und betrachtet dies als einen Beweis für die oben notierte Version. Da ${}x$ in ${}\beta$ gar nicht oder allenfalls gebunden vorkommt, ist die Ableitbarkeit beider Versionen auch prädikatenlogisch gleichwertig. Insofern spiegelt sich in der Alleinführung im Sukzedens eine wichtiger Aspekt der mathematischen Praxis.