Proof

Subsitution

Here we will do a simple example of a proof. Given two definitions of ONE and TWO we want to prove TWO=succ(succ(zero)). Definitions have automatic proofs created for them because they are try by definition. The proof is as follows. We create a function f such that f(a) matches one of our previous proofs. Then we combine that we a proof of a=b. And we get the proof f(b). This is another way of saying we are making a subtitution of b with a in the proof f(a). The function f just tells us where we are doing the substitution.

proof1:F(a) → proof2:a=b → proof3:F(b)

With proof3 = SUBST( F, proof1, proof2 )
A longer proof:

Logic

As before on the logic page we can show that if we have the definitions of ONE and TWO then we can form the pair of proofs:

Reflection

An equation like 2=2 is obviously true. There is a proof defined for these cases called rfl. Let us make the proof for the proposition 2=2 or False.

Classical Logic - ForAll

Let us prove Socrates is mortal. This is proved using the intro function which transforms the forall into the special case

Exists

To prove the statement that there exists something of a particular type. We just need to provide an example of it. Here we have a provide the value of 3 to the statement that there exists a natural number that equals 3. or to prove there exists someone who is mortal $$\sqrt{1}$$ Home