An intuitionistic theory of types

1998 ◽  
Author(s):  
Per Martin-Löf
Keyword(s):  
Set Theory ◽  
Predicate Logic ◽  
Mathematical Object ◽  
Present Theory ◽  
Reflection Principle ◽  
Simple Type ◽  
Elimination Rule ◽  
Mathematical Objects ◽  
Special Cases ◽  
Intuitionistic Mathematics

The theory of types with which we shall be concerned is intended to be a full scale system for formalizing intuitionistic mathematics as developed, for example, in the book by Bishop 1967. The language of the theory is richer than the language of first order predicate logic. This makes it possible to strengthen the axioms for existence and disjunction. In the case of existence, the possibility of strengthening the usual elimination rule seems first to have been indicated by Howard 1969, whose proposed axioms are special cases of the existential elimination rule of the present theory. Furthermore, there is a reflection principle which links the generation of objects and types and plays somewhat the same role for the present theory as does the replacement axiom for Zermelo-Fraenkel set theory. An earlier, not yet conclusive, attempt at formulating a theory of this kind was made by Scott 1970. Also related, although less closely, are the type and logic free theories of constructions of Kreisel 1962 and 1965 and Goodman 1970. In its first version, the present theory was based on the strongly impredicative axiom that there is a type of all types whatsoever, which is at the same time a type and an object of that type. This axiom had to be abandoned, however, after it was shown to lead to a contradiction by Jean Yves Girard. I am very grateful to him for showing me his paradox. The change that it necessitated is so drastic that my theory no longer contains intuitionistic simple type theory as it originally did. Instead, its proof theoretic strength should be close to that of predicative analysis. Mathematical objects and their types. We shall think of mathematical objects or constructions. Every mathematical object is of a certain kind or type. Better, a mathematical object is always given together with its type, that is, it is not just an object, it is an object of a certain type.

On soft set-valued maps and integral inclusions

2021 ◽  
pp. 1-15
Author(s):  
Monairah Alansari ◽  
Shehu Shagari Mohammed ◽  
Akbar Azam
Keyword(s):  
Fixed Point ◽  
Set Theory ◽  
Fuzzy Set Theory ◽  
Fixed Point Theorems ◽  
Soft Set ◽  
Mathematical Tool ◽  
Multivalued Maps ◽  
Soft Sets ◽  
Special Cases ◽  
New Development

As an improvement of fuzzy set theory, the notion of soft set was initiated as a general mathematical tool for handling phenomena with nonstatistical uncertainties. Recently, a novel idea of set-valued maps whose range set lies in a family of soft sets was inaugurated as a significant refinement of fuzzy mappings and classical multifunctions as well as their corresponding fixed point theorems. Following this new development, in this paper, the concepts of e-continuity and E-continuity of soft set-valued maps and αe-admissibility for a pair of such maps are introduced. Thereafter, we present some generalized quasi-contractions and prove the existence of e-soft fixed points of a pair of the newly defined non-crisp multivalued maps. The hypotheses and usability of these results are supported by nontrivial examples and applications to a system of integral inclusions. The established concepts herein complement several fixed point theorems in the framework of point-to-set-valued maps in the comparable literature. A few of these special cases of our results are highlighted and discussed.

scholarly journals Final coalgebras as greatest fixed points in ZF set theory

1999 ◽  
Vol 9 (5) ◽  
pp. 545-567 ◽  
Author(s):  
LAWRENCE C. PAULSON
Keyword(s):  
Fixed Points ◽  
Set Theory ◽  
Theorem Prover ◽  
Infinite Length ◽  
Special Cases ◽  
Definition Of ◽  
Recursive Definitions ◽  
Ordered Pairs

A special final coalgebra theorem, in the style of Aczel (1988), is proved within standard Zermelo–Fraenkel set theory. Aczel's Anti-Foundation Axiom is replaced by a variant definition of function that admits non-well-founded constructions. Variant ordered pairs and tuples, of possibly infinite length, are special cases of variant functions. Analogues of Aczel's solution and substitution lemmas are proved in the style of Rutten and Turi (1993). The approach is less general than Aczel's, but the treatment of non-well-founded objects is simple and concrete. The final coalgebra of a functor is its greatest fixedpoint.Compared with previous work (Paulson, 1995a), iterated substitutions and solutions are considered, as well as final coalgebras defined with respect to parameters. The disjoint sum construction is replaced by a smoother treatment of urelements that simplifies many of the derivations.The theory facilitates machine implementation of recursive definitions by letting both inductive and coinductive definitions be represented as fixed points. It has already been applied to the theorem prover Isabelle (Paulson, 1994).

Epistemic set theory is a conservative extension of intuitionistic set theory

1985 ◽  
Vol 50 (4) ◽  
pp. 895-902 ◽  
Author(s):  
R. C. Flagg
Keyword(s):  
Set Theory ◽  
Affirmative Answer ◽  
Conservative Extension ◽  
Successful Program ◽  
Power Set ◽  
Epistemic Notion ◽  
Intuitionistic Mathematics ◽  
Topological Boolean Algebra ◽  
Faithful Interpretation ◽  
Intuitionistic Set Theory

