A part of mathematical logic concerned with the notion of proof.

type theory

second order arithmetic, elementary function arithmetic

proof management system