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 ⊤ means "true". Mnemonic: it looks like a capital "T" for True.
It is always true, so we can prove it without any work.
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, when the ∀ and ∃ blocks quantify over ℝ₊, they require or supply a proof of positivity along with the real number, on a port of its own.
Recall that 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 enhance the algebra block to automatically deal with absolute values.
Thus, there's now 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 enhanced algebra 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 𝕊.)
The algebra block doesn't know anything about ω other than what you put into it.
For instance, it's true that 0<ω, but the algebra block doesn't know that unless you get it from ℝ<ω and wire it into the algebra block.
We say a surreal number is "infinitesimal" if its absolute value is less than all positive real numbers.
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.
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 and outputs of an algebra block never determine each other, so if you ever connect the output of one algebra block to the input of another algebra block I'll be stuck.
(This is true even if the output of the first algebra block is also connected somewhere else that gives it a label; I can be kind of dense sometimes.)
To help me out, you can 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.
After placing a label block, you can double-click on it to change the label.
With algebra blocks, you can also avoid this issue entirely by never attaching the output of one algebra block to the input of another.
There's no limit on the "amount of algebra" that can be done by one algebra block, so you can just attach all the inputs of the first block directly to the second instead of using an "intermediate result".
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 ¬.
(In Disjunction World I was willing to prove disequalities for you, but now that you know about ¬, it's your job!)
The only kind of disequalities the algebra block can prove automatically now 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 natural numbers are the non-negative integers.
I will let you use a natural number when I expect an integer, and the algebra block knows that every integer thereby obtained is non-negative.
To use an integer where I expect a natural number, you have to give me a proof that it is non-negative.
The ℤ→ℕ block converts an integer x together with a proof of x≥0 to a natural number that is equal to x.
We write ∀x<n and ∃x<n to quantify over the natural numbers less than n.
When the ∀ and ∃ blocks quantify in this way, they require or supply a proof that x<n along with the natural number x, on a port of its own.
Although the notation ∀x<n doesn't explicitly indicate it, remember that it assumes x is a natural number, and hence in particular non-negative.
Another essential fact is that every natural number is either zero or a successor.
We can't prove this with just algebra and logic; we need a new block.
Rather than state the axiom as an ∨ and require a separate case split, this block directly breaks the proof into cases based on whether the number is zero or a successor.
In the second case, we get a new natural number variable representing the predecessor.
The main part of the induction property is a rule similar to "prove ∀" for statements about all natural numbers, except that we also get to assume the statement we want is already known to be true about all smaller natural numbers.
This assumption is called the inductive hypothesis.
Phrased in this way, the rule is sometimes called strong induction.
We often combine it with the "use ℕ" rule, splitting the proof into a "base case" and an "inductive step", with the inductive hypothesis being used in the inductive step on the predecessor.
This special case is "weak" or "ordinary" induction.
Induction of all sorts is particularly useful when reasoning about a function that is defined by recursion.
Here we give the defining equations of a recursive function as hypothesized equations.
In some cases, however, we need more of the power of "strong" induction, applying the inductive hypothesis to something other than the immediate predecessor.
Often in this case we have to use the "use ℕ" rule more than once to extract multiple predecessors, leading also to multiple base cases.
A sequence (of real numbers) is a function from natural numbers to real numbers.
We say that a sequence s converges to a limit L if ∀ε∈ℝ₊,∃N∈ℕ,∀n∈ℕ,((N≤n)⇒(∣s(n)−L∣<ε)), and write lim (n↦s(n)) = L.
The block "Arch" supplies the "Archimedean property": that for any real number there is a natural number greater than it.
Remember also that the enhanced algebra 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.)
We say that a sequence s diverges to infinity if ∀M∈ℝ,∃N∈ℕ,∀n∈ℕ,((N≤n)⇒(M≤s(n))), and write lim (n↦s(n)) ↗∞.
