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.

Axioms of Q₀

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

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

$(2^{\alpha })$  $[x_{\alpha }=y_{\alpha }]\supset \centerdot \,h_{o\alpha }x_{\alpha }=h_{o\alpha }y_{\alpha }$

$(3^{\alpha \beta })$  $f_{\alpha \beta }=g_{\alpha \beta }=\forall x_{\beta }\centerdot f_{\alpha \beta }x_{\beta }=g_{\alpha \beta }x_{\beta }$

$(4)$  $[\lambda \mathbf {x_{\alpha }} \mathbf {B} _{\beta }]\mathbf {A} _{\alpha }=\mathbf {S} _{A_{\alpha }}^{\mathbf {x} _{\alpha }}\mathbf {B} _{\beta }$

$(5)$  ℩$_{i(oi)}[{\text{Q}}_{oii}y_{i}]=y_{i}\,$

(Axioms 2, 3, and 4 are axiom schemas—families of similar axioms. Instances of Axiom 2 and Axiom 3 vary only by the types of variables and constants, but instances of Axiom 4 can have any expression replacing A and B.)

The subscripted "o" is the type symbol for boolean values, and subscripted "i" is the type symbol for individual (non-boolean) values. Sequences of these represent types of functions, and can include parentheses to distinguish different function types. Subscripted Greek letters such as α and β are syntactic variables for type symbols. Bold capital letters such as A, B, and C are syntactic variables for WFFs, and bold lower case letters such as x, y are syntactic variables for variables. S indicates syntactic substitution at all free occurrences.

The only primitive constants are Q_((oα)α), denoting equality of members of each type α, and ℩_(i(oi)), denoting a description operator for individuals, the unique element of a set containing exactly one individual. The symbols λ and brackets ("[" and "]") are syntax of the language. All other symbols are abbreviations for terms containing these, including quantifiers ∀ and ∃.

In Axiom 4, x must be free for A in B, meaning that the substitution does not cause any occurrences of free variables of A to become bound in the result of the substitution.

About the axioms

• Axiom 1 expresses the idea that T and F are the only boolean values.
• Axiom schemas 2^α and 3^αβ express fundamental properties of functions.
• Axiom schema 4 defines the nature of λ notation.
• Axiom 5 says that the selection operator is the inverse of the equality function on individuals. (Given one argument, Q maps that individual to the set/predicate containing the individual. In Q₀, x = y is an abbreviation for Qxy, which is an abbreviation for (Qx)y.)

In Andrews 2002, Axiom 4 is developed in five subparts that break down the process of substitution. The axiom as given here is discussed as an alternative and proved from the subparts.

Inference in Q₀

Q₀ has a single rule of inference.

Rule R. From C and A_α = B_α to infer the result of replacing one occurrence of A_α in C by an occurrence of B_α, provided that the occurrence of A_α in C is not (an occurrence of a variable) immediately preceded by λ.

Derived rule of inference R′ enables reasoning from a set of hypotheses H.

Rule R′. If H ⊦ A_α = B_α, and H ⊦ C, and D is obtained from C by replacing one occurrence of A_α by an occurrence of B_α, then H ⊦ D, provided that:

• The occurrence of A_α in C is not an occurrence of a variable immediately preceded by λ, and
• no variable free in A_α = B_α and a member of H is bound in C at the replaced occurrence of A_α.

Note: The restriction on replacement of A_α by B_α in C ensures that any variable free in both a hypothesis and A_α = B_α continues to be constrained to have the same value in both after the replacement is done.

The Deduction Theorem for Q₀ shows that proofs from hypotheses using Rule R′ can be converted into proofs without hypotheses and using Rule R.

Unlike some similar systems, inference in Q₀ replaces a subexpression at any depth within a WFF with an equal expression. So for example given axioms:

1. ∃x Px
2. Px ⊃ Qx

and the fact that A ⊃ B ≡ (A ≡ A ∧ B), we can proceed without removing the quantifier:

3. Px ≡ (Px ∧ Qx)   instantiating for A and B
4. ∃x (Px ∧ Qx)   rule R substituting into line 1 using line 3.

References

• Andrews, Peter B. (2002). An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof (2nd ed.). Dordrecht, The Netherlands: Kluwer Academic Publishers. ISBN 1-4020-0763-9. See also https://www.springer.com/mathematics/book/978-1-4020-0763-7.
• Church, Alonzo (1940). "A Formulation of the Simple Theory of Types" (PDF). Journal of Symbolic Logic. 5: 56–58. doi:10.2307/2266170.

Further reading

• A description of Q₀ in more depth; part of an article on Church's Type Theory in the Stanford Encyclopedia of Philosophy.
• An overview on mathematical logics (including various successors of Q₀): Foundations of Mathematics. Genealogy and Overview doi:10.4444/100.111.