Intuitionistic Logic and Constructive Proof | Attic Philosophy

[@kaa1el960]

a^b^c is usually associated to the right = a^(b^c), and left association usually requires brackets: (a^b)^c = a^(bc)

[@johnward5102]

Beautiful piece of work, exploring the limits. I have no answers to the questions you pose. If I understand you correctly then Kurt Godel's incompleteness theorems are non-constructive. They show if a proposition is provable, or not, but if provable they will not help you find what the proof is. His theorems are very significant, but is it the case that if they did show what the proof was then they would disprove themselves, as theorems. There are limits to where logic can take us.

[@sakama239]

Is anyone else here cuz their symbolic logic professor sucks at teaching intro class 🙏 this video makes way more sense than my 6hr class, thx!

[@AtticPhilosophy]

Thanks! I honestly think logic can be made simple (without dumbing it down) - that's what I'm trying to do here. Glad it helped!

[@rafaelo6198]

great video, helped me to understand why exactly G3cp is not translatable into G3ip (and why it is using double negation for G3ip)

[@AnarchoAmericium]

This deserves more views.

[@AtticPhilosophy]

Thanks! I hope it does.

[@Guz579N]

Problem with exc-middle is applying it potentially endless entities. Though the principle can work on not-endless sets, like your example with a teacher and a class.

[@AtticPhilosophy]

Sometimes we want to apply excluded middle in those cases: e.g. every natural number is either even or not even.

[@vsevolod7850]

@@AtticPhilosophy In intuitionistic logic we are able to prove decidability of certain properties. Once proven, we can use law of excluded middle for them (either this property holds or not). Number being even or not is decidable because for any number we have constructive algorithm to check that. For any statement of the form "n is even or not" we can always tell which of the disjuncts is correct, so we are free to use it. However, your example with square root of two is correct, because property "n is rational or irrational" is undecidable. But I am not sure what are the implications for natural language.

[@johnmcdonagh]

"If it's the first case so like Platonism about mathematics then I guess it makes perfectly good sense to say there is a number even though we don't know what it is. In the Constructive case, the anti-realist case, where we're saying that numbers kind of depend on our thinking activity, then yeah..maybe it doesn't make sense to say that there is this number even though we don't know what it is." I believe there is an implicit mistake here. The formalist approach may be an imperfect description of Platonic truth, that whilst being very powerful, can fail. The Constructivist approach may be a more reliable (though potentially less powerful) tool, precisely because it is more restrictive. This does not preclude a "realist" approach, or a belief in the objective reality of Platonic forms, including mathematical truth. Constructivism does not negate Platonism.

[@AtticPhilosophy]

Constructivism and Platonism are definitely opposing views: the former says numbers are the results of (actual or potential) human mental activity, whereas the latter says numbers exist independently of any mental activity. The realist/constructivist debate is one of the central oppositions in the philosophy of maths.

[@johnmcdonagh]

@@AtticPhilosophy "the former says numbers are the results of (actual or potential) human mental activity" A) "Mental activity" does not preclude being informed by a Platonic realm (link blocked - google image "penrose platonism mental physical"). Did Brouwer ever claim such a thing? B) Belief in Platonism does not insist that we begin with a full and perfect perception of Platonic forms, and does not negate the use of Constructivist principles as a tool. Kurt Goedel was a committed Platonist who saw much value in intuitionism: (links to "Gödel’s Work in Intuitionistic Logic and Arithmetic" is blocking this comment) Constructivism can be a powerful tool and Platonist, objective mathematical forms can also be true. Regardless of anyone's personal beliefs. So while formalism may rely upon a mathematical system that is a flawed model of Platonic truth, Constructivism may be a more reliable, albeit less expressive, tool in the box.

[@AtticPhilosophy]

Here's the thing: constructivists say (e.g.) excluded middle & double negation elimination aren't valid, whereas Platonists say they are. They can't both be right!

[@johnmcdonagh]

