Logic

The basic idea is that given the rules of type theory only true statements can be constructed. We write the relation between a proof (A.proof) and the proposition it is proving (A) as:

A.proof : A

For example, A could be the proposition "All cats have whiskers" and A.proof would be the proof of that. The only statements we can create are definitions of terms and their rules for how they work. These are our axioms. And other terms constructed from these axioms. We might also have a proposition A without a proof. This proposition is called "unproven". An unproven proposition that can be shown to contradict a previously proof is then defined to be false.

Constructing the Axioms of Logic

True and false

Let us introduce two atomic propositions True and False. False, by definition, cannot have a proof. We introduce a proof for True which we call True.proof. So we have (by definition):

True.proof : True

And

If we have two proofs A.proof:A and B.proof:B and they are both true we can construct a combined proof of the proposition, A ∧ B. We introduce a proof function for this which is simply going to be a pair of proofs:

pair _A,B(A.proof , B.proof) : A ∧ B

For example we can constuct in this way a proof, (True.proof, True.proof) : True ∧ True but there is no proof of proposition True ∧ False for example.

Or

If we have a proof of proposition A then it is true that A or B is true where B is some other proposition. It is also true that B or A is true. We can construct these two new statements with the functions left andright.

left _A,B (A.proof) : A ∨ B

right _A,B (B.proof) : A ∨ B

This allows us to create proofs of propositions True ∨ False but not False ∨ False
Example:

Imply

If a proposition A implies another proposition B, (written A.to(B) ) it means given A.proof we can construct a B.proof. In other words we can construct a function, f, which takes in A.proof and returns B.proof. So f(A.proof)=B.proof. Thus we write

f : A → B

We introduce f = id_True = (x:True)⇒(x:True) for the proof of True → True.

Not

We define Not(A) as equivalent to the proposition A→False. Then we can create a proof of not False using id.

Qualifiers

A simple example. Find a proof that forall x show that x or True is true. This involves creating a function of the correct type.

An example of a proof of the chaining rule (Prop.compose):

Deducibility

Here is a proof for (T→F)→F or more generally (T→x)→x

Double Negation

This should technically work, but the definitional equality is not simplifying enough: (Note in general it is not possible to prove that Not Not x = x for any x in constructive type theory unless we assume law of excluded middle. )

First/Second

We can use the first and second elements of a pair to prove things like:
Also:
We can use left and right to prove:

Cases

Approximately the not rule for AND and OR: