Q0 (mathematical logic)

Q₀ is Peter Andrews' formulation of the simply-typed lambda calculus, and provides a foundation for mathematics comparable to first-order logic plus set theory. It is a form of higher-order logic and closely related to the logics of the HOL theorem prover family.

The theorem proving systems TPS and ETPS are based on Q₀. In August 2009, TPS won the first-ever competition among higher-order theorem proving systems.

The system has just five axioms, which can be stated as:

${\displaystyle (1)}$  ${\displaystyle g_{oo}T\land g_{oo}F=\forall x_{o}\centerdot g_{oo}x_{o}}$

...
Wikipedia