The boxes on the left are assumptions or hypotheses.
The box on the right is the desired conclusion.
Your goal is to connect them with wires so that all the labels match, thereby proving the conclusion.
A dot on the right of a box is an output port.
If I know what the label of the wire coming out of an output port would be, I'll label it in black:
A dot on the left of a box is an input port.
If I know what the label of the wire coming into of an input port must be, I'll label it in red:
Create a wire connection by clicking on an output port and dragging it to an input port:
To view this hint again during this level (or any other hint during the level it was given), click "Show Hint" in the upper-right corner.
You can view the hint for an older level from the "Select Level" screen by clicking on the "i" in the corner of the level when it was given.
Every input port must have a wire connected to it, but you don't have to use every output port.
You can add new boxes to the proof by dragging them from the palette on the left.
If a box has a symbol on the right, it is called a prove rule, and you should connect its output port to something first.
That will give me more information about what its other ports must be.
The output port should be connected to an input port whose label uses the same symbol:
Therefore, if you have an open input port using some symbol, you probably want to add a box that has that symbol on the right.
The symbol ∧ means "and". Mnemonic: it looks like a capital "A" for And, or like a lowercase "n" as in "salt 'n pepper".
You can use a hypothesis, or other intermediate conclusion, as many times as you need to, by connecting multiple wires to its output port.
If a box has a symbol on the
left, it is called a
use rule, and you should connect one of its
input ports to something first.
That will give me more information about what its other ports must be.
The input port should be connected to an output port whose label uses the same symbol:
Therefore, if you have an open output port using some symbol, you may want to add a box that has that symbol on the left.
If you have both input and output ports using symbols, you'll probably want to add both "prove rules" and "use rules", and then try to connect them up in the middle.
When a "use rule" with its symbol on the left has more than one input port, the one you should connect first is the one whose shape involves that symbol:
The symbol ⇒ means "implies", so that P⇒Q means "P implies Q" or equivalently "if P, then Q".
Remember that a "prove rule" with its symbol on the right should have its
output port connected to something using the same symbol:
When a box has a "bracket" like this one, the output coming from the left inside the bracket is a
hypothetical assumption, which can
only be used to derive the corresponding
subgoal on the right of the same bracket.
You can also stretch the bracket by clicking on either side and dragging it out, so that the entire
subproof fits inside.
If a port label involves more than one symbol, the one
outside all the parentheses tells you which kind of box to connect it to first.
The symbol ∨ means "or". Mnemonic: it's the dual of ∧.
This box needs
both its input and output ports connected right away, but only the input port requires a specific symbol; the output port can connect to anything.
When a box has one or more "brackets" like this one, each output coming from the left inside a bracket is a
hypothetical assumption, which can
only be used to derive the corresponding
subgoal on the right of the same bracket.
You can also stretch a box with brackets by clicking on either side and dragging it out, so that the entire
subproofs fit inside.
Remember the output port of this box must be connected right away:
Almost always, this output port should be connected
directly to your current goal: either the overall conclusion, or the subgoal of some bracket that this block is inside.
Don't use the ∨
L or ∨
R blocks too soon and paint yourself into a corner.
Wires can't go in a loop; that's circular reasoning.
Local assumptions also can't "escape" from a bracket; they can only be used to prove the subgoal of that bracket.
However, remember that assumptions you already have can be brought into a bracket from the left, and that assumptions can be used more than once.
The symbol ⇔ means "if and only if". By definition, P⇔Q means (P⇒Q)∧(Q⇒P).
The symbol ⊤ mean "true". Mnemonic: it looks like a capital "T" for True.
The symbol ⊥ means "false" or "a contradiction".
Mnemonic: it's the dual of ⊤.
Since it's impossible for this to be true, if we ever have it as an assumption, we can immediately "close out" the proof (or any subproof) by formally deriving anything.
(Remember that the "algebra" block can also formally derive anything if given contradictory inputs.)
The symbol ∀ means "for all" or "for every".
Menomnic: it's an upside-down "A" for "for all".
To use ∀x∈A,P(x) we give a value for x and can deduce P of that value.
Here A denotes an arbitrary unknown set.
To prove ∀x∈A,P(x) we suppose an arbitrary value for x and prove P of that value.
When you add a box that introduces a new hypothetical value of this sort, you need to name that value with a new variable, which can't be the same as any other variable name.
You can change the name later by double-clicking on the box.
The symbol ∃ means "there exists".
Mnemonic: it's a backwards "E" for "there Exists".
To prove ∃x∈A,P(x) we specify a value of x that satisfies P(x).
Here A denotes an arbitrary unknown set.
When using ∃x∈A,P(x) we get such value of x that satisfies P(x) (and about which nothing else is known).
When adding this block, you have to name that value with a new variable, which can't be the same as any other variable name.
You can change the name later by double-clicking on the box.
For a,b∈ℤ, the notation "a ∣ b" means "a divides b" or "b is divisible by a".
By definition, this is the same as ∃k∈ℤ,(b=k·a).
For a,b,n∈ℤ, the notation "a ≡ b (mod n)" is pronounced as "a is congruent to b mod n".
By definition, this means ∃k∈ℤ,(a−b=k·n).
We write ℝ₊ to mean the set of positive real numbers.
For convenience, we introduce special blocks for quantifiers over ℝ₊ that require or supply both a real number and a proof of positivity.
The system 𝕊 of "surreal numbers" contains all the real numbers, and also "infinite" numbers like ω and "infinitesimal" numbers like 1/ω.
We say a surreal number is "finite" if its absolute value is less than some real number.
For convenience, we introduce here an enhanced algebra block "alg+" which can automatically deal with absolute values.
When "alg+" is available, there's no need to manually break up into cases in order to draw conclusions about absolute values.
But you should continue to write out all the necessary algebra steps on paper!
The "alg+" block can also automatically handle ∧s in its inputs and outputs, and ∨s in its outputs.
In particular, it subsumes the blocks "=∨≠", "?·?=0", and "≤∨>", all of which simply provide "algebraic facts" involving ∨.
Two surreal numbers are "comparable", written "x ∼ y", if their difference is finite.
The system 𝕊 of "surreal numbers" contains all the real numbers, and also "infinite" numbers like ω and "infinitesimal" numbers like 1/ω.
We say a surreal number is "positive infinite" if it is greater than all real numbers, and "negative infinite" if it is less than all real numbers.
The block "ℝ<ω" supplies the fact that any given real number is less than ω, so that ω is indeed positive infinite.
(This fact would be provable if we gave an actual definition of the number system 𝕊.)
We say a surreal number is "infinitesimal" if its absolute value is less than all positive real numbers.
We write ℝ₊ to mean the set of positive real numbers.
For convenience, we introduce special blocks for quantifiers over ℝ₊ that require or supply both a real number and a proof of positivity, and also an enhanced algebra block "alg+" which can automatically deal with absolute values.
When "alg+" is available, there's no need to manually break up into cases in order to draw conclusions about absolute values.
But you should continue to write out all the necessary algebra steps on paper!
The "alg+" block can also automatically handle ∧s in its inputs and outputs, and ∨s in its outputs.
In particular, it subsumes the blocks "=∨≠", "?·?=0", and "≤∨>", all of which simply provide "algebraic facts" involving ∨.
Zero is the only real number that is infinitesimal.
Remember that the algebra block can derive any algebraic conclusion if given impossible algebraic assumptions.
We say a surreal number is "infinite" if it is either positive or negative infinite.
We say two surreal numbers are "infinitely close", written "x≈y", if their difference x−y is infinitesimal.
The symbol ¬ means "not".
Mnemonic: it's like − for negating a number, but instead it negates a statement.
To use a negation, if we know both a statement and its negation, then this part of the proof is impossible, so we can "close it out" by formally deriving anything.
For this block, either input port can be the negated statement, and either one can be connected first:
Any statement at all can be proven by contradiction:
The "alg" (for "algebra") block can prove algebraic equations. If the equation is always true, it doesn't need any inputs.
Multiplication is denoted with a · as on paper, which you get by typing * as in many programming languages.
You cannot write xy as you often do on paper; it must be x·y.
Similarly, squaring is written x² as on paper, which you get by typing x^2, as in many programming languages.
Likewise, typing x^3 yields x³, and so on.
If an equation you want to prove isn't always true, but is true because of some assumptions, you can attach those assumptions as inputs to the algebra block.
You can attach as many assumptions as you need to the input port of the algebra block.
Although it has only one input port, you can attach as many wires as you want to that port.
My method of checking algebraic equations is very general and powerful, but it doesn't produce a human-readable proof.
When writing a proof for human readers, you should show the algebraic calculations.
Therefore, I strongly recommend that whenever you use an algebra block, you also do the algebra yourself on paper.
Remember that whenever you use an algebra block, you should also do the algebra yourself on paper!
Division by zero is never allowed, so if an algebra block needs to do division, be sure you connect it to enough inputs that guarantee anything it needs to divide by is nonzero.
The algebra block can also prove inequalities.
The statement "x≠y" means the same as "¬(x=y)", and is called a disequality.
I can't prove disequalities involving variables automatically; you have to use the rule blocks for ¬.
The only kind of disequalities the algebra block can prove automatically are disequalities between different constants, without any variables involved.
Usually I can guess the label that should go on any wire from the surrounding blocks and wires, if they are connected correctly.
However, the inputs of an algebra block never determine its output, and the output of a "use ¬" block never determines its inputs.
Therefore, if the both inputs of a "use ¬" block come from the outputs of algebra blocks, I have no way to guess what labels should go on those wires.
To help me out, use a "label" block (🏷) in between.
When you place a label block, I will prompt you for a statement, and then both the input and output wires of that block will be labeled with that statement (which must match the ports they are connected to).
After placing a label block, you can double-click on it to change the label.
Label blocks are never required on Adept or Master difficulty, since in that case you are directly labeling all the wires.
If we don't have any "or" statements as hypotheses, we can still do a case split by using some general fact.
For example, the block "=∨≠" gives us access to the fact that any two numbers are either equal or unequal.
(In negation world we'll be able to prove this fact; for now we assume it.)
You have to tell it which numbers to compare by connecting them to its inputs.
In general, blue ports, such as the first two inputs to this box, must be connected to blue wires, which carry values rather than statements.
Blue wires are labeled by the value along with the set it belongs to: x ∈ ℤ means the value x belongs to the set ℤ.
Here are the sets of numbers we'll be using:
| ℕ | The natural numbers: 0,1,2,3,… |
| ℤ | The integers: …,−3,−2,−1,0,1,2,3,… |
| ℚ | The rational numbers: fractions p/q where p,q∈ℤ, q≠0 |
| ℝ | The real numbers: finite or infinite decimals, e.g. π, √2 |
| ℂ | The complex numbers: a+bi where a,b∈ℝ and i²=−1 |
| 𝕊 | The surreal numbers: the real numbers plus "infinite" numbers like ω and "infinitesimal" numbers like 1/ω |
If you need an input to a blue "value" port that isn't just a variable, use the "expr" block.
This will prompt you for an expression; to change the expression later, double-click the block.
You must connect all the variables that occur in your expression to the input port of the expression block.
Warning: do not connect any black "statement" wires to a blue "expr" block!
And do not connect any blue "value" wires to a black "alg" box!
All the inputs to an "alg" box must be
equations (or inequalities), as those are the only things I can do algebra with; I can figure out on my own which variables appear in the equations.
The expression in an "expr" block does not have to involve any variables at all; it can be just a constant.
Once we've proven a certain fact, we can then
use that fact in other proofs without needing to re-prove it.
For example, we introduce a block "?·?=0" that applies the result of the previous level.
If the assumption on one side of a "use ∨" contradicts other facts we know, we can basically ignore that case.
However, since formally the subgoals on both sides must be connected to something, we allow the algebra block to "prove" anything at all if it is given multiple inputs that contradict each other.
Another important disjunctive fact is that numbers are "totally ordered": given any two numbers, one is less than or equal to the other.
The block ≤∨> proves this, in the form (x≤y)∨(x>y), about any two input expressions.
In addition, x≤y is, essentially by definition, the same as (x<y)∨(x=y).
Thus, you can treat it like an ∨ statement, using the same blocks to prove and use it.
One common situation in which we use this property is when reasoning about absolute value, since ∣x∣=x if x≥0 and ∣x∣=−x if x≤0.
(This is basically the definition of absolute value, and applies in any of our ordered number systems ℤ, ℚ, ℝ, 𝕊.)
The algebra block can't deal with absolute values on its own, but if we give it a hypothesis ensuring that one of these conditions holds, then the absolute value simplifies away and the algebra block takes over.
(Remember to also write out all the algebraic proofs on paper yourself, though!)
The block "Arch" supplies the "Archimedean property": that for any real number there is a natural number greater than it.
Remember also that the "alg+" block can automatically prove equations and inequalities involving absolute values.
(Although, as always, you should write out the algebra parts of your proofs explicitly on paper.)
