The Language
The language in which propositions or assertions are written consists of a recursively defined term:
A term (formula) is either:
The alpha set A is a finite set of elements called
proposition symbols or propositional variables,
otherwise referred to as atomic formulae or
terminal elements. 
A variable: X_{0}, X_{1}, X_{2} ... 
Or the omega set Ω is a finite set of elements called
operator symbols or logical connectives. The set
Ω is partitioned into disjoint subsets as follows: 
A /\ B 
A and B 
A \/ B 
A or B 
A => B 
A implies B 
A <=> B 
A if and only B 
¬A 
not A 
__ 
false 

The zeta set Z is a finite set of transformation rules that
are called inference rules when they acquire logical
applications. 

The iota set I is a finite set of initial points that are
called axioms when they receive logical interpretations. 

where A and B are further terms, metavariables used to describe the language.
Arguments, proofs or derivations in this language.
Assumption Rule
'A' a given term is taken to be true.
And
I have named these rules (in red) so that we can refer to them.
Or
If A\/B then we can't say anything about A and B individually but we can say that at least one of them is true. To codify this more formally we use assumptions:
The box, like this: 
[A]
... C 
means that [A] is an assumption. 
That is, if we assume A is true then C is true. These assumptions are only temporary so we draw them in boxes to partition them off from the main sequence of logic.
So the elimination rule (\/E) says that if:
 we have a rule that proves C from A
 and we have a rule that proves C from B
 and either A, B or both are true
then C is true because we know that we can use one or both of these rules.
Implication and Modus Ponens
Introduction 
Elimination 

(modus ponens) 


Alternatively we can represent modus ponens using context () as follows:
C (B => D) 
C /\ B D 

There is a good explanation of this in [1] (appendix A page 198)
Programming
I have implemented some logic using the Axiom/FriCAS program as described on the page here.
Formation Rules
Rules of syntax for the language of propositions.
What the types of the system are.
In the bottom row we convert to types (CurryHoward)
and 
or 
implication 
A is a formula B ^{ } is a formula 
(A/\B) is a formula 

(/\F) 

A is a formula B ^{ } is a formula 
(A\/B) is a formula 

(\/F) 

A is a formula B ^{ } is a formula 
(A=>B) is a formula 

(=>F) 

A is a type B ^{ } is a type 
Record(A,B) is a type 

(/\F) 

A is a formula B ^{ } is a type 
Union(A,B) is a type 

(\/F) 

A is a formula B ^{ } is a type 
(A>B) is a type 

(=>F) 

Introduction Rules
Which expressions are members of which types.
and 
or 
implication 


[x:A]
... 
e:B ^{ } 
(λx:A).e:A=>B 

(=>I) 

Elimination Rules
and 
or 
implication 

p:(A \/ B) f:(A=>C) g:(B=>C) 
cases p f g :C 

(\/E) 


Computation Rules
How to evaluate expressions.
and 
or 
implication 
fst(p,q)>p
snd(p,q)>q 
cases inl(q) f g > f q
cases inr(r) f g > f r 
(λx:A).e a > e[a/x]
βreduction 
Bibliography
[1] 

Sets for Mathematics  This
is a book about sets from category theory point of view. 
