Q0 Logic
   HOME

TheInfoList



OR:

Q0 is Peter Andrews' formulation of the
simply-typed lambda calculus The simply typed lambda calculus (\lambda^\to), a form of 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 ca ...
, and provides a foundation for mathematics comparable to first-order logic plus set theory. It is a form of
higher-order logic mathematics and logic, a higher-order logic is a form of predicate logic that is distinguished from first-order logic by additional quantifiers and, sometimes, stronger semantics. Higher-order logics with their standard semantics are more express ...
and closely related to the logics of the
HOL theorem prover HOL (Higher Order Logic) denotes a family of interactive theorem proving systems using similar (higher-order) logics and implementation strategies. Systems in this family follow the LCF approach as they are implemented as a library which defin ...
family. The theorem proving system
TPS and ETPS
are based on Q0. In August 2009, TPS won the first-ever competition among higher-order theorem proving systems.The CADE-22 ATP System Competition (CASC-22)
/ref>


Axioms of Q0

The system has just five axioms, which can be stated as: (1)  g_T \land g_F = \forall x_o _x_o/math> (2^\alpha)   _\alpha = y_\alpha\supset _x_\alpha = h_y_\alpha/math> (3^)  f_ = g_ = \forall x_\beta _x_ = g_x_\beta/math> (4)   lambda \mathbf \mathbf_\beta\mathbf_\alpha = \mathbf^_\mathbf_\beta (5)  ℩_ text_y_i= y_i\, (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 (5a)  ℩_ text_y_i= y_i\, is a theorem (number 5309). In other words, all types have a definite description operator. This is a
conservative extension In mathematical logic, a conservative extension is a supertheory of a theory which is often convenient for proving theorems, but proves no new theorems about the language of the original theory. Similarly, a non-conservative extension is a superthe ...
, 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 als

*{{Cite journal , last = Church , first = Alonzo , authorlink = Alonzo Church , title = A Formulation of the Simple Theory of Types , journal = Journal of Symbolic Logic , volume = 5 , pages = 56–58 , year = 1940 , doi=10.2307/2266170 , url = https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf , archive-url = https://web.archive.org/web/20190112232531/https://pdfs.semanticscholar.org/28bf/123690205ae5bbd9f8c84b1330025e8476e4.pdf , url-status = dead , archive-date = 2019-01-12


Further reading

*
description of Q0
in more depth; part of an article o
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