Second-order propositional logic
{{Short description|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. {{Harvp|Parigot|1997}} showed how this calculus can be extended to admit classical logic.
See also
References
- {{Cite journal |last=Parigot |first=Michel |date=Dec 1997 |title=Proofs of strong normalisation for second order classical natural deduction |url=https://www.cambridge.org/core/product/identifier/S002248120001584X/type/journal_article |journal=Journal of Symbolic Logic |language=en |publication-date=12 March 2014 |volume=62 |issue=4 |pages=1461–1479 |doi=10.2307/2275652 |issn=0022-4812 |jstor=2275652|url-access=subscription }}
{{logic-stub}}