SEPARATING THE FAN THEOREM AND ITS WEAKENINGS II

2019 ◽  
Vol 84 (4) ◽  
pp. 1484-1509
Author(s):  
ROBERT S. LUBARSKY
Keyword(s):  
Constructive Mathematics ◽  
Kripke Models ◽  
Fan Theorem

AbstractVarieties of the Fan Theorem have recently been developed in reverse constructive mathematics, corresponding to different continuity principles. They form a natural implicational hierarchy. Earlier work showed all of these implications to be strict. Here we reprove one of the strictness results, using very different arguments. The technique used is a mixture of realizability, forcing in the guise of Heyting-valued models, and Kripke models.

scholarly journals SEPARATING THE FAN THEOREM AND ITS WEAKENINGS

2014 ◽  
Vol 79 (3) ◽  
pp. 792-813 ◽  
Author(s):  
ROBERT S. LUBARSKY ◽  
HANNES DIENER
Keyword(s):  
Constructive Mathematics ◽  
Kripke Models ◽  
Fan Theorem

AbstractVarieties of the Fan Theorem have recently been developed in reverse constructive mathematics, corresponding to different continuity principles. They form a natural implicational hierarchy. Some of the implications have been shown to be strict, others strict in a weak context, and yet others not at all, using disparate techniques. Here we present a family of related Kripke models which separates all of the as yet identified fan theorems.

How connected is the intuitionistic continuum?

1997 ◽  
Vol 62 (4) ◽  
pp. 1147-1150 ◽  
Author(s):  
Dirk Van Dalen
Keyword(s):  
Real Function ◽  
Peculiar Feature ◽  
Constructive Mathematics ◽  
Fan Theorem ◽  
First Time ◽  
Uniformly Continuous ◽  
Intuitionistic Mathematics ◽  
Excluded Middle ◽  
Do So ◽  
The Continuum

In the twenties Brouwer established the well-known continuity theorem “every real function is locally uniformly continuous,” [3, 2, 5]. From this theorem one immediately concludes that the continuum is indecomposable (unzerlegbar), i.e., if ℝ = A ∪ B and A ∩ B = ∅ (denoted by ℝ = A + B), then ℝ = A or ℝ = B.Brouwer deduced the indecomposability directly from the fan theorem (cf. the 1927 Berline Lectures, [7, p. 49]).The theorem was published for the first time in [6], it was used to refute the principle of the excluded middle: ¬∀x ∈ ℝ (x ∈ ℚ ∨ ¬x ∈ ℚ).The indecomposability of ℝ is a peculiar feature of constructive universa, it shows that ℝ is much more closely knit in constructive mathematics, than in classically mathematics. The classically comparable fact is the topological connectedness of ℝ. In a way this characterizes the position of ℝ: the only (classically) connected subsets of ℝ are the various kinds of segments. In intuitionistic mathematics the situation is different; the continuum has, as it were, a syrupy nature, one cannot simply take away one point. In the classical continuum one can, thanks to the principle of the excluded third, do so. To put it picturesquely, the classical continuum is the frozen intuitionistic continuum. If one removes one point from the intuitionistic continuum, there still are all those points for which it is unknown whether or not they belong to the remaining part.

scholarly journals BROUWER’S FAN THEOREM AND CONVEXITY

2018 ◽  
Vol 83 (04) ◽  
pp. 1363-1375 ◽  
Author(s):  
JOSEF BERGER ◽  
GREGOR SVINDLAND
Keyword(s):  
Continuous Functions ◽  
Unit Interval ◽  
Binary Sequences ◽  
Constructive Mathematics ◽  
Convexity Condition ◽  
Fan Theorem ◽  
Image Position ◽  
Uniformly Continuous ◽  
Bishop’S Constructive Mathematics

AbstractIn the framework of Bishop’s constructive mathematics we introduce co-convexity as a property of subsets B of ${\left\{ {0,1} \right\}^{\rm{*}}}$, the set of finite binary sequences, and prove that co-convex bars are uniform. Moreover, we establish a canonical correspondence between detachable subsets B of ${\left\{ {0,1} \right\}^{\rm{*}}}$ and uniformly continuous functions f defined on the unit interval such that B is a bar if and only if the corresponding function f is positive-valued, B is a uniform bar if and only if f has positive infimum, and B is co-convex if and only if f satisfies a weak convexity condition.

