Some models for intuitionistic finite type arithmetic with fan functional

1977 ◽  
Vol 42 (2) ◽  
pp. 194-202 ◽  
Author(s):  
A. S. Troelstra
Keyword(s):  
Finite Type ◽  
Church’S Thesis ◽  
Proper Understanding ◽  
New Model ◽  
Fan Theorem ◽  
Church's Thesis ◽  
Definition Of ◽  
Intuitionistic Arithmetic

In this note we shall assume acquaintance with [T4] and the parts of [T1] which deal with intuitionistic arithmetic in all finite types. The bibliography just continues the bibliography of [T4].The principal purpose of this note is the discussion of two models for intuitionistic finite type arithmetic with fan functional (HAω+ MUC). The first model is needed to correct an oversight in the proof of Theorem 6 [T4, §5]: the model ECF+as defined there cannot be shown to have the required properties inEL+ QF-AC, the reason being that a change in the definition ofW12alone does not suffice—if one wishes to establish closure under the operations of HAωthe definitions ofW1σfor other σ have to be adopted as well. It is difficult to see how to do this directly in a uniform way — but we succeed via a detour, which is described in §2.For a proper understanding, we should perhaps note already here thaton the assumption of the fan theorem, ECF+as defined in [T4] and the new model of this note coincide (since then the definition ofW12[T4, p. 594] is equivalent to the definition forW12in the case of ECF); but inELit is impossible to prove this (and under assumption of Church's thesis the two models differ).

Stewart Shapiro. Introduction—intensional mathematics and constructive mathematics. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, vol. 113, North-Holland, Amsterdam, New York, and Oxford, 1985, pp. 1–10. - Stewart Shapiro. Epistemic and intuitionistic arithmetic. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 11–46. - John Myhill. Intensional set theory. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 47–61. - Nicolas D. Goodman. A genuinely intensional set theory. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 63–79. - Andrej Ščedrov. Extending Godel's modal interpretation to type theory and set theory. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 81–119. - Robert C. Flagg. Church's thesis is consistent with epistemic arithmetic. Intensional mathematics, edited by Stewart Shapiro, Studies in logic and the foundations of mathematics, pp. 121–172.

1991 ◽  
Vol 56 (4) ◽  
pp. 1496-1499 ◽  
Author(s):  
Craig A. Smoryński
Keyword(s):  
New York ◽  
Set Theory ◽  
Type Theory ◽  
Foundations Of Mathematics ◽  
Constructive Mathematics ◽  
Modal Interpretation ◽  
Church’S Thesis ◽  
Church's Thesis ◽  
Epistemic Arithmetic ◽  
Intuitionistic Arithmetic

Lifschitz' realizability

1990 ◽  
Vol 55 (2) ◽  
pp. 805-821 ◽  
Author(s):  
Jaap van Oosten
Keyword(s):  
Axiomatic Characterization ◽  
Uniqueness Condition ◽  
Church’S Thesis ◽  
Second Order Arithmetic ◽  
Elementary Analysis ◽  
Continuous Application ◽  
Church's Thesis ◽  
Order Arithmetic ◽  
Intuitionistic Arithmetic

AbstractV. Lifschitz defined in 1979 a variant of realizability which validates Church's thesis with uniqueness condition, but not the general form of Church's thesis. In this paper we describe an extension of intuitionistic arithmetic in which the soundness of Lifschitz' realizability can be proved, and we give an axiomatic characterization of the Lifschitz-realizable formulas relative to this extension. By a “q-variant” we obtain a new derived rule. We also show how to extend Lifschitz' realizability to second-order arithmetic. Finally we describe an analogous development for elementary analysis, with partial continuous application replacing partial recursive application.

Small decidable sheaves

1986 ◽  
Vol 51 (3) ◽  
pp. 726-731 ◽  
Author(s):  
Andreas Blass ◽  
Andre Scedrov
Keyword(s):  
Set Theory ◽  
Natural Numbers ◽  
Church’S Thesis ◽  
Internal Logic ◽  
Recursive Models ◽  
Fan Theorem ◽  
Church's Thesis ◽  
Divisible Hull ◽  
Constructive Algebra ◽  
Intuitionistic Set Theory

Fred Richman conjectured that the following principle is not constructive:(*) If A is a decidable subset of the set N of natural numbers and if, for every decidable subset B of N, either A ⊆ B or A ⊆ N − B, then, for some n ∈ N, A ⊆ {n}.A set A of natural numbers is called decidable if ∀n(n ∈ A ∨ ⌉ (n ∈ A)) holds. In recursive models, this agrees with the recursion-theoretic meaning of decidability. In other contexts, “complemented” and “detachable” are often used.Richman's conjecture was motivated by the problem of uniqueness of divisible hulls of abelian groups in constructive algebra. Richman showed that a countable discrete abelian p-group G has a unique (up to isomorphism over G) divisible hull if the subgroup pG is decidable. He also showed that the converse implies.We confirm the nonconstructive nature of by showing (in §1) that it is not provable in intuitionistic set theory, IZF. Thus, in the models we construct, there are countable discrete abelian p-groups G whose divisible hulls are unique but whose subgroups pG are not decidable.Our models do not satisfy further conditions imposed by Richman, namely Church's Thesis and Markov's Principle, so the full conjecture remains an open problem. We do, however, show (in §2) how to embellish our first model so that the fan theorem (i.e., compactness of 2N) fails. (Church's Thesis implies the stronger statement that the negation of the fan theorem holds.)Our models will be constructed by the method of sheaf semantics [1], [3]. That is, we shall construct Grothendieck topoi in whose internal logic fails.

Proving Church's Thesis

2000 ◽  
Vol 8 (3) ◽  
pp. 244-258 ◽  
Author(s):  
ROBERT BLACK
Keyword(s):  
Church’S Thesis ◽  
Church's Thesis

