Search

This paper addresses the long-standing question of the predicativity of the Mahlo universe. A solution, called the extended predicative Mahlo universe, has been proposed by Kahle and Setzer in the context of explicit mathematics. It makes use of the collection of untyped terms (denoting partial functions) which are directly available in explicit mathematics but not in Martin-Löf type theory. In this paper, we overcome the obstacle of not having direct access to untyped terms in Martin-Löf type theory by formalizing explicit mathematics with an extended predicative Mahlo universe in Martin-Löf type theory with certain indexed inductive-recursive definitions. In this way, we can relate the predicativity question to the fundamental semantics of Martin-Löf type theory in terms of computation to canonical form. As a result, we get the first extended predicative definition of a Mahlo universe in Martin-Löf type theory. To this end, we first define an external variant of Kahle and Setzer's internal extended predicative universe in explicit mathematics. This is then formalized in Martin-Löf type theory, where it becomes an internal extended predicative Mahlo universe. Although we make use of indexed inductive-recursive definitions that go beyond the type theory |$\mathbf {IIRD}$| of indexed inductive-recursive definitions defined in previous work by the authors, we argue that they are constructive and predicative in Martin-Löf's sense. The model construction has been type-checked in the proof assistant Agda. [ABSTRACT FROM AUTHOR]

There are several classical characterisations of the valuative dimension of a commutative ring. Constructive versions of this dimension have been given and proven to be equivalent to the classical notion within classical mathematics, and they can be used for the usual examples of commutative rings. To the contrary of the classical versions, the constructive versions have a clear computational content. This paper investigates the computational relationship between three possible constructive definitions of the valuative dimension of a commutative ring. In doing so, it proves these constructive versions to be equivalent within constructive mathematics. [ABSTRACT FROM AUTHOR]

While modern computers are fast, there are still many practical problems that require even faster computers. It turns out that on the fundamental level, one of the main factors limiting computation speed is the fact that, according to modern physics, the speed of all processes is limited by the speed of light. Good news is that while the corresponding limitation is very severe in Euclidean geometry, it can be more relaxed in (at least some) non-Euclidean spaces, and, according to modern physics, the physical space is not Euclidean. The differences from Euclidean character are especially large on micro-level, where quantum effects need to be taken into account. To analyze how we can speed up computations, it is desirable to reconstruct the actual distance values – corresponding to all possible paths – from the values that we actually measure – which correspond only to macro-paths and thus, provide only the upper bound for the distance. In our previous papers – including our joint paper with Victor Selivanov – we provided an explicit formula for such a reconstruction. But for this formula to be useful, we need to analyze how algorithmic is this reconstructions. In this paper, we show that while in general, no reconstruction algorithm is possible, an algorithm is possible if we impose a lower limit on the distances between steps in a path. So, hopefully, this can help to eventually come up with faster computations. [ABSTRACT FROM AUTHOR]

We study the properties of the constructive linear programming problems. The parameters of linear functions in such problems are constructive real numbers. Solving such a problem involves finding the optimal plan with the constructive real number components. We show that it is impossible to have an algorithm that solves an arbitrary constructive real programming problem. [ABSTRACT FROM AUTHOR]

We study the two algebras of complemented subsets that were introduced in the constructive development of the Daniell approach to measure and integration within Bishop-style constructive mathematics. We present their main properties both for the so-called here categorical complemented subsets and for the extensional complemented subsets. We translate constructively the classical bijection between subsets and Boolean-valued, total functions by establishing a bijection between complemented subsets (categorical or extensional) and Boolean-valued, partial functions (categorical or extensional). The role of Myhill’s axiom of non-choice in the equivalence between categorical and extensional subsets is discussed. We introduce swap algebras of type (I) and (II) as an abstract version of Bishop’s algebras of complemented subsets of type (I) and (II), respectively, and swap rings as an abstract version of the structure of Boolean-valued partial functions on a set. Our examples of swap algebras and swap rings together with the included here results indicate that their theory is a certain generalisation of the theory of Boolean algebras and Boolean rings, a fact which we find interesting both from a constructive and a classical point of view. [ABSTRACT FROM AUTHOR]

