tl;dr How would you write a blog post containing the proof for "if $m ∈ Z$ is even, then $m^2$ is even", such that it contained all definitions/theorems/proofs which it depends on, all the way back to the "base" definitions/theorems/proofs? If too involved, then how would you at least include enough so it didn't make large logical leaps?
I am looking for basic proofs which I can then translate into a formal DSL, in progress toward making an interactive theorem prover. One such DSL is formal logic notation, but I am working on a custom DSL for writing proofs, which includes a way to write theorems (as formal logical statements in some type of logic or type theory, which I'm still tinkering with), and now I'm trying proofs (as formal transformations of hypotheses to goals I guess, which I'm not totally sure how to formalize into a DSL atm).
One "basic" (i.e. simple, not too involved) proof I found which will help in this process is this:
Theorem: If $m ∈ ℤ$ is even, then $m^2$ is even.
Proof: Suppose $m ∈ ℤ$ is even. By definition of an even integer, there exists $n ∈ ℤ$ such that $m = 2n$.
Thus we get:
$$m^2 = (2n)^2 = 4n^2 = 2(2n^2)$$
and we have $m^2$ is also even.
Where this is the definition of an even integer:
Definition: An integer $∈ℤ$ is even if and only if it is divisible by $2$.
That's not so direct/explicit either. But anyways.
Here's sort of what I've been doing:
theorem "if number is even then square is even" {
let m
implication {
containment(m, Z)
evenness(m)
} => {
let m2 = square(m)
evenness(m2)
}
}
proof {
let m
suppose {
containment(m, Z)
evenness(m)
}
useDefinition("even integer") {
let n
gives {
containment(n, Z)
}
}
}
That's about as far as I've gotten with the proof structure. You don't really need to pay attention to it in detail. My actual DSL is a little more involved and not ready yet, but the result is that I end up with a tree structure for a logical sentence (the theorem as a tree), and soon enough, a tree or list sort of structure for the proof. With these formal data structures, I can have the computer run through the proof (and use the theorem as part of future proofs that get translated, etc.).
My main question -- to help me figure out how to write this -- is what is the formal proof in all its detail of this theorem? By that I mean, assuming "very little" prior knowledge about other definitions or theorems, how would you write the proof? By that I mean, you can use "by definition of even integers" in the proof, but you need to include the definition itself in the final writing so I can then write the formal structure for that definition. Etc., all the way down to the base, whatever it may be. If it is too involved to write it all the way down to the base (like you have to have hundreds of sentences defining what a number is and everything, etc.), then just what are the formal elements of the proof that don't make any large leaps in intuition, so I can have the computer ultimately be able to understand it? Something, anything, more fine-grained than the proof provided above, which the human mind somehow fills in the blanks for.
By that I mean, what is a mechanical proof, or rough approximation of a mechanical proof for this theorem? The one provided makes too many large leaps in intuition for a computer to easily understand (as far as I can tell).
For example, how did they arrive at "there exists $∈ℤ$ such that $=2$" from the definition of an "even integer"? Then how did they jump from that to "$m^2 = (2n)^2 = 4n^2 = 2(2n^2)$"? The "thus we get" throws me off. No, "thus we get". Really, you introduced a bunch of stuff. I am not concerned with the creativity of how this step of the proof was figured out. I am just wanting to see a more fine-grained step-by-step set of instructions for how this proof evolves, and "thus we get" is too far of a leap (for a computer, it seems). Maybe it would be more like (in formal logic notation, Coq, or whatever you would like to use, structured natural language even would work):
- First, introduce "$m^2$" (do we care about including a reason "why" here?)
- Next, substitute($2n$, for $m$), and get "$(2n)^2$"
- Next, distribute exponent, and get "$4n^2$"
- Next, factor out $2$, and get "$2(2n^2)$"
And then they make another big leap by saying "and we have $m^2$ is also even". How do we know that from "$2(2n^2)$"? What are the steps/rules involved in that transformation?
Basically, I would like to see what the proof for this looks like in more intricate details, and if possible, including any necessary definitions or dependent theorems so the proof has all of it's definitional "dependencies" in a self-contained post. If not possible, then as much work as you are willing to show so it doesn't appear to have any implicit logical leaps.
