 and three rules of inference: modus ponens, a rule of uniform substitution of formulas for propositional variables, and a rule of definitional replacement. On this basis, and using an extremely compressed linear notation for proofs which is at the opposite extreme of Frege’s space-occupying proofs, Łukasiewicz proves around 140 theorems in a mere 19 pages.