How orthodox is Constructivist mathematics in modern academia?
I don't know a lot about mathematics, but I'm studying Kant right now and his proposition that mathematics is synthetic a priori has piqued my interest in the foundations of mathematics; I wanted to hear some thoughts from Veeky Forums on the matter.
Other urls found in this thread:
math.stackexchange.com
math.fau.edu
people.vcu.edu
en.wikipedia.org
math.andrej.com
en.m.wikipedia.org
en.wikipedia.org
axiomsofchoice.org
twitter.com
>Constructivist mathematics
Tl; dr for brainlets?
Like example of something invalid in constructive mathematics.
Well, like I said in the post, my mathematical acumen isn't very developed. From my understanding, intuitionists/constructivists reject the law of the excluded middle i.e. either a proposition is true or its negation is true, and replace this with a sort of 'burden of proof,' where truth must be demonstrated or 'constructed' by providing a method for the creation of the mathematical object. It effectively rejects all truths but constructed proofs in mathematics, hence its notoriety.
If I've misrepresented it, feel free to correct me anyone.
I'm not OP, but in constructivist mathematics you have a slightly weaker logic so you can think of it as a generalization of classical mathematics (like how rectangles are a generalization of squares).
The core difference is that in classical logic you always have double negation in the sense that if "not not P" is a true sentence in classical logic then "P"is a true sentence in classical logic. In constructive logic you do not have this in general (this doesn't mean that P is false, in fact there are times when double negation will hold for a specific sentence and times when it will not). Sometimes this core difference is described in terms of the excluded middle, the two ways are equivalent.
A side effect of this is that some axioms are so strong that they imply double negation for a specific theory and so it doesn't typically make sense to talk about them in the context of constructive mathematics. This includes the axiom of choice for instance.
Another side effect is that you are forced to distinguish between two different forms of proof by contradiction:
>Suppose P is true, reach a contradiction, conclude not P is true.
>Suppose not P is true, reach a contradiction, conclude [not not P is true and therefore] P is true.
The second form here is not valid under constructive logic.
If you think about it really hard we never actually prove a sentence is false in classical logic, instead we only prove that the negation of true. In constructive logic we emphasize this by ensuring that any proof for a statement is a direct proof and not the result of a bunch of double negations.
(cont.)
(cont.)
Typically (given a system with classical axioms), every constructive proof is valid under classical logic and arguably easier to both understand and believe. However, there are many classical statements that are unprovable by the use of constructive proofs alone. The usual response is to restate the constructively unprovable statement into one that is constructively provable AND that is classically equivalent to the original sentence. As a result, in constructive mathematics one may have alternative definitions and theorems that look different on the surface but are actually nicer (classically equivalent) versions of classical definitions and theorems.
More recently people have been exploring the use of systems with anti-classical axioms. These are axioms that would result in an inconsistent system under classical logic but do not under constructive logic. Here one actually abuses stacked negations and unprovable sentences to do interesting and useful mathematics.
Note: Above I've described this as constructive logic but the correct term is intuitionistic logic.
Do you have a special interest in intuitionistic logic yourself?
>More recently people have been exploring the use of systems with anti-classical axioms. These are axioms that would result in an inconsistent system under classical logic but do not under constructive logic. Here one actually abuses stacked negations and unprovable sentences to do interesting and useful mathematics.
Is there any reading material you can refer me to that expands on this? Also, appreciative of the insightful responses.
Top quality stuff user, but I have a doubt:
> A side effect of this is that some axioms are so strong that they imply double negation for a specific theory and so it doesn't typically make sense to talk about them in the context of constructive mathematics. This includes the axiom of choice for instance.
Could you explain this further, please? I'm not sure what you're talking about, especially at the first sentence (I'm a bit familiar with the Axiom of Choice's fuckery).
Also, an example of this:
> As a result, in constructive mathematics one may have alternative definitions and theorems that look different on the surface but are actually nicer (classically equivalent) versions of classical definitions and theorems.
would be really appreciated.
why don't people like proof by contradiction? i don't really get this.
This guy probably knows a lot more than me about the subject, but all of my professors seemed to regard constructivist mathematics as something of the past. They said pretty much no working mathematicians are of that mindset anymore.
I haven't spent any time checking their claims though, so take my word with a grain of salt.
Regarding the axiom of choice: math.stackexchange.com
>> As a result, in constructive mathematics one may have alternative definitions and theorems that look different on the surface but are actually nicer (classically equivalent) versions of classical definitions and theorems.
I think an example of this is continuity. For example, in Bishop's Constructive Analysis, continuity actually means uniform continuity.
People should be constructive as often as possible, but restrictive constructivism is a meme.
Constructivism isn't quite Wildberger-tier retarded, but it's similarly useless.
Because proof by contradiction rarely tells you anything about why a theorem is true. The common proof that sqrt 2 is irrational tells you very little about sqrt 2. Same with the common proof of the infinitude of primes.
>This guy probably knows a lot more than me about the subject, but all of my professors seemed to regard constructivist mathematics as something of the past. They said pretty much no working mathematicians are of that mindset anymore.
I attended this AMS workshop on constructive mathematics a couple of years ago: math.fau.edu
I don't know if that workshop is still being held though.
Which people? Brouwer? Kronecker? Bishop?
> I think an example of this is continuity. For example, in Bishop's Constructive Analysis, continuity actually means uniform continuity.
>I don't know a lot about mathematics
Do you know high school algebra?
>piqued my interest in the foundations of mathematics; I wanted to hear some thoughts from Veeky Forums on the matter.
I suggest you read a few books and work through the exercises:
Book of Proof by Hammack (people.vcu.edu
Elements of Set Theory by Enderton
The Joy of Sets: Fundamentals of Contemporary Set Theory by Devlin
Introduction to Logic: and to the Methodology of Deductive Sciences (Dover Books) by Alfred Tarski
Introduction to Metamathematics by Kleene
Can you explain how the hell constructivist philosophers justify rejecting double negation?
The fact that "not (not P) = P" seems so obvious to me I can't even fathom somebody seriously disagreeing with it.
I think one of the problems of not (not P) = P is that it yields oddities like this one: en.wikipedia.org
Also, try proving not (not P) = P. Then you'll see how unobvious it is.
axioms? i'll prove it.
I believe the point he is making is that proving
not(not P) = P
Relies on the law of excluded middle. Constructivists reject the law of excluded middle, and therefore reject any derivative statements.
that seems insane...
Read up on intuitionistic logic. It is not insane, even if you might reject it for one reason or another.
The "paradox" here is in faulty human intuition, IMO, not contraposition itself.
Suppose I have a box. It has 5 ravens and 500 apples in it, and I say "there are 5 black objects". Right away, what is the probability that all ravens are black?
Then you proceed to pull out 499 green apples. What is the probability now that all ravens are black?
If you look at the last apple and it's green, all the ravens _must_ be black, even though you haven't looked at any.
The "paradox" here is that in the real "box" the number of non-black objects is so stupendously large compared to the amount of ravens that even if we restricted our search to "non-black birds" we could not make enough observations to get the impact to grow beyond ridiculously irrelevant.
The paradox exists precisely because the statement is equal to its contraposition, something that is true in classical logical, but not in constructive logic.
>The paradox exists precisely because the statement is equal to its contraposition, something that is true in classical logical, but not in constructive logic.
Nevermind. It is contraposition is true in constructive logic. I take back what I said that the paradox is caused by problems with classical logic.
I do have an interest in intuitionistic logic and logical pluralism (idea that there exist multiple correct logics) in general. The Curry Howard Correspondence gives us a correspondence between intuitionistic logic, Cartesian Closed categories, and lambda calculus. Taking this further we can reason about the semantics of programming languages by looking at logic, type theory, and category theory.
For more introductory info look at
math.andrej.com
and for a specific example of a theory using anti-classical axioms look at
en.m.wikipedia.org
If you're still confused look at Andrej Bauer's video at his page.
They're wrong but it's not their fault.
You are a meme.
The proofs are easier to trace and instantiate. Otherwise (with double negation) you get proofs for statements that don't give any instruction about how to actually use them.
You have no axioms, such statements are part of the proof system itself.
Don't misunderstand, intuitionist aren't saying double negation (or equivalently the excluded middle) is false but rather just that it is not true.
It's not insane. Law of excluded middle works because there's nothing in the middle. Under any logic where there was something else not p would not yet be a falsity, just the absence of truth. If p is not true, it could be false and undetermined for instance.
Type Systems are formulated in intuitionistic logic, some category theorists also jerk off to it. I'd say it is somewhat orthodox in the area of programming language theory and nearby fields, not so much in the muh numbers parts of maths.
One philosophical argument is that to "know" something is to construct an argument or proof for it. E.g. I know the table is red, because my eyes as sensing instruments are telling me it's red. In that sense, non-constructive proofs don't correspond to meaningful truths. This position is more broadly called verificationism and it's rather more convincing than it first seems after reading some arguments in favour.
By the way, I'd say it's not really orthodox, but if you work in logic or theoretical CS it is of equal interest as classic FOL.
Each classical statement has a constructively provable classically equivalent pendant. So you can prove the "same" things, but in lesser ways.
See also the ref for the next guy
>>
en.wikipedia.org
If you remove tools like this principle from a theory or logic, you can (superficially) derive less theorems, but the range of interpretation of the symbols on your piece of paper becomes richer.
A statement "not P" is proven by showing that assuming "P", we are led to a contradiction.
Assume [math] P = \forall x. \, e^x > 1 [/math].
Then we can consider the instance [math] x=0 [/math].
We conclude [math] e^0 > 1 [/math].
Rewrite as [math] 1 > 1 [/math].
This is in contradiction with the axioms of arithmetic, where [math] > [/math] is specified to be a total order, for which a number k can never be greater than k itself.
We conclude "P" is not true resp. "P" false.
We've given an argument here for "P" not being true.
Classical logic lets us say that having proven "Q" means 'Q is true' and having proven "not Q" means 'Q is not true' or 'Q is not false'.
In constructive logic, we want to be able to say that having proven "Q" implies "I have an argument for Q". Here having proven "not Q" means I have an argument for Q leading to a contradiction.
Now classically
>if 'Q is false' is false, then (as each statement is either true or false!) we have the Q is true'
In the constructive reading, instead we'd want our logic to express
>having a argument that 'Q leads to a contradiction' leads to a contradiction, gives us an argument for Q
The problem is that there may not be any argument for Q, other than this axiom / logical rule.
Refraining from refraining to drink the glass of water means you give in to drink it. Doing vs. refraining is the classical exclusive handle.
But not having a reason not to drink the glass of water doesn't mean you'll drink it.
The glass is full of water.
~(The glass is full of water) => the glass is empty?
What if it is half full? It's neither full or empty.
Reminder that Actual Infinity doesn't exist.
Your statement is not related to intuitionism though the issue of actual infinity is discussed in other logics and in logical pluralism.
tl;dr
our ways of proving things is reduced, but our interpretation of the meaning is richer.
Consider this: The law of excluded middle says that for all statement A, we have
A∨(¬A)
>Either 'A is true' or '(not A) is true'
or put differently,
>Either 'A is true' or 'A is false'
This doesn't hold in constructive mathematics.
Now if ⊥ denotes absurdum, one generally captures the sentence "A leads to a contradition" as
A→⊥
and one may always write A→⊥ instead of
¬A
The law of excluded middle is then written as
A∨(A→⊥)
>Either A holds, or A leads to a contradiction.
This doesn't hold constructively. It's not true that
>Either we have an argument for A, or we have an argument for A leading to a contradition.
This is because not having an arugment for A isn't counted as having an argument for a contradition
(While classically, this is just postulated by this very sentence A∨(¬A))
But consider this. There is of course the following statement that always holds
(P∧(P→B))→B
>If P and we have that (P implies B), then B
And in particular for P=A→B, the reads
((A→B)∧((A→B)→B))→B
>If (A implies B) and we have that (A implies B) implies B, then B
(if you know type thery, the constructive proof of the above is λx.(π2x)(π1x), where π are the left and right projections)
And we have
((A→⊥)∧((A→⊥)→⊥))→⊥
>If we have an argument that (A leads to a contradition) AND if having an argument that (A leads to a contradition) gives us a contradition, then we indeed have a contradition.
The above sentence doesn't give a way to conclude A→⊥ classically (i.e. ¬A) but instead ...→⊥ where ... is some convoluted expression.
However, the above is
¬(¬A∧¬(¬A))
And now CLASSICALLY we have ¬(P∧Q)↔(¬P∨¬Q) and P↔¬¬P and so this has the classical meaning
A∨(¬A)
!
We can't prove A∨(¬A) constructively, but this is classically equivalent to a statement we can prove constructively.
To be yet more explicit, the law of excluded middle is
A∨(¬A)
>Either A holds, OR (A is false) holds
and this is classically equivalent to
¬(¬A∧¬(¬A))
>It's not the case that both (A is false) AND (A is false) is false
The first can't be proven constructively, while the second can.
The constructive reading of the first is
>We always either have an argument for A being true OR A being absurd
(not having an argument for A being true doesn't count as A being absurd)
The constructive reading of the second is (to point out the crucial points where the "having an argument" issue matters)
>It would be absurd if we have an argument for A being absurd AND also one that an argument for A being absurd leading to a contradiction
Great posts!
I'm glad you gave the constructive reading.
Think of it as not having a proof and having a proof
instead of T and F
I go a little further down the rabbit hole in my notes, here in the "Discussion" section
axiomsofchoice.org