Q0 (mathematical logic)

Last updated

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.

Contents

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. [1]

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 A, B, and C are syntactic variables for WFFs, and bold lower case letters such as x, y are syntactic variables for variables. S indicates syntactic substitution at all free occurrences.

The only primitive constants are Q((oα)α), denoting equality of members of each type α, and (i(oi)), 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, x must be free for A in B, meaning that the substitution does not cause any occurrences of free variables of A to become bound in the result of the substitution.

About the axioms

In Andrews 2002, 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 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 HAα = Bα, and HC, and D is obtained from C by replacing one occurrence of Aα by an occurrence of Bα, then HD, provided that:

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.

Notes

Related Research Articles

<span class="mw-page-title-main">Transfinite induction</span> Mathematical concept

Transfinite induction is an extension of mathematical induction to well-ordered sets, for example to sets of ordinal numbers or cardinal numbers. Its correctness is a theorem of ZFC.

In statistics, a statistic is sufficient with respect to a statistical model and its associated unknown parameter if "no other statistic that can be calculated from the same sample provides any additional information as to the value of the parameter". In particular, a statistic is sufficient for a family of probability distributions if the sample from which it is calculated gives no additional information than the statistic, as to which of those probability distributions is the sampling distribution.

In mathematics, a measurable cardinal is a certain kind of large cardinal number. In order to define the concept, one introduces a two-valued measure on a cardinal κ, or more generally on any set. For a cardinal κ, it can be described as a subdivision of all of its subsets into large and small sets such that κ itself is large, and all singletons {α}, ακ are small, complements of small sets are large and vice versa. The intersection of fewer than κ large sets is again large.

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.

In mathematics, in set theory, the constructible universe, denoted by , is a particular class of sets that can be described entirely in terms of simpler sets. is the union of the constructible hierarchy. It was introduced by Kurt Gödel in his 1938 paper "The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis". In this paper, he proved that the constructible universe is an inner model of ZF set theory, and also that the axiom of choice and the generalized continuum hypothesis are true in the constructible universe. This shows that both propositions are consistent with the basic axioms of set theory, if ZF itself is consistent. Since many other theorems only hold in systems in which one or both of the propositions is true, their consistency is an important result.

System F is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphism in programming languages, thus forming a theoretical basis for languages such as Haskell and ML. It was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds.

In Bayesian probability theory, if the posterior distribution is in the same probability distribution family as the prior probability distribution , the prior and posterior are then called conjugate distributions, and the prior is called a conjugate prior for the likelihood function .

<span class="mw-page-title-main">Euler's rotation theorem</span> Movement with a fixed point is rotation

In geometry, Euler's rotation theorem states that, in three-dimensional space, any displacement of a rigid body such that a point on the rigid body remains fixed, is equivalent to a single rotation about some axis that runs through the fixed point. It also means that the composition of two rotations is also a rotation. Therefore the set of rotations has a group structure, known as a rotation group.

<span class="mw-page-title-main">Lambda cube</span>

In mathematical logic and type theory, the λ-cube is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to:

In mathematical logic, New Foundations (NF) is an axiomatic set theory, conceived by Willard Van Orman Quine as a simplification of the theory of types of Principia Mathematica. Quine first proposed NF in a 1937 article titled "New Foundations for Mathematical Logic"; hence the name. Much of this entry discusses NF with urelements (NFU), an important variant of NF due to Jensen and clarified by Holmes. In 1940 and in a revision in 1951, Quine introduced an extension of NF sometimes called "Mathematical Logic" or "ML", that included proper classes as well as sets.

Ridge regression is a method of estimating the coefficients of multiple-regression models in scenarios where the independent variables are highly correlated. It has been used in many fields including econometrics, chemistry, and engineering. Also known as Tikhonov regularization, named for Andrey Tikhonov, it is a method of regularization of ill-posed problems. It is particularly useful to mitigate the problem of multicollinearity in linear regression, which commonly occurs in models with large numbers of parameters. In general, the method provides improved efficiency in parameter estimation problems in exchange for a tolerable amount of bias.

In set theory, a subset of a Polish space is ∞-Borel if it can be obtained by starting with the open subsets of , and transfinitely iterating the operations of complementation and wellordered union. This concept is usually considered without the assumption of the axiom of choice, which means that the ∞-Borel sets may fail to be closed under wellordered union; see below.

<span class="mw-page-title-main">Fermat point</span> Triangle center minimizing sum of distances to each vertex

In Euclidean geometry, the Fermat point of a triangle, also called the Torricelli point or Fermat–Torricelli point, is a point such that the sum of the three distances from each of the three vertices of the triangle to the point is the smallest possible or, equivalently, the geometric median of the three vertices. It is so named because this problem was first raised by Fermat in a private letter to Evangelista Torricelli, who solved it.

In mathematics, a real or complex-valued function f on d-dimensional Euclidean space satisfies a Hölder condition, or is Hölder continuous, when there are real constants C ≥ 0, α > 0, such that

<span class="mw-page-title-main">Axiom of limitation of size</span>

In set theory, the axiom of limitation of size was proposed by John von Neumann in his 1925 axiom system for sets and classes. It formalizes the limitation of size principle, which avoids the paradoxes encountered in earlier formulations of set theory by recognizing that some classes are too big to be sets. Von Neumann realized that the paradoxes are caused by permitting these big classes to be members of a class. A class that is a member of a class is a set; a class that is not a set is a proper class. Every class is a subclass of V, the class of all sets. The axiom of limitation of size says that a class is a set if and only if it is smaller than V—that is, there is no function mapping it onto V. Usually, this axiom is stated in the equivalent form: A class is a proper class if and only if there is a function that maps it onto V.

In mathematics, the notion of cylindric algebra, invented by Alfred Tarski, arises naturally in the algebraization of first-order logic with equality. This is comparable to the role Boolean algebras play for propositional logic. Cylindric algebras are Boolean algebras equipped with additional cylindrification operations that model quantification and equality. They differ from polyadic algebras in that the latter do not model equality.

A ratio distribution is a probability distribution constructed as the distribution of the ratio of random variables having two other known distributions. Given two random variables X and Y, the distribution of the random variable Z that is formed as the ratio Z = X/Y is a ratio distribution.

In probability theory and statistics, the normal-gamma distribution is a bivariate four-parameter family of continuous probability distributions. It is the conjugate prior of a normal distribution with unknown mean and precision.

<span class="mw-page-title-main">Normal-inverse-gamma distribution</span>

In probability theory and statistics, the normal-inverse-gamma distribution is a four-parameter family of multivariate continuous probability distributions. It is the conjugate prior of a normal distribution with unknown mean and variance.

A geometric stable distribution or geo-stable distribution is a type of leptokurtic probability distribution. Geometric stable distributions were introduced in Klebanov, L. B., Maniya, G. M., and Melamed, I. A. (1985). A problem of Zolotarev and analogs of infinitely divisible and stable distributions in a scheme for summing a random number of random variables. These distributions are analogues for stable distributions for the case when the number of summands is random, independent of the distribution of summand, and having geometric distribution. The geometric stable distribution may be symmetric or asymmetric. A symmetric geometric stable distribution is also referred to as a Linnik distribution. The Laplace distribution and asymmetric Laplace distribution are special cases of the geometric stable distribution. The Mittag-Leffler distribution is also a special case of a geometric stable distribution.

References

Further reading