In [6] Gödel observed that intuitionistic propositional logic can be interpreted in Lewis's modal logic (S4). The idea behind this interpretation is to regard the modal operator □ as expressing the epistemic notion of “informal provability”. With the work of Shapiro [12], Myhill [10], Goodman [7], [8], and Ščedrov [11] this simple idea has developed into a successful program of integrating classical and intuitionistic mathematics.There is one question quite central to the above program that has remained open. Namely:Does Ščedrov's extension of the Gödel translation to set theory provide a faithful interpretation of intuitionistic set theory into epistemic set theory?In the present paper we give an affirmative answer to this question.The main ingredient in our proof is the construction of an interpretation of epistemic set theory into intuitionistic set theory which is inverse to the Gödel translation. This is accomplished in two steps. First we observe that Funayama's theorem is constructively provable and apply it to the power set of 1. This provides an embedding of the set of propositions into a complete topological Boolean algebra . Second, in a fashion completely analogous to the construction of Boolean-valued models of classical set theory, we define the -valued universe V(). V() gives a model of epistemic set theory and, since we use a constructive metatheory, this provides an interpretation of epistemic set theory into intuitionistic set theory.

Elastic Fields in Double Inhomogeneity by the Equivalent Inclusion Method

2000 ◽  
Vol 68 (1) ◽  
pp. 3-10 ◽  
Author(s):  
H. M. Shodja ◽  
A. S. Sarvestani
Keyword(s):  
Elastic Constants ◽  
Present Method ◽  
Present Theory ◽  
Actual Distribution ◽  
Equivalent Inclusion Method ◽  
Inclusion Method ◽  
Ellipsoidal Inhomogeneity ◽  
Equivalent Inclusion ◽  
Comparison Results ◽  
Special Cases

Consider a double-inhomogeneity system whose microstructural configuration is composed of an ellipsoidal inhomogeneity of arbitrary elastic constants, size, and orientation encapsulated in another ellipsoidal inhomogeneity, which in turn is surrounded by an infinite medium. Each of these three constituents in general possesses elastic constants different from one another. The double-inhomogeneity system under consideration is subjected to far-field strain (stress). Using the equivalent inclusion method (EIM), the double inhomogeneity is replaced by an equivalent double-inclusion (EDI) problem with proper polynomial eigenstrains. The double inclusion is subsequently broken down to single-inclusion problems by means of superposition. The present theory is the first to obtain the actual distribution rather than the averages of the field quantities over the double inhomogeneity using Eshelby’s EIM. The present method is precise and is valid for thin as well as thick layers of coatings, and accommodates eccentric heterogeneity of arbitrary size and orientation. To establish the accuracy and robustness of the present method and for the sake of comparison, results on some of the previously reported problems, which are special cases encompassed by the present theory, will be re-examined. The formulations are easily extended to treat multi-inhomogeneity cases, where an inhomogeneity is surrounded by many layers of coatings. Employing an averaging scheme to the present theory, the average consistency conditions reported by Hori and Nemat-Nasser for the evaluation of average strains and stresses are recovered.

scholarly journals MODAL STRUCTURALISM AND REFLECTION

2018 ◽  
Vol 12 (4) ◽  
pp. 823-860 ◽  
Author(s):  
SAM ROBERTS
Keyword(s):  
Set Theory ◽  
Reflection Principle ◽  
Reflection Principles

AbstractModal structuralism promises an interpretation of set theory that avoids commitment to abstracta. This article investigates its underlying assumptions. In the first part, I start by highlighting some shortcomings of the standard axiomatisation of modal structuralism, and propose a new axiomatisation I call MSST (for Modal Structural Set Theory). The main theorem is that MSST interprets exactly Zermelo set theory plus the claim that every set is in some inaccessible rank of the cumulative hierarchy. In the second part of the article, I look at the prospects for supplementing MSST with a modal structural reflection principle, as suggested in Hellman (2015). I show that Hellman’s principle is inconsistent (Theorem 5.32), and argue that modal structural reflection principles in general are either incompatible with modal structuralism or extremely weak.

scholarly journals A Theory of Mathematical Objects as a Prototype of Set Theory

1962 ◽  
Vol 20 ◽  
pp. 105-168 ◽  
Author(s):  
Katuzi Ono
Keyword(s):  
Set Theory ◽  
Axiom Of Choice ◽  
Simple System ◽  
Object Theory ◽  
Mathematical Objects ◽  
Axiom Scheme ◽  
The Axiom Of Choice ◽  
Primitive Notion

The theory of mathematical objects, developed in this work, is a trial system intended to be a prototype of set theory. It concerns, with respect to the only one primitive notion “proto-membership”, with a field of mathematical objects which we shall hereafter simply call objects, it is a very simple system, because it assumes only one axiom scheme which is formally similar to the aussonderung axiom of set theory. We shall show that in our object theory we can construct a theory of sets which is stronger than the Zermelo set-theory [1] without the axiom of choice.

Exploded Points

