Second-order propositional logic
Appearance
A second-order propositional logic is a propositional logic enriched by quantification over propositions.
The most widely known formalism is the intuitionistic theory, system F. Parigot (1997) showed how this calculus can extended to admit classical logic.
References
Parigiot, Michel (1997). Proofs of strong normalisation for second order classical natural deduction. Journal of Symbolic Logic 62(4):1461-1479.