What does /sci/ think of Intuitionist mathematics? I mainly work in functional analysis, so proof by contradiction is pretty essential. I want to convince myself rejecting the principle of excluded middle is stupid.
>>7707156
intuitionistic logic doesn't *have* to drop the law of the excluded middle, it just isn't axiomatic.
the fun is finding out how much you need it and in what form. you should look at topos theory. it was started by grothendieck (who started in functional analysis), and we now have a pretty good grasp on topoi enough to name some qualitative properties which will give you say, excluded middle, or choice.
a topos is "essentially" the model categories of intuitionist theories (and the theories themselves, depending on which point of view you take).
what's cool through intuitionism is that you can find out *which* topoi have excluded middle.
all in all, it's up to you and what you want to imagine. if you have a reason to be concerned about consructability, then you may want something weaker. if you are ok with anything you can imagine holding true, then go with topoi with excluded middle.
You can also ask about other properties in these settings. do you want extensionality, etc.
Enjoy your principle of excluded middle.
>>7707172
From a very cursory look at these topos, I don't really see what makes them distinct from sets of axioms besides semantics. That being said, I'll definitely have to take a look a deeper look.
I wasn't very clear in my original post, but I guess I'm more curious about Intuitionism (especially Brouwer's philosophy) as it relates to altering the logical basis of math. Classical predicate logic maintains the principle of excluded middle as axiomatic, so what are the arguments for why mathematics should privilege a different logical basis? Then again, we might as well ask why math should choose classical predicate logic as a basis.
[math]\mapsto[/math]
>>7707239
>Classical predicate logic maintains the principle of excluded middle (LEM) as axiomatic, so what are the arguments for why mathematics should privilege a different logical basis?
As the other anon points out, it's not a question of disregarding richer and "more careless" axiomatic frameworks, it's a matter of application.
If you reason about a subject that includes the statement
>It's true that today I'll eat at MacDonalds OR it's false that today I'll eat at MacDonalds
i.e. [math]M \lor \neg M[/math] where the semantics (I should maybe say 'subject', as semantics is used more technically too) of [math]M[/math] are "today I'll eat at MacDonalds ".
then adoption LEM is likely what you want to do.
If you reason about a subject that includes the statement
>It's the case that the talking stone is blue OR it's not the case that the talking stone is blue
I'm not sure anymore.
If you drop LEM, then your theory necessarily proves less theorems. What's nice is that you can then also adopt new non-constructive axioms, which if together with LEM would have produces an inconsistency. I.e. there are interesting theories which you can't axiomize in classical logic because of this.
Pic related is a theory of smooth closeness which breaks down by adding the nonconstructive LEM
https://en.wikipedia.org/wiki/Synthetic_differential_geometry
The message here is that by adopting this rule of inference, you actually choose the math you work with: given the axioms which are about the semantial things proper (vector space laws, MacDonalds laws, etc.) you also define that theories by the rules of inference you use. I.e. you narrowed down the range of possible theories by doing actively deciding the rules of logic. That's why it's interesting to see which part of functional analysis, say, does still hold in the weaker world of reasoning.
Finally: Why drop LEM and not some other law in classical logic? Why is LEM termed the nonconstructive one.
(cont.)
An appealing aspect of intuitionistic logic is that is has faithful semantics (in the sense of: let [math]M[/math] mean that „today I'll eat at MacDonalds.“) in something real, namely actions.
https://en.wikipedia.org/wiki/Brouwer%E2%80%93Heyting%E2%80%93Kolmogorov_interpretation
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
This logic is precisely the one which you can use to describe a cooking recopy or a programming language:
Read [math]A \land B[/math] (interpretation in logic: „it’s true that A holds and it’s true that B holds“) as
>I have a proof/reason to believe/argument for A and I have a proof/reason to believe/argument B
Read [math]A \lor B[/math] in the same way.
Read [math]A \to B[/math] (in logic: „if A is true, then B is true„) as
>If I have proof/reason to believe/argument for A, then I can conceive a proof/reason to believe/argument
and [math]\neg A[/math] (in logic „A is false“) as
>If I have proof/reason to believe/argument for A, then something’s wrong because that’s a contradiction and doesn’t make sense
The last connective is properly defined as [math]\neg A := A \to \bot[/math]
Now a statement like
[math](A \land B) \to A[/math]
is intutionistically true, because if I have a reason to believe A and one to believe B, then in particular I have a reason to believe A. Computationally, this „proof I just give corresponds to a function [math]f[/math] of type
[math](A \times B) \to A[/math]
i.e.
[math]f : (A \times B) \to A[/math]
namely
[math]f = \langle a, b\rangle \mapsto a[/math]
or written differently,
[math]f = p \mapsto \pi_1(p)[/math],
where [math]\pi_l[/math] is the left projection operation.
(cont.)
A reason g not to believe A, i.e.
[math]g: \neg A[/math] or [math]g: A\to \bot[/math]
can be read as a function that takes an argument a and A but never terminates. g(a) is looping on your hard drive forever.
The statement [math]A \to \neg ( \neg A )[/math] is also true: Having a reason to believe A means that also having a reason not to believe A would already be a contradiction.
The computational proof [math]h : A \to ( (A \to \bot) \to \bot) [/math] is simple too:
[math]h = a \mapsto ( H \mapsto H(a) )[/math]
Given an argument ‚a‘ and then a looping function [math] H : A\to \bot [/math], plugging in ‚a‘ into H will trigger an unending loop - the type matches.
But [math](A\to \bot) \to \bot \to A[/math] is constructively not true. To logical argument is this: Merely knowing that ‚a reason to believe A is absurd‘ would be absurd - this in itself is not a constructive argument for A.
Maybe the computational semantics is more clear here: Asking for a function of type
[math]( ( A \to \bot ) \to \bot) \to A[/math]
is asking for way to construct a term ‚a‘ using a functional which takes looping functions in [math]A \to \bot[/math] as argument but never terminates. How would a terms ‚a‘ ever come from this?? It doesn’t.
A more complicated but not too hard example, to conclude this, would be
[math] ( \neg A \land \neg B ) \implies \neg ( A \lor B ) [/math]
>If ‚A is false‘ as well as ‚B is false‘, then neither is 'A or B'.
or
[math] ( ( A \to \bot) \times ( B \to \bot ) ) \to (A+B) \to \bot [/math]
where + is the direct sum.
If next to the projection operators you introduce the programming concept of if-clauses now (as you have them in C++ or Phython), you’ll be able to proof this claim.
Indeed, provability and programmability coincide now, that’s the pretty thing.
Those few pages of pic related (booktitle in title) are a nice read.
Closer to you is maybe
https://en.wikipedia.org/wiki/Brouwer%E2%80%93Hilbert_controversy
>But [math](A\to \bot) \to \bot \to A[/math] is constructively not true.
Here, of course, I meant
[math]((A\to \bot) \to \bot ) \to A[/math]
or
[math](\neg ( \neg A) ) \to A[/math]
>>7707706
This looks interesting from a foundational point of view, but why would an analysis care? Is there any reference for intuitionistic analysis in abstract integration or functional analysis?
>>7708352
If by "analysist" you mean a guy who's studying classical analysis, then the question has probably no answer.
Dropping non-constructive axioms of your theories becomes relevant, for example, whenever you got to implement stuff. As you can't even list the element of [math]\mathbb R[/math], theorems in classical analysis will be vacuous for such realization. The good news is that people have spun the spiderwebs of theories like analysis in a constructive fashion long ago, see for example all the constrictive theorems that aggregate around the unprovable intermediate value theorem
https://en.wikipedia.org/wiki/Constructive_analysis#Examples
Syntetic analysis as in the pic from the book by Kock is relevant because the requirements for the theory are such that certain topoi give you internal analysis as a gift. That is you consider some topos, check if it has this and that property and then it might be implied that that topos really is about calculus/contains a theory of calculus and you can import all the theorems you already know - I mean that's the nice feat of category theory in general.
The category of sets [math]A, B, C,...[/math] (=objects) and functions [math]f, g ,h,...[/math] (=arrows) is a topos and thus has cartesian product [math]A\times B[/math] (=the categorical product) and function spaces [math]B^A[/math] (=internal, setty realizations of the arrow class from [math]A[/math] to [math]B[/math], which may be written [math]A \to B[/math])
A theorem of sets is that the function space
[math] (A\times B) \to C [/math]
is isomorphic to
[math] (B\times A) \to C [/math]
as well as
[math] A \to C^B [/math]
and
[math] B \to C^A [/math]
E.g. for A=B=C the reals the first space contains
[math] \langle a,b \rangle \mapsto \sin(a)+3b [/math]
which you can systematically map to the function
[math] \langle b,a \rangle \mapsto \sin(a)+3b [/math]
in the second space, or the function
[math] a \mapsto (b \mapsto \sin(a)+3b) [/math]
or
[math] b \mapsto (a \mapsto \sin(a)+3b) [/math]
The axioms of a topos have more than the sets as model, for example it provides an (intuitionistic logic), where the iso above means
„A and B being true implies C“
is equivalent to
„A being true implies B being true implies C“
Or you can take the classical identifications of the set theoretic operations as numerical operations. Forgetting what your finite sets are about, the above relation is the basic identity of numbers
[math] c^{a·b} = {c^a}^b [/math]
In the other direction, the relation
[math] c^{a+b} = c^a·c^b [/math]
provable in a topic, at the same time tells you for the categories of sets (where + is the disjoint/tagged union) that the function space
[math] (A+B) \to C [/math]
is iso (i.e. in bijection to) to
[math] (A\to C) \times (B\to C) [/math]
In logic,
„one of A or B being true already implies C“
is equivalent to
„A implies C and also B implies C“
In the other direction, a derivation rule like modus p.
„From A and A implies B follows B“
being true guarantees you that the function space
[math](A\times B^A)\to B[/math]
isn’t empty
Indeed, the evaluation function
[math] eval (a,f) := f(a) [/math]
works no matter which sets A and B are.
What I want to say is this: Formulating analysis synthetically in a basic object like a topos (as opposed to something hard to construct like R), makes theorems of analysis more than theorems of just analysis. And secondly, if you know that analysis works if a topos has this and that axioms, then you can further build your theory (like quantum field theory, kek) in such a setting without restricting you to muh reals and muh epsilons. Although the reals are nice of course.
the first number identity should was supposed to be
[math] c^{a·b} = (c^a)^b [/math]
I gave the example of how you find sets (and closely related: arithmetic) and logic in the same syntactic framework. Of course, what's nice is that at the same time you speak about typed lamdba calculus (i.e. a programming language) and, and this is the origin of the ideas (Grothendieck), the catgories of sheaves (topology, algebraic geometry) are to be found just one specification further.
Here I digress, sorry. I also have to say that speaking in this generality is exhausting and if you don't have a particular topos in mind the proofs in this subject are boring to do, imho.
