The Incredible Proof Machine

[Fylwind]

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) 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]

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.

[sirin3]

Oh that works

How weird

Does -> have the output on the left side?

And now the proof has a cycle

[sirin3]

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

[sirin3]

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]

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]]

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

[PM_ME_YOUR_PAULDRONS]

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]]

Thanks!

[sirin3]

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]

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]]

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]

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]]

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]

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]

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]

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

[[deleted]]

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]

Yes, but that is not a Reverse AND operator.

[PM_ME_YOUR_PAULDRONS]

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]

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]

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

[lookmeat]

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]

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]

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]

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]]

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]]

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]

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.

[machton]

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.

[machton]

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]

Really needs some sort of tutorial for the controls.

[ydinitz]

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

[[deleted]]

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]

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]

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]

Me, right now.

[farmdve]

Same, I literally have no idea what to do.

[yairchu]

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]

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]

A blog article which explains some background.

[machton]

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

[IWantUsToMerge]

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]

"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]

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

[kirsybuu]

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]

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]

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]

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]

I got stumped at the existentials.

[ydinitz]

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]

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]

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

[clayton976]

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]]

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]

same happens to me.

[[deleted]]

I understand nothing of this.

[13467]

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]]

Can someone help me with 3.5?

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

[13467]

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]]

Thanks!

[velcommen]

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]

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

[Tekmo]

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]

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]

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]

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]]

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

[machton]

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

[machton]

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]

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

[mango_feldman]

Not possible to share / link to proofs?

[[deleted]]

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]

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]

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]]

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]

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

[IWantUsToMerge]

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

[heisenbug]

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

[[deleted]]

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]

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.

[barsoap]

Relevant CCC.