With the language of the previous chapter in hand, we now turn our attention to a general the notion of formal proof.
No matter how trivial or well known a claimed expression might be, in absence of any other information about the formal system we are considering we have no way of knowing if it is a theorem or not.
Example . The following are well known facts in mathematics, but are not theorems in systems like the circle-dot system, so are indeterminate.
$1+1=2$
$A\subseteq A$
I’m pretty sure that $5$ is prime
Assumptions never require a feedback marker because they are just announcing that we are temporarily pretending it is true so we can determine the consequences if that were the case, not claiming that it actually is true. Once we assume something is valid we then can consider it valid as long as that assumption is in effect (until the end of the document, proof, subproof, or theorem that contains it).
Let’s illustrate this with an example.
Example The following document environment has a Subproof environment on line 3, and expressions on lines 1,2,4,5. There are only two different statements in the entire proof $n$ is even and $m$ is odd. The first statement is assumed on line 1, and therefore valid as a claim everywhere after line 1. The second is assumed on line 3(a) inside the Subproof on line 3, and therefore is only valid until the end of that subproof (as seen on line 3.c), but no longer valid after that (as seen on line 5). Notice that the statements on lines 1 and 3.a do not get validity markers because they are assumptions.
For convenience, we can also declare consecutive expressions to all be assumptions by declaring the first one to be an assumption and then chaining them together with meaningful commas. Instead of writing this
Assume $n$ is prime, assume $n$ is odd, and assume $n\in\ZZ$. Then clearly $n$ is odd .
we can write this
Assume $n$ is prime, $n$ is odd, and $n\in\ZZ$. Then clearly $n$ is odd .
Compare the comma colors in the two situations.
It is interesting to notice here that a document like this one
If $5$ is prime then $5$ is prime .
is true about every formal proof system. No matter what system we might be considering, if $5$ is prime is a theorem, then $5$ is prime is a theorem. It is functionally the very thing we mean when we say we assume something.
We would like to know when a claim follows from what has already been said before it in the document, even if what has been said is not yet justified. For this reason, when checking the validity of individual claims, we temporarily treat everything that has been said before it as an assumption.
Example . Notice that earlier indeterminate claims justify later references to themselves as if they were assumptions, but still get a validity marker indicating that they themselves are indeterminate.
$5$ is prime
$5$ is prime
If we know $B\subseteq B$ , then $B\subseteq B$ .
Such claims don’t need to be consecutive.
Gina loves chocolate
$5$ is prime
Oh, by the way Gina loves chocolate .
Having discussed validation involving expressions we now consider environments.
It is useful to be able to talk about the nesting of environments and the expressions they contain.
Definition . Every environment contains a list of zero or more expressions and/or environments called its children. A descendant of an environment is either a child of the environment or a child of a descendant.
The first environment in Example 4.2 has five children. The third child is a Subproof environment which has three children of its own. The Proof itself has eight descendants – seven expressions and one environment.
Proof and Subproof environment are exactly the same as far as validation goes. A Subproof is just a proof environment inside of another Proof environment, so from now on when we refer to a Proof environment it whatever we say also applies to Subproof environments. Proof environments are claims.
A Proof environment that has only claims as children is unnecessary because it will not affect the validity of the proof. It’s like putting extra parentheses around and expression that doesn’t need them, e.g., $((x^2)+(x))$ instead of just $x^2+x$. Such an environment is just claiming that its children are all valid. It will be marked as valid only if all of its children are valid.
Example . The Subproof in Proof A only contains claims, so is extraneous and can be omitted as shown in Proof B.
Proof A.
Gina loves chocolate
$5$ is prime
Gina loves chocolate
$n$ is even
$5$ is prime
$n$ is even
Proof B.
Gina loves chocolate
$5$ is prime
Gina loves chocolate
$n$ is even
$5$ is prime
$n$ is even
There is, however, one particular kind of environment that will be very useful.
Definition . An if-then environment is an environment containing (as children) one or more assumptions (called premises) followed by one or more claims (called conclusions). It asserts that if the premises are valid, so are the conclusions.
A Proof environment whose children are all assumptions has no conclusions, and therefore is meaningless and ignored.
A Premise environment can be thought of as an assumed Proof environment. If it contains only claims, it is equivalent to assuming all of them. The premise in Proof A is an assumption that the claims inside it are valid.
Example . The following two proofs are equivalent.
Proof A.
Gina loves chocolate
$5$ is prime
$5$ is prime
Proof B.
Given Gina loves chocolate
Given $5$ is prime
$5$ is prime
An if-then Premise environment can be thought of as assuming that its conclusions are valid if its premises are. With such an assumption if we assume or can prove that all of its premises are valid, then we can conclude that it’s conclusions are as well.
Example . In addition to earlier statements justifying later ones, an assumed if-then environment and its premises justify its conclusions. Notice that the Premise environment does not have a validation marker because it is an assumption.
Suppose mocha is chocolate. Additionally, suppose we assume that
if mocha is chocolate then Gina loves mocha.
Then we can conclude that Gina loves mocha .
In mathematics we often want to claim or assume infinitely many facts of a certain type. For example, suppose we want to say that any number multiplied by $0$ is equal to zero, i.e., $$0\cdot 0=0,\quad 0\cdot 1=0,\quad 0\cdot 2=0,\quad 0\cdot 3=0,\quad \ldots $$ That’s infinitely many facts, so we can’t list them all. In algebra class we might state all of these facts using a formula like this $$0\cdot n=0$$ where the identifier $n$ can be replaced by any number we like to obtain a valid fact. We cannot, however, replace the other identifiers in that formula ($0, \cdot,$ and $=$) to obtain a valid fact because in algebra those symbols are constants.
Thus, if we would like to use formulas in our proofs we need a way to specify which identifiers are constants.
Definition . Identifiers can be declared to be constants by listing them separated by commas after the word declare. A declared constant is treated as a constant globally throughout the entire document. An identifier in a formula that is not a constant is called a meta-variable.
For convenience, we will assume that identifiers which are strings of digits are automatically declared to be constants (e.g. $0$, $42$, $1234$, etc.)
The Rule and Theorem environments are both formulas. They justify an infinite family of facts obtained by substituting expressions for their metavariables (the identifiers they contain that are not declared to be constants). Proof and Premise environments are not formulas. Thus, the four environments are defined by whether or not they are assumptions and whether or not they are formulas.
| is a formula | is not a formula | |
|---|---|---|
| is an assumption | Rule | Premise |
| is a claim | Theorem | Proof/Subproof |
Thus, we can use Rule environments and Premises to state the assumptions we are making about the formal systems we are considering.
Example . If we make $0\cdot n=0$ a Rule with constants $0,\cdot$, and $=$ we can use it to justify that $0$ times anything equals $0$.
Declare $0,\cdot,$ and $=$ to be constants. Consider the following rule.
Multiplication by Zero. $$0\cdot n= 0$$
Then we know all of the following are valid, $0\cdot n=0$ , $0\cdot m=0$ , $0\cdot 0=0$ , $0\cdot 42=0$ , $0\cdot (x+1)=0$ , $0\cdot n=0$ , and $0\cdot n=0$ . But $0+1=0$ is not valid because $\cdot$ is declared to be a constant, and therefore is not a metavariable that can be replaced with $+$.
Note that Rules and Theorems cannot appear inside of other Rules, Theorems, or Premises.
With our language and reasoning in hand, we are ready to begin proving theorems about our formal systems, and build mathematics from the ground up, starting from scratch. To do so we will specify the rules that our formal systems behave. There are many ways to format the same rules, but we will use two in particular. The first is similar to the style of theorems sometimes used in high school geometry texts.
Definition . A rule is specified in given-conclude style if it is of the form
RuleName
Given
$W_1$
$\vdots$
$W_m$
Conclude
$V_1$
$\vdots$
$V_n$
where $W_1,\ldots,W_m,V_1,\ldots,V_n$ are all claims and RuleName is replaced with the name of the rule. The conclusions $V_1,\ldots,V_n$ are all expressions, but any of the $W_1,\ldots,W_m$ can be an expression or an environment.
In the situation where all of the rule premises are expressions, we can also format our rules more cleanly as a sentence.
Definition . A rule is specified in if-then style if it is of the form
RuleName. If $W_1,\ldots,W_m$ then $V_1,\ldots,V_n$.
where $W_1,\ldots,W_m,V_1,\ldots,V_n$ are all expressions.
Finally, it will be convenient to define one other form of Rule or Theorem.
Definition . A rule or theorem is an equivalence or Iff style if it is of the form
RuleName. $W_1,\ldots,W_m \equiv V_1,\ldots,V_n$.
where $W_1,\ldots,W_m,V_1,\ldots,V_n$ are all expressions. This rule is a compact way to write the two if-then rules
RuleName. If $W_1,\ldots,W_m$ then $V_1,\ldots,V_n$.
RuleName. If $V_1,\ldots,V_n$ then $W_1,\ldots,W_m$.
It will sometimes be convenient to write down an environment without having to use colored boxes. So we define a useful notation for that.
Definition . We write $$(W_1,\ldots,W_m \vdash V_1,\ldots,V_n)$$ for an if-then environment with premises $W_1,\ldots,W_m$ and conclusions $V_1,\ldots,V_n$. Similarly we write $$(W_1,\ldots,W_m \equiv V_1,\ldots,V_n)$$ for an iff environment.
This notation can be nested if any of the $W_1,\ldots,W_m, V_1,\ldots,V_n$ are themselves environments.
It is commonplace in mathematics to write a theorem immediately before its proof, which unfortunately would mean that the proof could be justified by the theorem rather than the other way around. To allow for this, we make the convention that if a Theorem environment occurs immediately before a Proof environment, then it will be treated as if they occur in the reverse order, with the Theorem coming after the Proof.
We have already seen examples of theorems that do not require any proof, because they immediately follow from the meaning of assumptions and if-then environments. Type the following theorems into Lurch, each inside a separate Proof environment (not a Theorem environment), and verify that they all validate correctly.
if $3$ is odd then $3+1$ is not odd,
then $3+1$ is not odd.
if mocha is chocolate then Gina loves mocha.
and assume mocha is chocolate, and Gina loves chocolate. Then Gina loves mocha and Gina loves chocolate.
if $1\lt 2$, and $2\lt 3$ then $1\lt 3$
and
if $1\lt 3$, and $3\lt 4$ then $1\lt 4$
then $1\lt 4$.
$n$ is even $\equiv$ $n+1$ is odd
and
$3\cdot n$ is even $\equiv$ $n$ is even
Then if $n+1$ is odd it follows that $3\cdot n$ is even.
