The example you give of "Sam is not the murderer" is a bad example of the usefulness of the law of excluded middle because you don't need the law of excluded middle to prove negations of statements. Not P means the same thing as P implies False, and you prove P implies false by assuming P and getting a contradiction.
@@cube2fox Obviously intuitionistic logic isn't just one thing, but generally it is allowed. Most intuitionistic logics and type theories are natural-deduction style systems where you prove implications by assuming the antecedent and proving the consequent, and it's quite common to define "not P" to be the same thing as "P -> False", so that you just reuse the implication introduction rule to prove negations. If you don't treat it as mere syntax sugar, then the next most common thing is that the intro-rule for negation will demand you assume P and derive False anyway.
I thought I should also add something about what *is* disallowed. In constructive logics, if you assume not P, and manage to get a contradiction, you don't get to conclude P, but rather, what you've done is to prove not (not P). If P were something like an existential, something like "there exists x such that Q(x)" a constructive proof of that is required to give the x for which Q(x) holds, and the whole logic is designed in such a way that when you prove things, you can turn the proofs into programs that will for instance, compute witnesses to things like existentials. That's sort of the whole point. But from a proof of not (not (exists x. Q(x))), it's not possible to recover which x does the trick, it only gives us that from the assumption that not (exists x. Q(x)), we can somehow deduce a contradiction -- that doesn't necessarily help us compute an x for which exists x. Q(x) -- though of course, if we had one, we'd be able to use it to conclude not (not (exists x. Q(x))) very easily. So these doubly-negated statements sort of play the role of classical non-constructive logical assertions within constructive logic (in fact, classical logic embeds into constructive logic in that way), but these doubly-negated statements are in some sense saying much less than their plain counterparts. So that's the sense in which you're "not allowed to do proof by contradiction". It's just when proving *positive* statements that it isn't the way to go. Also, there are often restricted forms of the law of excluded middle which are provable, and so those also enable proofs by contradiction in some cases -- you just have to show that it really works first.
@@aaronwelson One of more amazing facts about math is that more I study and understand math, the wider the landscape of math becomes, and the amount of math I do not understand grows and grows.
There's another huge advantage of constructive mathematics over classical one: computers can follow the former, but not the latter. The reason is that computers can follow algorithms, so if you can construct one, a computer can follow the algoritm to produce a mathematical object as an evidence of the truth of your theorem. This fact is the foundation of the branch of mathematics/computer science called type theory, which investigates the relations between statements and proofs on one hand and between types and programs on the other. Turns out these relations are very similar, which allows us to encode statements as types; programs as proofs and by the virtue of type-checking provide an algorithm to verify whether or not a certain proof (program) proves some theorem. There are programming languages like Agda, Coq, Isabelle and others, which leverage this fact to provide a nice environment for writing proofs and having them automatically verified by the computer. Unfortunately, if you try to introduce LEM into such a system, it immediately falls apart, because computer cannot follow proofs by contradiction (because they're not based on algorithms). So all these systems only support constructive logic.
Oh yes, Curry-Howard isomorphism is a name I defeinitely should hvae mentioned. But also on a more fundamental level since 1930s we know there are certain problems in mathematics which are *undecideable*, meaning certain classes of propositions cannot be proven either true or false. So in a sense LEM does not actually hold in reality, so it shouldn't be used in reasoning at all.
Thats not true! There are proof checkers and proof assistants for classical logic (eg. Metamath) and you can just introduce LEM in constructive type theories as an axiom. You can even embed classical logic into intuitionistic logic via things like the Gödel-Gentzen translation. There are advantages to do constructive mathematics in type theory (you get an algorithm for each proof), but that is a tradeoff and you can just as easily add LEM, choice etc. as an axiom.
LEM is not an axyom just an statistically relevant assumption. For things classical logic cared it was a reasonable condition, like the fifth postulate is for most of our daily geometry, but with the ocean of problems of the 21st century, it should not hold valid for every problem
Come on! The LEM is already true in constructive logic at the level of double negations! This is very important--- constructive logic is not a weakening of classical logic, it includes classical logic as a subsystem which deals with doubly-negated statements.
This is a good introduction, if a little light. I didn't know that Bauer's "five stages" paper was a response! Note that our construction of the mean still proceeds by axioms: x < y, so x + x < x + y < y + y by adding x and y to both sides of two copies and pasting; then, divide everything by 2 to show x < (x+y)/2 < y. We do the same steps in the proof as in the algorithm; "add x, add y, divide by 2". This is an instance of the Curry-Howard correspondence!
Constructive math is amazing. Especially if one is coming from a lifelong classical perspective. I stumbled upon this through type theory and it was super cool.
I think that for most things and build up a knowledge base we had to go the classical path, but some adventures are outside the realm of classical logic
I do a lot of extremal graph theory and general combinatorics, which essentially makes constructivism impossible in many cases. I like constructive proofs, but avoiding nonconstructive methods would be deadly
I straight up hate graph theory. I bought a book on it and did a course on it. Like dude. With the normal math you learn its like you get to learn the components behind something, and you get to play around with the components. Then you get to build stuff with it, you have cool generalizations of stuff, and its like playing Minecraft. But then fucking combinatorics and graph theory. HOW IS IT FUN FOR ANYBODY. Your just basically solving puzzles. Once you solve it, its just meh. Doesnt even mean anything. It doesnt feel like your creating tools and real objects you can use. It feels like your just mining for "Facts" to put in a "fact book" for people to litterally not care afterwards.
@@honkhonk8009 What is meaningful is entirely up to you. I find algebra pointless and ugly. Meanwhile, I find I often think combinatorially and the problems end up being quite significant to me. Although, your problem may lie in shallower fields.
@@rhubarbman2425 Yea facts. I heard people call graph theory shallow, and highkey I agree with it. I looked at complex analysis, and honestly it just look more fun. You have actual mathematical objects being used in it. I also found spectral graph theory interesting. Litterally only cus it used linear algebra and was satisfying to see how it works. I think for me, stuff is only fun if you see it as components. It just makes it fun. Which is wierd yk. I guess you could call that "a field being deep"
The axioms were actually stated long after many many theorems were discovered. That's simply fact of history of mathematics. So talking about "manipulation of axioms" seems misleading to me. The axiomatic method is used to make mathematics more rigorous, but mathematics as a whole is much more creative than that.
I understand that formalization takes place way after the discovery of maths. But I do feel like there are many ways to describe what maths is, and of course none being more correct than the other. I feel like studies into the formalization of maths has paved a different way to describe and think about maths, that is, as a manipulation of axioms. For example, the development of automated theorem provers makes maths feel like it can be thought of as a more mechanized thing. But of course I do agree that there is a lot of creativity and beauty involved in maths as well. For the purposes of this video however, I felt like it was more appropriate to describe maths as a manipulation of axioms. I hope that explains things, if you would like to discuss things further I would not mind at all. Sharing ideas and viewpoints is cool
I wonder if folks still agree today with these comments, now that Terrence Tao and other folks are doing groundbreaking new math in Lean. I think it's true that math doesn't have to be done in constructive logics, but there are real mathematicians doing new work guided by proof assistants these days.
while that is true, the manipulation of axioms is at the core of mathematics, without assuming some fundamental truths there is no way to form any statements that could be true or false, right?
If one could only think in the rules of math only literally one would not be able to discover even slightly nontrivial identities, one must be able to think in the ideas of math and see the contextual landscape set out by even just some observed rule or structure
You can have a proof of contradiction in constructive logic if you want to prove ~p. You assume p and when you reach a contradiction you would have proved ~p. In fact ~p is often defined as (p -> false) The problem is if you want to prove p. If you assume ~p when you reach a contradiction you would have proven ~~p. The problem is you don't have double negation elimination in constructive logic because it is equivalent to the law of excluded middle. ~~p in constructive logic is weaker than p.
But you DO have "triple negation elimination", i.e. ~~~p is equivalent to ~p, so if you just slap on the appropriate number of "~~" in front of the appropriate parts, you can convert classical logic into constructive. This is called "Godel Gentzen double-negation embedding".
Actually is a common mistake to believe that in constructive (intuitionist) mathematics you can't do proofs by contradiction at all. The law of excluded middle still there in a softer form: a statement is not either true or false, but it's proved true or not proved true. If you have a proposition A that leads to a contradiction, then you have proved "Not A", even in constructive math. No problem in that. What you can't do is having a proposition "NOT A", that leads to a contradiction and therefore deduce A. This is forbidden in constructive math, because it allows the "theological proofs of existence", without show the object that is claimed to exist. That's because is not " the law of excluded middle" that is not valid, but the counternegative: "not not A", doesn't mean A. In constructive math A is true means that, using axioms, you proved A. "Not A" means that, using axioms, you proved that A can't be proved (and It couldn't be proven even if you add tailor-made axioms that do not lead to contradictions). "Not not A" doesn't mean "A" in constructive mathematics, but it means that, using axioms, you can prove that is impossible to prove that A can't be proved (even by adding tailor made axioms, without leading to a contradiction). It seems a twist tongue, isn't it? The fact that the law of excluded middle isn't valid at all in constructive math is a very common misconception that makes most people rise the eyebrow and refute to use constructive mathematics. It's not about the LEM, it's about what you mean by "true". In constructive math it means "provable", while in classical math it is thought that a statement can be true or false, but maybe not provable with the current set of axioms. That is the problem with classical logic: that metaphisical concept of truth that can trascend the system of axioms you are in.
Well, it’s not just general proof by contradiction. In constructive logic, deriving a contradiction from a positive statement to prove the negative is allowed, however a double negative does not get you the positive. But also, you lose excluded-middle arguments, where you derive a third statement from both a positive and its negative.
Existence is consistent and non existence is inconsistent Both not only are true, but should be demonstrably true Assume there exists no number in-between x and y. When looking at numbers in an ordered field (which is the case) field and order properties dictate that (x+y)/2 exists in the field and that x < (x+y)/2 < y. This is a contradiction in the hypothesis that there does not exist such a number, therefore there does exist such a number.
It's not that constructive mathematicians don't believe any statement is either true or false, it's rather that they just don't care. Constructive logic, as its name suggests, is not about truthness but about what you *can* construct (proofs). For instance, the "there exists" symbol in classical maths only means that there theoretically exists such an object but with no guarantee at all that you can find it. While in constructive maths, the only way you have to prove a "there exists" statement is to actually exhibit such an object. This is the same reasoning for the LEM. As a matter of fact, everything you've proven with constructive maths also stands in classical maths, but not the other way around. Having a constructive proof with you is more powerful as it just says more, so that's why you should fallback on classical proofs only when mandatory and when you only care about truth.
3:25: This is a bad example. While it's not generally true in constructive logic that (not not P) => P, it is still true that (not not not P) => (not P). So we can acquit the suspect under constructive logic. 6:25: I don't think a classical mathematician would actively search for a proof by contradiction if there was a much simpler proof that didn't use LEM.
I don't think this video is very useful since it barely gets into the difference between the two and the motivation for them. I mainly consider myself a constructivist in the sense that you should be able to directly construct anything which you claim exists. I can say that pi exists because I can specify it's value using various definitions, algorithms, etc. The same for sqrt(2), ln(2), the golden ratio, e, etc. But claiming a number exists which you can't actually specify seems dodgy. Using proof by contradiction is completely valid. All kinds of "non-constructive" proofs are valid and often they are technically constructive, especially when dealing with finite sets. Eg) A proof using the pigeonhole principle might not always "construct" a specific solution, but if the total space involved is finite, a simple algorithm for constructing a solution can be specified - just search the entire space! As a specific example, if you pick any 11 positive integers, I know that at least two of them must end with the same digit (since there are only 10 different digits but 11 numbers - there must be an overlap). That's non-constructive, but it's easy to search all 55 pairs among your 11 integers and find the ones which match. So there's no difference in this context between classical and constructive. I only favour constructive maths when we're talking about infinite and very complex objects. That's where some non-constructive proofs rely on objects which can't even be explicitly defined. The axiom of choice is a prime example. It asserts that you can always choose one element from each of an infinite collection of sets, without specifying how. But if you can do that, why does it need to be asserted as an axiom? Shouldn't it be a theorem which you prove? What if it can't always be done? That's where I think a constructive approach is necessary and the axiom of choice is completely invalid. Eg) Breaking the real numbers up into cosets of the form x + Q, where x is a real number and Q is the rationals. Supposedly an infinite set of values for x can be "chosen", but also, it can be proven that no explicit list actually exists. In my opinion, that kind of concept is just useless and meaningless. It has no application in the real world, it only applies to other layers of meaningless maths built on top of it. Hence why the continuum hypothesis is unprovable - it just shows that you've reached a state of making things up, not investigating anything tangible. TLDR: Constructivism only differs from classical maths when dealing with infinite objects. Most proofs in finite contexts are the same and one can easily switch between the two approaches. But with some infinite objects, classical maths is actually quite loose and meaningless while constructivism insists on more concrete reasoning.
This video is so misleading. Firstly, this is a video comparing constructivist vs non-constructivist. No "classical" mathematician would prove that numbers exist in between using squeeze theorem. That proof is just forcing non-constructivism and is a pretty bad example. See the proof of the fact that irrational power of irrational numbers can be rational. In that case, a non-constructivist proof is extremely simple. Also, this video makes it seem like mathematicians just avoid constructivist math because it's difficult and hard to teach when in reality, the main problem with it is that it cannot prove a significant portion of mathematics. When I say cannot, I don't mean it is difficult, I mean it literally cannot. This was completely ignored.
I initially thought that classical logic is a subset of constructive logic, since constructive logic has less inference rules than the classical, thus has the potential to add more non-classical inference rules. But everything accepted by constructive logic also accepted by classical logic, so constructive logic is a subset of classical logic like what this video said.
1. As others have pointed out (see pinned comment) if by irrational we mean "not rational" then a proof that sqrt(2) is irrational is equivalent to a proof that "sqrt(2) is rational" implies a "contradiction". Therefore, the standard proof by infinite descent is indeed constructive. 2. Induction is constructive
So basically, classical proofs are what you might learn in a discrete math textbook. Constructivist proofs are the intuitive ones where you construct such an object, and make more sense if you learnt coding before you learnt math.
I need some explanation. If we select x = 3 and y = 4 then x + y/2 is going to be 5, which is not really in between 3 and 4? Or is it actually (x + y)/2 ?
Am I the only one who'll react that it should be (x + y)/2 not x + y/2 at 7:21? Otherwise interesting Cuz otherwise imagine x = 2. y=3. Then we'd have x + y/2 = 2 + 1.5 = 3.5 which is not inbetween x and y You meant it as (2 + 3) / 2 = 5/2 which is inbetween x and y
Sorry for sounding unnecessarily pedantic before (on a vid I've now realized is 2 years old, and someone already pointed it out). I loved the image on 2:22! & thnx for the reply
Wow, i'm undergrad and learning some math as cs. There is a lot of proofs and i have problem with them, especially because i don't understand "why this proof proving theorem" and now i understood why. i should dive into math logic.
The constructive proof is not complete. Firstly, we have to define what our numbers x and y actually are, I think you are referring to real numbers. It remains to be shown, that x+y/2 is indeed in the Intervall (x,y). Firstly, because the real numbers are closed regarding addition and multiplication, we know that (x+y)/2 is indeed a real number. We know that x
8:03 "Meanwhile the classical mathematician never actually shows that there exists the number ... " - Sorry, nonsense. "Classical" mathematicians use constructive proofs all the time. As you have said yourself, constructive methods of proof are a subset of classical methods of proof. Classical mathematics has no restriction that would say "you must NOT construct the object and prove it's existence by contradiction itself. Both types of mathematicians will probably use the same proof in this case ...
Yeah, that's my bad. Should have paid more attention and clarified a bit more on that part. Thanks for pointing it out, I'll try to be more careful in the future
The distinction I would make is that constructive maths always requires that you CAN explicitly construct something (a number, set, function, whatever) while "classical" maths does not require that. In most contexts, construction is easy and implied. The issue is some areas of maths where certain things are asserted to exist, but no concrete example is ever provided. That's where I think some maths falls apart. Anything relating to the uncountability of the reals is usually in this category.
Maybe we can use classical techniques to lazily evaluate the mathematical landscape before constructive techniques come in, it could save a lot of time.
"The classical mathematician is correct, but the proof - uh, well - it’s rather useless, isn’t it?" That is a ridiculous exaggeration, and pairing it with the condescending tone is not a good sales pitch. It only takes away from what you explained up to that point.
You could equally say that classical logic is a subset of constructive logic, by doing a double-negation embedding. It's a huge mistake to claim that something is a subset of something else in math, like, for example "a permutation group is a subset of ALL groups", or, equally, "any group is a subgroup of a permutation group". Both statements are valid. Constructive logic makes manifest the duality between logic and computer programming. Classical logic hides this duality. That's the real difference.
Yeah, I only learned about this concept a year after I made the video through propositional truncations from type theory. I'm cringing at how many mistakes this video has
I think it's potentially misleading to depict constructivism as a subset of classical mathematics rather than vice versa. In terms of model theory, it's more accurate to say that classical logic is a model of constructivist logic rather than the other way around, since constructivist logic is more general. That is, classical logic would never reject any constructivist proof, but constructivist logic may reject a classical proof; truths of classical logic are either true or undecidable in constructivist logic, but all truths of constructivist logic are true in classical logic.
I’m not an expert in logic so don’t take my word for it, but I think godel talks about the unprovability of some statements rather than the notion of “truth” or “false” which is different (somehow)
@@aaronwelson There are several results of Gödel in this context. One of them is, as you mentioned, the unprovability of true statements, one of them is that there are statements that are netiher true nor false. "This statement is false" is the simplest example to such a statement. It can be neither true nor false. Self-referrence is problematic in this context. Anywho, the logical base of the different types of mathematics that you've mentioned is also axiomatic. So there are logical axioms, where the mathematical axioms are constructed on top of. Maybe it would be interesting for you to dive into that too.
@@yauchy5965Godel did not prove that there are statements which are neither true nor false, his results were strictly about provability. Moreover, nobody has or will find any such statements, because that would imply LEM is false, and "LEM is false" is false. Even a constructivist will agree: although constructive logic does not prove "LEM is true", it *does* prove "LEM is not false", and so the assertion that "LEM is false" is a contradiction even for a constructivist. This result is due to the Godel-Gentzen negative translation, named after the very same Godel we are talking about. In regards to your example, Tarski's undefinability theorem asserts that the truth of statements in a mathematical theory cannot be defined using the language of that theory, and so the English expression "this statement is false" cannot be encoded in any mathematical theory whatsoever. In other words, the expression "this statement is false" is not even a statement. Godel did show, however, that we can build statements which essentially say "this statement is unprovable". Truth is not the same thing as provability, and that exact concept is precisely what Godel is best known for.
@@JadeVanadiumResearch I am too lazy to write a long answer here so just read "Relationship with the liar paradox" in the wikipedia page for "Gödel's incompleteness theorems"
A big problem with the Law of Excluded Middle in mathematics is that it is uninformative. Let's say my thesis is: "either 23 divided by 45 plus 86 is equal to 286 or it isn't equal to 286." Within classical logic, this is a tautology and a perfectly valid conclusion. However, what it doesn't tell us is whether this equation does - or does not - equal 286.
better proof by contradiction. sam was asleep and in a completely different location than where the murder occured. and you can't be in two different places at once
what is your opinion on number zero? by introducing number zero negative numbers were introduced which are irregular (can't take square root of, multiplication doesn't give negative number)? wouldn't this make mathematics less perfect ? If we think of number zero as an input/output device of an abstract computing machine (which is mathematics) , wouldn't it be more correct to explicitly construct and destruct numbers instead of having zero which is a placeholder for construction/destruction right now?
=59x5O9 zero added 2x3x5x7x11x13+1..= Number umbra sombre sombrero shadow... Intro inert trine as winding (anda ellipse) number up or down..or left or down..symmetry and rotation. Plus minus. Wh-y can't DIVision vibration fibration be possible as in 1÷0? No rotation. Tiling not possible. Constructive frustration. Glassical me chain x. Speed Force chromodynam x. Soul Forge. Hole among imaginary is 1. Resonant + TWiST... 2 spheres are twist away. Hoorey!
first off, square roots of negative numbers are possible, and it introduces an extra special direction to a number line. complex numbers are also pretty useful. and +x*-x =( -x^2) you’re thinking of (-x)^2 always being positive, but a positive by a negative is always negative. there’s nothing wrong with negative numbers; in fact, they’re great.
@@axelinedgelord4459 well, complex number is not a number in the first place. Complex number is a function of two variables. Because you created zero and divided number space in two sets (negative and positive) you now got additional complexity in the number space because you have to fix the problem of the square root of negative number. If you never had zero number you wouldn't need to invent complex numbers. The zero number created an irregularity in mathematics, see from -1 to 1 you have a distance of 2, while between 1 and 2 you have distance of 1. Imagine you are building a house out of bricks of the same size, but then you suddenly get a brick that doesn't fit and break the alignment with the other bricks. How cool is that? Not cool,this is why zero is mostly avoided when applying math to real problems.
the "sam is not a murderer" example is tragically terrible: we literally proved the statement ¬(sam is the murderer), which is literally equivalent to (sam is the murderer) ⇒ ⊥. We didn't even need to use the law of excluded middle. also, one can always prove ¬¬¬A ⇒ A in constructive logic. therefore, only statements like "there is an even number that is not the sum of two primes" could possibly only be proved in classical logic by showing that "all even numbers are the sum of two primes" leads to a contradiction.
Proof assistants based on constructive logic (which also happen to be programming languages) such as coq or lean are total, which implies that they always terminate. So indeed, the halting problem is solved in such languages. (actually you can often bypass this restriction (i.e. with the keyword "partial" in lean) but by doing that you're leaving the realm of constructive logic anyway)
To be honest I think this is nothing but distorting the logical conditions until they generate problems where there are none and then dividing people into opposing sides. Is that simple as getting rid of the _"either always LEM or never LEM"_ mentality. If you wanna construct maths to logically characterize some information, you must *decide* if you wanna work with all the load of truth determined or you just don't mind, but none of this has anything to do with "proof by contradiction". This one type or proof is actually like a proof by counterreciprocal, but instead of proving an implication you prove the sentence by having determined that the other is false (whether by definition, by axiomatics or by whatever reason you want). If it turns out the other one can't be proven or disproved you just just look for another way to prove it (without so much drama). 🤷
