Second-order propositional logic

Template:Short description A second-order propositional logic is a propositional logic extended with quantification over propositions. A special case are the logics that allow second-order Boolean propositions, where quantifiers may range either just over the Boolean truth values, or over the Boolean-valued truth functions.

The most widely known formalism is the intuitionistic logic with impredicative quantification, System F. Template:Harvp showed how this calculus can be extended to admit classical logic.

See also

• True quantified Boolean formula
• Second-order arithmetic
• Second-order logic
• Type theory