Extensional quotients for type theory and the consistency problem for NF

1998 ◽  
Vol 63 (1) ◽  
pp. 247-261
Author(s):  
Gian Aldo Antonelli
Keyword(s):  
Equivalence Relation ◽  
Open Problem ◽  
Type Theory ◽  
Partial Solution ◽  
Weak Version ◽  
New Foundations ◽  
Multiple Copies ◽  
Consistency Problem ◽  
Membership Relation ◽  
Main Ideas

Quine's “New Foundations” (NF) was first presented in Quine [10] and later on in Quine [11]. Ernst Specker [15, 13], building upon a previous result of Ehrenfeucht and Mostowski [5], showed that NF is consistent if and only if there is a model of the Theory of Negative (and positive) Types (TNT) with full extensionality that admits of a “shifting automorphism,” but the existence of such a model remains an open problem.In his [8], Ronald Jensen gave a partial solution to the problem of the consistency of Quine's NF. Jensen considered a version of NF—referred to as NFU—in which the axiom of extensionality is weakened to allow for Urelemente or “atoms.” He showed, modifying Specker's theorem, that the existence of a model of TNT with atoms admitting of a “shifting automorphism” implies the consistency of NFU, proceeding then to exhibit such a model.This paper presents a reduction of the consistency problem for NF to the existence of a model of TNT with atoms containing certain “large” (unstratified) sets and admitting a shifting automorphism. In particular we show that such a model can be “collapsed” to a model of pure TNT in such a way as to preserve the shifting automorphism. By the above-mentioned result of Specker's, this implies the consistency of NF.Let us take the time to explain the main ideas behind the construction. Suppose we have a certain universe U of sets, built up from certain individuals or “atoms.” In such a universe we have only a weak version of the axiom of extensionality: two objects are the same if and only if they are both sets having the same members. We would like to obtain a universe U′ that is as close to U as possible, but in which there are no atoms (i.e., the only memberless object is the empty set). One way of doing this is to assign to each atom ξ, a set a (perhaps the empty set), inductively identifying sets that have members that we are already committed to considering “the same.” In doing this we obtain an equivalence relation ≃ over U that interacts nicely with the membership relation (provided we have accounted for multiplicity of members, i.e., we have allowed sets to contain “multiple copies” of the same object). Then we can take U′ = U/≃, the quotient of U with respect to ≃. It is then possible to define a “membership” relation over U′ in such a way as to have full extensionality. Relations such as ≃ are referred to as “contractions” by Hinnion and “bisimulations” by Aczel.

The equivalence of NF-style set theories with “tangled” type theories; the construction of ω-models of predicative NF (and more)

1995 ◽  
Vol 60 (1) ◽  
pp. 178-190 ◽  
Author(s):  
M. Randall Holmes
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
The Other ◽  
Natural Numbers ◽  
Consistency Proof ◽  
Natural Behaviour ◽  
New Foundations ◽  
Consistency Problem

AbstractAn ω-model (a model in which all natural numbers are standard) of the predicative fragment of Quine's set theory “New Foundations” (NF) is constructed. Marcel Crabbé has shown that a theory NFI extending predicative NF is consistent, and the model constructed is actually a model of NFI as well. The construction follows the construction of ω-models of NFU (NF with urelements) by R. B. Jensen, and, like the construction of Jensen for NFU, it can be used to construct α-models for any ordinal α. The construction proceeds via a model of a type theory of a peculiar kind; we first discuss such “tangled type theories” in general, exhibiting a “tangled type theory” (and also an extension of Zermelo set theory with Δ0 comprehension) which is equiconsistent with NF (for which the consistency problem seems no easier than the corresponding problem for NF (still open)), and pointing out that “tangled type theory with urelements” has a quite natural interpretation, which seems to provide an explanation for the more natural behaviour of NFU relative to the other set theories of this kind, and can be seen anachronistically as underlying Jensen's consistency proof for NFU.

scholarly journals Quotienting the delay monad by weak bisimilarity

2017 ◽  
Vol 29 (1) ◽  
pp. 67-92 ◽  
Author(s):  
JAMES CHAPMAN ◽  
TARMO UUSTALU ◽  
NICCOLÒ VELTRI
Keyword(s):  
Computer Science ◽  
Equivalence Relation ◽  
Type Theory ◽  
Partial Functions ◽  
Homotopy Type Theory ◽  
Inductive Type ◽  
Alternative Approach ◽  
The One ◽  
Axiom Of Countable Choice

