"In 2022, I had reached the zenith of my depression, listening to Billie Joe Armstrong systematically deconstruct all experience as the qualia of quanta's existence in various logical relation. The terror gripped me once more. Perhaps this is why we find no civilizations among the stars."
One surprising result of this non constructive nature of the classical math tradition is the linear algebra theorem that affirms the existence of a basis(particularly in an infinite dimensional spaces like real functions). However, nobody has any idea what this basis could "look like," it's kinda disappointing.
Excelent! But i'd like to revise something: did you say that to assert ¬A v ¬(¬A) (11:19) would be a contracdition? That would be only in the conjunction case, right?
Thanks! I think what I was saying there is this: given ~~A and a choice between A and ~A, we would have to choose A, since accepting both ~~A and ~A would be inconsistent. (So, as you say, the contradiction is with conjunction.)
What is the purpose behind intuitionistic logic? Or what can it be used for that other logics cant? I'm new to logic and I always wonder why different logics were created. I think explaining the purposes of the different logical systems you discuss would be a great video topic!
Some philosophers/logicians think some of the rules of classical logic are meaningless. Intuitionistic logic drops those rules. Have a look at the video on the philosophy behind intuitionistic logic if you’re interested in this.
I would add that intuitionistic logic is the one used in proof assistants, automatic theorem provers and programming. There are niche use cases for modal logics in programming and proof theory as well (like when you want to prove a deadlock or that you aren't accidentally reading from an improper part of memory)
@@AtticPhilosophy The philosophical reasons are quite strong, therefore I think that it could be enjoyed by a wide audience. Of course it all depends on the amount of technical details you plan to focus on.
Two comments. First, the law of excluded middle should be expressed using an exclusive or, not an inclusive or. That is, either a or b, but not both. Second, it would help to connect up front the rejection of the law of excluded middle to the lack of completeness and decidability in mathematics, Basically, "true or false" gets replaced by "provably true, provably false, undecidable"
No, intuitionists explicitly reject LEM with inclusive or. Rejecting the exclusive version is compatible with accepting the inclusive version, which intuitionists don’t do. LP, for example, accepts LEM but rejects the exclusive or version.
I just want to observe that poof by contradiction is invalid if LEM is expressed using inclusive or, because it allows for both p and not p to be true. So, intuitionists and classicists alike will reject that formulation. I am questioning the (acknowledged, long-standing) tradition of expressing LEM using the inclusive or, not your very fine and accurate presentation. LEM is always rendered in English using "either...or" which typically signals an exclusive or.
@@jcshultis OK I see what you're trying to say, but it's mistaken: proof by contradiction is classically valid however LEM is expressed. Even if you drop LEM completely proof by contradiction (from assuming p & inferring a contradiction to ~p) is valid, as it is in intuitionistic logic (which lacks LEM). Here's what's going on. LEM rules out 1 option for p: neither T nor F. *Other* laws rule out the option of both T and F for p. So the fact that LEM (on its own, expressed inclusively) seems to allow both T,F isn't the crucial point, given what the other laws do. So in that sense, in the classical setting, the inclusive and exclusive expressions of LEM are equivalent. But they're not equivalent in some non-classical settings, e.g. in LP, where the inclusive but not the exclusive version is valid.
@@jcshultis I see what you're trying to say, but it's mistaken: proof by contradiction (from assuming A, inferring a contradiction, to ~A) is classically valid however LEM is formulated, or even without it, as in intuitionistic logic. LEM rules out 1 option: neither T nor F. Other rules rule out the other option: both T and F. It's not the job of LEM to rule out both T and F, other rules do that. That's how we can drop LEM but keep things consistent (as in K3) or keep LEM but allow inconsistency (as in LP).
A suggestion: the words / letters around 2:04 are difficult to read. For any international students who may not be familiar with our cursive writing, it Kaye be unreadable to them.
This type of logic is odd to me. It seems like the goal is to convolute and confuse scenarios when in reality once you boil the scenarios down the outcome is still a scenario that is A or ~A.
It was popular at various points in the 20th century, e.g. with those who connected meaning to proof or use. It's now popular with computer scientists, who often say, if it can't be computed even in theory, then it's meaningless.
This is very clear and very helpful, so firstly, thank you! Can you give me an intuition for how this applies to designing type systems in programming languages? I understand the benefit of verifiability, but I'm not clear on the benefit dispensing with "negative information". Can someone help me understand / ELI5?
Hi, computer scientist here! In type systems, types are like tags we give to data/programs. So for example, 3 is of type int, or "hello" is of type string. Types that have some data associated with them are called "inhabited". There is one special type called the Empty type, denoted with the symbol '⊥'. It has no data associated with it, i.e. it is not inhabited. You can think of it as undefined behavior and you can get any arbitrary data from it. (akin to Ex Falso Quadlibet) Negation ~A in a type system is hence defined as ~A := A → ⊥. Data of type A →⊥ is a function which takes data of type A and outputs data of type ⊥. Since ⊥ doesnt have any data, then its impossible to produce data of type A (assuming your type system is sound). Now going back to why ~~A doesnt imply A. ~~A means "If we have data of type A → ⊥, then we can produce data of type ⊥", but this is not the same as "We have data of type A". We cant create new programs/data out of thin air just because we know that its negation is absurd.
could you create a logic which would present common errors (like idk the an algea in a pond doubles every day, it reaches it maximum on day 100, when was it half the size) ie like a like hmmmm like a truth value based upon a minimum step minimal complexity proof where not (a and b ) = not a and not b not a and b = not a or b ie like where we act like demorgan's law doesn't exist, allow bad statements and try ascertain the most simple solution and see if those are common logical fallacies or like the thinking fast/slow shortcuts? :thinky: :thinky: like an illogical logical logic :)
oooo the existence of everything all swans are black == everything that is not black is not a swan, thingy? so like every yellow shirt i have helps let me know that swans are all black? (i created a probabilistic argument in one of my papers in the only logic course i had in uni - ie the domain of the objects which are not black is just too massive, that yeah while we can bayesian update the probility that the statement is true the update is minimal, we covered a little fuzzy and talked alot about bonobos)
Hmm tricky because any A is equivalent to A&T (where T is a tautology) so ~A equivalent to ~(A&T), whereas ~A&~T is impossible. So no negation could ever be true!
hey, man! love your videos! I was wondering if you could say more about the grounds for rejecting the law of excluded middle. I suppose I find it so intuitive (pun totally intended) that I have difficulty understanding what justifies its denial. I'm quite probably misunderstanding your example, but I wonder: Would it be so strange not to know who scored 90% on the test if, say, you yourself didn't grade them, or you simply forgot because there were so many, or they used ID numbers rather than names, etc.? I take it there could be all manner of instances where we can know or trust that someone made such a score, even though we don't know who. (If, for example, we learned by hearsay that someone got 90%, or happen to have glimpsed the teacher's gradebook and seen the column of scores but not the column of names, etc.) I suspect you mean that it would be strange if none of these conditions held and you *still* couldn't say who got 90%, that it would be odd if there were some in-principle constraint or obstacle that kept you from knowing. And here I quite agree, but I suppose I'm curious about what this principle is, exactly, and what reason there is to think that it holds generally or even in this case in particular. I think there's something not quite clicking for me about the stipulation... With respect to the mathematics example, isn't this just what it means to have grounds to believe something? And aren't there analogous cases that arise all the time? It seems to me that I can make quite warranted claims about all kinds of things without being able to offer further specifics. Like, say my colleague's fifth grade class is having Orange Day, where all her students wear orange sweaters to celebrate the arrival of Autumn. After lunch, I discover that someone left their orange sweater in the cafeteria. Can't I justly say that one of her students lost their sweater (i.e., "there is a student that X"), even though I don't know which one? I suppose I'm a bit unsure as to how being unable to identify *which* X something is, is grounds for revoking license to claim (deductively or otherwise) that *there is* some X. I readily concede that determining *which* X something is might require additional premises whose form and substance differ according to circumstance. But still I wonder: If I see my dog run excitedly into a room of identical dogs, aren't I warranted in assuming my dog is in there, even if I can't say which one it is? And perhaps I should ask: What are the epistemic consequences of denying that I am? I can't help but wonder whether denial doesn't in some form or other lead to incoherence or contradiction. (For example, I'm terribly curious-and would love to know your thoughts-about what implications a denial of intuitionism would have for topos theory.) At any rate, I'm sure I'm missing something, lol. I should also say: I'm quite sympathetic to meaning-as-use theories (perhaps especially inferentialism). But I wonder if this is even required for or entailed by the acceptance of such theories. Anyway, thanks so very much for the help! Your videos rock!
There’s a few different reasons one might reject LEM. One is from truth-value gaps. Eg you might think facts about the future aren’t yet settled, so statements about the future aren’t yet true or false, and on that basis, you might reject LEM for such statements. Another case is vagueness: for borderline claims, you might reject LEM. Intuitionists have a different viewpoint. They think of truth along the lines of evidence or proof. For some mathematical statements A, you can’t prove A and you can’t prove ~A, and so they conclude we can’t assert A v ~A.
@poklar Here's one where it is relevant in mathematics: applications. There's two kinds of settings where this is true. One of them is the computer science inspired form of constructive logic where you redefine existence to mean that you have a practical algorithm to compute something, and truth to mean that you can prove that it is true with a computation, and where AND and OR means you have computations proving both, and a computation proving one or a computation proving the other, respectively. In that case, you do not have excluded middle, because that is just not how computations work. You do not choose the rules, you just define what the symbols mean in the practical application you are interested in and then write down the rules they actually satisfy. The other common way this pops up is in topos theory, which are (simplifying to the most basic and most often used case of Sh(X) where X is a topological space) logics talking about things that are locally true in space. In that case, a covering is a family of open subsets of the space (open means the set does not include its boundary), such that every point is part of one of those open subsets. Then we define A OR B to mean that there is a covering, and in each subset A holds or B holds, but on different subsets different options can be true. Similarly, A => B means that A implies B on every open subset, and NOT A means A holds on no open subset. That logic is useful because anything you prove on several open subsets can be glued together to hold on their union, so that you only need to prove things locally. So basically, from a mathematicians point of view, you do this because you are interested in that application, and the law of the excluded middle is just false in that application. Often you still accept excluded middle in the "outside" logic, but the thing you defined that happens to behave exactly like a logic and lets you do short "internal" proofs of the things you care about that translate into possibly exponentially longer proofs in the "outside" logic is not a classical logic. It has nothing to do with any person's sensibilities or what they would like to be true, and you just go along with the rules of the incredibly interesting object you are actually discovering the features of.
Nice content! Just one detail: The way you define classical logic does not really work because quite some non-classical logics satisfy your criteria. In free logic, for example, every sentence is true or false and negation toggles between truth-values, but free logic is not (generally) considered classical. Now you might object because variable domain modal logic is a free logic, but there are other examples such as some connexive logics, non-monotonic logics or paraconsistent logics which are not dialetheic. Keep up the good work!
You're absolutely right, 'classical logic' is hard to pin down with absolute precision. (Must it have compactness? Löwenheim-Skolem? Interpolation?) LEM doesn't cut it, since LP has that. But all of that is a long way down the road from intro logic! At this point, 'exactly 1 of 2 truth-values + DNE' gives a good enough handle on what 'classical' is meant to mean.
That's right. All intuitionistic rules are also classically valid, so any intuitionistic proof also counts as a proof in classical logic. If you take the intuitionistic rules and add double-negation elimination (~~p -> p) or excluded middle (p v ~p) you get classical logic.
@@AtticPhilosophy thank you :), i also thought that way, but i wasn't sure. I want to learn more about synthetic a priori, and why Kant said that math is Synthetic a priori. The content about that would be great.
Good question! It goes back to Kant: he thought we had an a priori intuition of space & time. Brouwer, the founder of intuitionism, thought we have a similar intuition of natural numbers, one after the other, like moments of time. The name stuck.
Or... all is ontologic in nature. thank you you for this content. I have a particular dificulty on mathmatics and specially in logic, disregarding the fact I work with descriptive logic on a almost daily basis. The thing is... I have never accepted in my mind, in my very hearth a proposition kind of "A or B", because it is not damn logic! What is A? What the hell is B for I can say it is true or false? So... it is great relief finding stuff like that. Personally I think nothing exists out of an identity perspective. Be it an action,a fact, a thing, an abstract word like when... logic is just logic when the observed is given an identity, properties, relations. when we have an existential characterization of one, be it an individual or a conceptual, just in this moment we can say it is true or false, or better saying who or what it is, so just after that comes up the possibility of disjuction analisys. So if I say When or What?... ok! It is true for both. When is possible and what is also in negation of when assuming that when is temporal, but time does not happens out of no fact at all. So if there is a When there is a what expected to happen. But if this what does not happen, so what happens instead? Langacker and other authors on cognitive linguistics say language is not apart from cognitiion, learned experience, social interaction. All this is our self ontology, that lives in our minds. Great night! I want to know more about intuitionistic logic.
I don't think you've grasped what 'constructive reasoning' means. It's the requirement that, e.g., a proof of 'there exists a number such that X' specifies which specific number that is. That's a proof even by non-constructive lights, so definitely not 'making it up'.
"In 2022, I had reached the zenith of my depression, listening to Billie Joe Armstrong systematically deconstruct all experience as the qualia of quanta's existence in various logical relation. The terror gripped me once more.
Perhaps this is why we find no civilizations among the stars."
this explains better than the set theory book i'm using now. Thank you so much
Great introduction, thank you!
Thanks!
It will be perfect if you could indicate the bibliography of each topic that you explain in each video. Or further readings
One surprising result of this non constructive nature of the classical math tradition is the linear algebra theorem that affirms the existence of a basis(particularly in an infinite dimensional spaces like real functions). However, nobody has any idea what this basis could "look like," it's kinda disappointing.
This channel is criminally underrated
Thanks!
Coq
Excelent! But i'd like to revise something: did you say that to assert ¬A v ¬(¬A) (11:19) would be a contracdition? That would be only in the conjunction case, right?
Thanks! I think what I was saying there is this: given ~~A and a choice between A and ~A, we would have to choose A, since accepting both ~~A and ~A would be inconsistent. (So, as you say, the contradiction is with conjunction.)
🔥🔥🔥🔥
What is the purpose behind intuitionistic logic? Or what can it be used for that other logics cant? I'm new to logic and I always wonder why different logics were created. I think explaining the purposes of the different logical systems you discuss would be a great video topic!
Some philosophers/logicians think some of the rules of classical logic are meaningless. Intuitionistic logic drops those rules. Have a look at the video on the philosophy behind intuitionistic logic if you’re interested in this.
I would add that intuitionistic logic is the one used in proof assistants, automatic theorem provers and programming. There are niche use cases for modal logics in programming and proof theory as well (like when you want to prove a deadlock or that you aren't accidentally reading from an improper part of memory)
Thank you for the great work! What about a series focusing on relevance logic?
I'd love to - do you think it's too niche or advanced for this audience?
@@AtticPhilosophy The philosophical reasons are quite strong, therefore I think that it could be enjoyed by a wide audience. Of course it all depends on the amount of technical details you plan to focus on.
@@AtticPhilosophy I vouch for a series on relevance logic! Paradoxes of material implication might be worth exploring.
Yeah, I would love to watch such a video too!
Two comments. First, the law of excluded middle should be expressed using an exclusive or, not an inclusive or. That is, either a or b, but not both. Second, it would help to connect up front the rejection of the law of excluded middle to the lack of completeness and decidability in mathematics, Basically, "true or false" gets replaced by "provably true, provably false, undecidable"
No, intuitionists explicitly reject LEM with inclusive or. Rejecting the exclusive version is compatible with accepting the inclusive version, which intuitionists don’t do. LP, for example, accepts LEM but rejects the exclusive or version.
I just want to observe that poof by contradiction is invalid if LEM is expressed using inclusive or, because it allows for both p and not p to be true. So, intuitionists and classicists alike will reject that formulation. I am questioning the (acknowledged, long-standing) tradition of expressing LEM using the inclusive or, not your very fine and accurate presentation. LEM is always rendered in English using "either...or" which typically signals an exclusive or.
@@jcshultis OK I see what you're trying to say, but it's mistaken: proof by contradiction is classically valid however LEM is expressed. Even if you drop LEM completely proof by contradiction (from assuming p & inferring a contradiction to ~p) is valid, as it is in intuitionistic logic (which lacks LEM). Here's what's going on. LEM rules out 1 option for p: neither T nor F. *Other* laws rule out the option of both T and F for p. So the fact that LEM (on its own, expressed inclusively) seems to allow both T,F isn't the crucial point, given what the other laws do. So in that sense, in the classical setting, the inclusive and exclusive expressions of LEM are equivalent. But they're not equivalent in some non-classical settings, e.g. in LP, where the inclusive but not the exclusive version is valid.
@@jcshultis I see what you're trying to say, but it's mistaken: proof by contradiction (from assuming A, inferring a contradiction, to ~A) is classically valid however LEM is formulated, or even without it, as in intuitionistic logic. LEM rules out 1 option: neither T nor F. Other rules rule out the other option: both T and F. It's not the job of LEM to rule out both T and F, other rules do that. That's how we can drop LEM but keep things consistent (as in K3) or keep LEM but allow inconsistency (as in LP).
Thank you very much :)
You're welcome!
Great explanation
Thanks!
It has positivistic roots?
More like the other way around: intuitionistic/constructive thinking from early 20thC influenced some positivistic thinking in early-mid 20thC.
A suggestion: the words / letters around 2:04 are difficult to read. For any international students who may not be familiar with our cursive writing, it Kaye be unreadable to them.
Good sound, my handwriting is terrible! Hopefully the captions make sense for non-English speakers.
Great video!
Thanks!
This type of logic is odd to me. It seems like the goal is to convolute and confuse scenarios when in reality once you boil the scenarios down the outcome is still a scenario that is A or ~A.
It was popular at various points in the 20th century, e.g. with those who connected meaning to proof or use. It's now popular with computer scientists, who often say, if it can't be computed even in theory, then it's meaningless.
Yaaaassssssss i found explanatioooooon!!! Thaaaaanks!!!!!!! jeeeez u the greatest!
You’re welcome!
This is very clear and very helpful, so firstly, thank you! Can you give me an intuition for how this applies to designing type systems in programming languages? I understand the benefit of verifiability, but I'm not clear on the benefit dispensing with "negative information". Can someone help me understand / ELI5?
Hi, computer scientist here!
In type systems, types are like tags we give to data/programs. So for example, 3 is of type int, or "hello" is of type string. Types that have some data associated with them are called "inhabited".
There is one special type called the Empty type, denoted with the symbol '⊥'. It has no data associated with it, i.e. it is not inhabited. You can think of it as undefined behavior and you can get any arbitrary data from it. (akin to Ex Falso Quadlibet)
Negation ~A in a type system is hence defined as ~A := A → ⊥.
Data of type A →⊥ is a function which takes data of type A and outputs data of type ⊥.
Since ⊥ doesnt have any data, then its impossible to produce data of type A (assuming your type system is sound).
Now going back to why ~~A doesnt imply A. ~~A means "If we have data of type A → ⊥, then we can produce data of type ⊥", but this is not the same as "We have data of type A". We cant create new programs/data out of thin air just because we know that its negation is absurd.
@@nukeeverything1802 This is extremely enlightening, thank you! 🙏
could you create a logic which would present common errors (like idk the an algea in a pond doubles every day, it reaches it maximum on day 100, when was it half the size) ie like a like
hmmmm like a truth value based upon a minimum step minimal complexity proof where
not (a and b ) = not a and not b
not a and b = not a or b
ie like where we act like demorgan's law doesn't exist, allow bad statements and try ascertain the most simple solution and see if those are common logical fallacies or like the thinking fast/slow shortcuts?
:thinky:
:thinky:
like an illogical logical logic :)
oooo the existence of everything
all swans are black == everything that is not black is not a swan, thingy?
so like every yellow shirt i have helps let me know that swans are all black?
(i created a probabilistic argument in one of my papers in the only logic course i had in uni - ie the domain of the objects which are not black is just too massive, that yeah while we can bayesian update the probility that the statement is true the update is minimal, we covered a little fuzzy and talked alot about bonobos)
Hmm tricky because any A is equivalent to A&T (where T is a tautology) so ~A equivalent to ~(A&T), whereas ~A&~T is impossible. So no negation could ever be true!
hey, man! love your videos! I was wondering if you could say more about the grounds for rejecting the law of excluded middle. I suppose I find it so intuitive (pun totally intended) that I have difficulty understanding what justifies its denial. I'm quite probably misunderstanding your example, but I wonder: Would it be so strange not to know who scored 90% on the test if, say, you yourself didn't grade them, or you simply forgot because there were so many, or they used ID numbers rather than names, etc.? I take it there could be all manner of instances where we can know or trust that someone made such a score, even though we don't know who. (If, for example, we learned by hearsay that someone got 90%, or happen to have glimpsed the teacher's gradebook and seen the column of scores but not the column of names, etc.) I suspect you mean that it would be strange if none of these conditions held and you *still* couldn't say who got 90%, that it would be odd if there were some in-principle constraint or obstacle that kept you from knowing. And here I quite agree, but I suppose I'm curious about what this principle is, exactly, and what reason there is to think that it holds generally or even in this case in particular. I think there's something not quite clicking for me about the stipulation... With respect to the mathematics example, isn't this just what it means to have grounds to believe something? And aren't there analogous cases that arise all the time? It seems to me that I can make quite warranted claims about all kinds of things without being able to offer further specifics. Like, say my colleague's fifth grade class is having Orange Day, where all her students wear orange sweaters to celebrate the arrival of Autumn. After lunch, I discover that someone left their orange sweater in the cafeteria. Can't I justly say that one of her students lost their sweater (i.e., "there is a student that X"), even though I don't know which one? I suppose I'm a bit unsure as to how being unable to identify *which* X something is, is grounds for revoking license to claim (deductively or otherwise) that *there is* some X. I readily concede that determining *which* X something is might require additional premises whose form and substance differ according to circumstance. But still I wonder: If I see my dog run excitedly into a room of identical dogs, aren't I warranted in assuming my dog is in there, even if I can't say which one it is? And perhaps I should ask: What are the epistemic consequences of denying that I am? I can't help but wonder whether denial doesn't in some form or other lead to incoherence or contradiction. (For example, I'm terribly curious-and would love to know your thoughts-about what implications a denial of intuitionism would have for topos theory.) At any rate, I'm sure I'm missing something, lol. I should also say: I'm quite sympathetic to meaning-as-use theories (perhaps especially inferentialism). But I wonder if this is even required for or entailed by the acceptance of such theories. Anyway, thanks so very much for the help! Your videos rock!
There’s a few different reasons one might reject LEM. One is from truth-value gaps. Eg you might think facts about the future aren’t yet settled, so statements about the future aren’t yet true or false, and on that basis, you might reject LEM for such statements. Another case is vagueness: for borderline claims, you might reject LEM. Intuitionists have a different viewpoint. They think of truth along the lines of evidence or proof. For some mathematical statements A, you can’t prove A and you can’t prove ~A, and so they conclude we can’t assert A v ~A.
@poklar Here's one where it is relevant in mathematics: applications. There's two kinds of settings where this is true.
One of them is the computer science inspired form of constructive logic where you redefine existence to mean that you have a practical algorithm to compute something, and truth to mean that you can prove that it is true with a computation, and where AND and OR means you have computations proving both, and a computation proving one or a computation proving the other, respectively. In that case, you do not have excluded middle, because that is just not how computations work. You do not choose the rules, you just define what the symbols mean in the practical application you are interested in and then write down the rules they actually satisfy.
The other common way this pops up is in topos theory, which are (simplifying to the most basic and most often used case of Sh(X) where X is a topological space) logics talking about things that are locally true in space. In that case, a covering is a family of open subsets of the space (open means the set does not include its boundary), such that every point is part of one of those open subsets. Then we define A OR B to mean that there is a covering, and in each subset A holds or B holds, but on different subsets different options can be true. Similarly, A => B means that A implies B on every open subset, and NOT A means A holds on no open subset. That logic is useful because anything you prove on several open subsets can be glued together to hold on their union, so that you only need to prove things locally.
So basically, from a mathematicians point of view, you do this because you are interested in that application, and the law of the excluded middle is just false in that application. Often you still accept excluded middle in the "outside" logic, but the thing you defined that happens to behave exactly like a logic and lets you do short "internal" proofs of the things you care about that translate into possibly exponentially longer proofs in the "outside" logic is not a classical logic. It has nothing to do with any person's sensibilities or what they would like to be true, and you just go along with the rules of the incredibly interesting object you are actually discovering the features of.
Nice content! Just one detail: The way you define classical logic does not really work because quite some non-classical logics satisfy your criteria. In free logic, for example, every sentence is true or false and negation toggles between truth-values, but free logic is not (generally) considered classical. Now you might object because variable domain modal logic is a free logic, but there are other examples such as some connexive logics, non-monotonic logics or paraconsistent logics which are not dialetheic. Keep up the good work!
You're absolutely right, 'classical logic' is hard to pin down with absolute precision. (Must it have compactness? Löwenheim-Skolem? Interpolation?) LEM doesn't cut it, since LP has that. But all of that is a long way down the road from intro logic! At this point, 'exactly 1 of 2 truth-values + DNE' gives a good enough handle on what 'classical' is meant to mean.
any prove in Intuitionistic Logic is it valid in Classical Logic?
That's right. All intuitionistic rules are also classically valid, so any intuitionistic proof also counts as a proof in classical logic. If you take the intuitionistic rules and add double-negation elimination (~~p -> p) or excluded middle (p v ~p) you get classical logic.
@@AtticPhilosophy thank you :), i also thought that way, but i wasn't sure. I want to learn more about synthetic a priori, and why Kant said that math is Synthetic a priori. The content about that would be great.
Why is it called 'intuitionistic'?
Good question! It goes back to Kant: he thought we had an a priori intuition of space & time. Brouwer, the founder of intuitionism, thought we have a similar intuition of natural numbers, one after the other, like moments of time. The name stuck.
Or... all is ontologic in nature. thank you you for this content. I have a particular dificulty on mathmatics and specially in logic, disregarding the fact I work with descriptive logic on a almost daily basis. The thing is... I have never accepted in my mind, in my very hearth a proposition kind of "A or B", because it is not damn logic! What is A? What the hell is B for I can say it is true or false? So... it is great relief finding stuff like that. Personally I think nothing exists out of an identity perspective. Be it an action,a fact, a thing, an abstract word like when... logic is just logic when the observed is given an identity, properties, relations. when we have an existential characterization of one, be it an individual or a conceptual, just in this moment we can say it is true or false, or better saying who or what it is, so just after that comes up the possibility of disjuction analisys. So if I say When or What?... ok! It is true for both. When is possible and what is also in negation of when assuming that when is temporal, but time does not happens out of no fact at all. So if there is a When there is a what expected to happen. But if this what does not happen, so what happens instead? Langacker and other authors on cognitive linguistics say language is not apart from cognitiion, learned experience, social interaction. All this is our self ontology, that lives in our minds. Great night! I want to know more about intuitionistic logic.
14 minutes of stating the Law of Excluded Middle in different ways.
Basically the method of presenting any real proof in symbolic systems...
"Constitutive reasoning" is just making it up as you go (lying). 🤦🏼♂️
I don't think you've grasped what 'constructive reasoning' means. It's the requirement that, e.g., a proof of 'there exists a number such that X' specifies which specific number that is. That's a proof even by non-constructive lights, so definitely not 'making it up'.
@@AtticPhilosophyJust sounds like lying to me?🤷🏽♂️
It's not a matter of lying because it is a symbolic system. It doesn't envelope and neither superposes with physical or material reality.