Seems like the standard "By Way of Contradiction" is predicated on this Law of Excluded Middle.

@benjaminpedersen9548

Жыл бұрын

It is.

@pfeilspitze

Жыл бұрын

Yes. Look up _Intuitionistic Logic_ if you want to see more about what happens if you take away excluded middle.

@Jcarr250

Жыл бұрын

Not always, as used here it's proving a falsehood. You can prove that statements are false by showing that they result in a contradiction, but without LEM you cannot prove statements are true by proving a contradiction from their falsehood.

man this gives me nostalgia to one of the first intro to abstract maths lectures in my first semester. all of it seemed almost magical and now it’s just another thing i take to be self-evident :p

@kkanden

Жыл бұрын

okay i think i need to correct my statement a bit: not nostalgia but rather depressive melancholy

@utof

Жыл бұрын

@@kkanden lmao :D

@MyOneFiftiethOfADollar

9 ай бұрын

if you think abstract algebra is "self-evident" , then you. don't understand it

Very nice. Gelfond's constant is actually the number e^π. The Gelfond-Schneider constant is 2^sqrt2, and the square root of that is sqrt2^sqrt2, which is the number you explore in the video. Thanks for the content, as always!

@kmyc89

Жыл бұрын

And just like 6 days later, Mates Mike* wrote _Gelfond_ also wrong. * (10:13) /watch?v=8BFTk8TH_x8

10:55 The law of identity, the law of non-contradiction and now The law of the excluded middle.

"Well, this is easy. It's not a set." If only Michael Penn had been around earlier so that Frege wouldn't have had to throw his life's work away.

@simonmultiverse6349

Жыл бұрын

Michael, did you know that you look a bit like Quentin Tarantino?

I gently pressed that like button! Love your videos.

It would be interesting to see a discussion of the law of excluded middle in relation to undecideable problems.

AAAAA i thought the video would have an actual feature from the YTers mentioned in the title, and now i REALLY REALLY want to see it!!! Especially I would love to see @PhilosophyTube talk about the philosophical implications of the law of excluded middle in other contexts. (I would also love to see you address ideas like Modal Logic, which use two additional operators similar but not identical to existential operators)

@luisaleman9512

Жыл бұрын

Same. I really want to know what Legal Eagle thinks about this.

I guess any proof by contradiction presupposes the law of excluded middle in some way.

@TheEternalVortex42

Жыл бұрын

There are two types of proofs by contradiction. The first type is (P -> F) -> ¬P, which does not require the law of the excluded middle. This type of proof is basically required any time you want to prove a negation, for example "sqrt(2) is not rational". If we substitute ¬P for P in that one we get (¬P -> F) -> ¬¬P, and now if we apply the law of the excluded middle (P ¬¬P is an equivalent formulation) we replace ¬¬P with P to get the *second* type, which is (¬P -> F) -> P. There are some useful statements that can only be proven in this setting (as far as we know), for example the Intermediate Value Theorem from calculus.

@tomprince8223

Жыл бұрын

To expand on that, depending on the underlying logical formalism, "not P" is sometimes *defined* to be "P implies False", so the way you prove not P is exactly a proof by contradiction. So, a proof by contradiction only involves the law of the excluded middle when you are proving a positive statement. That said, after I started to pay attention, I noticed that many proofs of this type barely make use of the assumed contradiction. I'm fairly certain I've seen proofs that are essentially "Assume not P. Prove P. This contradicts our assumption of not P, so we can conclude". Even in cases where the assumption is used non-trivially, it is often only for a single step at the end and the meat of the proof could be extracted into a positively stated lemma that doesn't use proof by contradiction or the law of the excluded middle.

@fartsniffa8043

Жыл бұрын

@@TheEternalVortex42 im not really following how you didnt use the LEM. Since in your first type, to reach a contradiction you assume that, either ¬P or ¬¬P has to be "true" which is exactly the LEM. Either way, with proofs by contradiction you can do em with the law of non-contradiction, which is how its usually done anyways and doesn't even use the LEM. Note that there is a connection between the LNC and the LEM since the former can be used to prove the latter(bit of a sketchy proof if you ask me).

@MuffinsAPlenty

Жыл бұрын

@@TheEternalVortex42 I'm a complete novice with constructive mathematics. I'm trying to formulate what you're saying in a bunch of different ways, and I'm wondering if the following is correct. One can think of LEM as saying that ¬F implies T and also ¬T implies F. In constructivist mathematics, one keeps the implication that ¬T implies F, but does not keep the implication that ¬F implies T. Is that correct?

@swenji9113

Жыл бұрын

@@fartsniffa8043 The real question is "what is notP?" In proof theory, the classic definition of this statement is "P -> False". In other words, without any assumption on the system of proof you're using, it is widely accepted that "proving notP" means "proving that P leads to a contradiction". Even though the word contradiction shows up, this is not controversial at all. Suppose for example that you want to prove that √2 is irrational : you have to clarify what do you mean by that. The most intuitive and logical definition of "irrational number" is "a real number that is not rationnal", therefore what you're trying to prove is "√2 is not a rationnal number". Well what does it mean to have a proof of this negation? It precisely means that you have a proof that "√2 is rationnal leads to a contradiction". And that's precisely what we usualy do. This is the first kind of proof by contradiction. There is no controversy on the technique used, it is a very universaly accepted proof. Now there is a very interesting axiom that some logics use and some do not which is called "reductio ad absurbum". This axiom states that for any proposition P, "if notP leads to a contradiction, then we have P". Another formulation is "not(notP) leads to P". This axiom is very much controversial and it is equivalent to the law of excluded middle. Without entering a discussion on whether it is true or false, we can all agree that it is suited for certain kinds of logic but not for others. For example, in truth-functional propositional calculus, one assigns a value (true or false) to any proposition. Therefore reductio ad absurbum stands: if the value associated with a proposition is not false, then it is the other value, thus true. In contrast, in proof theory we like to say that a proposition P is true when it can be deduced logically by using axioms. In this context, the proposition notP is equivalent to having a proof that P leads to a contradiction, using only axioms. This is not always the case that we have either P or notP. Sometimes the axioms just don't give enough information so it depends a lot on what your theory defines as its axioms. Kurt Godel proved that any theory that can develop the foundations of mathematics (in a sense I will not explain here) and which does not contain contradictions cannot be complete. This precisely means that there are propositions P such that neither P nor notP have proofs using the axioms. Therefore reductio ad absurbum is not valid to determine if a proposition can be proven. If you can't get a proof of notP, that doesn't necessarily means that there exists a proof of P...

