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 ETPSare based on Q0. In August 2009, TPS won the first-ever competitionamong higher-order theorem proving systems.[1]
The system has just five axioms, which can be stated as:
(1)
gooT\landgooF=\forallxo[gooxo]
(2\alpha)
[x\alpha=y\alpha]\supset[ho\alphax\alpha=ho\alphay\alpha]
(3\alpha\beta)
f\alpha=g\alpha=\forallx\beta[f\alphax\beta=g\alphax\beta]
(4)
[λ
| x\alpha |
B\beta]A\alpha=
| x\alpha | |
| S | |
| A\alpha |
B\beta
(5)
i(oi)[Qoiiyi]=yi
(Axioms 2, 3, and 4 are axiom schemas—families of similar axioms. Instances of Axiom 2 andAxiom 3 vary only by the types of variables and constants, but instances of Axiom 4 can haveany 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 functiontypes. Subscripted Greek letters such as α and β are syntactic variables for typesymbols. Bold capital letters such as,, and are syntactic variables for WFFs, and bold lower case letters such as, are syntactic variables for variables. indicates syntactic substitution at all free occurrences.
The only primitive constants are, denoting equalityof members of each type α, and, denoting adescription 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, must be free for in,meaning that the substitution does not cause any occurrences of free variables of to become bound in the result of the substitution.
In, 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.
Andrews extends this logic with definitions of selection operators for collections of all types, so that
(5a)
\alpha(o\alpha)[Qo\alpha\alphayi]=yi
is a theorem (number 5309). In other words, all types have a definite description operator.This is a conservative extension, so the extended system is consistent ifthe core is consistent.
He also presents an additional Axiom 6, which statesthat there are infinitely many individuals, along with equivalent alternativeaxioms of infinity.
Unlike many other formulations of type theory and proof assistants based ontype theory, Q0 does not provide for base types other than o and i,so the finite cardinal numbers for example are constructed as collections of individualsobeying the usual Peano postulates rather than a type in the sense of simpletype theory.
Q0 has a single rule of inference.
Rule R. From and to infer the result of replacing one occurrence of in by an occurrence of,provided that the occurrence of in 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,and, and is obtained from by replacing one occurrence of by an occurrenceof, then, provided that:
Note: The restriction on replacement of by in ensures that any variablefree in both a hypothesis and continues to be constrained to have the same value in both after the replacementis 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 depthwithin a WFF with an equal expression. So for example given axioms:
1.
2.
and the fact that, we can proceed without removing the quantifier:
3. instantiating for A and B
4. rule R substituting into line 1 using line 3.
. Peter B. Andrews . An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof . 2nd . . Dordrecht, The Netherlands . 2002 . 1-4020-0763-9 . See also https://web.archive.org/web/20100224074552/http://www.springer.com/mathematics/book/978-1-4020-0763-7