ON FINITE TYPE 3-MANIFOLD INVARIANTS I

1996 ◽  
Vol 05 (04) ◽  
pp. 441-461 ◽  
Author(s):  
STAVROS GAROUFALIDIS
Keyword(s):  
Vector Space ◽  
Finite Type ◽  
Commutative Algebra ◽  
Integral Homology ◽  
Knot Invariants ◽  
Finite Type Invariants ◽  
Definition Of ◽  
Type 3

Recently Ohtsuki [Oh2], motivated by the notion of finite type knot invariants, introduced the notion of finite type invariants for oriented, integral homology 3-spheres. In the present paper we propose another definition of finite type invariants of integral homology 3-spheres and give equivalent reformulations of our notion. We show that our invariants form a filtered commutative algebra. We compare the two induced filtrations on the vector space on the set of integral homology 3-spheres. As an observation, we discover a new set of restrictions that finite type invariants in the sense of Ohtsuki satisfy and give a set of axioms that characterize the Casson invariant. Finally, we pose a set of questions relating the finite type 3-manifold invariants with the (Vassiliev) knot invariants.

scholarly journals Reflections on Church's thesis.

1987 ◽  
Vol 28 (4) ◽  
pp. 490-498 ◽  
Author(s):  
Stephen C. Kleene
Keyword(s):  
Church’S Thesis ◽  
Church's Thesis

scholarly journals Bisimulation from Open Maps

1994 ◽  
Vol 1 (7) ◽  
Author(s):  
André Joyal ◽  
Mogens Nielsen ◽  
Glynn Winskel
Keyword(s):  
Petri Nets ◽  
Parallel Computation ◽  
Transition Systems ◽  
New Model ◽  
Event Structures ◽  
Uniform Definition ◽  
Refinement Operators ◽  
Definition Of ◽  
Open Maps

An abstract definition of bisimulation is presented. It enables a uniform definition of bisimulation across a range of different models for parallel computation presented as categories. As examples, transition systems, synchronisation trees, transition systems with independence (an abstraction from Petri nets) and labelled event structures are considered. On transition systems the abstract definition readily specialises to Milner's strong bisimulation. On event structures it explains and leads to a revision of history-preserving bisimulation of Rabinovitch and Traktenbrot, Goltz and van Glabeek. A tie-up with open maps in a (pre)topos, as they appear in the work of Joyal and Moerdijk, brings to light a promising new model, presheaves on categories of pomsets, into which the usual category of labelled event structures embeds fully and faithfully. As an indication of its promise, this new presheaf model has ``refinement'' operators, though further work is required to justify their appropriateness and understand their relation to previous attempts. The general approach yields a logic, generalising Hennessy-Milner logic, which is characteristic for the generalised notion of bisimulation.

scholarly journals Desarrollo de entornos para la creación y reproducción de Docusquemas

2005 ◽  
Author(s):  
Jesús Caudeli Tomé ◽  
José Jesús García Rueda
Keyword(s):  
Multimedia Learning ◽  
Software Tools ◽  
Web Pages ◽  
Web Browser ◽  
Multimedia Presentations ◽  
Java Applet ◽  
New Model ◽  
Written Text ◽  
Java Language ◽  
Definition Of

El Docusquema representa un nuevo modelo para construir presentaciones multimedia destinadas al aprendizaje basándose en los principios del Aprendizaje Receptivo Significativo. Este modelo otorga mayor protagonismo a la imagen y el sonido frente al texto escrito tradicional. En este proyecto se ha definido un lenguaje para describir los Docusquemas utilizando XML, y se han desarrollado dos herramientas software utilizando el lenguaje Java. La función de la primera de ellas es generar y editar Docusquemas, mientras que la segunda es un applet que permite reproducirlos a través de Internet, integrando las presentaciones en páginas web.Development of Environments for the Creation and Display of Docuschemas.AbstractDocuschemas are a new model for the construction of multimedia, learning oriented presentations based on the Meaningful Receptive Learning. This model gives a more important role to image and sound, considering traditional written text a secondary option. In this project a language for the definition of Docuschemas has been defined using XML, and two software tools have been developed using the Java language. The first one’s aim is to generate and edit Docuschemas, while the second is an a Java applet to display them in a Web browser, integrating the multimedia presentations into Web pages.

scholarly journals THE ISSUE OF THE TRANSITION TO THE DIGITAL ROUBLE

2021 ◽  
pp. 198-208
Author(s):  
Иван Владимирович Кисаров
Keyword(s):  
Monetary Policy ◽  
Point Of View ◽  
Economic Point ◽  
New Model ◽  
Digital Currency ◽  
Definition Of ◽  
Monetary Circulation

Цель статьи - рассмотреть причины и императивы перехода валюты в цифровое состояние. Дано определение цифрового рубля, его особенностей с экономической точки зрения. Указаны возможные технологические решения при внедрении цифровой валюты. Отражено возможное влияние ввода цифрового рубля на денежно-кредитную политику, а также предложен вариант внедрения новой формы рубля в экономику. Выделены необходимые качества, которым должен обладать цифровой рубль. Научная новизна заключается в акцентировании внимания на проблемах, которые могут возникнуть в связи с переходом к новой модели цифрового кредитно-денежного обращения. The purpose of the article is to consider the reasons and imperatives of the transition of the currency to a digital state. The author gives the definition of the digital rouble describes its features from an economic point of view. The research indicates possible technological solutions for digital currency implementation and possible impact of the introduction of the digital rouble on monetary policy. The author highlights some necessary qualities characteristic for a digital ruble. The scientific novelty is to focus on the problems that may arise from the transition to a new model of digital monetary circulation.

Sign in / Sign up

Export Citation Format

Share Document