/sci/ - Science & Math

Bumpoffsky

>>7522829
>Axiom of Choice valid in constructive mathematics
>One (in)famous claim Bishop makes is that "A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence" (Bishop & Bridges, 1985, p. 12). The axiom is in fact provable in some constructive theories (see Section 5). However, Diaconescu has shown that AC implies PEM, so it would seem that constructivists ought to accept PEM after all (the proof in Diaconescu (1975) is actually remarkably simple). And as we have seen, for some constructivists it would actually be inconsistent to accept PEM. It thus seems that AC, while very important, presents a significant problem for constructivists. However, as we now discuss, such a conclusion is hasty and unjustified.

>>7522890
>The key observation to make regards the interpretation of the quantifiers. AC comes out as provable only when we interpret the quantifiers under BHK: for then the hypothesis ∀x∈A∃y∈BP(x,y) says that there is an algorithm which takes us from elements x of A together with the data that x belongs to A, to an element y of B. Thus only if there is no extra work to be done beyond the construction of x in showing that x is a member of A (that is, if this can be done uniformly) will this be a genuine function from A to B. We will revisit this in Section 5. Thus the classical interperatation of AC is not valid under BHK, and PEM cannot be problematically derived.

Let us return to Bishop's statement at the start of this section, regarding the existence of a choice function being implied by the meaning of existence. The context in which his claim was made illuminates the situation. The passage (Bishop & Bridges, 1985, p. 12) goes on to read: "[Typical] applications of the axiom of choice in classical mathematics either are irrelevant or are combined with a sweeping use of the principle of omniscience." This also shows that blaming the axiom of choice for non-constructivity is actually a mistake—it is the appeal to PEM, LPO, or similar absolute principles applied to objects other than the finite which prevent proof from being thoroughly algorithmic. Some constructive mathematicians adopt various weakenings of AC which are (perhaps) less contentious; Brouwer, as we saw in Section 2, adopts Continuous Choice.

>>7521194
>>
>http://math.andrej.com/2009/09/07/constructive-stone-finite-sets/
>>Proposition: The following are equivalent:
>>The law of excluded middle.
>>Subsets of finite sets are finite.
>>Intersections of finite sets are finite.

>>7522894
>Within Martin-Löf type theory, the axiom of choice, stated symbolically as
∀x∈A∃y∈B P(x,y)⟹∃f∈B^A ∀x∈A P(x,f(x))
>is derivable. Recall that this would be inconsistent, if AC were interpreted classically. However the axiom is derivable because in the construction of types, the construction of an element of a set (type) is sufficient to prove its membership. In Bishop-style constructive mathematics, these sets are "completely presented", in that we need to know no more than an object's construction to determine its set membership. Under the BHK interpretation, the added requirement on the proof of ∀x∈AP(x) that the algorithm may depend also on the data that x belongs to A and not just on the construction of x itself is thus automatically satisfied.


>It is worth noting that sets construed in this theory are constrained by this realizability criterion. For example, in Martin-Löf's theory, the power set axiom is not accepted in full generality—the power set of N, for example, is considered to be what would in classical theory be called a class, but not a set (Martin-Löf, 1975).

>>7522913
Ultrafinitists in a nutshell.

>>7522894
You see, BHK is merely pulling oneself outa water by his own hair like Münchhausen and nothing else. It's just a sly way to bypass the actual problem with AC. Instead of directly addressing it, let us turn around, close our eyes and pretend that the problem does not exist.

Why? Because BHK is a metamathematical concept. It is as it is: an interpretation. Here is the trick: if I prove a ∀x.∃y.φ(x,y), then of course I need to provide a realizer f(x) as soon as I'm in constructive setting. BUT the actual cornerstone of this story is to PRETEND that f(x) magically appears as soon as ∀x.∃y.φ(x,y) is claimed. This is the other way around.

It makes sense in theory (say, in an effective topos) that f(x) has to pop up when you work out your proofs, but it has zero applicable content. f(x) is merely SOME computable function that emits y's outa x's satisfying φ(x,y) and that's it. Just a black box. What do we know about it? Frankly such a black box generating machine must suffer from Halting problem. At least. We can tell more. What if that computable function entails Ackerman trees and some other freakin shit? That's the point: you pursue a clear connection to computer implementation but in the meantime you can provide to implementation. All you can do is: hurr-durr, here is the black box the damn AC machine gave, I have no idea what it does, but hurr-durr φ(x,y).

>>7522924
>Friedman trees
of course

>>7522924
the question is why do you care about BHK

>>7522923
>Ultrafinitists
totally based

>>7522923
>Ultrafinitists
totally based>>7522924
>f(x) magically appears as soon as ∀x.∃y.φ(x,y) is claimed.
but to claim ∀x.∃y.φ(x,y) is precisely somehow obtaining a f:

