Suppose you know this, from an earlier level.
Then you can apply it anywhere in the current level.
Each hypothesis of the applied level becomes something you need to prove. But once you do, you get to use the conclusion.
Occasionally, there are levels with blue outlines. These do not need to be solved; they give you facts for free. They're there so they can be used in later levels.
For instance, the above example comes from such a level. It's the main way to prove that two gray wires are equal to each other. Other blue-circled levels include the basic rules of algebra. In general, if you can't prove it in-game, it'll be provided for you.
When proving a theorem, sometimes it helps to prove something else first. We call that a lemma.
Once this feature is unlocked, you can click a gray wire to say "Let's prove this first.".
Be careful; if you try to prove something false, you'll get stuck!
The conjunction a ∧ b is read "a and b". As that suggests, a ∧ b is the statement that a and b are both true.
If you know a, and you know b, you can prove a ∧ b.
If you know a ∧ b, you can prove a and b.
More generally, you can take a conjunction of three propositions, or seven, or umpteen million. Or even zero!
For the conjunction to hold, all of the individual propositions must be true. In the "zero propositions" case, that's trivial, so the conjunction is always true.
The disjunction a ∨ b is read "a or b". It's true whenever a is, or b is, or both.
If you know a, you can prove a ∧ b. Same if you know b.
If you know a ∨ b, there are two cases. Either a holds, or b does. Handle both cases to complete the proof!
Just like conjunctions, you can take a disjunction of any number of propositions.
For the disjunction to hold, at least one of the individual propositions must be true. In the "zero propositions" case, that can't happen, so the disjunction is always false.
Note: When you use a disjunction, you end up with one case for each individual proposition. For a disjunction of zero propositions, that means there's nothing left to do! This is the principle of explosion: if you can prove False, you can prove anything.
The implication a ⇒ b is read "a implies b". It says that if you knew a, you would know b as well.
To show a ⇒ b, you must show that if you knew a, you would be able to prove b.
If you know a ⇒ b, and you know a, you can prove b.
The equation a = b is read "a equals b". It says that a and b represent the same thing.
You can prove that anything equals itself.
If two things are equal, they are interchangeable. Anything that's true about one is true about the other.
If something is not not true, it's true. Obvious, right?
Surprisingly, this fact can't be proven from the other rules of logic! When we allow ourselves to use this rule, we're working in "classical logic"; when we don't, it's "constructive" or "intuitionistic" logic.
There's some interesting intuition here. If I constructively prove a ∨ b, I can always tell you which of a or b is true. But if I prove it classically, I might not know.
The Riemann Hypothesis is either true or false. Which is it? There's a million dollar prize on that!
Classical logic is the standard in mathematics. Yet while sometimes it feels like the most natural thing in the world, other times it feels like an extra axiom thrown in for no good reason. Depends what type of math you're doing, I guess.
It's well known that you can't divide by zero. 1/0 isn't a number.
Unfortunately, I couldn't get that to work in-game. There's nothing stopping you from doing this:
So I allow 1/0 to be a number, but say nothing about which one. All the rules about division stop working if you divide by zero.
This works perfectly fine... in classical logic. Constructively, it allows you to prove (a = b) ∨ (a ≠ b), when you otherwise couldn't. For this reason, division isn't unlocked until you've completed the classical logic levels.