@@AtticPhilosophy Actually, Platonism does not prescribe the law of the excluded middle, nor double negation elimination. Platonism is not a formal system of mathematical logic. It is in fact perfectly possible to believe in Platonism without believing that we have so far, or ever can, accurately and fully percieve Platonic idealizations. However, I even see classical mathematics as being compatible with constructivism: A system that utilizes the law of the excluded middle can also be compatible with Constructivism once you accept that it depends upon the context in which each is applied. You could say that value of the law of the excluded middle depends upon the system to which it is applied. It's analagous to developing more and more sophisticated models and deciding which is appropriate to use in different contexts. Constructivism's rejection of the law of the excluded middle (or constructivism itself) should be seen as an ad hoc working hypothesis rather than some kind of universal law. Did Brouwer ever indicate otherwise? Goedel was a firm Platonist, despite defeating Hilbert's formalism. I just had a quick look to see what I could find about Goedel's position on the matter: "each form of constructivism in mathematics already admits (or at least is compatible with) some form of Platonism; and within each meaningful form of constructivism or Platonism there is room for specialized investigations. Thus we arrive at a comprehensive perspective which replaces a major part of the conflicts of views about the same subject matter with choices to specialize in fairly well-defined mathematical domains of one degree of certainty and clarity or another." pp22 A Logical Journey - From Goedel to Philosophy and the following quotation from Goedel: "Without idealizations nothing remains: there would be no mathematics at all, except the part about small numbers. It is arbitrary to stop anywhere along the path of more and more idealizations. We move from intuitionistic to classical mathematics and then to set theory, with decreasing certainty. The increasing degree of uncertainty begins [at the region] between classical mathematics and set theory. Only as mathematics is developed more and more, the overall certainty goes up. The relative degrees remain the same."

[@johnmcdonagh]

If you have nothing more to add, then can you at least tell me where you got that stripey philosopher shirt? Thanks!

[@camerongreen7934]

Classical Logicians do actually care about existential statements having witnessing constants. This is why there are classical inductive proofs and lemmas for existential completeness, that for every sentence in the language of the form “exists x P”, there is a sentence P(a/x) which satisfies it by serving as a witness to it. Without this result, classical first order logic would be unsound.

[@AtticPhilosophy]

That’s true, but the point here is, classical logic allows an existential to be valid without any particular instance being valid, and similarly, it allows a disjunction to be valid without either disjunct being valid. Intuitionistic logic doesn’t.

[@Bunnokazooie]

Loving the essay videos right now. But I was reminded recently of Peirce's law and I'm having some trouble comprehending it. Maybe another video topic down the road? It's unprovable in intuitionistic logic.

[@AtticPhilosophy]

Peirce’s law, ((A → B) → A) → A, is weird. Even though it’s purely implicational, containing just →, it can’t be proved with just →I and →E. that’s why it’s not intuitionistic ally valid. The reason it implies excluded middle goes like this. In intuitionistic logic, although Av~A isn’t valid, ~~(Av~A) is. So from (Av~A)→F, anything can be derived. In particular, Av~A follows from (Av~A)→F. So applying Peirce’s law, with (Av~A) for A and F for B, we can infer Av~A, all with intuitionistic reasoning. A video on this is a great idea, thanks!

[@nikaeloliveira2093]

Hi, I'm brazilian student. Thank U 4 your explication. I just wanted to ask U to put de references on video description or reading suggestions on the subjetc

[@AtticPhilosophy]

Thanks for the suggestion, I’ll do that. I’m away this week, I’ll add some references when I’m back.

[@BelegaerTheGreat]

Well, the Grelling-Nelson Paradox ruins LEM's unanimity.

[@AtticPhilosophy]

I’m not sure intuitionistic logic does any better on this score, because intuitionism’s accept LEM for decidable cases, and also hold that meanings have to be decidable. So if “heterological” is genuinely meaningful, in the intended sense, intuitionism is should accept LEM for cases involving whether a word is heterological. So it’s a problem for both or neither.

[@idiomaxiom]

Is the square root of -2 rational or irrational?

[@AtticPhilosophy]

Complex by definition (so not rational)

[@idiomaxiom]

@AtticPhilosophy exactly, door number 3.

[@Pitometsu]

Isn't your example with a mirror -- an instance of abduction, more related to epistemology and the scientific method (some statistics maybe as well)? And the formal logic is about deduction only, so it's kinda not correlated, isn't it?

[@AtticPhilosophy]

Maybe. The issue being discussed here isn't formal logic per se, but how we justify philosophically the principles we accept or reject. Specifically, intuitionists say: you're not allowed to assert an existential ExFx unless you can assert Fx of some specific x. The example was intended to show that it's sometimes meaningful to assert ExFx without any specific x in mind.

[@Pitometsu]

@@AtticPhilosophy thank you for your content, it gives a deep intuition about the way how to perceive logics.

[@lukamiler5824]

I can't help but struggle with the reasoning behind the intuitionist point of view. The non-constructive mathematics proof you gave is based on the fact that a number is either rational or irrational, which is true by definition as irrational numbers are defined as not rational. How can the proof for sqrt(2)^sqrt(2) not be a rational number then? Regardless of our ability to produce the result, the number can not be not rational, so therefore it must be rational.