A type-free Gödel interpretation

1978 ◽  
Vol 43 (2) ◽  
pp. 213-227 ◽  
Author(s):  
Michael Beeson
Keyword(s):  
Present Author ◽  
Formal System ◽  
Constructive Mathematics ◽  
Kripke Models ◽  
Mathematical Content ◽  
Growing Body ◽  
Intended Interpretation ◽  
Close Relatives ◽  
Original Motivation ◽  
Intuitionistic Mathematics

In 1930, A. Heyting first specified a formal system for part of intuitionistic mathematics. Although his rules were presumably motivated by the “intended interpretation” or meaning of the logical symbols, over the years a number of other possible interpretations have been discovered for which the rules are also valid. In particular, one might mention the realizablity interpretation of Kleene, the (Dialectica) interpretation of Gödel, and various semantic interpretations, such as Kripke models. (Each of these has several variants or close relatives.) Each such interpretation can be regarded as defining precisely a certain “notion of constructivity”, the study of which may illuminate the still rather vague notions which underlie the intended interpretation; or, if one doubts that there is a single interpretation “intended” by all constructivist mathematicians, the study of precisely defined interpretations may help to delineate and distinguish the possibilities.In the last few years, Heyting's systems have been vastly extended, in order to encompass the large and growing body of constructive mathematics. Several kinds of new systems have been put forward and studied. The present author has extended the various realizability interpretations to several of these systems [B1], [B2] and drawn a number of interesting applications. The mathematical content of the present paper is an interpretation in the style of Godel's Dialectica interpretation, but applicable to the new systems put forward by Feferman [Fl]. The original motivation for this work was to obtain certain metamathematical applications: roughly speaking, Markov's rule and its variants.

scholarly journals Formula size games for modal logic and μ-calculus

2019 ◽  
Vol 29 (8) ◽  
pp. 1311-1344 ◽  
Author(s):  
Lauri T Hella ◽  
Miikka S Vilander
Keyword(s):  
Modal Logic ◽  
Optimal Strategy ◽  
Order Logic ◽  
First Order Logic ◽  
Kripke Models ◽  
First Order ◽  
Modal Operators ◽  
Crucial Difference ◽  
Definition Of ◽  
Person Game

Abstract We propose a new version of formula size game for modal logic. The game characterizes the equivalence of pointed Kripke models up to formulas of given numbers of modal operators and binary connectives. Our game is similar to the well-known Adler–Immerman game. However, due to a crucial difference in the definition of positions of the game, its winning condition is simpler, and the second player does not have a trivial optimal strategy. Thus, unlike the Adler–Immerman game, our game is a genuine two-person game. We illustrate the use of the game by proving a non-elementary succinctness gap between bisimulation invariant first-order logic $\textrm{FO}$ and (basic) modal logic $\textrm{ML}$. We also present a version of the game for the modal $\mu $-calculus $\textrm{L}_\mu $ and show that $\textrm{FO}$ is also non-elementarily more succinct than $\textrm{L}_\mu $.

A Modal Semantics of Negation in Logic Programming

1992 ◽  
Vol 16 (3-4) ◽  
pp. 231-262
Author(s):  
Philippe Balbiani
Keyword(s):  
Modal Logic ◽  
Logic Programming ◽  
Modal Logics ◽  
Kripke Models ◽  
Logic Programs ◽  
Modal Semantics ◽  
Soundness And Completeness ◽  
Modal Completion ◽  
Well Foundedness

The beauty of modal logics and their interest lie in their ability to represent such different intensional concepts as knowledge, time, obligation, provability in arithmetic, … according to the properties satisfied by the accessibility relations of their Kripke models (transitivity, reflexivity, symmetry, well-foundedness, …). The purpose of this paper is to study the ability of modal logics to represent the concepts of provability and unprovability in logic programming. The use of modal logic to study the semantics of logic programming with negation is defended with the help of a modal completion formula. This formula is a modal translation of Clack’s formula. It gives soundness and completeness proofs for the negation as failure rule. It offers a formal characterization of unprovability in logic programs. It characterizes as well its stratified semantics.

Sign in / Sign up

Export Citation Format

Share Document