The article provides a review of the book "Critical Mathematics Education" by Ole Skovsmose, which offers a unique perspective on mathematics education. Skovsmose emphasizes the importance of mathematics as a practice and explores the concepts of hope and social justice in critical mathematics education. The book also discusses the role of real-world problem areas as learning contexts and the idea of risk in mathematical modeling. It delves into the reasons behind low achievement in mathematics and students' lack of interest, arguing that learning should be an active process influenced by social, political, and economic factors. The book introduces new concepts and analyses, drawing on philosophers to offer a philosophy of critical mathematics education that considers power, positioning, and pedagogy. It also explores the ethics of mathematics and the impact of mathematics on society. The book concludes with a personal story from the author's experiences, highlighting the global need for critical mathematics education. [Extracted from the article]

The Workshop ‘Mathematical Logic: Proof Theory, Constructive Mathematics’ focused on proof-theoretic research on the foundations of mathematics, on the extraction of explicit computational content from given proofs in core areas of ordinary mathematics using proof-theoretic methods as well as on topics in proof complexity. The workshop contributed to the following research strands: • Interactions between foundations and applications. • Proof mining. • Constructive and semi-constructive reasoning. • Proof theory and theoretical computer science. • Structural proof theory. [ABSTRACT FROM AUTHOR]

Semi-unification is the combination of first-order unification and first-order matching. The undecidability of semi-unification has been proven by Kfoury, Tiuryn, and Urzyczyn in the 1990s by Turing reduction from Turing machine immortality (existence of a diverging configuration). The particular Turing reduction is intricate, uses noncomputational principles, and involves various intermediate models of computation. The present work gives a constructive many-one reduction from the Turing machine halting problem to semi-unification. This establishes RE-completeness of semi-unification under many-one reductions. Computability of the reduction function, constructivity of the argument, and correctness of the argument is witnessed by an axiom-free mechanization in the Coq proof assistant. Arguably, this serves as comprehensive, precise, and surveyable evidence for the result at hand. The mechanization is incorporated into the existing, wellmaintained Coq library of undecidability proofs. Notably, a variant of Hooper's argument for the undecidability of Turing machine immortality is part of the mechanization. [ABSTRACT FROM AUTHOR]

We study the properties of the constructive linear programming problems. The parameters of linear functions in such problems are constructive real numbers. Solving such a problem involves finding the optimal plan with the constructive real number components. We show that it is impossible to have an algorithm that solves an arbitrary constructive real programming problem.

In the context of constructive reverse mathematics, we show that weak Kőnig's lemma (WKL$\mathsf {WKL}$) implies that every pointwise continuous function f:[0,1]→R$f : [0,1]\rightarrow \mathbb {R}$ is induced by a code in the sense of reverse mathematics. This, combined with the fact that WKL$\mathsf {WKL}$ implies the Fan theorem, shows that WKL$\mathsf {WKL}$ implies the uniform continuity theorem: every pointwise continuous function f:[0,1]→R$f : [0,1]\rightarrow \mathbb {R}$ has a modulus of uniform continuity. Our results are obtained in Heyting arithmetic in all finite types with quantifier‐free axiom of choice. [ABSTRACT FROM AUTHOR]

In this paper, we consider a constructive proof of the termination of the normal form (NF) algorithm for multivariate polynomials, as well as the related concept of admissible ordering < on monomials. In classical mathematics, the well-quasiorder property of relation < is derived from Dickson's lemma, and this is sufficient to justify the termination of the NF algorithm. In provable programming based on constructive type theory (Coq and Agda), a somewhat stronger condition (in constructive mathematics) of the well-foundedness of the ordering (in its constructive version) is required. We propose a constructive proof of this theorem (T) for < , which is based on a known method that we refer to here as the "pattern method." This theorem on the well-foundedness of an arbitrary admissible ordering is also important in itself, independently of the NF algorithm. We are not aware of any other works on constructive proof of this theorem. However, it turns out that it follows, not very difficultly, from the results achieved by other researchers in 2003. We program this proof in the Agda language in the form of our library AdmissiblePPO-wellFounded of provable computational algebra programs. This development also uses the theorem to prove termination of the NF algorithm for polynomials. Thus, the library also contains a set of provable programs for polynomial algebra, which is significantly larger than that needed to prove Theorem T. [ABSTRACT FROM AUTHOR]