[@AtticPhilosophy]

You use the premise that every number is either F or not-F, ie law of excluded middle, which is precisely what intuitionistic logic rejects.

[@DustinRodriguez1_0]

This seems extremely problematic (intuitionistic logic I mean). How could they possibly ever even begin an argument? They can't assume anything, because that would violate their principle of needing to construct everything. They can't use conditionals, because consistency would require them to bail out at the word "if" in preference of stating beforehand what is true. They'd have to remain mum on whether there are infinite prime numbers even though the proof is simple. If they "prove" with intuitionistic "logic" that a statement is true... I assume they then are required to separately prove that its negation is false? Assuming truth implies falsehood of the negation would violate their dislike of double negation. How do they deal with a situation in which they have proven something true, but are incapable of proving that its negation is not also true? Or do they simply allow that a thing can be both true and false? What is their meaning of 'true' and 'false' then? When a person dedicated to guiding their life with intuitionistic logic wakes in the morning, how can they determine that they need to eat and consume water in order to preserve and extend their life? Sure those who starve and die of dehydration die, but it doesn't seem like they could extrapolate from that (or any degree of reading about biochemistry or nutrition, etc) that they would be required to eat and drink simply because they are human. It might seem absurd to consider the situation, but logic is used by human beings to determine life and death situations every day. Considering the consequence of consistently adopting a different standard of logic might not do anything to prove or disprove its validity, but it does at least reveal who is taking their claimed standards of proof seriously.

[@AtticPhilosophy]

It’s definitely not that bad! For implications, ‘if then’, you assume A and see if you can reason to B. If you can, you can assert ‘if A then B’. You can still assume whatever you like, as usual in logic. Intuitionistic reasoning is just like classical, but without double negation elimination, positive reductio, and excluded middle.

[@kgullion]

Both the car mirror and the classroom examples strike me as odd. Using the classroom example, we assert that the teacher was hit with the sweet. We can also deduce that if a student threw the sweet than the sweet was thrown by one of the students. We cannot use that to then say that a student must have thrown the sweet. While it's probable a student threw the sweet, it's not necessarily true. By asserting the disjunction you are asserting that you have accounted for every possible disjunct. This is a presupposition on the teachers part, not a logical deduction. A similar argument could be made for the car mirror, you even discount the perfectly good possibility that it could be an "act of god" in the video.

[@AtticPhilosophy]

The issue is whether you have *evidence* which warrants your assertion, 'Someone threw a sweet at me'. Since sweets generally don't fly on their own, I'd say you do. If you don't like the example, pick another one: you find your car smashed up, with graffiti on it, "I did this hahaha". Pretty clear you have evidence that someone did it, but still, you can't say who.

[@kgullion]

@@AtticPhilosophy Any model of reality seems to necessarily be incomplete. The sweet may have been thrown through an open window and not by a student in the disjunction. A trash bin blowing down the street may have broken your mirror and not a person. The graffiti corner cases would be even more outlandish but still potentially there. It seems that, for it to be useful, a standard of evidence must be chosen that excludes the outlandish/unknowable. The intentional vagueness of truth in intuitionism seems to acknowledge that limitation by saying that we cannot know the actual truth of a statement without a witness. Great videos on a fascinating subject, just something that struck me as an odd.

[@markuspfeifer8473]

Classical logic can be used to deduce that a crime has been committed. Intuitionist logic must be used to find out who did it. Usually, you do the rather cheap classical inference to justify the expensive constructive investigation.

[@AtticPhilosophy]

We’ll anything you can prove in intuitionistic logic, you can also prove (in the same way) in classical logic. Constructive proofs are fine in classical logic, it just doesn’t require them.

[@markuspfeifer8473]

@@AtticPhilosophy Sure, but it doesn’t work the other way, and often, classical proofs are simply not good enough. If you use non-constructive methods to establish that something important exists, that’s often just a starting point to find a way to actually construct it.

[@patrickwithee7625]

Isn’t the root(2) example a poor one for intuitionism since, by the definition of a ratio, it is already a theorem that a number is rational or irrational? Nothing else in the proof is non-constructive if we already have this instance of the law of the excluded middle, even if we were to reject it as a general principle.

[@AtticPhilosophy]

To show a number is irrational constructively, you need a proof that it can't be expressed as a fraction. But we can't assume that such a proof exists for all irrational numbers. The 'rational or irrational' theorem you mention uses classical reasoning.