It's a bit funny that you use a proof by contradiction to show that log_2(9) is irrational, since that's equivalent to the law of the excluded middle.

@stevenraanes4786

Жыл бұрын

Assuming p, getting a contradiction and concluding not p does not use the law of excluded middle. It is only assuming not p, getting a contradiction and concluding p that uses the law of excluded middle, as that uses that not not p implies p.

@half_pixel

Жыл бұрын

@@stevenraanes4786 Oh, good point! Never mind then.

@Megumin_Random

Жыл бұрын

@@stevenraanes4786 Technically, that’s not true (or, it shouldn’t be true). The point of the Law of Excluded Middles is that only “P” and “not P” exist, so proving P disproves “not P”. If you take the Law of Excluded Middles away, then you have the situation where neither P and “not P” are both true, sure. But you can also equally have P and “not P” both true. So, technically, you are using Excluded Middles by assuming P proves “not P” false. Because without excluded middles, nothing about P affects “not P” TLDR: P disproves “not P” if and only if “not P” disproves P

@stevenraanes4786

Жыл бұрын

@@Megumin_Random You can still do one type of proof by contradiction without the law of excluded middle. TheEternalVortex left a good comment explaining this in another thread, and the talk "Five Stages of Accepting Constructive Mathematics" by Andrej Bauer covers this at the beginning, around the 2 minute mark. The intuitive reason one type of proof by contradiction (assume p, get a contradiction, conclude not p) is valid without the law of excluded middle is that what you have proved is exactly that p cannot hold. If p holds, you get a contradiction, so p cannot be true. Thus not p. Without the law of excluded middle, it may also be that not not p holds, but you have shown not p.

@Megumin_Random

Жыл бұрын

@@stevenraanes4786 But that’s exactly the point I’m trying to make. By saying P doesn’t hold, thus “not P”, you are excluding anything “in the middle” between P and “not P”. Thus, that IS a type of Exclusive Middle. In order to not imply an exclusive middle, you would need to prove P and “not P” entirely separately. My opinion only (but then again, I agree with Exclusive middle, so whatever :P )

Great video... Thanks

The description is wild

Michael Penn and Philosophy Tube is a crossover I didn't know I needed in my life

@notnilc2107

Жыл бұрын

dg gl

I was hoping for some discussion about rejecting the law of the excluded middle and constructivist math. I've always found this topic interesting since it somehow seems more 'useful'. For example, in computation we can only ever deal with (a subset of) constructive methods. It would be quite amusing if one were to prove that P = NP non-constructively.

@JadeVanadiumResearch

Жыл бұрын

Actually there's a specific algorithm which solves every P problem in polynomial time. If it were proven (even nonconstructively) that P=NP, then that specific algorithm would solve every NP problem in polynomial time. Of course, if the proof were nonconstructive, we'd have no way of knowing exactly how fast the algorithm is, so it might still be so slow that it's useless. In the (likely) event that P is not NP, the algorithm will necessarily have super-polynomial runtime on NP hard problems. For the curious, the algorithm is really simple: it takes as input a polynomial-time verifier for the problem, then it "concurrently" runs every Turing machine until one of them halts with a correct solution. You can run all machines concurrently since the set of Turing machines are recursively enumerable, so you run the enumeration program and, each time it enumerates a new program, you start running that at half the speed of the previous one. The end result is that the n'th machine runs 2^n times slower than it normally would, but if there exists a polynomial time algorithm to solve the problem, you reach that algorithm in finite time and then it finds you a solution in polynomial time despite the slowdown.

@danyilpoliakov8445

Жыл бұрын

non-constructive proof of existence can be used as a intermediary step to invent new constructive methods. So, whilst you are not using non-constructive methods in computation you still use fruits of it. My point is that you still use non-constructive methods in computation - just indirectly

@danyilpoliakov8445

Жыл бұрын