Working constructively, we study continuous directed complete posets (dcpos) and the Scott topology. Our two primary novelties are a notion of intrinsic apartness and a notion of sharp elements. Being apart is a positive formulation of being unequal, similar to how inhabitedness is a positive formulation of nonemptiness. To exemplify sharpness, we note that a lower real is sharp if and only if it is located. Our first main result is that for a large class of continuous dcpos, the Bridges–Vîţǎ apartness topology and the Scott topology coincide. Although we cannot expect a tight or cotransitive apartness on nontrivial dcpos, we prove that the intrinsic apartness is both tight and cotransitive when restricted to the sharp elements of a continuous dcpo. These include the strongly maximal elements, as studied by Smyth and Heckmann. We develop the theory of strongly maximal elements highlighting its connection to sharpness and the Lawson topology. Finally, we illustrate the intrinsic apartness, sharpness, and strong maximality by considering several natural examples of continuous dcpos: the Cantor and Baire domains, the partial Dedekind reals, the lower reals and, finally, an embedding of Cantor space into an exponential of lifted sets. [ABSTRACT FROM AUTHOR]

This work presents game semantics of Martin-Löf type theory (MLTT) equipped with the One, the Zero, the N, Pi, Sigma and Id types. Game semantics interprets a wide range of logic and computation, even the polymorphic $\lambda$ -calculus; however, it has remained a well-known challenge in the past 25 years to achieve game semantics of dependent type theories such as MLTT, and past attempts lack directness or generality. For instance, the approach taken by Abramsky et al. interprets Sigma types indirectly by formal lists, not by games, making an interpretation of universes hopeless, and it is limited to a very specific class of dependent types. The difficulty of this challenge comes from a conflict between the extensionality of dependent types and the intensionality of game semantics. We overcome the challenge by inventing a novel variant of games, while we keep strategies unchanged, in such a way that this variant inherits the strong points of conventional game semantics. Also, our method enables an interpretation of subtyping on dependent types for the first time as game semantics. We finally give a new, game-semantic proof of the independence of Markov's principle from MLTT. This proof illustrates an advantage of our intensional model over extensional ones such as Hyland's effective topos. [ABSTRACT FROM AUTHOR]

Infinite Gray code has been introduced by Tsuiki [Ts02] as a redundancyfree representation of the reals. In applications the signed digit representation is mostly used which has maximal redundancy. Tsuiki presented a functional program converting signed digit code into infinite Gray code. Moreover, he showed that infinite Gray code can effectively be converted into signed digit code, but the program needs to have some non-deterministic features (see also [TS05]). Berger and Tsuiki [BT21a, BT21b] reproved the result in a system of formal first-order intuitionistic logic extended by inductive and co-inductive definitions, as well as some new logical connectives capturing concurrent behaviour. The programs extracted from the proofs are exactly the ones given by Tsuiki. In order to do so, co-inductive predicates S and G are defined and the inclusion S ⊆ G is derived. For the converse inclusion the new logical connectives are used to introduce a concurrent version S2 of S and G ⊆ S2 is shown. What one is looking for, however, is an equivalence proof of the involved concepts. One of the main aims of the present paper is to close the gap. A concurrent version G* of G and a modification S * of S2 are presented such that S * = G*. A crucial tool in [BT21a] is a formulation of the Archimedean property of the real numbers as an induction principle. We introduce a concurrent version of this principle which allows us to prove that S * and G* coincide. A further central contribution is the extension of the above results to the hyperspace of non-empty compact subsets of the reals. [ABSTRACT FROM AUTHOR]

