Q zero

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.^[1]

Axioms of Q₀

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

$(1)$ $g_{oo}T \and 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 \bold{x_\alpha} \bold{B}_\beta] \bold{A}_\alpha = \bold{S}^{\bold x_\alpha}_{A_\alpha}\bold{B}_\beta$

$(5)$ $\iota_{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. $\existsx Px$
2. $Px \supset Qx$

and the fact that $A \supset B \equiv (A \equiv A \land B)$ , we can proceed without removing the quantifier:

3. $Px \equiv (Px \land Qx)$ instantiating for A and B
4. $\existsx (Px \land Qx)$ rule R substituting into line 1 using line 3.

Notes

↑ The CADE-22 ATP System Competition (CASC-22)

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 http://www.springer.com/mathematics/book/978-1-4020-0763-7.
Church, Alonzo (1940). "A Formulation of the Simple Theory of Types". Journal of Symbolic Logic 5: 56–58. doi:10.2307/2266170.

Q zero

Axioms of Q0

About the axioms

Inference in Q0

Notes

References

Further reading

Axioms of Q₀

Inference in Q₀