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