/sci/ - Science & Math

>>12447854
It's another thread about the reals... Pick up a book on analysis already and stop being faggots.

>What am I missing something here?
In the standard model of things, Cauchy reals are equivalence classes (each real being of set cardinality [math]|{\mathbb R}|[/math], mind you) of Cauchy sequences.

A disadvantage of the Cauchy reals is that the completeness property of them as a set is harder to get.
(On the flipside, to even make the Dedekind reals a set, you need stronger powerset-like axioms.)

Btw. I came across of probably very nice papers recently, in those directions.

>Real Analysis in Reverse
https://arxiv.org/pdf/1204.4483.pdf
Now classically discussing in detail all the nice properties (TM) of the reals, or rather their relationship to Dedekind completeness (and I'm sure it's a good ref for having all those at hand formally)

>Completeness of Ordered Fields
https://arxiv.org/pdf/1101.5652.pdf
Classically discussing how far away Dedekind completeness is from the vantage point of having an ordered arithmetical field

The rest is from a constructive angle:

>On the Cauchy Completeness of the Constructive Cauchy Reals
https://arxiv.org/pdf/1510.00639.pdf
Looking at the pains of indeed talking about the Cauchy completness of set collection of Cauchy reals in the strong-as-possible-without-LEM set theory
Keyword: Modulus of convergence

Same author + Rathjen discssing the Dedekind reals here
>On the Constructive Dedekind Reals
http://math.fau.edu/lubarsky/Dedreals.pdf