The delay datatype was introduced by Capretta (Logical Methods in Computer Science, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad–a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (Extensional Constructs in Intensional Type Theory, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωcppos).Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534–549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive–inductive type is the free ωcppo on a type X essentially by definition; this allowed them to obtain a monad of free ωcppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.

Quantumness, generalized spherical 2-design, and symmetric informationally complete POVM

2007 ◽  
Vol 7 (8) ◽  
pp. 730-737
Author(s):  
I.H. Kim
Keyword(s):  
Hilbert Space ◽  
Lower Bound ◽  
Equivalence Relation ◽  
Open Problem ◽  
Natural Generalization ◽  
Quantum States ◽  
Minimal Set ◽  
Dimensional Hilbert Space

Fuchs and Sasaki defined the quantumness of a set of quantum states in \cite{Quantumness}, which is related to the fidelity loss in transmission of the quantum states through a classical channel. In \cite{Fuchs}, Fuchs showed that in $d$-dimensional Hilbert space, minimum quantumness is $\frac{2}{d+1}$, and this can be achieved by all rays in the space. He left an open problem, asking whether fewer than $d^2$ states can achieve this bound. Recently, in a different context, Scott introduced a concept of generalized $t$-design in \cite{GenSphet}, which is a natural generalization of spherical $t$-design. In this paper, we show that the lower bound on the quantumness can be achieved if and only if the states form a generalized 2-design. As a corollary, we show that this bound can be only achieved if the number of states are larger or equal to $d^2$, answering the open problem. Furthermore, we also show that the minimal set of such ensemble is Symmetric Informationally Complete POVM(SIC-POVM). This leads to an equivalence relation between SIC-POVM and minimal set of ensemble achieving minimal quantumness.

scholarly journals FRAGMENTS OF FREGE’SGRUNDGESETZEAND GÖDEL’S CONSTRUCTIBLE UNIVERSE

2016 ◽  
Vol 81 (2) ◽  
pp. 605-628 ◽  
Author(s):  
SEAN WALSH
Keyword(s):  
Set Theory ◽  
The Other ◽  
Structure Theory ◽  
Sufficient Condition ◽  
Weak Version ◽  
Power Set ◽  
Consistency Problem ◽  
Universe Of Sets ◽  
The 19Th Century ◽  
Abstraction Principles

AbstractFrege’sGrundgesetzewas one of the 19th century forerunners to contemporary set theory which was plagued by the Russell paradox. In recent years, it has been shown that subsystems of theGrundgesetzeformed by restricting the comprehension schema are consistent. One aim of this paper is to ascertain how much set theory can be developed within these consistent fragments of theGrundgesetze, and our main theorem (Theorem 2.9) shows that there is a model of a fragment of theGrundgesetzewhich defines a model of all the axioms of Zermelo–Fraenkel set theory with the exception of the power set axiom. The proof of this result appeals to Gödel’s constructible universe of sets and to Kripke and Platek’s idea of the projectum, as well as to a weak version of uniformization (which does not involve knowledge of Jensen’s fine structure theory). The axioms of theGrundgesetzeare examples ofabstraction principles, and the other primary aim of this paper is to articulate a sufficient condition for the consistency of abstraction principles with limited amounts of comprehension (Theorem 3.5). As an application, we resolve an analogue of the joint consistency problem in the predicative setting.

scholarly journals A further study on ordered regular equivalence relations in ordered semihypergroups

2018 ◽  
Vol 16 (1) ◽  
pp. 168-184 ◽  
Author(s):  
Jian Tang ◽  
Xinyang Feng ◽  
Bijan Davvaz ◽  
Xiang-Yun Xie
Keyword(s):  
Equivalence Relation ◽  
Open Problem ◽  
Equivalence Relations ◽  
Ordered Semigroups ◽  
Regular Equivalence

AbstractIn this paper, we study the ordered regular equivalence relations on ordered semihypergroups in detail. To begin with, we introduce the concept of weak pseudoorders on an ordered semihypergroup, and investigate several related properties. In particular, we construct an ordered regular equivalence relation on an ordered semihypergroup by a weak pseudoorder. As an application of the above result, we completely solve the open problem on ordered semihypergroups introduced in [B. Davvaz, P. Corsini and T. Changphas, Relationship between ordered semihypergroups and ordered semigroups by using pseuoorders, European J. Combinatorics 44 (2015), 208–217]. Furthermore, we establish the relationships between ordered regular equivalence relations and weak pseudoorders on an ordered semihypergroup, and give some homomorphism theorems of ordered semihypergroups, which are generalizations of similar results in ordered semigroups.

A construction of non-well-founded sets within Martin-Löf's type theory

1989 ◽  
Vol 54 (1) ◽  
pp. 57-64 ◽  
Author(s):  
Ingrid Lindström
Keyword(s):  
Equivalence Relation ◽  
Type Theory ◽  
Additional Condition ◽  
Complete System ◽  
Definition Of ◽  
Induction Scheme

AbstractIn this paper, we show that non-well-founded sets can be defined constructively by formalizing Hallnäs' limit definition of these within Martin-Löfs theory of types. A system is a type W together with an assignment of and to each ∝ ∈ W. We show that for any system W we can define an equivalence relation =w such that ∝ =w ß ∈ U and =w is the maximal bisimulation. Aczel's proof that CZF can be interpreted in the type V of iterative sets shows that if the system W satisfies an additional condition (*), then we can interpret CZF minus the set induction scheme in W. W is then extended to a complete system W* by taking limits of approximation chains. We show that in W* the antifoundation axiom AFA holds as well as the axioms of CFZ−.

A coherence theorem for Martin-Löf's type theory

1998 ◽  
Vol 8 (4) ◽  
pp. 413-436 ◽  
Author(s):  
MICHAEL HEDBERG
Keyword(s):  
Large Class ◽  
Equivalence Relation ◽  
Type Theory ◽  
Category Structure ◽  
Arbitrary Type ◽  
Unique Identity ◽  
Equality Relation ◽  
Coherence Theorem ◽  
Initial Category

In type theory a proposition is represented by a type, the type of its proofs. As a consequence, the equality relation on a certain type is represented by a binary family of types. Equality on a type may be conventional or inductive. Conventional equality means that one particular equivalence relation is singled out as the equality, while inductive equality – which we also call identity – is inductively defined as the ‘smallest reflexive relation’. It is sometimes convenient to know that the type representing a proposition is collapsed, in the sense that all its inhabitants are identical. Although uniqueness of identity proofs for an arbitrary type is not derivable inside type theory, there is a large class of types for which it may be proved. Our main result is a proof that any type with decidable identity has unique identity proofs. This result is convenient for proving that the class of types with decidable identities is closed under indexed sum. Our proof of the main result is completely formalized within a kernel fragment of Martin-Löf's type theory and mechanized using ALF. Proofs of auxiliary lemmas are explained in terms of the category theoretical properties of identity. These suggest two coherence theorems as the result of rephrasing the main result in a context of conventional equality, where the inductive equality has been replaced by, in the former, an initial category structure and, in the latter, a smallest reflexive relation.

An application of PER models to program extraction

1993 ◽  
Vol 3 (3) ◽  
pp. 309-331 ◽  
Author(s):  
Stefano Berardi
Keyword(s):  
Equivalence Relation ◽  
Type Theory ◽  
Lambda Calculus ◽  
Higher Order ◽  
Constructive Proof ◽  
Program Extraction ◽  
Relation Model

Type theory allows us to extract from a constructive proof that a specification is satisfiable a program that satisfies the specification. Algorithms for optimization of such programs are currently the object of research.In this paper we consider one such algorithm, which was described in Beeson (1985) and which we will call ‘Harrop’. This algorithm greatly simplifies programs extracted from proofs in the Pure Construction Calculus. We use a Partial Equivalence Relation model for higher order lambda calculus, to check that t and Harrop(t) return the same outputs from the same inputs, i.e. that they are extensionally equal.As a corollary, we show that it is correct (and, of course, useful) to replace a program t with Harrop(t). Such a correctness result has already been proved by Möhring (Möhring 1989a, 1989b) using realizability semantics, but we obtain it as a corollary of a new result, the extensional equality between t and Harrop(t). Also the semantic method we use is interesting in its own right.

Sign in / Sign up

Export Citation Format

Share Document