Ciro Santilli @cirosantilli 40

This is the part of the formalization of mathematics that deals only with the propositions.

In some systems, e.g. including Metamath, modus ponens alone tends to be enough, everything else can be defined based on it.

See: eigenvalues and eigenvectors.

Advanced. Not beginner friendly, very clunky.