Alleinführung im Antezedens/Konjunktion der Monoidaxiome/Beispiel

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

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

wobei ${}\beta$ die Konjunktion der zwei Monoidaxiome (also Assoziativität und Existenz des neutralen Elementes) 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 ein „festes, aber beliebiges“ Monoid ${}M$ „denken“, und darin ein „festes, aber beliebiges“ ${}x\in M$. Für dieses ${}x$ beweist man dann die Aussage, dass wenn ${}xz=z$ für alle ${}z\in M$ 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.