Alleinführung im Antezedens/Konjunktion der Monoidaxiome/Beispiel

Aus Wikiversity
Zur Navigation springen Zur Suche springen

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

wobei die Konjunktion der zwei Monoidaxiome (also Assoziativität und Existenz des neutralen Elementes) und ist. In ist nicht gebunden, in schon. In einem mathematischen Beweis wird man sich dann ein „festes, aber beliebiges“ Monoid „denken“, und darin ein „festes, aber beliebiges“ . Für dieses beweist man dann die Aussage, dass wenn für alle gilt, dass dann sein muss. Im Beweis selbst wird nicht über quantifiziert, dies steckt gewissermaßen in der gewählten Beliebigkeit drin. Man beweist also eher die Aussage

und betrachtet dies als einen Beweis für die oben notierte Version. Da in 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.