Email Gateway (Aug 06 2026 at 16:04): Email Gateway (Aug 06 2026 at 16:04):From: Lawrence Paulson <lp15@cam.ac.uk>
Subject: [isabelle] New in the AFP: Completeness of the Q0 Higher-Order Logic
Completeness of the Q0 Higher-Order Logic
Asta Halkjær From, Jonathan Julian Huerta y Munive and Anders Schlichtkrull
Abstract
We formalize the completeness of Peter B. Andrews' system Q0, an implementation of Higher-Order Logic (also called simple type theory), following his textbook An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof. Our work builds on Díaz's formalization of Q0's syntax, semantics, soundness and consistency. The completeness is with respect to general models. We prove completeness by introducing an abstract consistency property for Q0 using the framework for abstract consistency properties by From and Schlichtkrull to get a model existence theorem for Q0. We adapt proofs from Andrews' book to this context.
https://isa-afp.org/entries/Q0_Completeness.html
And no AI was used!
Larry
Last updated: Aug 12 2026 at 20:47 UTC