Using an alternative to Tarskian semantics for first-order logic known as possibility semantics, I introduce an approach to nonstandard analysis that remains within the bounds of semiconstructive mathematics, i.e., does not assume any fragment of the Axiom of Choice beyond the Axiom of Dependent Choices. I define the Fr'echet hyperreal line †R as a possibility structure and show that it shares many fundamental properties of the classical hyperreal line, such as a Transfer Principle and a Saturation Principle. I discuss the technical advantages of †R over some other alternative approaches to nonstandard analysis and argue that it is well-suited to address some of the philosophical and methodological concerns that have been raised against the application of nonstandard methods to ordinary mathematics. [ABSTRACT FROM AUTHOR]

On account of being governed by constructive logic, intuitionistic theories T often enjoy various existence properties. The most common is the numerical existence property (NEP). It entails that an existential theorem of T of the form (∃x∈N)A(x) can be witnessed by a numeral n¯ such that T proves A(n¯). While NEP holds almost universally for natural intuitionistic set theories, the general existence property (EP), i.e. the property of a theory that for every existential theorem, a provably definable witness can be found, is known to fail for some prominent intuitionistic set theories such as Intuitionistic Zermelo–Fraenkel set theory (IZF) and constructive Zermelo–Fraenkel set theory (CZF). Both of these theories are formalized with collection rather than replacement as the latter is often difficult to apply in an intuitionistic context because of the uniqueness requirement. In light of this, one is clearly tempted to single out collection as the culprit that stymies the EP in such theories. Beeson stated the following open problem: 'Does any reasonable set theory with collection have the existence property? and added in proof: The problem is still open for IZF with only bounded separation.' (Beeson. 1985 Foundations of constructive mathematics, p. 203. Berlin, Germany: Springer.) In this article, it is shown that IZF with bounded separation, that is, separation for formulas in which only bounded quantifiers of the forms (∀x∈a),(∃x∈a),(∀x⊆a),(∃x⊆a) are allowed, indeed has the EP. Moreover, it is also shown that CZF with the exponentiation axiom in place of the subset collection axiom has the EP. Crucially, in both cases, the proof involves a detour through ordinal analyses of infinitary systems of intuitionistic set theory, i.e. advanced techniques from proof theory. This article is part of the theme issue 'Modern perspectives in Proof Theory'. [ABSTRACT FROM AUTHOR]

This is a survey of formal axiomatic systems for the three main varieties of constructive analysis, in a common language and with intuitionistic logic, which are as nearly as possible compatible with classical analysis and with one another. Classically sound consequences of principles of intuitionistic mathematics are emphasized. Compatibility with classical analysis is of two kinds. On the one hand, Bishop's constructive mathematics and a very substantial part of intuitionistic analysis are classically correct, sharing with constructive recursive mathematics a neutral subsystem adequate for recursive function theory and elementary real analysis. On the other hand, each constructive system considered here is separately consistent with the negative interpretation of each of its classically sound subsystems, establishing internal compatibility with the classical context it is intended to refine. A possibly new criterion for the transposability of unique existential quantifiers and a recent theorem of Vafeiadou on the internal compatibility of classical and intuitionistic analysis are included. This article is part of the theme issue 'Modern perspectives in Proof Theory'. [ABSTRACT FROM AUTHOR]

From the conceptual viewpoint, many mathematical propositions implicitly contain at least two kinds of principle. One is a logical principle such as the law-of-excluded-middle or De Morgan's law. Another is a function–existence principle. For both conceptual and practical reasons, it is an interesting enterprise to calibrate how amount of logical and function–existence principles are implicit in mathematical theorems and axioms. This is the topic of constructive reverse mathematics, which specifies necessary and sufficient axioms to prove each mathematical proposition constructively. In this paper, we decompose weak König's lemma with a uniqueness hypothesis WKL!! by Moschovakis, into logical and function–existence principles in a recent framework of constructive reverse mathematics. This article is part of the theme issue 'Modern perspectives in Proof Theory'. [ABSTRACT FROM AUTHOR]