The Dedekind variant opens up some (arguably hard formalist) theories, locales etc. (https://ncatlab.org/nlab/show/locale))
I think Bauer generally prefers to allow for rich such frameworks and he even has some code going in that direction
https://github.com/andrejbauer/dedekind-reals

There's more angles, though, I know of a few recent type theory PhD theses who are basically about formalization, and some are inbetween those variants.

>>12447891
>Pick up a book on analysis already and stop being faggots.
Give an example of a book on analysis that discusses these issues. I'm genuinely very curious to know. I've read many books on analysis and none of them talk about this.

>>12447908
>In the standard model of things, Cauchy reals are equivalence classes (each real being of set cardinality |R||R|, mind you) of Cauchy sequences.
Yeah I know, I'm talking about how to compute with them.
There is no way to implement this "equivalence class of sequences" because there isn't even a a good definition of what as sequence is, nor a way to implement it computationally.
So I resort to looking only at specific objects and implementing them. I ignore the equivalence class thing which essentially all it does is lets you replace the relation ~ with genuine equality.
So instead I look at reals as representatives of these classes and replace the notion of equality not as the equality of algorithms but as the Cauchy definition (lim a_n - b_n = 0).
Given that, there are still many ways to implement real numbers.
I even missed some subtleties in the OP.
For example, I forgot to make the distinction of different implementations of Dedekind cuts where:
1. Program lets you input a rational number and halts when rational number is smaller than your real, but doesn't halt when it's bigger.
2. Program lets you input a rational number, always halts with a definite answer of whether it's smaller, bigger, or equal.
This give you different possibilities. For example, with 1 you can take the sup of a sequence of reals but with 2 you can't (as I noted in the OP: I only looked at implementation 2).
Comparing two real numbers is the same in both implementations. You can detect when they're unequal but there's no way to check if they're equal.
Still it seems like the reals as Cauchy sequences are the best.

>>12447946
>Yeah I know, I'm talking about how to compute with them.
Then sure, the definition is then also closer of use to Type 2 notion of real number computation alla
https://en.wikipedia.org/wiki/Computable_analysis

I've recently bit pushing in that direction and work out e.g. how you can model something like exp(\pi), where both function and argument have non-rational value in general and combined

https://youtu.be/MUbZ9XqWsuc

>>12447854
You're missing the crystal clear geometry behind the Dedekind cut definition, which solidly asserts it as the superior definition.

>>12448335
this. literally defines holes in the rational number line as concrete objects.

>>12448337
>as concrete objects

>>12447854
>No way to check whether two numbers are equal (reduces to the Halting problem).

The only way you realistically encounter a real number is in an expression, in which case you'd never have to pick members of the equivalence classes on either side to check. Why would this be a disadvantage?

>>12448453
>in which case you'd never have to pick members of the equivalence classes on either side to check
What did you mean by this?

>>12447854
>- Cannot add, subtract, multiply, divide.
huh

you can do this with dedekind cuts, even in constructive maths, which is why they use those cuts

A lambda calculus for real analysis
Paul Taylor

This paper is an introduction to Abstract Stone Duality and its in particular its application to real analysis that is indended for the general mathematician. It was published in the Journal of Logic and Analysis 2(5) 1–115 on 18 August 2010 (BibTeX).
Abstract

Abstract Stone Duality is a revolutionary paradigm for general topology that describes computable continuous functions directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis.

This language is applied to the Intermediate Value Theorem: the solution of equations for continuous functions on the real line. As is well known from both numerical and constructive considerations, the equation cannot be solved if the function “hovers” near 0, whilst tangential solutions will never be found.

In ASD, both of these failures and the general method of finding solutions of the equation when they exist are explained by the new concept of overtness. The zeroes are captured, not as a set, but by higher-type modal operators. Unlike the Brouwer degree, these are defined and (Scott) continuous across singularities of a parametric equation.

>>12448576
Expressing topology in terms of continuous functions rather than sets of points leads to treatments of open and closed concepts that are very closely lattice- (or de Morgan-) dual, without the double negations that are found in intuitionistic approaches. In this, the dual of compactness is overtness. Whereas meets and joins in locale theory are asymmetrically finite and infinite, they have overt and compact indices in ASD.

Overtness replaces metrical properties such as total boundedness, and cardinality conditions such as having a countable dense subset. It is also related to locatedness in constructive analysis and recursive enumerability in recursion theory.
History

This paper was presented at

Computability and Complexity in Analysis, Kyoto, 25-29 August 2005, using these slides;
Canadian Mathematical Society Summer Meeting, Calgary, 3–5 June 2006, using these improved slides; and
Third Workshop on Formal Topology, Padova, 7–12 May 2007, using these slides, In defence of Dedekind and Heine–Borel.

More than 1500 distinct non-robot sites downloaded this paper between September 2007 and June 2010, including over 150 universities.


Acknowledgements

As I was a reluctant analyst, this work would never have been done without the persistent (but friendly) cajoling of Graham White and Andrej Bauer. I would like to express my warmest appreciation for the ongoing encouragement that they have both given me. In particular, during my visit to Ljubljana in November 2004, Andrej provided the construction of the supremum of a compact overt subspace in Section 12 using Dedekind cuts that is the keystone of this paper.

This work was presented at Computability and Complexity in Analysis in Kyoto in August 2005, and I am grateful to Peter Hertling and the CCA programme committee for the indulgence of allowing me to occupy altogether 80 pages of their (pre-conference) proceedings.

>>12448546
I forgot to make the distinction of different implementations of Dedekind cuts. In the OP I considered the implementation in which a cut is a program P such that for every rational x it decides whether or not x is in the cut.
With this implementation you can neither add, nor subtract, nor multiply the reals.
However, if you change the implementation where x in C is only semidecidable (halts if true and loops if not) then you can indeed add, subtract and multiply the reals.

>>12448590
The paper that you see here is the fruit of illuminating discussions with numerous people since the conference. I would particularly also like to thank Jeremy Avigad, Vasco Brattka, Douglas Bridges, Robin Cockett, Thierry Coquand, Martín Escardó, Nicola Gambino, André Joyal, Achim Jung, Norbert Müller, Erik Palmgren, Petrus Potgieter, Pino Rosolini, Giovanni Sambin, Peter Schuster, Anton Setzer, Bas Spitters and Steve Vickers for their interest and encouragement in this project.

Finally, I would like to thank the anonymous referees for their care. Lengthy technical papers are not so uncommon, but in this case someone from well outside my usual circle was obliged to make a seismic shift in his entire understanding of the way in which mathematics is done. I deeply appreciate the grace with which he was willing and able to do this.

BibTEX entries

@article{TaylorP:lamcra,
author = {Taylor, Paul},
title = {A Lambda Calculus for Real Analysis},
journal = {Journal of Logic and Analysis},
year = 2010, month = {August},
volume = 2, number = 5, pages = {1--115},
doi = {10.4115/jla.2010.2.5},
url = {PaulTaylor.EU/ASD/lamcra}}

@inproceedings{TaylorP:lamcra-,
author = {Taylor, Paul},
title = {A Lambda Calculus for Real Analysis},
booktitle = {Computability and Complexity in Analysis},
editor = {Grubba, Tanja and Hertling, Peter and
Tsuiki, Hideki and Weihrauch, Klaus},
year = 2005, month = {July},
series = {Informatik Berichte},
volume = 326, pages = {227--266},
publisher = {FernUniversit\"at in Hagen},
note = {Proccedings of the second international conference,
Kyoto, Japan, August 25--29, 2005}}
https://paultaylor.eu/ASD/lamcra/
https://paultaylor.eu/ASD/lamcra/
https://paultaylor.eu/ASD/lamcra/
https://paultaylor.eu/ASD/lamcra/

>Real Analysis in Abstract Stone Duality
Paul Taylor
Abstract Stone Duality is a new paradigm for general topology and real analysis that is based directly on continuous functions and predicates, and not sets. It is both constructive and computable, but its idioms of reasoning often look like a sanitised form of classical logic. The papers below on real analysis currently provide the best introduction to ASD. The core theory is developed in the papers on locally compact spaces, but these rely on a deeper understanding of categorical techniques.
Axioms for the real line
The real line and its topology are characterised uniquely by the following properties:

R is an overt space, with an existential quantifier ∃;
it is Hausdorff, with an inequality or apartness relation, ≠ ;
the closed interval [0,1] is compact, with a universal quantifier ∀x:[0,1];
R has a total order, i.e. (x ≠ y) (x < y) ∨(y < x);
it is Dedekind complete, in a sense in which the two halves of a cut are open;
it is a field, where x−1 is defined iff x ≠ 0; and
Archimedean, i.e. y > 0 ∃n:Z. y(n−1) < x < y(n+1).

Each of the papers (separately) explains what these axioms (and those of the wider theory) mean formally.
The syntactic language that this description provides may be roughly summed up in the following table of operations:

>>12447891
dumbfuck, these constructions are from any book in analysis. What OP is trying to discuss is computable analysis, which itself is very close to constructive analysis.

>>12448599
Which paper should I read first?
Each of the following papers has been written independently of the others, and provides an introduction to ASD that is suitable for a particular audience. So, depending on your background, you should read

A Lambda Calculus for Real Analysis if you are interested in (constructive, computable or classical) real analysis, or indeed in the heritage of mathematics in general;
Interval Analysis Without Intervals if you are interested in interval analysis, "exact" real arithmetic or real-valued logic programming;
Efficient Computation with Dedekind Reals by Andrej Bauer for another point of view on computation;
The Dedekind Reals in ASD if you are interested in domain theory or continuous lattices; or
Foundations for Computable Topology if you are interested in category theory, Stone duality, locale theory or the philosophy of mathematics.

https://paultaylor.eu/ASD/analysis
https://paultaylor.eu/ASD/analysis
https://paultaylor.eu/ASD/analysis

>>12448540
I guess he means that there's no realistic scenario where you're unable to compare two real numbers because they're given as cauchy sequence and your only bet is to check the elements one by one.

>>12448609
>realistic scenario where you're unable to compare two real numbers
I can literally give you realistic scenarios right now where comparing two computably defined real numbers gives you a solution to twin prime problem or 3k+1 problem.

so basically if you want to have a nice set, space, locale of the reals, you have to go constructive and you get all the theorems you have in classical maths with sets and

for locale theory, an introduction is here

https://boards.fireden.net/sci/thread/12166845/#12170887

as an aside, Bauer published a little intro to Type theory

http://math.andrej.com/

A general definition of dependent type theories

14 September 2020 Andrej Bauer Publications, Type theory

The preprint version of the paper A general definition of dependent type theories has finally appeared on the arXiv! Over three years ago Peter Lumsdaine invited me to work on the topic, which I gladly accepted, and dragged my student Philipp Haselwarter into it. We set out to give an answer to the queation:

What is type theory, precisely?

At least for me the motivation to work on such a thankless topic came from Vladimir Voevodsky, who would ask the question to type-theoretic audiences. Some took him to be a troll and others a newcomer who just had to learn more type theory. I was among the latter, but eventually the question got through to me – I could point to any number of specific examples of type theories, but not a comprehensive and mathematically precise definition of the general concept.

It is too easy to dismiss the question by claiming that type theory is an open-ended concept which therefore cannot be completely captured by any mathematical definition. Of course it is open-ended, but it does not follow at all that we should not even attempt to define it. If geometers were equally fatalistic about the open-ended notion of space we would never have had modern geometry, topology, sheaves – heck, half of 20th century mathematics would not be there!

Of course, we are neither the first nor the last to give a definition of type theory, and that is how things should be. We claim no priority or supremacy over other definitions and views of type theory. Our approach could perhaps be described as "concrete" and "proof-theoretic":

We wanted to stay close to traditional syntax.
We gave a complete and precise definition.
We aimed for a level of generality that allows useful meta-theory of a wide range of type theories.

One can argue each of the above points, and we have done so among ourselves many times. Nevertheless, I feel that we have accomplished something worthwhile – but the ultimate judges will be our readers, or lack of them. You are kindly invited to take a look at the paper.

Download PDF: arxiv.org/pdf/2009.05539.pdf

Last link for stone duality, to get all this in the archive

Due to Paul Taylor, Abstract Stone Duality (ASD) is a reaxiomatisation of the notions of topological space and continuous function in general topology in terms of a lambda-calculus of computable continuous functions and predicates that is both constructive and computable. It thus forms one approach to synthetic topology.

The topology on a space is treated not as a discrete lattice, but as an exponential object of the same category as the original space, with an associated λ-calculus (which includes an internal lattice structure). Every expression in the λ-calculus denotes both a continuous function and a program. ASD does not use the category of sets (or any topos), but the full subcategory of overt discrete objects plays this role (an overt object is the dual to a compact object), forming an arithmetic universe (a pretopos with lists) with general recursion; an optional ‘underlying set’ axiom (which is not predicative) will make this a topos.

The classical (but not constructive) theory of locally compact sober topological spaces is a model of ASD, as is the theory of locally compact locales over any topos (even constructively). In “Beyond Local Compactness” on the ASD website, Taylor removes the restriction of local compactness.

https://ncatlab.org/nlab/show/abstract+Stone+duality

>>12448643
I wouldn't say Bauers paper counts as an intro to the subject.

>>12447854
what is this autism and why is it relevant

bump

>>12449325
Do you know anything about the real numbers?

ok

based logic thread, have a bump

yes

>>12447891
>BELIVE THE SYSTME GOY
>DON'T THINK FOR YOURSELF
>OF CROUSE THIS THING I BELIVE FERVENTLY CAN'T BE QUESTIONED.

>>12447854
>www.paultaylor.eu/ASD/dedras.pdf
>someday I will have what I need to understand this paper