Actually the basic idea of zero-knowledge proofs, that are used a lot in nowadays crypto computations, is in non-constructive proof (you need to prove you have some number with specific properties - but you do not provide any easy(computationally affordable) way to reconstruct it by design

@annaclarafenyo8185

Жыл бұрын

Using constructive methods DOES NOT WEAKEN MATHEMATICS. Classical logic embeds into intuitionistic logic by double-negation. What it does is be more specific about exactly what you are proving. When you prove "not A" you give an algorithm that produces a contradiction from a proof of A. On the other hand when you prove A, you actually might be providing a stronger algorithm. The point is that every construction of intuitionistic logic you get a specific computer program, unifying computer science and logic. That's the point. Constructive mathematics IS NOT WEAKER, it's VASTLY STRONGER.

@annaclarafenyo8185

Жыл бұрын

@@danyilpoliakov8445 There is no such thing as a "non constructive proof", there are just proofs that construct different things than what they say they do.

Just a note about the spelling. Mathematicians Alexander Gelfond (known for Gelfond's constant and Gelfond-Schneider theorem) and Israel Gelfand (known for... many things) are different people 😊 √2^√2 is known as Gelfond's (not Gelfand's) constant.

@TimMaddux

Жыл бұрын

Isn’t this actually the Gelfond-Schneider constant whereas the Gelfond constant is e^pi?

@dbmalesani

Жыл бұрын

@@TimMaddux you seem to be correct! I should not go around spell-checking without knowing what I'm talking about... Actually, now I see that the Gelfond-Schneider constant is reported by Wikipedia to be 2^√2, not √2^√2.

Regarding the final proof: I have never gotten a real intuition for intuitionistic logic and denying the law of the excluded middle. But isn't proof by contradiction using the law of the excluded middle, by way of claiming not not P is equivalent to P?

@benjaminpedersen9548

Жыл бұрын

Yes

Kane B is a great philosophy channel that I’d love to see you collab with

Mr. Penn, please also send this video to attorney Tom!

Michael - The difficulty with the Law of the Excluded Middle is that it presumes that statements are decidable. Not all statements are decidable. It's a little bit like the "divide-by-zero" restriction for ordinary fields such as real numbers. If we try to include "proofs" that have a step that divides by zero, then we get contradictions. So we exclude that particular step from proofs, and we carefully study proofs so that cases that could include division by zero are excluded as exceptions from our theorems. The Law of the Excluded Middle also has to exclude statements that are nondecidable.

A discussion with alex o'connor would be interesting

I'd also love a collab with another mathematician who's a youtuber, probably someone like the math sorcerer

Legal eagle is another one of my followed channels, would love a collab between you two!

@rhaq426

Жыл бұрын

law and maths? I wonder what they'd talk about. That could be quite interesting

Thank you. Now my brain is broken!

I think the community to look for is the constructive mathematicians, proof theorists, category theorists, logicians, proof assistant developers or so.

My roommate studies category theory, and he rejects the LEM. He says he feels like it doesn’t give you any information in a proof, and according to Type Theory, there are still plenty of instances where LEM holds.

@annaclarafenyo8185

Жыл бұрын

Rejecting the excluded middle DOES NOT reject the excluded middle, because you still have (not not A) or (not A). This is enough to embed classical logic in intuitionistic logic. What that MEANS is simply that you are more specific about whether you have proved A or not not A, and this is very important as the two proofs become completely different algorithms when reinterpreted as computer programs. It is only when you are that pedantic that you can map proofs to programs one-to-one.

@JM-us3fr

Жыл бұрын

@@annaclarafenyo8185 I didn’t completely understand what you said, but my roommate has mentioned multiple times that computer programs have an easier time understanding logic via Type Theory rather than our current formalism. It’s very interesting!

@annaclarafenyo8185

Жыл бұрын

@@JM-us3fr I'll say it like this: in classical logic, the statements "A or 'not (not A)' " are completely equivalent. If A is true, then the negation of A is false. Proving one is equivalent to proving the other. In intuitionistic logic, proving "not not A" is easier, because you CAN use excluded middle, while proving "A" is harder, because you can't use excluded middle. So every statement you prove 'true' classically is still proved 'true' in a weaker sense in type theory, it's not-not double negation is provable. BUT, only SOME statements are provable without the double-negation, and those statements can be immediately turned into a computer program to calculate what they claim to prove exists.

@trueriver1950

9 ай бұрын

If LEM does not hold, can you still have LEMMAs? (runs hides ducks)

Doesn't proof by contradiction (used in showing that log_2(9) is irrational) use the law of the excluded middle implicitly? Its even listed as an example of such at the start of the video. This would mean that neither method shown here actually shows that there exists an x^y \in Q for irrational x, y; contradicting the claim at 10:45. I'm not even sure it's possible to define irrational numbers without using the law of the excluded middle in some way. Saying that every number in R is either in Q or in R\Q sounds suspiciously like the law of the excluded middle.

@swenji9113

Жыл бұрын

That's a good question. Being irrationnal is usualy defined as not being rational. Therefore, proving that a number x is irrational means proving that if it was rationnal, it would lead to a contradiction (that's the definition for a proof of a proposition notP). Depending on what logic you use, you'll be able to state that every real number is either rationnal or irrationnal... or you won't. However, the proof by contradiction used here does not use law of excluded middle. Law of excluded middle is equivalent to reductio ad absurbum, which states that "if notP leads to a contradiction, than P". Here we simply use the definition of irrationnality: to not be rationnal. How would you prove that log_2(9) is irrationnal? Well you need to prove that if it was rationnal, there would be a contradiction. That's what is done in the video. Thus it doesn't use the law of excluded middle. But you're right, one cannot prove that any real is either rationnal or irrationnal without LEM. Also, if you wanted to prove that some real number x is rationnal by assuming that it is irrational and getting a contradiction, then you would be using reductio ad absurbum, and therefore LEM implicitely.

@swenji9113

Жыл бұрын

But note that you don't need the law of excluded middle at all to define irrationnal numbers! You need it to prove basic properties such as "every real number is either rationnal or irrationnal". For classic real numbers such as 0; 1; 3/4; sqrt(2); e; π; log_2(9), you can tell if they are rationnal or not without LEM. For a random real number, you can't say anything

the cannel name dialect seems to be making a series on something like the law of excluded middle, and he's quite philosophical.

Russel's paradox was a good example of where mathematicians hold the law of excluded middle in high regard. While the last specific case that proves the rule shows that mathematicians also like to circumvent it :) On a similar note, with the "if a number isn't even, then it's odd (i.e. not even)" example... Could we circumvent the use of the law of excluded middle via the fundamental theorem of arithmetic? An odd number being even would violate unique prime factorization.

@RexxSchneider

10 ай бұрын

It may be even easier than that. Define an even number as an integer that leaves a remainder of 0 when divided by 2, and an odd number as one that leaves a remainder of 1 when divided by 2. Then because remainders are always less the divisor (by definition), we see that { 0, 1 } are the only possibilities for remainders when dividing by 2. That immediately partitions the integers into the two mutually exclusive sets, odds and evens. In this case, an odd number can't be even because 1 ≠ 0. Note that no integer exists that doesn't leave a remainder of 0 or 1, so all integers (including zero) have to be either even or odd.

@MyOneFiftiethOfADollar

9 ай бұрын

The integers are the disjoint union of the even and odd integers So if n is not even then n is odd. appealing to the prime factorization completely unnecessary. Also dragging LEM into this is pointless.

For ever n in +ve integers - n is either prime or n is not prime?

oh cool you like legal eagle and PT? they're nice!

This is a solid presentation of mathematical logic or, as I prefer, philosophy of mathematics. It’s important to emphasize that LEM does not state that P must be true or false-this is a quirk of ordinary language. The idea that P can be “true” rather than “provable” only has formal meaning within the context of the axioms chosen to develop/construct a logical system. For cases involving paradoxes, like Russell’s paradox or the Liar’s paradox; it’s possible to hold that those statements have no truth value under the logic of the axiomatic system. Here Russell’s paradox is a not a properly formed logical statement, it just appears to be. In ordinary language I can construct a sentence that, arguably, only appears to be an English sentence. “My socks ate my water.” Outside of artistic license and metaphor, this has no meaning. Socks are not things that can eat; one cannot eat but only drink water. It’s that or you take the Platonism route, one I actually admire a great deal, but it’s worth knowing that I’m not a logician; my work was in philosophical anthropology and I took a sharp career turn so I don’t hold an advanced degree in philosophy.

This discussion might lead to considering multi-variable truth logics, where there is no excluded middle.

What about Euclid's 5th axiom??

I'd be happy to help you decode papers from Bauer or Escardó, but I don't really have any novel work to add to a collaboration. The biggest reason to reject LEM, personally, is that it's not computable. The biggest reason to accept it, personally, is that otherwise subsets of finite sets are not necessarily finite!

@MyOneFiftiethOfADollar

Жыл бұрын

If a subset of a finite set was infinite(not necessarily finite as you put it", then it could not be the subset of a finite set. Don't get why rejecting LEM could lead to "subsets of finite sets are not necessarily finite" unless you mean this is just one of the more than two possible outcomes. This really possesses me to wonder how LEM could possibly be doubted.

@Tridar918

Жыл бұрын

​@@MyOneFiftiethOfADollar When you work constructively without LEM, you often find that definitions which were classically equivalent are no longer the same. And you've actually pointed out a really good example of that. Classically, "infinite" means both "not finite" as well as "contains infinitely many elements" (I'll define that in a non-circular way below). So it really would be quite absurd if a subset of a finite set were not finite, since it implies that the finite set contains a not finite set, which has infinitely many elements. Constructively, we have to be more careful. The typical definition for infinite is "a set that contains at least n elements for every natural number n" (this is how we avoid that circular definition above, by the way). So that means that, for a set to be infinite constructively, you have to have concrete examples of infinitely many distinct elements in that set. Compare that with the classical definition, where it was fine to show that the set didn't contain exactly n elements for some natural number n. Now, how do we get that whole crazy example of a "subset of a finite set that is not finite"? Well, we certainly won't find an infinite (constructive definition) subset of a finite set and so I can't give you an example of a set which is classically not finite. But I can give you the next best thing: an example of a subset of a finite set that, if it were finite, implies LEM. Classically, this isn't a problem, but constructively, it means that everything is actually classical. Here's the idea of the proof. Consider the statement P and the set A = {0, 1}. Clearly A is finite. Define the subset B = { a ϵ A | a = 0 or P holds true}. Classically, we know that either P holds true or ~P holds true, so either B = A or B = {0}, but constructively we don't make that assumption. Now, let us assume that B is finite, i.e. B has exactly n elements for some natural number n. Under that assumption, then we know that B has either exactly 1 element or exactly 2 elements (you actually need to justify this statement, but it's a bit tedious, so let's skip it). If B has 1 element, then clearly B = {0} (since 0 ϵ B). But then we can conclude that ~P holds. If B has 2 elements, then B = A and we can conclude that P holds. Thus, under the assumption that B was finite, we showed that P holds or ~P holds. So when we assume that every subset of a finite set is finite, we can show that for any statement P whatsoever, either P holds or ~P holds. In other words, we have proven LEM. So constructively we have shown (every subset of a finite set is finite) => LEM. If we doubt that LEM holds true, then we have to doubt the the first statement holds true. tl;dr: Constructively, we don't find a concrete example of an infinite subset of a finite set, but we do find that, if we assume that every subset of a finite set is finite, then we might have as well assumed LEM and just worked classically in the first place

@MyOneFiftiethOfADollar

Жыл бұрын

@@Tridar918 thx for depth and breadth of your reply! The inherent ambiguity of “common language” is part of the problem it seems. Can see why David Hilbert , Frege and others wanted to reduce all of math to set theory and 2nd order logic with precise ordering of universal and existential quantifies. Lot of the problem is related to “understood” omissions of quantifiers.

2^a isn't necessarily even, just consider a=0 :P

@Packerfan130

Жыл бұрын

Here, a =/= 0 since y = log_2 9 and y = a/b. If a = 0, then log_2 9 = 0, impossible. It's fairly obvious so it didn't need a separate mention by the proof writer.

Re Russell's paradox, why not conclude that A is the empty set?

The sqrt(2) x sqrt(2) is a bit of a loaded example, as the irrational number defined by sqrt(2) was obtained in a very special way that more or less "stacked the deck." That is, sqrt(2) was chosen for this counter-example as a special inverse function. It would be more interesting to prove the point without using such a "special" number. In general, it seems that one could prove many similar interesting things by finding an inverse function of a rational number, where that inverse function has an irrational value.

I enjoyed the proof of the statement: There exist irrational x and y such that x^y is rational. Thank you.

The white text on the left of the board at the start is incomplete. The law of excluded middle requires that either p is true, or not p is true, AND NOT BOTH. If we read the word 'or' as the usual interpretation in logic, it allows both alternatives to be true, so we have to remove the possibility of that. More briefly: say ... exclusive or ...

What's always confused me in formal logic. Gödel's First incompleteness theorem states that "any consistent logical system that is sufficiently strong to define the natural numbers is inconsistent." Inconsistence being that there are statements which can neither be proven true or false. So far so good. But now let's take a hypothesis, that can be disproven with a counter example (Riemann Hypothesis, Goldbach conjecture, Collatz conjecture etc.). If any of those are shown to be undecidable under, ZFC for instance, the statement: There is no proof for conjecture X under ZFC. Meaning that they MUST be true, because otherwise we could "simply" find a counter example. With a simple counter example we'd have a proof of X under a given logical system. But Gödel's first incompleteness theorem has been proven within ZFC, meaning that the tool used to prove there is no proof is itself the proof that the theorem is true. I'm pretty sure I'm misunderstanding something along the way, either there being some meta layer and Gödel's incompleteness not being entirely within ZFC. Or is the actual conclusion that any hypothesis that can be disproven by counter example can't be independent from a given logical system

4:10 makes me wonder why Hilbert didn't use LEM to prove the completeness of mathematics. Is it because the dismissal a bit hand wavy? Basically if we take a consistent formal system and use LEM on it as a pruning mechanism, aren't we producing a system that is both consistent and complete (and therefore proving Gödel wrong)?

@JadeVanadiumResearch

Жыл бұрын

LEM has to do with truth: it asserts that either P is true or P is not true. Because LEM is an axiom of classical logic, most mathematical theories will prove "P or not P". Completeness has to do with provability: it asserts that either P is provable or the negation of P is provable. A proof is a complex sequence of steps that follow restrictive rules, and even if you know that P is provable, it's often very hard to find a proof. Hilbert's question, in part, was about the relationship: if P is true, is P necessarily provable? In essence, Hilbert wanted to find a perfect theory of mathematics, one which could tell us everything true about numbers without giving the wrong answer, so that we could decide every mathematical question. Godel proved that it's impossible, there is no effectively enumerable theory of arithmetic which decides all questions consistently. There is no computer sophisticated enough, or mathematician clever enough, to produce every true statement, and *only* true statements, about numbers. We can't have all the answers.

Are there any alternative math systems with the opposite axia? Would be interesting to see whether you could get anything like a set theory or number theory with a system that had a 3rd or more options.

@annaclarafenyo8185

Жыл бұрын

That's not what denying excluded middle does. There are still only "two options" for "philosophical truth", but there are an infinite number of different WAYS of proving a given statement, each corresponding to the different types of constructions which prove the result. The intuitionistic logic matches proofs one to one to computer programs in a very specific way, the proofs become inhabitants of "types" in the typed lambda calculus. This can be used to write proof systems on computers which convert proofs to programs, and in fact, this has been done in the Calculus of Constructions.

@trueriver1950

9 ай бұрын

Actually: I'm sure I've come across logics where the middle is not excluded. So yes: I think those systems do exist. Whether they are pure_mathematically useful is another thing. An example that comes to mind is an SQL database with a table (relation) with a Boolean value ALLOWED NULL would be an example that is useful in data handling. Instead of what a mathematician would expect of a Boolean, that column would be populated with values taken from { TRUE, NULL, FALSE } In SQL the algebra is effectively that any binary operation that includes a NULL in one or both terms gives a NULL result. This leads to the apparent oddity that NULL = NULL evaluates to FALSE because there is a NULL on at least one side of the binary operator. There is a unary operator IS NULL which returns true if the operand is null and false otherwise. This this algebra is at least closed and commutative. I'll leave it's other properties to be discussed. Why this is useful is more a question for a discussion of databases, but very hand wavingly it's a bit like the Don't Know in an answer to a public survey. A rather different alternative to the classical excluded middle comes in quantum computing, where a quantum binary bit ("qubit") can be in a superposition of True and False at the same time. That is very interesting maths but it's too big to fit into this -margin- reply box

the law of the excluded middle is deterministic. in the stochastic world this can be denied

For the second proof, is the law of excluded middle not built in to your proof by contradiction? Since you asserted that y is either rational or irrational.

Awesome

The claim made about x^y being in Q when x,y, are not in Q is interesting, though the existence of logarithms does make constructing a proof by example trivial. Curiously, If x,y are restricted to the Algebraic Numbers (or even the Constructible Numbers) that are irrational, we might not be able to make use of the excluded-middle proof presented here, because we would need to show that Gelfand's Number is, itself Algebraic (or Constructible), and I'm not sure that it is.

I thought LegalEagle was going to be in this video for a second. Anyhow I don't he does philosophy, but US law but I may be wrong.

The Law of the Excluded Middle is also know as "Tertium non datur".

There must be 2 'A's: One is green, and the other is red 😁😁😁

Nice

People seem to not like LEM because it allows one to circumvent constructivity, but you can get around that by simply rephrasing your assertion or just deciding to construct

@swenji9113

Жыл бұрын

Lol people love LEM when they have to do maths... Constructivism is very interesting but it's such a pain in the arse... I think when "complain" about LEM they don't refute it, but rather recall what it cannot do

As far as I remember, the same results should be proofable with and without the rule.

Are there examples of transendental numbers that exponentiate to a rational number ?

@blableu4519

Жыл бұрын

e^ln(2) e and ln(2) being transcendental Or, in general (for any x): e^x = integer

@Gardenmonkey78

Жыл бұрын

@@blableu4519 indeed thanks!

Please look at the 2nd century Buddhist philosopher Nagarjuna's tertalemma (4 modal logic).

It would be fun to see you explore constructive real analysis. Very strange results there

@MyOneFiftiethOfADollar

Жыл бұрын

Thx for that. Would love to see the constructive Dedekind cut construction of the real numbers and how the “real numbers” actually inherit all the familiar properties from the infinite set of rational numbers that define single real number. Oppressively tedious but needs to be seen at least once by those who choose the vocation or avocation of mathematics!

Simpler example: e is irrational. ln 2 is irrational. e ^ ln 2 = 2, which is rational.

@trueriver1950

9 ай бұрын

Or indeed b ^ (log_b 2) where b is any positive irrational.

The quarrel with the law of excluded middle, at least, in my opinion, isn't that it's incorrect, but that it makes one's proofs mean less. If you can establish a result constructively, your proof _is also an algorithm._ I.e., if you prove for all x, P holds, then a constructive proof is an algorithm that converts any x into a proof of P for x. This is contrasted with classical logic, where you have things like Brouwer's fixed-point theorem, which tells you that a fixed point exists but not where it is. Furthermore, there's a subset of constructive logic that's isomorphic to classical logic; the correspondence between the two given by the Gödel-Gentzen translation. So, in a very real sense, constructive logic is strictly stronger than classical logic, even though one might find it _prima facie_ weaker.

@r.maelstrom4810

Жыл бұрын

It's just the other way round. Constructive logic is weaker tha classical.

@JadeVanadiumResearch

Жыл бұрын

Just because the translation sends the set of formulae to a strict subset doesn't really mean anything. The translation which takes a formula "P" and translates it to "P and True" also sends formulae to a strict subset, but even in constructive logic that translation is merely the identity map, up to logical equivalence. As pointed out by R. Maelstrom, constructive logic is strictly weaker than classical logic. The *theorems* of constructive logic are a strict subset of the theorems of classical logic, so classical logic proves everything that constructive logic proves, and more. The double negation translation is identity when performed in classical logic, and constructive logic can't disprove LEM, so constructive logic can't prove the double negation translation isn't identity. Saying constructive logic has more expressions than classical logic is like saying Robinson's Q has more numbers than Peano Arithmetic. That being said, it's true that constructive proofs help us get algorithms for witness extraction. Albeit my personal opinion is that if we're trying to talk about algorithms, we should actually talk about algorithms. The algorithm which takes a constructive proof and produces a witness can only be performed in a metatheory where we can talk about, and quantify over, proofs themselves. That metatheory would be easier to use if it had LEM. The relationship between constructive proofs and witness extraction is beautiful, and useful, and we should use it whenever it's needed. When it's not needed though, it seems like an incredible waste of energy. Skepticism about LEM only serves to overcomplicate what would otherwise be the *simplest* branch of mathematics.

@tomprince8223

Жыл бұрын

@@r.maelstrom4810 I suspect you are using weaker in a different way than the person you are replying to. If you take classical logic to *be* the image of the Gödel-Gentzen embedding, then intuitionistic logic proves more formula than does classical logic (since it proves things that are not in the image). I don't think it is unreasonable to describe this (at least informally) as stronger.

@JadeVanadiumResearch

Жыл бұрын

​@@tomprince8223 To say that you can "use LEM when it's desired" is just to say that LEM is an axiom. Moreover, constructive logic itself already proves "not [not P and not not P]" for all sentences P, so you cannot consistently assert that AC is both not true and not false. Constructive logic does not say what you think it says. Constructive logic does not say anything that classical logic doesn't also say, because "LEM isn't an axiom" isn't an axiom. You can't use it for anything. We agree that constructive existence statements are often more useful than their nonconstructive counterparts, insofar as witness extraction is useful, but there are also instances where witness extraction is both not useful and inconvenient. If you want to perform a constructive existence proof in classical logic, you can just perform the constructive existence proof. If you want to perform a nonconstructive existence proof in constructive logic, you can't.

@duncanw9901

Жыл бұрын

Except you can. Via Gödel-Gentzen. Picking a logic to work in doesn't prevent you from reasoning internally about what answers another system would provide---this is the (more semantically grounded) sense in which I'm using the word "weaker," as conjectured above. ATP software does this almost invariably: in Lean, for example, you can use the "nonconstructive" keyword to just...use LEM, whenever you want, and the same theorem-proving tactics and strategies that are natively constructive simply work. I can't say I know for sure it's implemented this way, but it stands to reason they employ an analogous translation between constructive and nonconstructive variants of their type theory. Picking the strongest such reasonable (i.e. nicely philisophically interpretable) system allows you to have a more significant weight to proofs, and to reason at the metamathematical level more successfully, without sacrificing any power.

Isn't supposing that y is rational OR y is NOT rational using the law of excluded middle?

@assassin01620

Жыл бұрын

@@tomprince8223 but its supposed to be a constructive proof, which means that it doesn't use the law of excluded middle...

@MuffinsAPlenty

Жыл бұрын

@@tomprince8223 I think the question here is about proving log_2(9) is irrational. Michael says this proof is constructive, and I *think* Shimmering Bass is saying that the argument resembles "log_2(9) is not rational; therefore, it is irrational" and therefore relies on LEM (since I am also still trying to wrap my head around constructive mathematics. So I want to see if I'm understanding this too. One defines irrational numbers are real numbers which are not rational. Now, the argument shows that if log_2(9) is rational, then we get a contradiction. Therefore, log_2(9) is not rational. This is perfectly fine reasoning in constructive mathematics, as a proof of the negation. Since irrational numbers are defined as real numbers which are not rational, we conclude that log_2(9) is irrational. Still totally fine. From here, we show that sqrt(2)^log_2(9) is rational, and since we have an explicit witness, we can conclude that "an irrational raised to an irrational can be rational" is true. On the other hand, the non-constructive proof in the video posits two hypothetical witnesses, but does not definitively provide a witness. Therefore, it's non-constructive. Are the above two paragraphs correct?

You can view the Russell's paradox as a proof that the set A doesn't exist - and then there is no problem

Dialethism w Grahm Priest. Intuitional logic. Multi-valued logic. Fuzzy logic. Database (3 valued) logic.

By using a proof by contradiction aren't you assuimng the law of excluded middle? Because if it wasn't true, when you find the contradiction "nP" doesn't mean it's "P" Great video as always btw

(sqrt(2))^(sqrt(2)) is in the form a^b a and b algebraic? ✔️ (sqrt(2) is the solution to x^2-2=0) a≠0 and a≠1? ✔️ b irrational? ✔️ Thus, by the Gelfond-Schneider theorem, (sqrt(2))^(sqrt(2)) is transcendental, and by extension, irrational.

Note, that 2^a can be odd at a=0 (but the result still follow)

@RexxSchneider

10 ай бұрын

Indeed, but then b=0 as well since 3^b has to equal 2^0 = 1. That means the rational number a/b would be 0/0, and that's an indeterminate value, i.e. it's no longer guaranteed to be rational. Hence we can exclude it, and the result still follows, as you say.

9:30 aren't a and b integers (i.e. allowed to be negative)? does it even make sense to talk about "even" and "odd" in that context, since 2^a and 9^b could be fractions?

@MrConverse

Жыл бұрын

I agree with you but it would be an easy thing to finish proving using cases. If exactly one of a & b is negative then exactly one of 2^a & 9^b is an integer and the other is a unit fraction and they clearly cannot be equal. And if both are negative then their reciprocals are integers where one is even and the other is odd which is a contradiction.

@gerryiles3925

Жыл бұрын

But they would be one over an even number and one over an odd number which can still never be equal...

@MrConverse

Жыл бұрын

@@gerryiles3925, that’s what I said. ;-)

@reeeeeplease1178

Жыл бұрын

You can restrict them to be positive as log(9) is always positive

@MrConverse

Жыл бұрын

@@reeeeeplease1178, couldn’t a & b both be negative?

Dilemma you say. Baby Rudin says sqrt(2) is least upper bound of a Cauchy sequence of rational numbers and shows all the arithmetic operations are well defined. So get busy exponentiating.

I am no philosopher by account of years of study. I am commenting for fun. The law of excluded middle seems to have surface level appeal to pretty much anybody and would make it seem a commonsense tautology. From a language point of view, "or" presumes the existence of a general ground of sets A U B out of which A and B are distinguished by our focus. When I was studying mechanical engineering we did a little electronic logic. The Exclusive OR operator explicitly highlights the strict focus for either option between signals. Again, this special distinction is only possible with the set of elements/(sets) as globally contained by A U B. Thus the "tautology" of "P v nP" is arguably a veiled reference to [A U B], the only local sphere of reference? Since nothing else was brought into the scope of the argument, that is all what we can say. And there I think of the very first and very last clauses in Wittgenstein's Tractatus. small lol. As for Russell's paradox, it is a lovely tie-in to the Zermelo/Peano et al. axioms which carve the mathematical world away from more "discursive" logic! On the more practical mathematical level, I think it would absolutely astonishing to be able to define predictively conditions where irrationals/transcendentals "boiled down" to rationals! I love your work.

I think LEM might not apply to some of the more sketchy categories. For instance, since evolution is gradual and no child is a different species from it's parents, then the cutoff between homo erectus and homo sapiens is arbitrary and a matter of expert judgement. So if you experts disagree on where or not a given fossil belongs to erectus or sapiens, there's no objective way to decide that one is right and the other is wrong. We could conceivably say they're both right, violating LEM, or perhaps that the set inclusion is partial in each. The latter case is fuzzy logic where p and not p can be nonzero.

Now do Axiom of Choice.

You already did a video on Z2/[x^2+x+1], which is F4. x^2 + x + 1 = 0 is the Boolean Algebra equivalent of x and not x = true.

@tomholroyd7519

Жыл бұрын

Sorry I pressed send by accident. Lol. But the point is: the liar sentence is morally equivalent to x^2+1 = 0, and has the same solution: instead of reals you have complex numbers. Instead of binary truth values you get complex truth values (two of them) which form a more general system that includes FOUR, the four valued logic, and RM3, a three valued logic (that is also equivalent to Linear Logic (sic) which is really non-linear --- Linear is misnomer here)

I nominate www.youtube.com/@KaneB for a collaboration.

There are only two options Smth is on or smth is off. Therefore there is online meeting or offline meeting Thus, when people doing sex, they are not in any way related to any line, which is nonsense (we just proofed that everything is online or offline) That's why sex dosnot exists

To “p” or not to “p”

Don’t forget there are only two categories of people. Those who dichotomize and those who don’t

proof by contradiction relies on the law of excluded middle right?

@tomprince8223

Жыл бұрын

Only if you are trying to prove P by assuming not P. If you are trying to prove not P by assuming P and finding a contradiction that doesn't involve the law.of the excluded middle.

@writerightmathnation9481

Жыл бұрын

@@tomprince8223 The name for this is "Proof of the Negation", instead of "Proof by Contradiction".

@swenji9113

Жыл бұрын

@@writerightmathnation9481 Exactly, proof of the negation (the one used for log_2(9) for example) doesn't rely on law of excluded middle. "Real" proofs by contradiction rely on the law of excluded middle. I prefer to call these "real" proofs by contradiction "proofs by reductio ad absurbum" which makes things much clearer

I don't think the even/odd is a good example of the law of the excluded middle. The law of excluded middle gets you to for every integer n, n is even, or for every integer n, n is not even. You need to bring in knowledge of the properties of integers to know that a non-even number is an odd number.

If you use "proof by contradiction", then you assume(!) the law of excluded middle ;) Hence your proof is not constructive. In Intuitionistic Logic (or "geometric logic§" in a Topos) you can only assume than not(not(not(P) = not(P). But I am very happy, that you bring up this issue, as many people still think that Intuitionistic Logic and constructive mathematics is a fluke, especially analytically minded people (no harm intended). A good way to start is the accessible book by Lawvere and Rosebrugh. Chees and good work. I enjoyed especially the more abstract videos about Vertex Oprerators, Witt- and Virasoro Algebras, please more of those ;)

@russellsharpe288

Жыл бұрын

A fluke? A lucky accident?

You forgot to take P=NP into account ^^

4:30 a non empty set that doesn't exist? It is easier to claim that set theory is problematic

P and not P is valid. See, the thing is, in non-binary logic you need to expand your definitions of "not" and "valid". "Valid" doesn't just mean true. It also includes P & ~P. That's VALID. This all makes sense if you realize that logical possibility is a monad; P(a) = P(P(a)) because it's a lattice. P(x) has to preserve the ordering

Call Wisecrack!

Actually it is Gelfond, not Gelfand (both great mathematicians)

Well the statement "this statement is false" is neither true nor false, but excluded middle applies to things that aren't self-referential.

Only that the law of the excluded middle is NOT true, unless you want to exclude (at least part of) integer arithmetic from mathematics.

Also, (sqrt(2))^(sqrt(2)) is the square root of the Gelfond-Schneider constant. e^pi is Gelfond's constant

@imeprezime1285

Жыл бұрын

e^π is important number and deserves to be called constant. (✓2)^✓2 is irrelevant random number with no particular important application.

@Vega1447

Жыл бұрын

Not true. Why post this?

@seroujghazarian6343

Жыл бұрын

@@Vega1447 absolutely true. en.m.wikipedia.org/wiki/Gelfond%E2%80%93Schneider_constant#:~:text=The%20Gelfond%E2%80%93Schneider%20constant%20or,by%20Rodion%20Kuzmin%20in%201930. en.m.wikipedia.org/wiki/Gelfond%27s_constant

@Vega1447

Жыл бұрын

@@seroujghazarian6343 what exactly are you claiming in terms of \sqrt 2 and exp(\pi)? Thanks.

@seroujghazarian6343

Жыл бұрын

@@Vega1447 sqrt(2)^sqrt(2) isn't gelfond's constant

There is a clear distinction between the "OK" examples and the "problematic" ones. Self referential logic does not follow the standard logic rules. So any self referential statement CAN'T be used in formal proofs. They can be crafted to always lead to contradictions. They are fun for puzzles though. I don't see a problem with the Law of Excluded middle. It is kind of like the proof of 1 + 2 + 3 + ... = -1/12. You are breaking one of the requirements of one of the steps. Same goes here. Law of excluded middle only applies to non self referential statements.

I know you're pushing the saturation way up to make the colored chalk "pop" a little more, but it also has the effect of making it look like the good professor did a rather poor job of applying lipstick. Or perhaps he's a Mentat. Yes, that would make more sense...

If x^y is a complex number, is it defined as "rational" only if both its real and imaginary parts are themselves rational?

@pierreabbat6157

Жыл бұрын

A complex number whose imaginary part is nonzero is irrational. However, a complex number can be "rational" relative to an algebraic integral domain. An Eisenstein rational is the quotient of two Eisenstein integers (the denominator being nonzero), and similarly for a Gaussian rational. So all cube roots of 27/8 are Eisenstein rationals, but only one is a rational or a Gaussian rational, and 3i/4 is a Gaussian rational, but not an Eisenstein rational or a rational.

@trueriver1950

9 ай бұрын

Your first sentence implies that the irrational numbers are not a subset of the reals. That's a culture shock to me! Why? Thinks for a moment... It looks kind of partly right because i is not expressible as the tattoo of two interests But it looks wrong because the number i for example does not partition the reals into those larger and those smaller than itself, which I had always understood was an essential part of the definition of an irrational: in ordinary language it says that the originals are on the real number line whereas the complex numbers are not. Or are you defining some other kinds of number: a complex irrational or some such?

Doesn't proof BWOC require the law of the excluded middle? Tautology show that ~P => ~P. The contradiction shows P=> ~P. Using rules of inference you can then get P or ~P => ~P. But you still need to assume P or ~P before you derive ~P from it.

@andrewlitfin1977

Жыл бұрын

So in constructive logic you have to distinguish between proof by contradiction and proof of negation. Proof by contradiction: Assume ~P, get contradiction, therefore P. Proof of negation: Assume P, get contradiction, therefore ~P. Strangely enough, while contradiction is invalid in constructive logic, proof of negation is totally fine.

@richardfarrer5616

Жыл бұрын

@@andrewlitfin1977 Excellent, thank you. It's been many decades since I was taught any of this and it's a bit rusty (if I ever really understood it in the first place). So, if Michael asserts that log_2 (9) is rational then he can prove there is a contradiction and get that it is not rational. However, if he asserts P:"log_2 (9) is not rational" then all he can prove is ~~P which, if I recall correctly is not the same as P unless you assume the law of the excluded middle.

@andrewlitfin1977

Жыл бұрын

@@richardfarrer5616 Correct on all counts

👍

I don't know if it fits but the professor who taught me mathematical logic (Kazimierz Świrydowicz) proved in one of his works that there are exactly three different consistent logics that do not contain law of excluded middle so if we get rid of it (as some researchers in ML want to do) we would have a hard time to justify picking one instead of other two

@tomprince8223

Жыл бұрын

Well, particularly in the case of applications to something like ML, you'd pick between different logics based on how useful it is for your application. There is no need to justify it in a philosophical sense. Even when thinking about mathematical foundations, I suspect much of it comes down to the same type of argument.

@splo2766

Жыл бұрын

Wow, interesting. Maybe it will depend on the logic and its practical implications. As Poincare says "Geometry is not true, it is advantageous", it might be the same with logic!

@pmcate2

11 ай бұрын

I can't find this paper

@trueriver1950

9 ай бұрын

I'm curious as to whether his threesome of logics included the one where an logical value in a proposition can contain a superposition of True and False, as is fundamental in Quantum Computing logic. If not then quantum mechanics has extended the range...

#RM3 The Liar Paradox is Valid, the answer is Both, it's both true and false (same as russell's thing)

√2^√2 is irrational: The Gelfond-Schneider theorem states that given algebraic numbers a,b where a≠0,1 and b is irrational, a^b is transcendental. sqrt(2)^sqrt(2)^sqrt(2) works but sqrt(2)^sqrt(2) is not rational

@robertveith6383

Жыл бұрын

If you are intending sqrt(2)^sqrt(2) to be a base, then you need to place it inside grouping symbols, such as: [sqrt(2)^sqrt(2)]^sqrt(2). Else, a^b^c = a^(b^c).

Note: the law of Excluded middle is actually not needed to show that every integer is either odd or even, nor for Russel Paradox to lead to a contradiction. Of the three examples you give only "x in Q or x not in Q" can fail if we don't assume the law of excluded middle. In the first case it boils down to the fact that "for all n in N, n = 0 or n >0" can be proved by induction, and so, many other properties of the integers can be shown from this to also satisfies excluded middle even if we don't assume it (for e.g. x is even if x mod 2 =0 and odd if x mod 2 >0). For Russel paradox it works because if you assume that A \in A, then it leads to a contradiction, from which we can deduce that "A is not in A". This step isn't a use of excluded middle, this is the definition of the negation ("not P" means "P implies false"), and finally "A not in A" also leads to a contradiction.

Is you is or is you ain't my baby?

In fact, sqrt(2) is a little like the Russell's paradox statement P. After all, it is easy enough to define sqrt(2) without actually computing it, just as it is easy to define P. But when you try to look at the insides of it, things fall apart. Since sqrt(2) is "represented" by an infinite decimal expansion, we can never actually take a number that we claim to be sqrt(2) and multiply it by itself to show that the product does in fact equal the rational number 2 (ie, with nothing but zero's in any decimal place whatsoever). So we can glibly talk about sqrt(2) as if it really exists, but we cannot show that it really exists - similar to P.

What you are missing is that in intuitionistic logic, you make the distinction between proving "not every irrational number to irrational power is irrational" and "There *exists* a pair of irrational numbers such that the power of one by the other is rational". The reason is simply that the proofs prove two different things, not that one proof is somehow invalid. The strong existence proof provides an algorithm for producing two irrationals with the given property, while the weak existence proof only provides an algorithm for converting a proof of the for-all statement into a contradiction. They are two different COMPUTER PROGRAMS, therefore they should be distinguished. That's what intuitionistic logic is about. By the double-negation embedding, there is NOTHING STRONGER about traditional logic, it's just less specific about what exactly is being proved.

Waste of my time It will not make any difference to my life if I know how to solve this math problem or not

Wait....Is 0 an...irrational number? 🤯 It's not a ratio of integers, unless you a) define 0 as an integer and b) it's the numerator in the ratio that is considered as rational. FWIW same would apply to, say, pi where e.g. pi/2 would be rational IF pi would be defined as an integer. The point I'm making is that something like 1, 2, 3... would still be clearly rational as e.g. 2/2, 4/2, 6/2 would satisfy the ratio, where as 0 always needs 0 in the ratio (as would e.g. pi).

@MyOneFiftiethOfADollar

Жыл бұрын

0=0/k for all k not equal to 0. So not only is it rational, but it is one helluva rational number.

@Packerfan130

Жыл бұрын

It is, if you can write it as a ratio of two integers where the denominator isn't 0, then its rational.

Mark Thorsby has a very good channel about philosophy and formal logic.

@MyOneFiftiethOfADollar

Жыл бұрын

Advertising another channel on this channel where many years of hard traffic building work have been invested. Your channel or friend who will share their ad revenue with you?

I have been thinking about this law for a few weeks now, after I watched another video on the same topic. And I've come to the conclusion it is unnatural in general (i.e. in real life) to assume this. That being said, it is for sure necessary in mathematics! Which I find pretty interesting

@QuantumHistorian

Жыл бұрын

That's because absolute dichotomies are rare in real life, but common in mathematics (by construction). Not sure there's more depth to it than that?

@Bird1502

Жыл бұрын

Wait, are there actually mathematicians that take the stance that modern mathematics doesn’t require LEM for everything to hold up? That seems insanely unlikely to me…

@teeweezeven

Жыл бұрын

@@Bird1502 I'm not sure. I think I've heard of a branch of mathematical logic where they try to work without contrapositives ("not B implies not A" being the same as "A implies B"). Maybe even without contradiction. But contradiction is very powerful so basically all mathematics is built on it

@swenji9113

Жыл бұрын

It is not "necessary" in maths. It really depends on what you're trying to do. I like to think of it this way: Consider a natural number: it is either even or odd, it is either a square or it is not, it is either greater than 6 or it is not. LEM makes sense for situations where you're describing an object (assuming you have all the informations, which is purely ideal I agree). Now consider abstract propositions like "all natural numbers are a product of primes". You cannot say if it is true or not by looking at each natural number, you will need a proof! If you find a proof, then well done, it is true. If you don't... well is it necessarily false? From the moment the notion of truth changes from observation to demonstration, its properties change as well, and that includes the LEM. You might know that there are mathematical propositions that cannot be proved nor refuted. In this context, LEM is not only unnecessary, it is false. This is, of course, not the only example, but I think it highlights a very important fact about logic: in mathematics and particularly in real life, being true does not always mean the same thing depending on the context. There are many different forms of logic, some with precise rules and some without, and among the first category, many logics use LEM and many others don't :)

@swenji9113

Жыл бұрын

@@Bird1502 I'm not sure what your question is exactly. I'd say mathematicians are pretty much aware of what can be done with LEM and what cannot. Some of them specialize in branches of mathematics where they explore what can be said without using LEM, that's all. As for their beliefs I can't tell if they think constructivism (for example) is the "good logic" but I'd say they're convinced that studying it will lead to many discoveries of interest!