INTUITIONISTIC ANALYSIS AT THE END OF TIME

2017 ◽  
Vol 23 (3) ◽  
pp. 279-295 ◽  
Author(s):  
JOAN RAND MOSCHOVAKIS
Keyword(s):  
Formal System ◽  
Choice Sequence ◽  
Definite Sequence ◽  
Image Position

AbstractKripke recently suggested viewing the intuitionistic continuum as an expansion in time of a definite classical continuum. We prove the classical consistency of a three-sorted intuitionistic formal system IC, simultaneously extending Kleene’s intuitionistic analysis I and a negative copy C° of the classically correct part of I, with an “end of time” axiom ET asserting that no choice sequence can be guaranteed not to be pointwise equal to a definite (classical or lawlike) sequence. “Not every sequence is pointwise equal to a definite sequence” is independent of IC. The proofs are by Crealizability interpretations based on classical ω-models ${\cal M}$ = $\left( {\omega ,{\cal C}} \right)$ of C°.

scholarly journals On choice sequences determined by spreads

1984 ◽  
Vol 49 (3) ◽  
pp. 908-916 ◽  
Author(s):  
Gerrit van der Hoeven ◽  
Ieke Moerdijk
Keyword(s):  
Formal System ◽  
Formal Theory ◽  
Restricted Class ◽  
Continuous Choice ◽  
Choice Sequence ◽  
Finite Sequences ◽  
The Moment ◽  
Basic Axiom ◽  
Image Position ◽  
Do So

From the moment choice sequences appear in Brouwer's writings, they do so as elements of a spread. This led Kreisel to take the so-called axiom of spreaddata as the basic axiom in a formal theory of choice sequences (Kreisel [1965, pp. 133–136]). This axiom expresses the idea that to be given a choice sequence means to be given a spread to which the choice sequence belongs. Subsequently, however, it was discovered that there is a formal clash between this axiom and closure of the domain of choice sequences under arbitrary (lawlike) continuous operations (Troelstra [1968]). For this reason, the formal system CS was introduced (Kreisel and Troelstra [1970]), in which spreaddata is replaced by analytic data. In this system CS, the domain of choice sequences is closed under all continuous operations, and therefore it provides a workable basis for intuitionistic analysis. But the problem whether the axiom of spreaddata is compatible with closure of the domain of choice sequences under the continuous operations from a restricted class, which is still rich enough to validate the typical axioms of continuous choice, remained open. It is precisely this problem that we aim to discuss in this paper.Recall that a spread is a (lawlike, inhabited) decidable subtree S of the tree N< N of all finite sequences, having all branches infinite:

Positive Definite Sequence of Operators and a Fixed Point Theorem

1972 ◽  
Vol 15 (2) ◽  
pp. 295-295
Author(s):  
A. T. Dash
Keyword(s):  
Hilbert Space ◽  
Fixed Point ◽  
Fixed Point Theorem ◽  
Point Theorem ◽  
Positive Definite ◽  
Definite Sequence ◽  
Positive Definite Sequence ◽  
Image Position

The purpose of this note is to prove the following:Theorem. Let {An} be a positive definite sequence of operators on a Hilbert space H with A0=1. If A1f=f for some f in H, then Anf=f for all n.Note that a bilateral sequence of operators {An:n = 0, ±1, ±2,…} on H is positive definite iffor every finitely nonzero sequence {fn} of vectors in H [1].

MARKOV’S PRINCIPLE AND SUBSYSTEMS OF INTUITIONISTIC ANALYSIS

2019 ◽  
Vol 84 (02) ◽  
pp. 870-876
Author(s):  
JOAN RAND MOSCHOVAKIS
Keyword(s):  
Formal System ◽  
Analytical Form ◽  
Image Position

