In the figure1 (see attachment) we show part of the proof of the theorem 2 + 2 = 4, called 2p2e4 in the database. We will show how we arrived at proof step 2, which is an intermediate result stating that (2 + 2) = (2 + (1 + 1)). (This figure is from an older version of this site that didn't show indentation levels, and it is less cluttered for the purpose of this tutorial. The indentation levels and the little colored numbers can make a higher-level view of the proof easier to grasp.)
(1) Look at Step 2 of the proof. In the Ref column, we see that it references a previously proved theorem, opreq2i. The theorem opreq2i requires a hypothesis, and in the Hyp column of Step 2 we indicate that Step 1 will satisfy (match) this hypothesis.
(2) We make substitutions into the variables of the hypothesis of opreq2i so that it matches the Expression shown for Step 1. To achieve this, we substitute the expression "2" for variable and the expression "(1 + 1)" for variable . The middle symbol in the hypothesis of opreq2i is "=", which is a constant, and we are not allowed to substitute anything for a constant. Constants must match exactly.
Variables are always colored, and constants are always black (except the gray turnstile , which you may ignore). This makes them easy to recognize. The variables in our database have 3 possible colors, blue, red, and purple, representing wffs, sets, and classes respectively. Don't worry about what these terms mean right now. All variables, regardless of color, follow the same substitution rule. In our example, the purple letters are variables, whereas the symbols "(", ")", "1", "2", "=", and "+" are constants.
In this example, the constants are probably familiar symbols. In other cases they may not be. You should focus only on whether the symbols are variables or constants, not on what they "mean." Your only goal is to determine what substitutions into the variables of the referenced theorem are needed to make the symbol strings match.
(3) In the Expression column of the Assertion box of opreq2i, there are 4 variables, , , , and . Because we have already made substitutions into the hypothesis, variables and have been committed to the assignments "2" and "(1 + 1)" respectively, and we can't change these assignments. However, the new variables and can be assigned to any expression we want (subject to the legal syntax requirement described below). By substituting "2" for and "+" for , we end up with (2 + 2) = (2 + (1 + 1)) that we show in the Expression column for Step 2 of the proof of 2p2e4.
When we first created the proof, why did we choose these particular substitutions for and ? The reason is simple?they make the proof work! But how did we know these particular substitutions should be picked, and not others? That's the hard part?we didn't know, nor did we know that opreq2i should be referenced in the second proof step, nor did we know that Step 1 would have the right expression to match the hypothesis of opreq2i. The choices were made using intelligent guesses, that were then verified to work. This is a skill a mathematician develops with experience. Some of the proofs in our database were discovered by famous mathematicians. The Metamath Proof Explorer recaptures their efforts and shows you in complete detail the proof steps and substitutions already worked out. This allows you to follow a proof even if you are not a mathematician, and be convinced that its conclusion is a consequence of the axioms.
Sometimes a referenced theorem (or axiom or definition) has no hypotheses. In that case we omit (1) and (2) above and immediately proceed to (3). When there are multiple hypotheses, we repeat (1) and (2) for each one.
Or in the simple way use abacus to get yourself satisfied in place of wasting your precious time.
Moderation Team
![[Post New]](/templates/default/images/icon_minipost_new.gif){kind=icon}
![[Up]](/templates/default/images/icon_up.gif "[Up]"){kind=icon}
0
1
![[Thumb - Theorem opreq2i.gif]](/upload/2007/12/15/75d4a3c3a158ddea30d90db978dd2bb0_6633.gif_thumb)
