From Sets and Types to Topology and Analysis: Towards practicable foundations for constructive mathematics
From Sets and Types to Topology and Analysis: Towards practicable foundations for constructive mathematics
Cite
Abstract
Constructive mathematics is a vital area of research which has gained special attention in recent years due to the distinctive presence of computational content in its theorems. This characteristic had been already stressed by Bishop in his fundamental contribution to the subject, Foundations of Constructive Analysis (1967). Following Bishop's new approach to mathematics based on intuitionistic logic, various formal systems were introduced in the early 1970s with the intent to clarify the notion of set theory underlying his work. This book addresses the relationship between foundations and practice of constructive mathematics Bishop-style, by presenting on the one hand some very recent contributions to constructive analysis and formal topology, and on the other hand studies which underline the capabilities and expressiveness of various formal systems which have been introduced as foundations for constructive mathematics, like constructive set and type theories. The book aims to provide a point of reference by pesenting up-to-date contributions by some of the most active scholars in each field. A variety of approaches and techniques are represented to give as wide a view as possible and promote cross-fertilization between different styles and traditions. The book also aims at further promoting awareness and discussion on the issue of bridging foundations and practice of constructive mathematics, thus filling the apparent distance that has emerged between them in recent years.
-
Front Matter
-
1
INTRODUCTION
-
PART I Foundations
-
2
GENERALIZED INDUCTIVE DEFINITIONS IN CONSTRUCTIVE SET THEORY
Michael Rathjen
-
3
CONSTRUCTIVE SET THEORIES AND THEIR CATEGORY-THEORETIC MODELS
Alex Simpson
-
4
PRESHEAF MODELS FOR CONSTRUCTIVE SET THEORIES
Nicola Gambino
-
5
UNIVERSES IN TOPOSES
Thomas Streicher
-
6
TOWARD A MINIMALIST FOUNDATION FOR CONSTRUCTIVE MATHEMATICS
Maria Emilia Maietti andGiovanni Sambin
-
7
INTERACTIVE PROGRAMS AND WEAKLY FINAL COALGEBRAS IN DEPENDENT TYPE THEORY
Peter Hancock andAnton Setzer
-
8
APPLICATIONS OF INDUCTIVE DEFINITIONS AND CHOICE PRINCIPLES TO PROGRAM SYNTHESIS
Ulrich Berger andMonika Seisenberger
-
9
THE DUALITY OF CLASSICAL AND CONSTRUCTIVE NOTIONS AND PROOFS
Sara Negri andJan Von Plato
-
2
GENERALIZED INDUCTIVE DEFINITIONS IN CONSTRUCTIVE SET THEORY
-
PART II Practice
-
10
CONTINUITY ON THE REAL LINE AND IN FORMAL SPACES
Erik Palmgren
-
11
SEPARATION PROPERTIES IN CONSTRUCTIVE TOPOLOGY
Peter Aczel andChristopher Fox
-
12
SPACES AS COMONOIDS
A. Bucalo andG. Rosolini
-
13
PREDICATIVE EXPONENTIATION OF LOCALLY COMPACT FORMAL TOPOLOGIES OVER INDUCTIVELY GENERATED TOPOLOGIES
Maria Emilia Maietti
-
14
SOME CONSTRUCTIVE ROADS TO TYCHONOFF
Steven Vickers
-
15
AN ELEMENTARY CHARACTERIZATION OF KRULL DIMENSION
Thierry Coquand Henri Lombardi andMarie-Françoise Roy
-
16
CONSTRUCTIVE REVERSE MATHEMATICS: COMPACTNESS PROPERTIES
Hajime Ishihara
-
17
APPROXIMATING INTEGRABLE SETS BY COMPACTS CONSTRUCTIVELY
Bas Spitters
-
18
AN INTRODUCTION TO THE THEORY OF C*-ALGEBRAS IN CONSTRUCTIVE MATHEMATICS
Hiroki Takamura
-
19
APPROXIMATIONS TO THE NUMERICAL RANGE OF AN ELEMENT OF A BANACH ALGEBRA
Douglas Bridges andRobin Havea
-
20
THE CONSTRUCTIVE UNIQUENESS OF THE LOCALLY CONVEX TOPOLOGY ON ℝN
Douglas Bridges andLuminita Vîtă
-
21
COMPUTABILITY ON NON-SEPARABLE BANACH SPACES AND LANDAU'S THEOREM
Vasco Brattka
-
10
CONTINUITY ON THE REAL LINE AND IN FORMAL SPACES
-
End Matter
Sign in
Personal account
- Sign in with email/username & password
- Get email alerts
- Save searches
- Purchase content
- Activate your purchase/trial code
- Add your ORCID iD
Purchase
Our books are available by subscription or purchase to libraries and institutions.
Purchasing informationMonth: | Total Views: |
---|---|
October 2022 | 1 |
October 2022 | 1 |
October 2022 | 1 |
October 2022 | 3 |
October 2022 | 1 |
October 2022 | 1 |
October 2022 | 1 |
October 2022 | 4 |
October 2022 | 3 |
October 2022 | 1 |
October 2022 | 1 |
October 2022 | 1 |
October 2022 | 1 |
October 2022 | 1 |
October 2022 | 2 |
October 2022 | 2 |
October 2022 | 1 |
October 2022 | 1 |
October 2022 | 1 |
October 2022 | 2 |
October 2022 | 1 |
October 2022 | 1 |
November 2022 | 1 |
November 2022 | 2 |
November 2022 | 1 |
November 2022 | 1 |
November 2022 | 1 |
November 2022 | 4 |
November 2022 | 1 |
November 2022 | 1 |
December 2022 | 1 |
December 2022 | 1 |
December 2022 | 1 |
December 2022 | 2 |
January 2023 | 2 |
January 2023 | 1 |
January 2023 | 3 |
February 2023 | 1 |
February 2023 | 5 |
February 2023 | 2 |
March 2023 | 3 |
March 2023 | 5 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 2 |
March 2023 | 2 |
March 2023 | 2 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 2 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 2 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 2 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 3 |
March 2023 | 3 |
April 2023 | 2 |
May 2023 | 2 |
May 2023 | 1 |
June 2023 | 1 |
June 2023 | 1 |
June 2023 | 1 |
June 2023 | 1 |
June 2023 | 1 |
July 2023 | 2 |
August 2023 | 1 |
August 2023 | 1 |
August 2023 | 1 |
September 2023 | 1 |
September 2023 | 1 |
September 2023 | 4 |
September 2023 | 1 |
October 2023 | 2 |
October 2023 | 1 |
October 2023 | 1 |
November 2023 | 1 |
November 2023 | 3 |
November 2023 | 2 |
November 2023 | 1 |
December 2023 | 2 |
December 2023 | 2 |
December 2023 | 4 |
December 2023 | 3 |
December 2023 | 2 |
December 2023 | 3 |
December 2023 | 4 |
January 2024 | 1 |
January 2024 | 1 |
January 2024 | 3 |
January 2024 | 2 |
February 2024 | 2 |
February 2024 | 2 |
March 2024 | 2 |
March 2024 | 1 |
March 2024 | 3 |
March 2024 | 2 |
March 2024 | 2 |
April 2024 | 2 |
April 2024 | 2 |
April 2024 | 3 |
April 2024 | 1 |
April 2024 | 5 |
April 2024 | 2 |
April 2024 | 2 |
May 2024 | 5 |
May 2024 | 3 |
May 2024 | 3 |
May 2024 | 2 |
May 2024 | 3 |
May 2024 | 12 |
May 2024 | 2 |
May 2024 | 3 |
May 2024 | 4 |
May 2024 | 3 |
May 2024 | 5 |
May 2024 | 3 |
May 2024 | 3 |
May 2024 | 3 |
May 2024 | 3 |
May 2024 | 3 |
May 2024 | 6 |
May 2024 | 2 |
May 2024 | 1 |
May 2024 | 3 |
May 2024 | 3 |
May 2024 | 3 |
May 2024 | 3 |
May 2024 | 2 |
May 2024 | 3 |
May 2024 | 3 |
May 2024 | 3 |
June 2024 | 1 |
June 2024 | 1 |
June 2024 | 2 |
June 2024 | 1 |
June 2024 | 7 |
June 2024 | 2 |
June 2024 | 2 |
June 2024 | 4 |
June 2024 | 2 |
June 2024 | 2 |
June 2024 | 2 |
June 2024 | 1 |
June 2024 | 8 |
June 2024 | 2 |
June 2024 | 1 |
June 2024 | 5 |
June 2024 | 4 |
June 2024 | 4 |
June 2024 | 1 |
June 2024 | 1 |
June 2024 | 5 |
June 2024 | 2 |
June 2024 | 1 |
June 2024 | 1 |
July 2024 | 2 |
July 2024 | 2 |
July 2024 | 3 |
July 2024 | 2 |
July 2024 | 2 |
July 2024 | 2 |
July 2024 | 2 |
July 2024 | 2 |
July 2024 | 2 |
July 2024 | 2 |
July 2024 | 3 |
July 2024 | 3 |
July 2024 | 2 |
July 2024 | 2 |
July 2024 | 3 |
July 2024 | 2 |
July 2024 | 2 |
July 2024 | 4 |
July 2024 | 1 |
August 2024 | 1 |
August 2024 | 1 |
September 2024 | 2 |
September 2024 | 1 |
September 2024 | 1 |
October 2024 | 1 |
October 2024 | 6 |
November 2024 | 2 |
December 2024 | 1 |
December 2024 | 2 |
December 2024 | 1 |
December 2024 | 1 |
January 2025 | 1 |
January 2025 | 1 |
January 2025 | 3 |
February 2025 | 1 |
February 2025 | 2 |
March 2025 | 2 |
March 2025 | 1 |
March 2025 | 2 |
March 2025 | 3 |
April 2025 | 4 |
April 2025 | 2 |
April 2025 | 1 |
April 2025 | 1 |
Get help with access
Institutional access
Access to content on Oxford Academic is often provided through institutional subscriptions and purchases. If you are a member of an institution with an active account, you may be able to access content in one of the following ways:
IP based access
Typically, access is provided across an institutional network to a range of IP addresses. This authentication occurs automatically, and it is not possible to sign out of an IP authenticated account.
Sign in through your institution
Choose this option to get remote access when outside your institution. Shibboleth/Open Athens technology is used to provide single sign-on between your institution’s website and Oxford Academic.
If your institution is not listed or you cannot sign in to your institution’s website, please contact your librarian or administrator.
Sign in with a library card
Enter your library card number to sign in. If you cannot sign in, please contact your librarian.
Society Members
Society member access to a journal is achieved in one of the following ways:
Sign in through society site
Many societies offer single sign-on between the society website and Oxford Academic. If you see ‘Sign in through society site’ in the sign in pane within a journal:
If you do not have a society account or have forgotten your username or password, please contact your society.
Sign in using a personal account
Some societies use Oxford Academic personal accounts to provide access to their members. See below.
Personal account
A personal account can be used to get email alerts, save searches, purchase content, and activate subscriptions.
Some societies use Oxford Academic personal accounts to provide access to their members.
Viewing your signed in accounts
Click the account icon in the top right to:
Signed in but can't access content
Oxford Academic is home to a wide variety of products. The institutional subscription may not cover the content that you are trying to access. If you believe you should have access to that content, please contact your librarian.
Institutional account management
For librarians and administrators, your personal account also provides access to institutional account management. Here you will find options to view and activate subscriptions, manage institutional settings and access options, access usage statistics, and more.