AbstractUsing a technique developed by Coquand and Hofmann [3] we verify that adding the analytical form MP1: $\forall \alpha (\neg \neg \exists {\rm{x}}\alpha ({\rm{x}}) = 0 \to \exists {\rm{x}}\alpha ({\rm{x}}) = 0)$ of Markov’s Principle does not increase the class of ${\rm{\Pi }}_2^0$ formulas provable in Kleene and Vesley’s formal system for intuitionistic analysis, or in subsystems obtained by omitting or restricting various axiom schemas in specified ways.

The permutability of rules in the classical inferential calculus

1952 ◽  
Vol 17 (4) ◽  
pp. 245-248 ◽  
Author(s):  
Haskell B. Curry
Keyword(s):  
Formal System ◽  
Underlying Theory ◽  
Finite Sequences ◽  
Image Position ◽  
Single Proposition

We consider any set of Gentzen-type rules in a formal system of the following sort. The terms of the system are propositions, generally to be thought of as the propositions of some underlying theory. The elementary statements are of the formwhere and are finite sequences of propositions and (1) expresses a relation, called entailment, between such sequences. These sequences will be called prosequences; they may be void, or consist of a single proposition; and they may contain repetitions of the same proposition. The members of a prosequence will be called its constituents. Two prosequences which are permutations of one another will be regarded as the same. Prosequences will be designated by German letters, single propositions by Latin ones.The rules of the system are to be of the following form:This notation is to be understood as indicating p premises and a conclusion, each of the form (1). The constituents of and occur in all premises and conclusion; they are called the parametric constituents, or simply the parameters, of the inference.

The gergonne relations

1955 ◽  
Vol 20 (3) ◽  
pp. 207-231 ◽  
Author(s):  
J. A. Faris
Keyword(s):  
Necessary Conditions ◽  
Formal System ◽  
Class Relations ◽  
French Mathematician ◽  
Sufficient And Necessary Conditions ◽  
Image Position

In this paper I am going to set forth a formal system based on five inter-class relations. These relations exist respectively between a class of a's and a class of b's.(i) if and only if every a is a b and every b is an a,(ii) if and only if every a is a b and not every b is an a,(iii) if and only if it is not the case that either every a is a b or every b is an a or no a is a b,(iv) if and only if every b is an a and not every a is a b,(v) if and only if no a is a b.These relations between classes, which correspond, as will be seen, to the five relations between two circles a and b shown in the well-known Eulerian diagrams,are of course connected in an intimate way with the four forms of proposition, A, E, I, O, of the traditional syllogistic logic. The French mathematician, J. D. Gergonne, seems to have been the first to recognize these relations explicitly and to understand their importance in syllogistic theory. It is therefore appropriate that they should be called by his name.Gergonne first of all showed with reference to these relations what are the sufficient and necessary conditions of the truth of propositions of each of the four traditional forms: for example, an A proposition, ‘All a is b’ is true if and only if either the first or the second relation exists between the class of a's and the class of b's.

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 ω.

Logics without the contraction rule

1985 ◽  
Vol 50 (1) ◽  
pp. 169-201 ◽  
Author(s):  
Hiroakira Ono ◽  
Yuichi Komori
Keyword(s):  
Intuitionistic Logic ◽  
Formal System ◽  
The Other ◽  
Promising Tool ◽  
Nonclassical Logics ◽  
Relevant Logics ◽  
Exchange Rule ◽  
Distributive Law ◽  
Image Position ◽  
Partially Ordered Monoids

We will study syntactical and semantical properties of propositional logics weaker than the intuitionistic, in which the contraction rule (or, the exchange rule or the weakening rule, in some cases) does not hold. Here, the contraction rule means the rule of inference of the formif we formulate our logics in a Gentzen-type formal system. Some syntactical properties of these logics have been studied firstly by the second author in [11], in connection with the study of BCK-algebras (for information on BCK-algebras, see [9]). There, it turned out that such a syntactical method is a powerful and promising tool in studying BCK-algebras. Using this method, considerable progress has been made since then (see, e.g., [8], [18], [27]).In this paper, we will study these logics more comprehensively. We notice here that the distributive lawdoes not hold necessarily in these logics. By adding some axioms (or initial sequents) and rules of inference to these basic logics, we can obtain a lot of interesting nonclassical logics such as Łukasiewicz's many-valued logics, relevant logics, the intuitionistic logic and logics related to BCK-algebras, which have been studied separately until now. Thus, our approach will give a uniform way of dealing with these logics. One of our two main tools in doing so is Gentzen-type formulation of logics in syntax, and the other is semantics defined by using partially ordered monoids.