We investigate predicative aspects of constructive univalent foundations. By predicative and constructive, we respectively mean that we do not assume Voevodsky's propositional resizing axioms or excluded middle. Our work complements existing work on predicative mathematics by exploring what cannot be done predicatively in univalent foundations. Our first main result is that nontrivial (directed or bounded) complete posets are necessarily large. That is, if such a nontrivial poset is small, then weak propositional resizing holds. It is possible to derive full propositional resizing if we strengthen nontriviality to positivity. The distinction between nontriviality and positivity is analogous to the distinction between nonemptiness and inhabitedness. Moreover, we prove that locally small, nontrivial (directed or bounded) complete posets necessarily lack decidable equality. We prove our results for a general class of posets, which includes e.g. directed complete posets, bounded complete posets, sup-lattices and frames. Secondly, the fact that these nontrivial posets are necessarily large has the important consequence that Tarski's theorem (and similar results) cannot be applied in nontrivial instances. Furthermore, we explain that generalizations of Tarski's theorem that allow for large structures are provably false by showing that the ordinal of ordinals in a univalent universe has small suprema in the presence of set quotients. The latter also leads us to investigate the inter-definability and interaction of type universes of propositional truncations and set quotients, as well as a set replacement principle. Thirdly, we clarify, in our predicative setting, the relation between the traditional definition of sup-lattice that requires suprema for all subsets and our definition that asks for suprema of all small families. [ABSTRACT FROM AUTHOR]

Copyright of Cahiers de Topologie et Geometrie Differentielle Categoriques is the property of Andree C. EHRESMANN and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

Copyright of Cahiers de Topologie et Geometrie Differentielle Categoriques is the property of Andree C. EHRESMANN and its content may not be copied or emailed to multiple sites or posted to a listserv without the copyright holder's express written permission. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)

Artemov and Protopopescu proposed intuitionistic epistemic logic (IEL) to capture an intuitionistic conception of knowledge. By establishing completeness, they provided the base for a meta-theoretic investigation of IEL, which was continued by Krupski with a proof of cut-elimination, and Su and Sano establishing semantic cut-elimination and the finite model property. However, no analysis of these results in a constructive meta-logic has been conducted, arguably impeding the intuitionistic justification of IEL. We aim to close this gap and investigate IEL in the constructive-type theory of the Coq proof assistant. Concretely, we present a constructive and mechanised completeness proof for IEL, employing a syntactic decidability proof based on cut-elimination to constructivise the ideas from the literature. Following Su and Sano, we then also give constructive versions of semantic cut-elimination and the finite model property. Given our constructive and mechanised setting, all these results now bear executable algorithms. Our particular strategy to establish constructive completeness exploiting syntactic decidability can be used for similar modal logics, which we illustrate with the examples of the classical modal logics K, D and T. For modal logics including the four axioms, however, the method seems not to apply immediately. [ABSTRACT FROM AUTHOR]

We prove that for any ring R of Krull dimension not greater than 1 and n ⩾ 3, the group En (R[X, X−1]) acts transitively on Umn(R[X, X−1]). In particular, we obtain that for any ring R with Krull dimension not greater than 1, all finitely generated stably free modules over R[X, X−1] are free. All the obtained results are proved constructively. [ABSTRACT FROM AUTHOR]

• In section 2 we include all definitions and facts on Bishop spaces that are necessary to the rest of the paper. • In section 3 we give all definitions and results on the canonical neighborhood structure of a Bishop topology. • In section 4 we introduce Bishop topological groups and we prove some of their basic properties. • In section 5 we prove fundamental properties of closed sets in Bishop topological groups. As we work with functions and positively defined concepts, avoiding the use of choice, our proofs generate clear algorithms. We introduce the notion of a Bishop topological group i.e., a group X equipped with a Bishop topology of functions F such that the group operations of X are Bishop morphisms with respect to F. A closed subset in the neighborhood structure of X induced by its Bishop topology F is defined in a positive way i.e., not as the complement of an open subset in X. The corresponding closure operator, although it is not topological, in the classical sense, does not involve sequences. As countable choice (CC) is avoided, and in agreement with Richman's critique on the use of CC in constructive mathematics, the fundamental facts on closed subsets in Bishop topological groups shown here have a clear algorithmic content. We work within Bishop's informal system of constructive mathematics BISH, without countable choice, equipped with inductive definitions with rules of countably many premises. [ABSTRACT FROM AUTHOR]