[@patrickwithee7625]

@@AtticPhilosophy but that's just the *definition* of a rational number. It seems perfectly obvious without any reasoning other than reading the definitions of 'ratio' and 'integer' that a number has to be irrational or not.

[@AtticPhilosophy]

@@patrickwithee7625 maybe, but that's not a constructive proof! To assert constructively that x is rational, you need to construct x and prove its identity to a fraction. But the theory of integers with multiplication/division isn't decidable. So there's no constructively-acceptable way to assert that every number is rational or not.

[@patrickwithee7625]

@@AtticPhilosophy there are constructively acceptable ways of listing all and only the Rationals. As such, you at least *in principle* have a way of excluding any number not identical to a member of that list. This is because a number is either rational or irrational.

[@AtticPhilosophy]

@@patrickwithee7625 To prove identity or nonidentity, you need to use basic arithmetic: the theory of + and x on rationals. But that theory is undecidable. So you have no guarantee of a proof, for each n, whether n is rational.

[@IterativeTheoryRocks]

I disagree about the chalk. Perhaps a book fell on a desk and propelled the chalk towards the teacher. The teacher is assuming a complete set of possibilities. Ie one of the pupils. But without a constructive proof, he can’t know.

[@IterativeTheoryRocks]

Love the video 👍

[@AtticPhilosophy]

OK, if you think that, switch the example slightly: "something caused the chalk to hit me". You know that, but you can't say what caused it.

[@neopalm2050]

I'd like to bring up something I'll call "coconstructive" proof/reasoning/logic or "cointuitionistic" logic. You might not find any literature using these names since it's something I made semi-independently. The idea is that you use mostly classical logic, but reject that A∧¬A -> ⊥. (Instead of ⊤ -> A∨¬A.) You still keep that ⊥ -> A for any proposition A and that A->B is equivalent to ¬B->¬A. What changes is that ¬A can no longer be thought of as shorthand for A->⊥. It is instead shorthand for ⊤-/>A*. Intuitionistic logic primarily focuses on showing things are true and that implications are valid and hyperfocuses on giving examples to disjunctions and existential quantifiers. Cointuitionistic logic is the opposite. Instead, it focuses on showing things are false and showing that anti-implications are invalid and hyperfocuses of giving counterexamples to conjunctions and universal quantifiers. Instead of gathering information to put on the left of the turnstile in a conjunction and making the goal on the right simpler (and hopefully ⊤ or something you know), it will instead gather information on the right of the turnstyle in a disjunction to make the goal on the left simpler (and hopefully ⊥ or something you know). *The -/> symbol is similar to the -> symbol. A⊢B can be turned into both ⊤⊢A->B and A-/>B⊢⊥. The idea behind how you use it is (remember, we're aiming to show absurdity) "if B is wrong then A is wrong (but otherwise we're not saying anything so default to falsum, the disjunctive identity)." Classically, A-/>B is equivalent to ¬(A->B). Warning: I haven't thought about this enough to be sure everything I just said is true. I'm pretty certain the logic exists and can be used but the specifics aren't something I've figured out yet.

[@AtticPhilosophy]

Very nice thought! Here's a very quick thought: would the following models be appropriate? We take Kripke models with an 'anti-heredity' condition: if Rsu and p in Vu then p in Vs. (So in a tree, going up from the root, we lose information.) Then define: s |= A-/> B iff for some u: s |= A & not s |= B (So:) s |= ~A iff for some u: not s |= A Then Av~A is valid (true at every root) but A&~A doesn't entail arbitrary B: take the 2-state model with A at the root but not at the top state, with B at neither state. The root verifies A&~A but not B. Moreover, A-/> B |= ⊥ iff never Very nice thought! Here's a very quick thought: would the following models be appropriate? We take Kripke models with an 'anti-heredity' condition: if Rsu and p in Vu then p in Vs. (So in a tree, going up from the root, we lose information.) Then define: s |= A-/> B iff for some u: s |= A & not s |= B (So:) s |= ~A iff for some u: not s |= A Then Av~A is valid (true at every root) but A&~A doesn't entail arbitrary B: take the 2-state model with A at the root but not at the top state, with B at neither state. The root verifies A&~A but not B. Moreover, we get (the semantic version of) your deduction theorem for A-/> B: A-/> B |= ⊥ iff never s |= A-/> B iff (s |= A implies s |= B) iff A |= B. So maybe that's a semantic way to understand this logic? Good luck with it!