Jump to content

Second-order propositional logic

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Chalst (talk | contribs) at 12:56, 1 July 2009 (Start stub). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.
(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

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.