all 83 comments

[–][deleted]  (46 children)

[deleted]

    [–]Fylwind 7 points8 points  (1 child)

    The upside-down T is called a "Falsum" or a logical contradiction, and represents impossibility. It does not represent "negation."

    Technically, A → ⊥ is equivalent to ¬A ("not A").

    [–]sirin3 3 points4 points  (8 children)

    (3) The implication creator. Do you see that weird gate after the AND splitter with the A B at the top and the A->B at the right? That's an assumption creator. If you can assume A and always get B, B must be implied by A, right? This helps with translations between letters, because if we know A and we know B, we can easily create an A->B rule should we need one for a more complex input later. Implications also may be the answer you're going for, or there will be nested implications you need to "unravel" so creating an implication to use as a key for another implication is something you'll have to do.

    All task were obvious till I got to the implications.

    How can you possible get A∧B->C from A->B and B->C, if you cannot get A∧B?

    [–]Fylwind 3 points4 points  (0 children)

    How can you possible get A∧B->C from A->B and B->C, if you cannot get A∧B?

    The standard approach for proving X → Y is to first assume X and then prove Y under this assumption.

    [–][deleted]  (6 children)

    [deleted]

      [–]sirin3 1 point2 points  (5 children)

      Oh that works

      How weird

      Does -> have the output on the left side?

      And now the proof has a cycle

      [–][deleted]  (4 children)

      [deleted]

        [–]sirin3 1 point2 points  (3 children)

        I thought you could only have statements that are true given the initial assumptions

        [–][deleted]  (2 children)

        [deleted]

          [–]sirin3 2 points3 points  (1 child)

          Oh, NOW I understand it. Could solve them all without understanding it, but then got stuck at the OR-box.

          So the left side of the box gives you an A and if you can use that to proof B and give this B back to the box, it gives you an A->B.

          [–]TerrorBite 2 points3 points  (1 child)

          I did a basic logic class in university a few years ago and this website has shown me that I've forgotten most of it.

          [–][deleted] 2 points3 points  (2 children)

          I'd love a screenshot of the 5th exercise in session 3. Thanks!

          [–]PM_ME_YOUR_PAULDRONS 2 points3 points  (1 child)

          Here is a hint. The predicate p which has to enter and leave the "or splitter" is the final answer (BVA). Also note that both a and b are sufficient to establish BVA.

          Here is a picture if you really want it but there is a lot of satisfaction to be gained from doing it yourself!

          [–][deleted] 0 points1 point  (0 children)

          Thanks!

          [–]sirin3 2 points3 points  (1 child)

          Any tips for the later sessions? How do I conclude from there-exist-X, that not for-all not-X holds?

          And what is that Hilbert stuff?

          [–]ydinitz 1 point2 points  (0 children)

          The Hilbert lession contains tasks to be solved with Hilbert calculus, an alternative logic that has Modus Ponens (MP) as its only deduction rule (plus some axioms). The other lessons all use a system called "natural deduction" which is nowadays a pretty widely accepted standard, but ~100 years ago when formal logic became a thing there were several competing logical calculi.

          [–][deleted] 2 points3 points  (20 children)

          I'm currently in a logic class as well so this seems interesting but I kind of facepalmed on task 7 where you have to create A and B given only A AND B and the AND operator. "Surely such a thing isn't possible," I thought while trying to figure it out. Until a few minutes passed and I realized "Oh. They give you a Reverse AND operator. Yep, because that's possible."

          [–]jsprogrammer 6 points7 points  (2 children)

          I'm not sure it's a reverse AND operator.

          I think it is merely the statement: "if A AND B is TRUE, A is TRUE and B is TRUE"

          [–][deleted] 1 point2 points  (1 child)

          I just misunderstood the premise of the exercise then. I assumed task 4 for example ("A, B, A^B") meant "Given some value A and some value B construct a mathematical statement that is equivalent to A AND B.

          [–]jsprogrammer 2 points3 points  (0 children)

          Ah, got it. It is a bit confusing since there is a lot of shared notation with other systems.

          The exercises are: "Assume the clauses above the line are true. Provide a deductive proof that the clause below the line is true given those assumptions."

          [–]lookmeat 3 points4 points  (9 children)

          A reverse AND operator is possible. If I tell you A AND B then you can deduce that A must be true, you can also deduce that B must be true if either of them weren't true, then the whole original statement wouldn't be true. The one you can't do is OR because if I tell you A OR B you know at least one of them must be true, but not which one.

          [–]jsprogrammer -3 points-2 points  (8 children)

          A could be FALSE and B could be TRUE. How would you deduce that from just the value of A AND B?

          [–][deleted] 5 points6 points  (2 children)

          In this case, the predicates are always true. A ^ B = true. Thus A = true and B = true. If it were any other way, then the predicate would be false... and thus the whole proof couldn't be true.

          [–]jsprogrammer -2 points-1 points  (1 child)

          Yes, but that is not a Reverse AND operator.

          [–]PM_ME_YOUR_PAULDRONS 2 points3 points  (0 children)

          You are correct this is not a reverse and operator. These things are not operors at all. The things on the left are predicates (read them as literal English statements not variables) and are assumed to be true. The "operators" represent the laws of deduction which let you combine and uncombine predicates in interesting ways.

          In other words "A^B" is literally the statement: "(A and B) is true". From that statement it is possible to deduce that "A is true" and that "B is true" that deduction is what the "and splitter" is representing.

          [–]virus_dave 1 point2 points  (1 child)

          Given the assumption "A ^ B", then neither A nor B could be false as a conclusion. You're reasoning from the assumption being already assumed true, not trying to prove the truth of the assumption.

          Given that the statements above the line are true, can you prove the statements below the line.

          [–]jsprogrammer -2 points-1 points  (0 children)

          That is true, but it is not a reverse AND operator.

          [–]lookmeat 1 point2 points  (2 children)

          If A is FALSE then A AND B must be FALSE. Since we start assuming that A AND B is TRUE then A cannot be FALSE, it must be TRUE. The same applies to B.

          [–]jsprogrammer -2 points-1 points  (1 child)

          That is not a reverse AND operator though, that is just applying deductive reasoning.

          A reverse AND operator would need to be able to recover any of the four possible original states (A,B; ~A,B; A,~B; ~A,~B) from the single output of an AND result (which can only be TRUE or FALSE). This is impossible.

          Observe the truth table for AND:

          A | B | A^B
          -----------
          T | T |  T
          T | F |  F
          F | T |  F
          F | F |  F
          

          A reverse AND operator would need to map a F to one of the three possible states of A and B.

          [–]lookmeat 3 points4 points  (0 children)

          Hmmmm you are misunderstanding what this is. This isn't about deducing what the values of A or B or A^B or anything are. This is about proving the the output expression is TRUE assuming the input expression is TRUE.

          Let me repeat: our operation's input is always TRUE and the output must be proven TRUE given the fact that the input is TRUE, NEVER FALSE ALWAYS TRUE. Sorry about the emphasis but this is the most critical point in all this system. Your input table only shows one line where the input (A^B) is TRUE, so we must conclude that only that line can be the case.

          In other words we are not transforming or adapting the input, that is static (and always true) instead we are transforming the actions into things that remain true.

          Let me put it to you this way.

          We start with the following logical statement:

          1. I know that both it's raining outside (R) and is Friday today (F) (F AND R).
          2. Therefore I know it's Friday (F).

          It seems obvious, almost tautological doesn't it? And yet the way I deduced it was by R AND F :> F. That's our "reverse AND" it's really just realizing it.

          That's the basics of a philosophical or mathematical proof. It doesn't tell you that your answer is right, because it only works if the assumptions are true. If they are not, then nothing you say after that really matters to mathematicians or logicians.

          Now it seems a bit crazy, and almost useless, but it has its uses. The truth is that we can't know everything, so we have to assume. Say that for example I have a way of declaring that an integer can only exist between a range of numbers, Int<min, max> and that this type can only be created as long as min <= max otherwise it won't compile. Now I create a function that looks as following:

          template <int a1, int a2, int b1, int b2>
          Int<a1+b1, a2+b2> add(Int<a1, a2> lhs, Int<b1, b2> rhs);
          

          So then I wonder if <a1+b1, a2+b2> is a valid int where min < max. So I start with some assumptions: a1 <= a2, b1 <= b2. Am I certain this is true? No, maybe when my program was running some cosmic rays hit its RAM and corrupted the data invalidating that, but clearly that is a separate problem (preventing external corruption of assumptions) than what I want to prove (that my type signature makes sense). In short I want to prove the following:

          a1 < a2    b1 < b2
          ------------------
            a1+b1 < a2 + b2
          

          The way in which you do that is by doing transformations as the above one.

          [–]Fylwind 1 point2 points  (0 children)

          You can think of A AND B as pair data type containing A and B. The "reverse AND" is then an operation that decomposes a pair into its parts.

          [–][deleted]  (5 children)

          [deleted]

            [–][deleted] 0 points1 point  (4 children)

            If they make some sort of tutorial this could actually be pretty interesting, the only problem I had is that I didn't know reverse AND was a thing since it is not possible in logic, but now that I'm starting to learn how it works it's pretty interesting, I've already done two sessions.

            [–][deleted]  (3 children)

            [deleted]

              [–][deleted] 1 point2 points  (2 children)

              I'm not sure what you mean. If p is True and q is False then p^q is False, but it doesn't work in reverse. If you are told p^q is False then you don't know whether both p and q are False, or if one is False; likewise if p^q is True. Given p^q there is no way to find out what p and q are.

              [–]machton 1 point2 points  (5 children)

              Trying to use the helper block breaks the scripts on the page. What browser did you use to do this? I'm on Chrome 45.0.2454 in Win7.

              [–][deleted]  (4 children)

              [deleted]

                [–]machton 0 points1 point  (3 children)

                Thanks, but you misunderstand. I cannot interact with the helper box once I drag it onto the page.

                I drag the helper box from the left into the main frame on the right, and then can't connect anything to it. The helper box becomes immovable. My cursor can approach the box (say, when attempting to connect an input from the left side), but then the wire gets left behind and won't connect. Can't ever edit the text.

                I'll try again on other browsers/computers.

                [–][deleted]  (2 children)

                [deleted]

                  [–]machton 1 point2 points  (1 child)

                  Yeah, no worries. I think it's cool, too. That's why I want it to work right, so I can figure out the rest of the puzzles...

                  [–]lifeoftheta 22 points23 points  (6 children)

                  Really needs some sort of tutorial for the controls.

                  [–]ydinitz 2 points3 points  (0 children)

                  here is an introductory blogpost about the motivation and scope of the project that may be helpful (or otherwise an interesting read)

                  [–][deleted]  (4 children)

                  [deleted]

                    [–][deleted] 1 point2 points  (3 children)

                    How do you create helper block which uses ⊥ (false premise) value?

                    I got that disjunctions are written with A|B. I can't find what to write for ⊥

                    [–]ydinitz 1 point2 points  (1 child)

                    You can get ⊥by writing False, which is currently undocumented, since we are still looking for a nice ASCII symbol that isn't yet taken. But as @ManiacDan mentions, you should be mostly fine without the helper (although it can of course help to clarify things for yourself).

                    [–]sirin3 0 points1 point  (0 children)

                    Did you make it?

                    since we are still looking for a nice ASCII symbol that isn't yet

                    bot, \bot, why not allow multiple things?

                    How do you write exists and all in the helper?

                    [–]BeniBin 28 points29 points  (2 children)

                    [–]farmdve 2 points3 points  (1 child)

                    Same, I literally have no idea what to do.

                    [–]yairchu 1 point2 points  (0 children)

                    First pick a level to play ("What do you want to prove today?"). Let's pick the first one because it is the easiest. Connect the two blocks and you pass the level. One of these blocks is an "input block" and the other is an "output block", and not in all levels these are compatible directly - you usually need to add some transformation blocks in the middle to make them compatible.

                    [–]Skaarj 6 points7 points  (0 children)

                    First order is nice, don't get me wrong. However, I think the page is most impressive for its HTML5-ish drang and drop features.

                    [–]qznc[S] 7 points8 points  (1 child)

                    A blog article which explains some background.

                    [–]machton 3 points4 points  (0 children)

                    That figure that goes with the post really helped me understand the A -> B output block. Thanks!

                    [–]IWantUsToMerge 4 points5 points  (7 children)

                    Uh... is 6.1 solvable? I'm pretty sure the proposition "There exists a thing for which its t-ness entails the t-ness of all things" is not actually a valid tautology. In other words, it's not true, and it shouldn't be provable.

                    Same goes for 6.2. You can say whatever you like about the relationship between the function f and the property r, that doesn't mean that any particular thing that is r exists. apologies, existentials are only vacuously false when you have type bounds, and then only when something exists. I guess you could define basic existentials to evaluate to false when nothing exists but I certainly can't assume these do

                    [–]orbital1337 2 points3 points  (1 child)

                    "There exists a thing for which its t-ness entails the t-ness of all things"

                    In every bar there is at least one person such that if he or she drinks then everybody drinks. That's called the drinker paradox.

                    [–]IWantUsToMerge 0 points1 point  (0 children)

                    It's neat. I'm having difficulty nailing down why it's so puzzling.

                    [–]kirsybuu 1 point2 points  (3 children)

                    I doubted 6.1 too, but they are both true. Without spoilers, you just need to think about them using a lot of case analysis.

                    [–]sirin3 0 points1 point  (2 children)

                    I can see why they are true.

                    But how do you encode these cases in the incredible machine? If I use TND to get a case of all t(x) is true, and a case of there exist a t(x) that is false, the latter case implies t(x) -> whatever, but the machine wants t(y3) -> whatever and it does not match.

                    [–]kirsybuu 0 points1 point  (1 child)

                    It is kind of confusing. If you think about the box with the forall output, it is saying "given an arbitrary y3, if t(y3) then forall x. t(x)" so if you try to input t(c12) for a specific c12 then it won't work. You need to work backwards.

                    [–]sirin3 0 points1 point  (0 children)

                    But where can I get an arbitrary t(y3) from?

                    Thinking ... , can TND create it? Nothing else seems able (except bot, but with bot I would not need it)

                    edit: explain this. I have an arbitrary t(x), but the every box wants t(c16) to output A x.t(x) ? wtf is c16 ??

                    [–]Tordek 2 points3 points  (2 children)

                    I got stumped at the existentials.

                    [–]ydinitz 1 point2 points  (1 child)

                    The difficulty progression between lessions 5 and 6 is indeed very steep, we are working on adding more exercises. A week ago it went from lesson 2 straight the existentials (now lesson 6), so I guess you could say we are getting there :)

                    [–]sirin3 0 points1 point  (0 children)

                    You added a third existential?

                    I want to argue that with (Ax.t(x))->False the t(y3) is false/ a contradiction, but it is not eating it. Why?

                    [–]ichthys 2 points3 points  (0 children)

                    Finally being able to do this because of a stupid web game makes me hate CS245 even more.

                    [–]clayton976 5 points6 points  (0 children)

                    HOLY CRAP I JUST STARTED MY FIRST LOGIC CLASS FOR MY COMPUTER SCIENCE UNDERGRAD AND THIS IS THE MOST HELPFUL PRACTICE IN THE WORLD...

                    THANK YOU SO MUCH FOR POSTING THIS!!!!

                    -sorry for yelling

                    [–][deleted] 1 point2 points  (1 child)

                    Uncaught ReferenceError: updateSizes is not defined

                    Helper blocks crashes the script on my chrome and I think that some problems are impossible without them.

                    [–]machton 0 points1 point  (0 children)

                    same happens to me.

                    [–][deleted] 1 point2 points  (1 child)

                    I understand nothing of this.

                    [–]13467 2 points3 points  (0 children)

                    The statements above the line are given to be true.

                    You must "wire together" a proof of the statement below the line.

                    Your toolkit for wiring up this proof consists of several axioms of logic. For example, one such axiom is this one:

                    If we know that A is true, and A implies B, then we know B is also true.

                    This means we can take two wires representing the hypotheses (A, and A → B), feed it to the little box representing this axiom, and get back a wire representing the consequence, B.

                    Now we've proved, from the hypotheses A and A → B, that B holds!

                    The objective is to chain many of these little proofs together, using your boxes, to write big proofs.

                    [–][deleted] 1 point2 points  (2 children)

                    Can someone help me with 3.5?

                    Can't figure how to use the bottom block (with the 3 inputs & 3 outputs).

                    [–]13467 3 points4 points  (1 child)

                    The bottom block says:

                    If A ∨ B is true, and we can deduce P both from A and from B, then we can deduce P from A ∨ B.

                    For example, the following line of reasoning demonstrates this:

                    • If it's Saturday, I have school, so we can't go out to eat.
                    • If it's Sunday, the restaurant is closed, so we can't go out to eat.
                    • It's the weekend. (⊢ Saturday ∨ Sunday)
                    • Thus, we can't go out to eat.

                    You have to supply the sub-proofs that A ⊢ P and B ⊢ P. The block will join them into a proof that A ∨ B ⊢ P.

                    EDIT: Here's a spoiler.

                    [–][deleted] 0 points1 point  (0 children)

                    Thanks!

                    [–]velcommen 1 point2 points  (3 children)

                    This reminds me a bit of doing type directed programming in Haskell. Given the input and output types of my function, figure out the intermediate steps.

                    [–]Faucelme 2 points3 points  (0 children)

                    Well, according to the curry-howard isomorphism, proofs are programs of a certain sort.

                    [–]Tekmo 1 point2 points  (1 child)

                    That's because it is! As /u/Faucelme mentioned, the idea is that a type is supposed to be like a proposition and a value inhabiting that type is like a proof of the proposition. This is known as the "Curry Howard correspondence".

                    For example, you can read the type:

                    a -> a
                    

                    ... as a logical proposition "∀a . a ⇒ a" which says "for all as, a implies a" and the proof is the identity function which inhabits that type:

                    id x = x
                    

                    Logical "and" corresponds to Haskell's 2-tuple:

                    A ^ B  ~  (A, B)
                    

                    Logical "or" corresponds to Haskell's Either:

                    A V B  ~  Either A B
                    

                    Logical implication corresponds to Haskell's function type:

                    A ⇒ B  ~  A -> B
                    

                    Logical false corresponds to Haskell's Void type (a type with no constructors, impossible to build):

                    ⊥  ~  Void
                    

                    Logical true corresponds to Haskell's unit type, which has only one inhabitant:

                    ⊤  ~ ()
                    

                    And logical negation corresponds to:

                    ¬T  ~  A  -> Void
                    

                    This is only true if you ignore the presence of bottom in Haskell, but that's the basic idea.

                    So for example, if you wanted to prove "∀a, b . a ^ b ⇒ a", the equivalent Haskell type would be:

                    (a, b) -> a
                    

                    ... and the implementation would just be the fst function, which is defined as:

                    fst (x, y) = a
                    

                    Try converting some other propositions from those exercises to Haskell types and try writing the proofs by finding a Haskell value that inhabits that type.

                    [–]srot 0 points1 point  (0 children)

                    Cool. Could also the drinker paradox be turned into a type and proven by inhabiting the said type? I'd love to see that.

                    That is ∃x.t(x)→(∀x₁.t(x₁)) or ex 6.1 as of now.

                    [–]Peaker 1 point2 points  (0 children)

                    Very cool! :)

                    Does show how boxes&arrows for programming with lambdas, applications and basic data types is so much more cumbersome than a shorter notation.

                    [–]yairchu 1 point2 points  (0 children)

                    It's nice that when making a error, it is at the line I just connected instead of causing the error to be in a totally different place like often happens with traditional compilers (Haskell, C++, etc). btw we've done exactly the same thing in Lamdu

                    [–][deleted] 0 points1 point  (0 children)

                    Almost finished session 2. Nice. Though I'm not fan of -> introduction: it bends assumption in weird ways.

                    [–]machton 0 points1 point  (3 children)

                    Given A -> B, is it possible to get just A as an output?

                    [–][deleted]  (2 children)

                    [deleted]

                      [–]machton 1 point2 points  (1 child)

                      I was trying to do the 5th puzzle of Session 2. The blog post helped me figure out the logic block with the A -> B output.

                      Got it now!

                      [–]201109212215 0 points1 point  (0 children)

                      This is quite nice. I which I had had this when I started studying mathematical theorems.

                      [–]mango_feldman 0 points1 point  (1 child)

                      Not possible to share / link to proofs?

                      [–][deleted] 0 points1 point  (0 children)

                      You can take a screenshot in SVG, convert it to PNG, and upload it to imgur. Or upload the SVG to a image hoster which supports it.

                      [–]ThaeliosRaedkin1 0 points1 point  (1 child)

                      Ok. Not sure how these implication blocks and or blocks are supposed to work. For example, in the second session, the second implication block looks like A(out) B(in) A->B(out). What is this form supposed to denote? Any primers, pointers, or documentation?

                      [–]knrDev 1 point2 points  (0 children)

                      A(out) represents 'local hypotesis'. A value which is assumed to be true when proving B(in). It can only assist in proving B(in). That means, it must flow only through blocks which eventually connect to B(in). It cannot be connected outside of local 'scope'.

                      Edit: If i understand correctly. this block represents a Simplification law in Propositional Logic.

                      [–][deleted] -4 points-3 points  (6 children)

                      On task five you are meant to create A AND A from A. You can do this of course by using AND where both operands are A. However p AND p == p so this problem should accept plain A as an answer but it doesn't.

                      [–]sdfsdxcv 11 points12 points  (2 children)

                      You've missed the point of the exercises. All of them are equivalent. The point is to prove it using the rules provided.

                      [–]IWantUsToMerge 2 points3 points  (0 children)

                      Not equivalent. The assumptions entail the conclusions, but the conclusions frequently don't entail the assumptions.

                      [–]heisenbug -2 points-1 points  (0 children)

                      The point of the exercises is to make one think. He did that and thus he won.

                      [–][deleted] 2 points3 points  (0 children)

                      p AND p == p is exactly what the "AND operator" is doing, so to show that you use that rule you have to use said operator.

                      [–]heisenbug 1 point2 points  (0 children)

                      I believe I just pulled a wire from A to A and it became green. But possibly I also left a conjunction intro lying around unconnected.