>>7522904
>In Bishop-style constructive mathematics, these sets are "completely presented", in that we need to know no more than an object's construction to determine its set membership. Under the BHK interpretation, the added requirement on the proof of ∀x∈AP(x) that the algorithm may depend also on the data that x belongs to A and not just on the construction of x itself is thus automatically satisfied.


you still see the AC from the classical viewpoint. You must change everything AC+whatever concept is used to state AC.

>>7522927
I personally don't care. I blame on it. I think its content is vague. The reason why I (and you) mentioned BHK is that it's allegedly a treatment of the said problem.

>>7522939
Aha! That's the subtlety. You seem to be deluded in the same way that advocates of AC are. In most of the proofs where AC is invoked, the whole process works the other way around: it's not that you build an explicit algorithm -- it's about showing ∀x.∃y.φ(x,y) ACTUALLY WITHOUT an explicit algorithm and CLAIM that it exists. This is used, for instance, in showing that x2+a has two (complex) roots. It is a magical choice function that picks precisely one branch to locate a root. Nothing can be said about it except that it's computable. But you can't exctract a valid algorithm from such a proof. Indeed, you never find example out there. On contrary, I know at least one well worked out framework of program exctraction which is even more or less readable. But it doesn't use Choice.

>>7522949
>This is used, for instance, in showing that x2+a has two (complex) roots. It is a magical choice function that picks precisely one branch to locate a root.
and this would be in Hott ?

I do not like the AC myself as soon as we leave a finitist stance.

>>7522958
Nothing so special about HoTT either. I prefer to look at the essence first. The essence is algorithms. That is what distinguishes constructive mathematics from the classical. In the latter, there is the Oracle that knows everything. We now need to kill the last Oracle -- that one that spits out algorithms.

>I do not like the AC myself as soon as we leave a finitist stance.
There is a good book on finitism demonstrating that there is no essential difference between finitism and constructivism. It is a delusion that the two differ much. The very ideas of constructivism are already finitistic. http://www.springer.com/us/book/9789400713468 demonstrates that practically all Bishop's constructions are readily finitistic. Funnily enough, it's not even the Axiom of Infinity that makes a theory not finitistic. There is even a category that has a natural numbers objects (=Axiom of Infinity) and whose internal logic is Primitive Recursive Arithmetic (Skolem's finitism).

>>7522977
>http://www.springer.com/us/book/9789400713468
I will be reading this

what stances do you like then ?. Do you like AC, PEM, the power set axiom ?

>>7523023
>>>http://www.springer.com/us/book/9789400713468


>The set R of real numbers is already defined.

Apparently, he takes the reals form Bishop. So does he think that the equality is decidable on R ?

I prefer the construction of R as a locale tbh.

>>7523030
My stance is choice-free constructivism (finitism as I said is close).

>Apparently, he takes the reals form Bishop
Yes these are Cauchy reals. But the difference is they are elementary recursive functions that eventually allow quantifier elimination. There is just a bit more care taken, but the framework as not that restrictive as it sounds like.

>So does he think that the equality is decidable on R
Of course not. Neither Bishop does.

I am not that much familiar with locales. It seems to be quite a crude theory so far. But definitely interesting and worth studying. The reason why I say "crude" is because Bishop's style is already quite worked out and popular. There is really a good potential of "constructivizing" a whole bunch of theorems laying out there. And it works. I'm currently developing a constructive version of one. But I won't tell until I submit my paper. I know a dude who could land good 8 papers in decent journals simply constructivizing some stuff a la Bishop.

Also regarding locales, I saw constructions quite similar to Cauchy reals (like they restore point first and then go to sequences). Why kind of locale theory do you prefer and what choice principles are there?

>>7523064
well I like the predicative constructive locale theory [the one that you do in any topos [with NNo]]. Note that there is classical treatment of locale theory. There is also what is called synthetic topology which uses the notion of a coverage to generate a locale.

In terms of logic you have the geometric logic
http://ncatlab.org/nlab/show/geometric+theory

it is a positive logic [a logic of ''observation'' thanks to the infinite disjunct], no PEM, no powerset, but finite subsets of Kuratowski finite set [see the quoted bit on finite subsets of finite sets above in the thread] and the power-locale for appropriate locales, no choice at all. You can quantify universally only on finite sets, on N, Z, Q, compact locales, but not R nor C.


THERE IS NO IMPLICATION [because it is not a geometric notion = it behaves badly when we transport the theory from topos to topos, as explained below]
The logic uses sequents and contexts for free variables which permits to deal with the empty set as a carrier set easily.
Locale theory is nice because you have, predicatively-constructively, all the theorems about R in topology that you want form your study of classical mathematics. I think that if you do pointless topology in intuitionist logic, you do not retrieve the theorems. integrals, C*-algebras, all the topology on the reals are defined in geometric logic.

Hott constructs the same localic reals in chapter 11.

there is a video by Johnstone himself explaining the construction of the reals

Peter Johnstone: "Topos-theoretic models of the continuum"
https://www.youtube.com/watch?v=pKWYa9sc5UI

