Es sei α {\displaystyle {}\alpha } eine aussagenlogische Tautologie.
Dann lässt sich dazu konstruktiv eine Ableitung für ⊢ α {\displaystyle {}\vdash \alpha } angeben.
