Q0 (mathematical logic)
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. Axioms of Q0 

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

  

  

  

  

  ℩

(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 , , 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 equality
of members of each type α, and , 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,  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. About the axioms 

 Axiom 1 expresses the idea that  and  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,  maps that individual to the set/predicate containing the individual. In Q0,  is an abbreviation for , which is an abbreviation for .) This operator is also known as the definite description operator. 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. Extensions of the logical core 

Andrews extends this logic with definitions of selection operators 
for collections of all types, so that 

  ℩

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 if
the core is consistent. He also presents an additional Axiom 6, which states
that there are infinitely many individuals, along with equivalent alternative
axioms of infinity. Unlike many other formulations of type theory and proof assistants based on
type 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 individuals
obeying the usual Peano postulates rather than a type in the sense of simple
type theory. Inference in Q0 

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 occurrence
of , then
, provided that:
 The occurrence of  in  is not an occurrence of a variable immediately preceded by , and
 no variable free in  and a member of  is bound in  at the replaced occurrence of . Note: The restriction on replacement of  by
 in  ensures that any variable
free in both a hypothesis and 
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. 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. Notes

References 
  See also

Further reading 

 A description of Q0 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 Q0): Foundations of Mathematics. Genealogy and Overview doi:10.4444/100.111. Logic in computer science