A note on Mathematics of infinity

1993 ◽  
Vol 58 (4) ◽  
pp. 1195-1200 ◽  
Author(s):  
Erik Palmgren
Keyword(s):  
Intuitionistic Logic ◽  
Type Theory ◽  
Natural Numbers ◽  
Disjunction Property ◽  
Recursive Functions ◽  
Choice Sequence ◽  
Heyting Arithmetic ◽  
Image Position

In the paper Mathematics of infinity, Martin-Löf extends his intuitionistic type theory with fixed “choice sequences”. The simplest, and most important instance, is given by adding the axiomsto the type of natural numbers. Martin-Löf's type theory can be regarded as an extension of Heyting arithmetic (HA). In this note we state and prove Martin-Löf's main result for this choice sequence, in the simpler setting of HA and other arithmetical theories based on intuitionistic logic (Theorem A). We also record some remarkable properties of the resulting systems; in general, these lack the disjunction property and may or may not have the explicit definability property. Moreover, they represent all recursive functions by terms.

On derivability

1937 ◽  
Vol 2 (3) ◽  
pp. 113-119 ◽  
Author(s):  
W. V. Quine
Keyword(s):  
Formal System ◽  
Free Variable ◽  
The Other ◽  
Free Variables ◽  
Image Position ◽  
Positive Integers

1. The notion of derivability. Italic capitals, with or without subscripts, will be used as variables. They are to take as values some manner of elements which may for the present be left undetermined. Now let us consider abstractly the notion of the derivability of an element X from one or more specified elements by a series of steps of a specified kind. This involves reference to two conditions upon elements. One of these conditions, expressible by some statement form containing a single free variable, determines the elements from which X is said to be derivable. The other condition, expressed say by a statement form containing k + 1 free variables, determines the kind of steps by which the derivation is to proceed; it is the condition which any elements Z1, … Zk, Y must fulfill if progress from Zi, …, Zk to Y is to constitute a step of derivation in the intended sense. Supposing “f(Y)” supplanted by the first of these statement forms, whatever it may be, and “g(Z1, …, Zk, Y)” supplanted by the other, let us adopt the form of notationto express derivability of X in the suggested sense. The meaning of (1) can be formulated more accurately as follows:(i) There are elements Y1 to Ym (for some m) such that Ym = X and, for each i≦m, either f(Yi) or else there are numbers j1 to Ym, each less than i, for which g(Yj1, …, Yjk, Yi).(Variable subscripts are to be understood, here and throughout the paper, as referring only to positive integers.)The notion (1) is illustrated in the ancestral R* of a relation R;1 for,Another illustration is afforded by metamathematics. Suppose our elements are the expressions used in some formal system; suppose we have defined “Post(Y)”, meaning that Y is a postulate of that system; and suppose we have defined “Inf(ZI, …, Zk, Y)” (for some fixed k large enough for all purposes of the system in question), meaning that Y proceeds from Z1, …, Zk by one application of one or another of the rules of inference of the system. Thenwould mean that X is a theorem of the system.

Simple Identification of Electron Diffraction Ring Patterns

1969 ◽  
Vol 27 ◽  
pp. 160-161
Author(s):  
Carolyn Nohr ◽  
Ann Ayres
Keyword(s):  
Electron Microscope ◽  
Electron Diffraction ◽  
Diffraction Ring ◽  
Image Position

Texts on electron diffraction recommend that the camera constant of the electron microscope be determine d by calibration with a standard crystalline specimen, using the equation

Sign in / Sign up

Export Citation Format

Share Document