The system has just five axioms, which can be stated as:
℩ The subscripted "o" is the type symbol for boolean values, and subscripted "i" is the type symbol for individual 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 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 5 says that the selection operator is the inverse of the equality function on individuals.
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.
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 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.
