Q zero

Q0 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 Q0. In August 2009, TPS won the first-ever competition among higher-order theorem proving systems.[1]

Axioms of Q0

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

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 Q0

Q0 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:

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 Q0 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 Q0 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.

Notes

References

Further reading

A description of Q0 in more depth; part of an article on Church's Type Theory in the Stanford Encyclopedia of Philosophy.

This article is issued from Wikipedia - version of the Saturday, May 10, 2014. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.