Technical reports
The representation of logics in higher-order logic
August 1987, 29 pages
DOI: 10.48456/tr-113
Abstract
Intuitionistic higher-order logic — the fragment comtaining implication, universal quantification, and equality — can serve as a meta-logic for formalizing various logics. As an example, axioms formalizing first-order logic are presented, and proved sound and complete by induction on proof trees.
Proofs in higher-order logic represent derivations of rules as well as proofs of theorems. A proof develops by deriving rules using higher-order resolutions. The discharge of assumptions involves derived meta-rules for ‘lifting’ a proposition.
Quantifiers require a similar lifting rule or else Hilbert’s ε-operator. The alternatives are contrasted through several examples. Hilbert’s ε underlies Isabelle’s original treatment of quantifiers, but the lifting rule is logically simpler.
The meta-logic is used in the latest version of the theorem prover Isabelle. It extends the logic used in earlier versions. Compared with other meta-logics, higher-order logic has a weaker type system but seems easier to implement.
Full text
PDF (1.3 MB)
BibTeX record
@TechReport{UCAM-CL-TR-113, author = {Paulson, Lawrence C.}, title = {{The representation of logics in higher-order logic}}, year = 1987, month = aug, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-113.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-113}, number = {UCAM-CL-TR-113} }