Second-order propositional logic

Type of propositional logic

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. Parigot (1997) showed how this calculus can be extended to admit classical logic.

## See also

[edit]

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

## References

[edit]

* Parigot, Michel (Dec 1997). "Proofs of strong normalisation for second order classical natural deduction". Journal of Symbolic Logic. 62 (4) (published 12 March 2014): 1461–1479\. doi:10.2307/2275652. ISSN 0022-4812. JSTOR 2275652.

This logic-related article is a stub. You can help Wikipedia by expanding it.

|

* v
* t
* e

*[v]: View this template
*[t]: Discuss this template
*[e]: Edit this template