scholarly journals Constructing a universe for the setoid model

2021 ◽  
pp. 1-21
Author(s):  
Thorsten Altenkirch ◽  
Simon Boulier ◽  
Ambrus Kaposi ◽  
Christian Sattler ◽  
Filippo Sestini
Keyword(s):  
Type Theory ◽  
Formal System ◽  
Model Construction ◽  
Inductive Definition ◽  
Recursive Definition

AbstractThe setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent propositions. The appeal of this model construction is that it can be constructed in a small, intensional, type theoretic metatheory, therefore giving a method to boostrap extensionality. The setoid model has been recently adapted into a formal system, namely Setoid Type Theory (SeTT). SeTT is an extension of intensional Martin-Löf type theory with constructs that give full access to the extensionality principles that hold in the setoid model.Although already a rich theory as currently defined, SeTT currently lacks a way to internalize the notion of type beyond propositions, hence we want to extend SeTT with a universe of setoids. To this aim, we present the construction of a (non-univalent) universe of setoids within the setoid model, first as an inductive-recursive definition, which is then translated to an inductive-inductive definition and finally to an inductive family. These translations from more powerful definition schemas to simpler ones ensure that our construction can still be defined in a relatively small metatheory which includes a proof-irrelevant identity type with a strong transport rule.

A proof of the cut-elimination theorem in simple type theory

1973 ◽  
Vol 38 (2) ◽  
pp. 215-226
Author(s):  
Satoko Titani
Keyword(s):  
Boolean Algebra ◽  
Type Theory ◽  
Arbitrary Number ◽  
Formal System ◽  
Cut Elimination ◽  
Simple Type ◽  
Inductive Definition ◽  
Simple Type Theory ◽  
Maximal Ideals ◽  
Definition Of

In [4], I introduced a quasi-Boolean algebra, and showed that in a formal system of simple type theory, from which the cut rule is omitted, wffs form a quasi-Boolean algebra, and that the cut-elimination theorem can be formulated in algebraic language. In this paper we use the result of [4] to prove the cut-elimination theorem in simple type theory. The theorem was proved by M. Takahashi [2] in 1967 by using the concept of Schütte's semivaluation. We use maximal ideals of a quasi-Boolean algebra instead of semivaluations.The logical system we are concerned with is a modification of Schütte's formal system of simple type theory in [1] into Gentzen style.Inductive definition of types.0 and 1 are types.If τ1, …, τn are types, then (τ1, …, τn) is a type.Basic symbols.a1τ, a2τ, … for free variables of type τ.x1τ, x2τ, … for bound variables of type τ.An arbitrary number of constants of certain types.An arbitrary number of function symbols with certain argument places.

A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS

1995 ◽  
Vol 06 (03) ◽  
pp. 203-234 ◽  
Author(s):  
YUKIYOSHI KAMEYAMA
Keyword(s):  
Type Theory ◽  
Characteristic Point ◽  
Logical Theory ◽  
Inductive Definition ◽  
Program Extraction ◽  
First Order ◽  
Inductive Definitions ◽  
Free Theory ◽  
Program Proof ◽  
Definition Of

This paper studies an extension of inductive definitions in the context of a type-free theory. It is a kind of simultaneous inductive definition of two predicates where the defining formulas are monotone with respect to the first predicate, but not monotone with respect to the second predicate. We call this inductive definition half-monotone in analogy of Allen’s term half-positive. We can regard this definition as a variant of monotone inductive definitions by introducing a refined order between tuples of predicates. We give a general theory for half-monotone inductive definitions in a type-free first-order logic. We then give a realizability interpretation to our theory, and prove its soundness by extending Tatsuta’s technique. The mechanism of half-monotone inductive definitions is shown to be useful in interpreting many theories, including the Logical Theory of Constructions, and Martin-Löf’s Type Theory. We can also formalize the provability relation “a term p is a proof of a proposition P” naturally. As an application of this formalization, several techniques of program/proof-improvement can be formalized in our theory, and we can make use of this fact to develop programs in the paradigm of Constructive Programming. A characteristic point of our approach is that we can extract an optimization program since our theory enjoys the program extraction theorem.

scholarly journals On the existence of Stone-Čech compactification

2010 ◽  
Vol 75 (4) ◽  
pp. 1137-1146 ◽  
Author(s):  
Giovanni Curi
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Natural Extension ◽  
Formal System ◽  
Topological Spaces ◽  
Completely Regular ◽  
Constructive Type Theory ◽  
Constructive Type ◽  
Constructive Set Theory ◽  
In Virtue Of