other people in the fields are everybody in HOTT, palgrem, paul taylor, steve vikers, maietti, all the people in synthetic topology.

>>7523556
I do not know much on locales so I will expose quickly. But when you a geometric theory doable only with propositions, you have a locale and the locale [the topological space] has a dual called a frame of opens, the frame is the Lindenbaum algebra of the theory.


one point of the locale is one generalized model of the theory.
So each open [each element of the frame] is a proposition of the theory

a generalized point of one locale is in an open when the model [the point] satisfies the proposition [the open], when the proposition true in the model.


for the geometric logic with predicates, the Lindenbaum algebra is the classifying topos of the theory. the topos is a topos of sheaves, The sheaves themselves are the generalization, on the predicate level, of the opens of the frame. This duality of frame/locales is a Stone duality in fact.

what matters is the geometric theory, because it is this structure which is preserved by the geometric functors. The frame is not a geometric notion, that is to say, the frame is not preserved by the geometric functors.
The point of geometric logic/locale theory is that you can externalize the locales who leaves inside a topos [the externalization is doable only because you use the geometric logic, that is to say, you sue only what is preserved under the geometric functors].
>In one word, geometric logic permits to do topology in any topos AS IF we were in SET = sheaves over 1. the good topology is not the classical topology with complements and all the usual semantic of the material implication in topological spaces.
The good topology in any topos [so in SET = sh(1)] is done in geometric logic.

>>7523559

So for instance, you begin in a topos. inside the topos X = sheaves(site) , you construct a geometric theory [of the reals say]
you have inside the topos a internal locale L of the reals + a internal frame, dual to the internal locale. [in fact, the internal locale does not exist, it is formally the dual of the frame; only the frame exists in the topos].

You can externalize the internal locale L of the reals. that is to say, you construct a geometric functor/a map Y -> X.
>Then there is what steven vickers call the fibrewise property.

If, in general, you wish to construct something with the localic reals, say take a subspace j:U=[0,1] >->R, then you can avoid doing it from inside the topos [where you must deal with the frames of opens, since the internal locale is purely fictional in the topos.]. Concretely, instead of defining what would be the internal frame of U in X, in terms of opens and covering relations, plus a map frame(R)->> frame(U), you do it externally in saying ''I construct the locale U->1 via a geometric theory [rigorously, in sheaves over 1, that is to say in SET]; I build geometrically a map j : U >->R [in SET] [rigorously a commutative triangle U->1, U>->R, R->1], so I can say that, since all my reasoning is geometric, I can pull back j, along the geometric functor X->sh(1), in order to get my sublocale U>->R over X [instead of initially over 1]
You can do your construction externally, if and only if your construction works ''fibrewise'', that is to say, if your construction is preserved under pullbacks of geometric functors, that is to say, your construction is geometric.

