Technical reports

The representation of logics in higher-order logic

Lawrence C. Paulson

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}
}