In this work we consider an extension MFcind of the Minimalist Foundation MF for predicative constructive mathematics with the addition of inductive and coinductive topological definitions sufficient to generate Sambin's Positive topologies, namely Martin-Löf-Sambin formal topologies (used to describe pointfree formal open subsets) equipped with a Positivity relation (used to describe pointfree formal closed subsets). In particular the intensional level of MFcind, called mTTcind, is defined by extending with coinductive topological definitions another theory mTTind extending the intensional level mTT of MF with the sole addition of inductive topological definitions. In previous work we have shown that mTTind is consistent with adding simultaneously formal Church's Thesis, CT, and the Axiom of Choice, AC, via an interpretation in Aczel's CZF +REA, namely Constructive Zermelo-Fraenkel Set Theory with the Regular Extension Axiom. Our aim is to show the expectation that the addition of coinductive topological definitions to mTTind does not increase its consistency strength by reducing the consistency of mTTcind+CT+AC to the consistency of CZF +REA through various interpretations. We reach our goal in two ways. One way consists in first interpreting mTTcind+CT+AC in the theory extending CZF with the Union Regular Extension Axiom, REAS, a strengthening of REA, and the Axiom of Relativized Dependent Choice, RDC. The theory CZF+REAS+RDC is then interpreted in MLS, a version of Martin-Löof's type theory with Palmgren's superuniverse S. The last step consists in interpreting MLS back into CZF +REA. The alternative way consists in first interpreting mTTcind+AC+CT directly in a version of Martin-Löf's type theory with Palmgren's superuniverse extended with CT, which is then interpreted back to CZF +REA. A key benefit of the first way is that the theory CZF + REAS + RDC also supports the intended set-theoretic interpretation of the extensional level of MFcind. Finally, all the theories considered to reach our goals, except mTTcind+AC + CT, are shown to be of the same proof-theoretic strength. [ABSTRACT FROM AUTHOR]

We present, in outline, a constructive development of set theory in the style of A.P. Morse's classical counterpart [10]. Since the development is carried in a very precise formal language, it readily lends itself to computer-assisted proof-checking and program extraction from proofs. • A development of constructive set theory in Morse's formal language, which should facilitate both proof checking and program extraction from proofs. • A powerful, general induction theorem. • Discussion of aspects of the proof that the Continuum Hypothesis implies excluded middle. [ABSTRACT FROM AUTHOR]

This analysis diagnoses a well-known and dominant theory of complex interval-valued intuitionistic uncertain linguistic (CI-VIUL) settings, which is considered to be a very powerful and capable tool to handle ambiguous sorts of theories. Furthermore, to enhance the features of the newly developed CI-VIUL information, we diagnose the algebraic laws, score value and accuracy value. Moreover, keeping in mind that the Heronian mean (HM) operator is a massive dominant operator that can suggest information on interrelationships, in this manuscript, we develop the CI-VIUL arithmetic HM (CI-VIULAHM) operator, CI-VIUL weighted arithmetic HM (CI-VIULWAHM) operator, CIVIUL geometric HM (CI-VIULGHM) operator, CI-VIUL weighted geometric HM (CI-VIULWGHM) operator and their well-known achievements in the form of some results, important properties and a discussion of some specific cases. At the end, we check the practicality and usefulness of the initiated approaches, and a multi-attribute decision-making (MADM) technique is implemented for CI-VIUL settings. The reliability of the proposed MADM tool is demonstrated by a computational example that evaluates the impact of the diagnosed approaches on various well-known prevailing theories. [ABSTRACT FROM AUTHOR]

Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to those normal forms. This higher structure can be captured by finding a homotopy basis for the rewriting system. We show that the basic notions of confluence and wellfoundedness are sufficient to recursively build such a homotopy basis, with a construction reminiscent of an argument by Craig C. Squier. We then go on to translate this construction to the setting of homotopy type theory , where managing equalities between paths is important in order to construct functions which are coherent with respect to higher dimensions. Eventually, we apply the result to approximate a series of open questions in homotopy type theory, such as the characterisation of the homotopy groups of the free group on a set and the pushout of 1-types. This paper expands on our previous conference contribution Coherence via Wellfoundedness by laying out the construction in the language of higher-dimensional rewriting. [ABSTRACT FROM AUTHOR]