1981 ◽  
Vol 36 (1) ◽  
pp. 72-75
Author(s):  
Okan Gurel
Keyword(s):  
Lorenz System ◽  
Stability Index ◽  
Mathematical Object ◽  
Recursive Formula ◽  
Functional Characteristics ◽  
Mathematical Objects ◽  
The Lorenz System ◽  
Definition Of

A new concept of a mathematical object of zero dimension, an exploded point, is introduced. The dimension used is defined on the basis of the functional characteristics of the system, thus it may be referred to as f-dimension. A stability index is also defined for the mathematical objects including exploded points, which can be related to the f-dimension. It is shown that the mathematical object exhibited by the Lorenz system after the second bifurcation is such a point. A recursive formula based on the definition of the exploded point

The distribution of stress and velocity in glaciers and ice-sheets

1957 ◽  
Vol 239 (1216) ◽  
pp. 113-133 ◽  
Keyword(s):  
Steady Flow ◽  
Longitudinal Velocity ◽  
Present Theory ◽  
Surface Velocity ◽  
General Flow ◽  
Glacier Valley ◽  
Compressive Flow ◽  
Special Cases ◽  
Flow Law ◽  
Distribution Of Stress

A block of ice resting upon a rough slope forms a theoretical model of a glacier or an ice-sheet, the sides of the glacier valley being ignored. Previous papers have described two types of steady flow in this model: ( a ) laminar flow, in which the longitudinal velocity gradient r is zero, and ( b ) extending or compressive flow, in which r is non-zero, ( a ) was derived under the assumption of a general flow law for ice, but ( b ) was only derived under the assumption of perfect plasticity. In the present paper a general flow law is used throughout, and the equations for steady flow, with r allowed to be non-zero, are found. The previous results ( a ) and ( b ) appear as special cases. Possible variations of density, temperature or flow law with depth are allowed for. If the density and the flow law are known as functions of depth in any region, and if the surface slope, the surface velocity, and the value of r are known, the equations give the stresses and velocity as functions of depth. The borehole experiment on the Jungfraufirn (1948-50) allows an experimental test. From the observed value of r , and Glen’s laboratory flow law for ice, a theoretical curve for the result of the experiment is calculated which is compared with the experimental curve. At a depth of 50 m the effect of ignoring r , as has been done hitherto, is to underestimate the shear rate by a factor of 50; on the present theory it is overestimated by a factor of 1∙33. The remaining discrepancy is probably mainly due to the effect of the glacier sides.

On a set theory of bernays

1967 ◽  
Vol 32 (3) ◽  
pp. 319-321 ◽  
Author(s):  
Leslie H. Tharp
Keyword(s):  
Set Theory ◽  
Free Variable ◽  
Reflection Principle ◽  
Formal Definition ◽  
Von Neumann ◽  
Starting Point ◽  
Definition Of ◽  
Image Position

We are concerned here with the set theory given in [1], which we call BL (Bernays-Levy). This theory can be given an elegant syntactical presentation which allows most of the usual axioms to be deduced from the reflection principle. However, it is more convenient here to take the usual Von Neumann-Bernays set theory [3] as a starting point, and to regard BL as arising from the addition of the schema where S is the formal definition of satisfaction (with respect to models which are sets) and ┌φ┐ is the Gödel number of φ which has a single free variable X.

Electron energy distributions in uniform electric fields and the Townsend ionization coefficient

1958 ◽  
Vol 244 (1237) ◽  
pp. 166-185 ◽  
Keyword(s):  
Differential Equation ◽  
Cross Section ◽  
Electric Fields ◽  
Cross Sections ◽  
Collision Cross Section ◽  
Present Theory ◽  
Uniform Electric Field ◽  
Ionization Coefficient ◽  
Special Cases ◽  
Wide Range

The second-order differential equation which expresses the equilibrium condition of an electron swarm in a uniform electric field in a gas, the electrons suffering both elastic and inelastic collisions with the gas molecules, is solved by the Jeffreys or W.K.B. method of approximation. The distribution function F(ε) of electrons of energy ε is obtained immediately in a general form involving the elastic and inelastic collision cross-sections and without any restriction on the range of E/p (electric strength/gas pressure) save that introduced in the original differential equation. In almost all applications the approximation is likely to be of high accuracy, and easy to use. Several of the earlier derivations of F(ε) are obtained as special cases. Using the function F(ε) an attempt is made to relate the Townsend ionization coefficient a to the properties of the gas in a more general manner than hitherto, using realistic functions for the collision cross-section. It is finally expressed by the equation α/ p = A exp ( — Bp/E ) in which A and B are functions involving the properties of the gas and the ratio E/p . The important coefficient B is directly related to the form and magnitude of the total inelastic cross-section below the ionization potential and can be evaluated for a particular gas once the cross-section is known experimentally. The present theory shows clearly the influence of E/p on both A and B, a matter which has not been satisfactorily discussed previously. The theory is illustrated by calculations of F (ε) and a/p for hydrogen over a range of E/p from 10 to 1000. The agreement between the calculated results and recent reliable observations of α/ p is surprisingly good considering the nature of the calculations and the wide range of E/p .

Sign in / Sign up

Export Citation Format

Share Document