Introduction. In 1937 E. Čech and M.H. Stone, independently, introduced the maximal compactification of a completely regular topological space, thereafter called Stone-Čech compactification [8, 23]. In the introduction of [8] the non-constructive character of this result is so described: “It must be emphasized that β(S) [the Stone-Čech compactification of S] may be defined only formally (not constructively) since it exists only in virtue of Zermelo's theorem”.By replacing topological spaces with locales, Banaschewski and Mulvey [4, 5, 6], and Johnstone [14] obtained choice-free intuitionistic proofs of Stone-Čech compactification. Although valid in any topos, these localic constructions rely—essentially, as is to be demonstrated—on highly impredicative principles, and thus cannot be considered as constructive in the sense of the main systems for constructive mathematics, such as Martin-Löf's constructive type theory and Aczel's constructive set theory.In [10] I characterized the locales of which the Stone-Čech compactification can be defined in constructive type theory CTT, and in the formal system CZF+uREA+DC, a natural extension of Aczel's system for constructive set theory CZF by a strengthening of the Regular Extension Axiom REA and the principle of Dependent Choice.

Syntactical and semantical properties of simple type theory

1960 ◽  
Vol 25 (4) ◽  
pp. 305-326 ◽  
Author(s):  
Kurt Schütte
Keyword(s):  
Type Theory ◽  
Formal System ◽  
Predicate Calculus ◽  
Simple Type ◽  
Inference Rules ◽  
Positive Part ◽  
Negative Part ◽  
Simple Type Theory ◽  
Theoretical Investigations ◽  
Order Predicate Calculus

In my paper [10] I introduced the syntactical concepts “positive part” and “negative part” of logical formulas in first-order predicate calculus. These concepts make it possible to establish logical systems on inference rules similar to Gentzen's inference rules but without using the concept “sequent” and without needing Gentzen's structural inference rules. Proof-theoretical investigations of several formal systems based on positive and negative parts are published in [11]. In this paper I consider a similar formal system of simple type theory.A syntactical concept of “strict derivability” results from the formal system in [10] by generalization of the axioms and inference rules from first to higher-order predicate calculus and by addition of inference rules for set abstraction by means of a λ-symbol which allows us to form set expressions of arbitrary types from well-formed formulas.

On the axiom of extensionality – Part I

1956 ◽  
Vol 21 (1) ◽  
pp. 36-48 ◽  
Author(s):  
R. O. Gandy
Keyword(s):  
Set Theory ◽  
Type Theory ◽  
Formal System ◽  
Free Variable ◽  
Simple Theory ◽  
Predicate Calculus ◽  
Simple System ◽  
System A ◽  
Image Position

In part I of this paper it is shown that if the simple theory of types (with an axiom of infinity) is consistent, then so is the system obtained by adjoining axioms of extensionality; in part II a similar metatheorem for Gödel-Bernays set theory will be proved. The first of these results is of particular interest because type theory without the axioms of extensionality is fundamentally rather a simple system, and it should, I believe, be possible to prove that it is consistent.Let us consider — in some unspecified formal system — a typical expression of the axiom of extensionality; for example:where A(h) is a formula, and A(f), A(g) are the results of substituting in it the predicate variagles f, g for the free variable h. Evidently, if the system considered contains the predicate calculus, and if h occurs in A(h) only in parts of the form h(t) where t is a term which lies within the range of the quantifier (x), then 1.1 will be provable. But this will not be so in general; indeed, by introducing into the system an intensional predicate of predicates we can make 1.1 false. For example, Myhill introduces a constant S, where ‘Sϕψχω’ means that (the expression) ϕ is the result of substituting ψ for χ in ω.

A general formulation of simultaneous inductive-recursive definitions in type theory

2000 ◽  
Vol 65 (2) ◽  
pp. 525-549 ◽  
Author(s):  
Peter Dybjer
Keyword(s):  
Type Theory ◽  
General Notion ◽  
Recursive Definition ◽  
Restricted Version ◽  
Inductive Definitions ◽  
Simultaneous Induction ◽  
Constructive Version ◽  
Small Set ◽  
Recursive Definitions ◽  
The Way

AbstractThe first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löfs universe à la Tarski. A set U0of codes for small sets is generated inductively at the same time as a function T0, which maps a code to the corresponding small set, is defined by recursion on the way the elements of U0are generated.In this paper we argue that there is an underlyinggeneralnotion of simultaneous inductive-recursive definition which is implicit in Martin-Löf's intuitionistic type theory. We extend previously given schematic formulations of inductive definitions in type theory to encompass a general notion of simultaneous induction-recursion. This enables us to give a unified treatment of several interesting constructions including various universe constructions by Palmgren, Griffor, Rathjen, and Setzer and a constructive version of Aczel's Frege structures. Consistency of a restricted version of the extension is shown by constructing a realisability model in the style of Allen.

Type Theory and Formal Proof

2009 ◽  
Author(s):  
Rob Nederpelt ◽  
Herman Geuvers
Keyword(s):  
Type Theory ◽  
Formal Proof
Sign in / Sign up

Export Citation Format

Share Document