We identify a notion of reducibility between predicates, called instance reducibility, which commonly appears in reverse constructive mathematics. The notion can be generally used to compare and classify various principles studied in reverse constructive mathematics (formal Church’s thesis, Brouwer’s Continuity principle and Fan theorem, Excluded middle, Limited principle, Function choice, Markov’s principle, etc.). We show that the instance degrees form a frame, i.e., a complete lattice in which finite infima distribute over set-indexed suprema. They turn out to be equivalent to the frame of upper sets of truth values, ordered by the reverse Smyth partial order. We study the overall structure of the lattice: the subobject classifier embeds into the lattice in two different ways, one monotone and the other antimonotone, and the ¬¬-dense degrees coincide with those that are reducible to the degree of Excluded middle. We give an explicit formulation of instance degrees in a relative realizability topos, and call these extended Weihrauch degrees, because in Kleene-Vesley realizability the ¬¬-dense modest instance degrees correspond precisely to Weihrauch degrees. The extended degrees improve the structure of Weihrauch degrees by equipping them with computable infima and suprema, an implication, the ability to control access to parameters and computation of results, and by generally widening the scope of Weihrauch reducibility. [ABSTRACT FROM AUTHOR]

In his previous work, the author has introduced the axiom schema of inductive dichotomy, a weak variant of the axiom schema of inductive definition, and used this schema for elementary ( Δ 0 1 ) positive operators to separate open and clopen determinacies for those games in which two players make choices from infinitely many alternatives in various circumstances. Among the studies on variants of inductive definitions for bounded ( Δ 0 0 ) positive operators, the present article investigates inductive dichotomy for these operators, and applies it to constructive investigations of variants of determinacy statements for those games in which the players make choices from only finitely many alternatives. As a result, three formulations of open determinacy, that are all classically equivalent with each other, are equivalent to three different semi-classical principles, namely Markov's Principle, Lesser Limited Principle of Omniscience and Limited Principle of Omniscience, over a suitable constructive base theory that proves clopen determinacy. Open and clopen determinacies for these games are thus separated. Some basic results on variants of inductive definitions for Δ 0 0 positive operators will also be given. [ABSTRACT FROM AUTHOR]

As a generalization of the minus ordering for regular fuzzy matrices, the minus ordering for k-regular intuitionistic fuzzy matrices is described in this study, and some of its features related to k-g inverses are examined. [ABSTRACT FROM AUTHOR]

The paper describes three models of the real field based on subsets of the integer sequences. The three models are compared to the Harthong–Reeb line. Two of the new models, contrary to the Harthong–Reeb line, provide accurate integer "views" on real numbers at a sequence of growing scales $B^n$ ( $B\ge2$). [ABSTRACT FROM AUTHOR]

In this paper we present a study that had as a guiding question: What is the beauty in mathematics and the beauty in Gödel's incompleteness theorem? We seek to present identifiable content for what we understand as beauty in Gödel's incompleteness theorem. For this, a bibliographic study was made and different notions of beauty in mathematics are brought and articulated. We also present our understanding of beauty in Gödel's theorem. We understand that the meaning of mathematical beauty of a theorem is that of an illumination that evidences the result. Moreover, we understand that this light allows itself to be seen insofar as one is familiar with the theory and with the tools used in the demonstration, to the point of being able to perceive the axioms used, the conciseness of the proof, the originality of the articulation of ideas, the possibilities of generalizing the result and the opening of new research fronts. We also recognize that the knowledge built by Gödel in the elaboration of his completeness theorem was fundamental in the view of the problem of the consistency of arithmetic and in the approach chosen to demonstrate the consistency of arithmetic, which became the demonstration of the incompleteness of the theory of arithmetic. [ABSTRACT FROM AUTHOR]