I just copy what I found here, even though the guy mixes constructive-predicative with intuitionistic at the end [since he talks about the interior of (U–P)uQ as the semantic of the material implication [which is forbidden since it is not preserved by geometric functors]

>>7523560
http://rin.io/swashbuckling-topoi/

>Why? The idea is this:
>Constructive reasoning allows maps to be treated as generalized points.
>Locales give a better constructive topology (better results hold) than ordinary spaces.
>The constructive reasoning makes it possible to deal with locales as though they were spaces of points.

>Conceptually, a locale is a propositional geometric theory pretending to be a space.

>space <> logical theory
>point <> model of the theory
>open set <> propositional formula
>sheaf <> predicate formula
>continuous map <> transformation of models that is definable within geometric logic
>Opens are Propositions

>A topology (on U, say) has enough lattice structure to model intuitionistic logic: ∩ and ∪, which both preserve openness, model the connectives ∧ and ∨.

>If a proposition P <> open set P,
>then ¬P <> the interior of U–P
>If a proposition Q <> open set Q,
>then P->Q <> the interior of (U–P)uQ

>When I say that a topos is a “generalized space,” it is a space in which the opens are insufficient to define the topological structure, and sheaves have to be used instead.

finally, I add that the sheaf toposes might not be the necessary and sufficient semantics for geometric logic. Apparently, what is called an arithmetic universe is so.

>>7523556
>other people in the fields are everybody in HOTT, palgrem, paul taylor, steve vikers, maietti, all the people in synthetic topology.
plus coquand and lombardi for the field of abstract algebras [fields, rings...]

>>7523556
>no PEM,
actually there is PEM up to Q, because the equality up to Q is decidable.

First of all, I do highly appreciate formal topology framework. However, how close is that to reproduce the usual theorems of analysis? I saw Paylor Taylor did quite a bit in that direction. ASD language, however, was far from being easily tractable by the time I looked at his lambda calculus for analysis. The thing with Bishop's style is that it's extremely natural and understandable. Looking forward to see more comprehensible derivations within ASD and formal topology.

ASD is really Topology as lambda-calculus. You must break into the formalism.

I think that there are two good introductions:


A Concise Presentation for Locally Compact Spaces, Paul Taylor
http://www.paultaylor.eu/ASD/conplc/conplc.pdf
The Dedekind Reals in Abstract Stone Duality Andrej Bauer and Paul Taylor 2009
http://www.paultaylor.eu/ASD/dedras/dedras.pdf


To me, Bishop is too close to classical mathematics in his formalism. I prefer arrows like in categories. I find them more rigorous and far far clearer than the bourbakian formalism.

>>7523783
ASD is really Topology as lambda-calculus. You must break into the formalism.

I think that there are two good introductions:


Overt Subspaces of Rn [in ordinary formalism for the traditional undergraduate] 2014
http://www.paultaylor.eu/ASD/overtrn/overtrn.pdf
A Concise Presentation for Locally Compact Spaces, Paul Taylor 2013
http://www.paultaylor.eu/ASD/conplc/conplc.pdf
The Dedekind Reals in Abstract Stone Duality Andrej Bauer and Paul Taylor 2009 [the picture is form here]
http://www.paultaylor.eu/ASD/dedras/dedras.pdf

To me, Bishop is too close to classical mathematics in his formalism. I prefer arrows like in categories, at least before using the ordinary notation. I find them more rigorous and far far clearer than the pure bourbakian formalism.

Since he is all alone, I do not think that he made crucial headways since you look at him.

>>7524342
>Overt Subspaces of Rn [in ordinary formalism for the traditional undergraduate] 2014
there is a bit on Bishop in this draft, see the picture.

it seems that he vulgarizes currently, more than pushing the development of analysis. he works on
http://www.paultaylor.eu/ASD/equitop/categories-110220
>Equideductive Topology seeks a new language for computable general topology.

>Whereas ASD gave an account of computably based LOCALLY COMPACT spaces,
the leading concrete model of the new theory is the category of all SOBER
topological spaces (in the traditional sense, rather than my abstract one).
Also, the two theories are based on different fundamental categorical ideas.
Whilst they have a lot in common, neither strictly speaking generalises
the other, so it is appropriate to regard this as a NEW research programme.

>The word "equideductive" is a double pun on Dana Scott's equilogical spaces
and on reasoning with equations. One of its motivations was to find out
exactly what kind of logic is needed to construct a cartesian closed
extension of categories of topological spaces. Indeed, this was the
first piece of work that I did with equideductive logic, but it is still
very unclear to me how the additional spaces behave, so I am nowhere near
ready to release a draft paper about them.

but you are right that doing topology through lattices is not funny at all. This is a good argument for geometric logic, since it wants to do topology with (generalized) points and, besides being tedious, the lattices are not even a geometric notion.

>>7522923
I lol'd

>>7524342
What are his axioms?

>>7524342
Well, that said, I do like formal topology approach and also ASD. I also find category-theoretic language absolutely superior. But I think that regardless of formalism that you use, the essence of right mathematics (we are talking about constructive mathematics here) is algorithms. This is the most essential difference to classical mathematics with its Oracle. Formalisms are merely wrappers for algorithms. They are as good as they represent algorithms concisely and clearly. And of course appropriate for automatic algorithm extraction and implementation in programming languages. Because that's the reason why we care at all.

Really in view everybody's stance should start with asking oneself:
1. Do I allow arbitrary choice algorithms for which no finite description of the rule can be given? (AC)
2. Do I allow an algorithm-generating machine? Each algorithm has a finite description, but there is no way to predict its behavior except that to require so or so property. (ACC)
3. Do I allow only explicit algorithms? I. e. no black box generating machine. All algorithm descriptions are available to the theory.

I think countable choice really means an algorithm-generating machine and as such it has a poor justification.

By the way, Munich school has already done some progress formalizing a bit of analysis in choice-free environment. The programs are quite tractable thanks to the simplicity and closeness of the formalism to computer programs.

Do you agree with my line of argument regarding 1., 2. and 3. here >>7524818?

The Axiom is only that until that math is proven by another??

>>7524956
You what or is axiom that or math is? Or?

>>7524818
indeed every student must reflect on the classical mathematics taught, but the teachers being classical mathematicians themselves and not even caring about it, it is a lost cause.

I think that the (finite) algorithms halting are a good compromise between the classical maths and the ultra-finist maths.
Recently, I have been very sceptic, up to having doubts about the halting (finite) algorithms themselves, say to generate N, compared to ''direct'' knowledge of a natural number. I do not know whether it makes sense to say that the set of natural numbers exists, for instance.


What do you think of the co-SHEP
http://ncatlab.org/nlab/show/presentation+axiom

On nlab, it is said that the co-shep implies the countable choice.
>Although perhaps not well known in the literature of constructive mathematics, the CoSHEP axiom may be justified by the sort of reasoning usually accepted to justify the axioms of countable choice and dependent choice (which it implies, by Proposition 1 below).

>To be explicit, every set A should have a ‘completely presented’ set of ‘canonical’ elements, that is elements given directly as they are constructed without regard for the equality relation imposed upon them. For canonical elements, equality is identity, so the BHK interpretation of logic justifies the axiom of choice for a completely presented set. This set is P , and A is obtained from it as a quotient by the relation of equality on A. This argument can be made precise in many forms of type theory (including those of Martin-Löf and Thierry Coquand), which thus justify CoSHEP, much as they are widely known to justify dependent choice.

Note that ASD consider /top and \bottom in doing topology.
On the computational side, like Taylor says, it means that there are two knowledge
-the one of halting [when the open/proposition is true in the model]
-the one of nontermination

>Computationally, we understand the elements > and ⊥ of Σ as termination (“yes”) and nontermination (“wait”) respectively; Σ is not a “Boolean” type, as there is no definite “no”

in constructive-predicative locale theory, there is no consideration of anything that is not \top, when we consider the opens/propositions. So in geometric logic, there is only halting programs.
I think that this is one of the main differences between the two approaches.

>>7524999
I think that having projectives in SET is already a from of AC. In my view, no matter what form of AC we assume we end up having some peculiar black boxes containing some algorithms which nothing can be said about. I personally don't find it nice. Another strong argument against ACC is that it can be avoided in suprisingly many cases.

>Recently, I have been very sceptic, up to having doubts about the halting (finite) algorithms themselves, say to generate N, compared to ''direct'' knowledge of a natural number. I do not know whether it makes sense to say that the set of natural numbers exists, for instance.
Well, in my view an algorithm is more fundamental than a set. Regarding N ... well. N is already quite basic. Of course at some point we end up giving cyclic definitions. Indeed, how to count algorithm's step let alone everything else countable without some notion of N. But such a cyclicity is not that bad I think. Regarding Q, R etc. it is natural to define them symbolically as wrappers for basic terms (see the book that I referenced).

>>7524794
>What are his axioms?
for what theory

the most readable axiomatic is the one in >>7524342
>A Concise Presentation for Locally Compact Spaces, Paul Taylor 2013
>http://www.paultaylor.eu/ASD/conplc/conplc.pdf
>The Dedekind Reals in Abstract Stone Duality Andrej Bauer and Paul Taylor 2009 [the picture is form here]
>http://www.paultaylor.eu/ASD/dedras/dedras.pdf
he believes in the set N, in the type \Sigma [the object classifier \Omega in topos theory and in constructive locale theory], in biproducts, in exponentiation [of compact stuff of course]

>>7525004
I think it is worth referring to this paper of Bauer and Taylor on Dedekind reals and their computational content in the context of ASD: math.andrej.com/wp-content/uploads/2008/08/abstract-cca2008.pdf

It turns out that pic related. There is the problem with Dedekind reals. I don't find them bad, but appealing are they definitely not. Unlike controlled Cauchy sequences which are readily computer programs.

>>7525010
> exponentiation
I hope he is careful enough with this.

>>7524965
I is or mean only math that until or axiom

I need to bump this for a couple of days more. Interesting discussion

bump

many have said that AC is needed in physics. It is actually debatable in quantum physics


for gleason theorem:

H. BILLINGE , A Constructive Formulation of Gleason’s Theorem, Journal of Philosophical Logic, vol. 26, no. 6, pp. 661–70, 1997


F. RICHMAN and D. BRIDGES , A Constructive Proof of Gleason’s Theorem, Journal of Functional Analysis, vol. 162, no. 2, pp. 287–312, 1999


for the spectral theorem:


B. SPITTERS , Constructive and intuitionistic integration theory and functional analysis, PhD thesis, Radboud University Nijmegen, 2003
B. SPITTERS , Constructive Results on Operator Algebras 1, Journal of Universal Computer Science, vol. 11, no. 12, pp. 2096–113, 2005
in general:

D. BRIDGES , Can Constructive Mathematics be Applied in Physics?, Journal of Philosophical Logic, vol. 5, no. 11, pp. 382–453, 1999
D. BRIDGES and K. SVOZIL , Constructive Mathematics and Quantum Physics, International Journal of Theoretical Physics , vol. 39, no. 3, pp. 503–15, 2000

many have said that AC is needed in physics. It is actually debatable in quantum physics


for gleason theorem:

H. BILLINGE , A Constructive Formulation of Gleason’s Theorem, Journal of Philosophical Logic, 1997


F. RICHMAN and D. BRIDGES , A Constructive Proof of Gleason’s Theorem, Journal of Functional Analysis, 1999


for the spectral theorem:


B. SPITTERS , Constructive and intuitionistic integration theory and functional analysis, PhD thesis, Radboud University Nijmegen, 2003
B. SPITTERS , Constructive Results on Operator Algebras 1, Journal of Universal Computer Science 2005
in general:

D. BRIDGES , Can Constructive Mathematics be Applied in Physics?, Journal of Philosophical Logic, 1999
D. BRIDGES and K. SVOZIL , Constructive Mathematics and Quantum Physics, International Journal of Theoretical Physics , 2000

>>7525355
Pleb here. When does one typically encounter this sort of stuff in their mathematical education?

>>7526785
I am a ph.d student and I never encountered this. I have run into zorns lemma and the axoim of choice in functional analysis but it never got this obsure/esoteric

>>7526785
when the teachers will begin to reflect on what they are doing in wondering what they want for once in their lives.

the mathematical education is the most outdated that we have today.
It is detrimental in other fields, such as physics and philosophy.

>>7526797
Gotcha, thanks. There isn't much of a chance I will ever encounter this then

>>7526803
Could you elaborate on how it is outdated? If that wouldn't deviate too much from the thread that is.

>>7526830
>>Could you elaborate on how it is outdated?
math is the discipline of abstraction, so math is

-the learning of the deduction
so we must learn the logic, but today logic is not learnt and second, the logic used day after day is the classical one

the point is to expose the various systems of reasons

logic today connects heavily with computers.
-after exposing the frameworks of abstract discourse, we must show that it is relevant to applied fields, to the every day life.
Typically, this would mean that in physics, for instance , for once, the physicist understands that he works with models before he can claim that his favorite models ''describe indeed the reality''


then the content of the course.
First, everybody forgets their lectures.

Then the point is not to stop at this old maths, like say doing on euclidean geometry, but , at least, to mention that there are other geometries.
that we can do topology without the epsilon-delta. that we can do category theory instead of set theory [the book in cover is a good book to start with category theory]


so today, the teaching exposes only a minute part of what math is, and inside this minute part, many mathematicians do not use today what the students learn today.

>>7526909

in the 70s, the liberals tried to improve the general level with new maths

https://en.wikipedia.org/wiki/New_Math

it is was a disaster since, as usual, irrespective of the relevance of the idea, as soon as the idea goes into the political field in republics, it turns into an excess which renders it sterile.

Plebs did you get your answers? Then leave the thread please

bump for this post
>>7525013

>Emma-Stone-fag why is Axiom of Choice valid in constructive mathematics including HoTT?
The fuck do you ask me?

Per Martin-Löf has a chapter on the axiom of choice in the text on (one version of) his theory, maybe that helps.
http://www.cip.ifi.lmu.de/~langeh/test/1984%20-%20Loef%20-%20Intuitionistic%20Type%20Theory.pdf

I don't quite understand your oracle thingy.

>Why can we literally treat Brouwer–Heyting–Kolmogorov interpretation and assume that if
<span class="math">\forall (n \in N).\ \exists (x\in X).\ \varphi [n,x][/spoiler]
then there has to be a function
<span class="math">f : N \to X [/spoiler]
>such that merely
<span class="math"> \varphi [n,f(n)] [/spoiler]
>and there is no fucking way to predict behavior of this magical function besides that
<span class="math"> \varphi [n,f(n)] [/spoiler]
>holds?

Seems there's no room for wishing and assuming here. What I can say is that to prove the proposition
<span class="math"> \Pi (n : N).\ \Sigma (x : X).\ \Phi [n,x] [/spoiler]
you need to find a function <span class="math">F[/spoiler] from <span class="math">N[/spoiler] into
<span class="math"> \Sigma (x : X).\ \ Phi [n,x] [/spoiler]
and then, by definition of Sigma, <span class="math"> F(n) = (f(n),g_n) [/spoiler] is always a pair with <span class="math">f(n) : X [/spoiler] and <span class="math"> g_n : \Phi [n,f(n)] [/spoiler].
So your task was constructing <span class="math"> F [/spoiler] and then <span class="math"> f = \pi_{left}\circ F [/spoiler].

Regarding extracting algorithms from proofs, I came acres the most dry book ever here
http://www.cambridge.org/us/academic/subjects/mathematics/logic-categories-and-sets/proofs-and-computations

>>7526923
Pic related
>does set theory make ill?
was on the cover of the kind of German Guardian back then.

>>7527138
The books on type theory don't give any new insight except that traditional explanation based on BHK which Bishop himself used. (pic related)

>I don't quite understand your oracle thingy.
What exactly you don't understand?

Your further line of argument suffers from the already somewhat traditional flaws of accepting the Axiom of Choice. Inside the theory, it does allow existence of certain functions WITHOUT having to construct them explicitly. If not then what's the point at all? You understand that the wording:

in order to prove
<span class="math"> \displaystyle \forall (n \in N).\ \exists (x\in X).\ \varphi [n,x] [/spoiler]
you need to find an appropriate function

makes the need for the Axiom of Choice totally flawed?

Explain WHY do you need AC when you already defined precisely what it means to prove a П_2 sentence?

The answer is because it does the dirty work for you: you don't have to construct functions rigorously, you can rely on AC to do it for you. Believe me they wouldn't introduce AC if there were no need for it. Clearly, theory with and without AC seem to be the same in the light of BHK, but they do differ dramatically. For instance, Cauchy reals in presence of AC are Cauchy complete whereas without AC they're not. That's a big difference. The point is that BHK is merely a metamathematical interpretation.

>>7527138
> Helmut Schwichtenberg
But he is known to be an opponent of Axiom of Choice users.

>>7527645
I can't help you, I don't understand the problem. (But I also don't understand the subject very well and I also don't really care for it. You know, I care for thermodynamics and stuff.)

>>7527835
What exactly you don't understand?

>>7527933
From my understanding (which is probably very false because you seem to have a problem somewhere), in those type theories, choice (in some form) either holds or not - it's not an axiom you decide to include or not in the definition of the theory.
If you prove it to be true for your theory at hand, you do so constructively and whenever you use it later, you can refer to the associated proof/algorithm you've established when you proved choice holds.

>>7526909
Thank you for the thoughtful response and resource. I am just now taking algebraic structures, but I spent part of the summer exploring set theory, mathematical logic, and similar areas, so I think I may be able to digest some of this.

>>7528046
I have looked at the book you referenced. Besides being indigestible, it doesn't seem to extract anything from Axiom of Choice.

Do you know any example in type theory, how a program algorithm is extracted from some proof that uses Axiom of Choice somewhere?

>>7528046
you can add the ac if you want

>>7529034
> this functions is not specified or determined in any known way
nuff said

exactly

>>7522829
>Why can we literally treat Brouwer–Heyting–Kolmogorov
We can and the resulting axiom will be sound with respect to BHK. Actually very similar axiom known as Church Thesis in constructive mathematics were considered for years. And number of principles for HA based on the intuition of that kind of literally reading of BHK had been actively used and studied within Markov school of constructivism.

>>7529095
Exactly what?

>>7529095
Hello?

bump

bump

bump

So let's clarify it once and for all.

I require answer to this >>7529247

>>7530904
exactly this>>7529060
>> this functions is not specified or determined in any known way


are you also a predicativist ?

>>7530988
Oh at last. So now I am convinced that advocates of Axiom of Choice really suffer from Münchhausen's syndrome

>are you also a predicativist ?
Yeah. I'd say so. What's the point to be a constructivist without being predicative?

>>7530996
>What's the point to be a constructivist without being predicative?
to be an intuitionist, I guess.

>>7531006
To be honest, I'm not so familiar with their difference. What does intuitionism say about the Axiom of Choice?

So let us conclude this thread by the following question:

So it is actually not possible to retrieve a computer program from the Axiom of Countable Choice?

bump

bump

So what's about this last question? Has anyone ever seen an algorithm extracted from constructive Axiom of Choice?

bump

>>7532646
all I know is that the constructive proof that ''AC => LEM'' by Dianocescu takes AC as countable choice.

[so classically, you say that ''noLEM=> noCountable choice'' which leads the constructivist to claim that ''to reject LEM implies the rebutal of {countable) choice'' ]

>>7532646#
all I know is that the constructive proof that ''AC => LEM'' by Dianocescu takes AC as countable choice.

[so classically, you say that ''noLEM=> noCountable choice'' which leads the classical mathematician to claim that ''to reject LEM implies the rebutal of {countable) choice'' ]

>>7532932
But constructive ACC and classical ACC are quite different things

>>7532948
D. uses the existence of a choice function on {X, Y}; since the family {X, Y} has only two sets, it is the ACC which is applied, is it not ?


onwiki

>In Martin-Löf type theory and higher-order Heyting arithmetic, the appropriate statement of the axiom of choice is (depending on approach) included as an axiom or provable as a theorem.[9] Errett Bishop argued that the axiom of choice was constructively acceptable, saying "A choice function exists in constructive mathematics, because a choice is implied by the very meaning of existence."[10] In constructive set theory, however, Diaconescu's theorem shows that the axiom of choice implies the Law of excluded middle (unlike in Martin-Löf type theory, where it does not). Thus the axiom of choice is not generally available in constructive set theory. A cause for this difference is that the axiom of choice in type theory does not have the extensionality properties that the axiom of choice in constructive set theory does.[11]
>The proof relies on the use of the full separation axiom. In constructive set theories with only the predicative separation, the form of P will be restricted to sentences with bound quantifiers only, giving only a restricted form of the law of the excluded middle. This restricted form is still not acceptable constructively.
In constructive type theory, or in Heyting arithmetic extended with finite types, there is typically no separation at all - subsets of a type are given different treatments. A form of the axiom of choice is a theorem, yet excluded middle is not.
https://en.wikipedia.org/wiki/Diaconescu%27s_theorem

>>7532965
In Martin-Löf's type theory, AC is a theorem. He clearly states that the proof of the antecedent already implies a function. To derive AC, it's just a matter of reformatting.

But the reason that AC is used in constructive math is deeper. Indeed, in most cases it is really an axiom, not a theorem, and there is a reason to assume it. However, it is debatable if such a principle is constructive. There is Gödel numbering of all computable functions and AC just implies that some suitable Gödel number is pulled out of a pocket. It does not give any information, which one exactly. I saw some stuff on algorithm extraction, but it all uses bar induction that is not constructive. Even though, AC does provide a computable function, it does not provide any information which one exactly. It seems to be constructive since the function is really computable, but no effective program can be extracted since we don't know which exact algorithm is in the black box.

This is quite a deep and disturbing observation.

>>7533015
>Even though, AC does provide a computable function, it does not provide any information which one exactly.
right, this is a point to have in mind

I am really lost between all the versions of AC, and what implies AC, what AC implies, in what theory and not in other theories. It is very nebulous.

>>7533032
That's why I take a pure algorithmic and programmer's stance and reject AC. As you can see this book http://www.mathematik.uni-muenchen.de/~schwicht/seminars/semss13/constr13.pdf develops constructive analysis from type level 0 objects without black box algorithms which are of no use. Moreover, apart from indigestible works that use the language of type theory or mathematical logic only, this setting provides readable examples of program extraction http://www.mathematik.uni-muenchen.de/~schwicht/papers/uppsala05/uppsala05.pdf.. There is also a handful of examples of extracted programs in Minlog (Scheme) on their website.

There is also a setting that uses Dedekind reals without choice, but their computational content is quite poor.

That's the situation so far.

>>7523556
Do you agree on the conclusion of this thread? >>7533059

Sorta related to the thread: There is an open seminar in Paris in 2 weeks.

http://ercpqg-espace.sciencesconf.org/resource/page/id/1

>>7533208
Will you be there?

>>7533246
No, but I try to be at the TQFT Seminar in Vienna one month later - I'm moving back there.

http://www.esi.ac.at/activities/events/2015/higher-topological-quantum-field-theory-and-categorical-quantum-mechanics

I'd mostly like to talk with Schreiber, but not even he knows when his on is yet.

>>7533208
seems that many important people will be there

>>7533266
Fuck me Emma-Stone-Fag. You're so cool. You talk to Schreiber like to a Kumpel. I talked only to Schwichtenberg once and it was more formal.

>>7533267
The month after, the frenchies have one organized by Connes and this one guys waifu

>>7533273
I feel there's no need to fear anyone of the under 40 SO crowd. I think it was OHP who's afraid of asking dumb questions on the nforum - that's silly.

>>7533291
I am jelly and glad about you at the same time. If you only knew how I struggle with shitty fixed-terms contracts, useless PhD and lack of publications because of lack of time. If only I had a good position like Urs and could apply for projects I like ... Well, it's just a lyrical digression. Sorry

>>7533301
If it helps, I'm far away from getting money for the stuff that would actually interests me. Pretty certain nobody in the 150 people institute I work with could tell you what a topological space is.

>>7533309
Thanks for the great discussion. So as a concluding remark, would you agree on
>>7529060
>>7533015
>>7533059

>>7533382
Well, because I don't know it, I must take the claim for granted, that the type theories choice (in the AC) is not constructive (even if the chosen function is).
That's not nice.

It does not bother me, however, to have a logic which involved propositions or functions that are
>not specified or determined in any known way.
Just like "(P and Q) implies Q" is a usefull statement about propositions where it doesn't matter too much what P and Q say (it's not specified further in our logic), I don't mind studying logics where functions are not determined to the level of being a recursive scheme.
Maybe I'm reasoning about a procedure <span class="math">f : \prod_{x:A} B(x)[/spoiler] and machine in the real world (where irl things A and B may be characterized in more detailed).
The logic reasoning about <span class="math">f[/spoiler] will be valuable to me, even if many things are left open
- left open from the perspective of a person that requires the only things allowed to be left open are the stirngs "0", "1", "2", ..., who believes in lifts, recursively defined + and · and then requires all functions in the theory must be constructive in the sense that they are defined somehow with the above tools.

It's like as if you'd disregard logical languages because it has semantics that specify the content more uniquely.
>We got Kripke semantics, so all those modal logics are just some languages, talking about some systems (sets) and not even specifying them uniquely
But I think it's harder to get new ideas if you work on that level.
There are so many logics... like...
https://en.wikipedia.org/wiki/Linear_temporal_logic#Syntax
>Why not just specify all events as points on the real line??

I'm fond of saying that the strength of some systems come with the weak specifications of it's components (I think I once came up with a German pun, but it doesn't translate).

I'm not in the foundation business, though, maybe that's why I worry less.
Maybe "One (constructive?) system!!" is a spook.

>>7533535
PS: And if there's a single thing to take away from my post here, then it's this:

This is a critical time in my life. Depending on what happens next, it's possible that for the rest of time, there will always be some time in the future when I will like chocolate. However, if the wrong thing happens next, then all bets are off and there's no guarantee about whether I'll ever like chocolate.

>>7533301
there was a phd position in HOTT with bauer

and there is a new one
http://math.andrej.com/

it would be another phd, but it is only a few years and in a booming slovenia.

Really nice discussion. I'm a bit upset that it goes to an end.

At least, I hope we learned something useful about AC.