Q0 Logic
Encyclopedia
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.
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.
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.
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:
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.
in more depth; part of an article on
Church's Type Theory
in the Stanford Encyclopedia of Philosophy.
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a 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
Higher-order logic
In mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and a stronger semantics...
and closely related to the logics of the
HOL theorem prover
HOL theorem prover
HOL denotes a family of interactive theorem proving systems sharingsimilar logics and implementation strategies....
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: 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 .)
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.
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.
Further Reading
A description of Q0in more depth; part of an article on
Church's Type Theory
in the Stanford Encyclopedia of Philosophy.