Logic is a language for reasoning.
On these pages I am mostly concerned with mathematical logic and the mathematical structures that are related to it. There are a common set of latticelike structures that occur in various branches of mathematics such as orders, logic and sets.
Order  Logic  Set  

T  top  true  universe 
__  bottom  false  Ø 
/\ (conjunction)  greatest lower bound  and  
\/ (disjunction)  least upper bound  or  U 
Logic
We often write a rule in logic like this: 

We take this to mean that, if all the things above the line are true, then the thing below the line is true.
Constants
Values have two values ether true of false, we may use alternative names as follows:
true  1 
T  
false  0 
In boolean algebra every value evaluates to either true or false. In intuitionistic logic or constructive logic a value may be neither true or false, it is only true or false when proven to be true or proven to be false.
Connectives
conjunction  /\  and  (boolean,boolean) > boolean 
disjunction  \/  or  (boolean,boolean) > boolean 
negation  ¬  not  boolean > boolean 
implication  ==>  if  (boolean,boolean) > boolean 
equivalence  <=>  if and only if (iff)  (boolean,boolean) > boolean 
Quantifiers
for all  
there exists (for some) 
Propositional, FOL and HOL
Propositional Logic  Has connectives:
Propositions could be seen as questions about set membership, for example, x is a member of X since we can construct X as a set with the property we want. 

First Order Logic  Extends Propositional Logic so it has connectives plus:
Predicates act like functions that take an input value and produce a true/false value. 

Higher Order Logic  As First Order Logic plus:

Boolean Algebra
A  B  ¬A  ¬B  or  and  xor  A ==> B  A <=> B 

0  0  1  1  0  0  0  1  1 
0  1  1  0  1  0  1  1  0 
1  0  0  1  1  0  1  0  0 
1  1  0  0  1  1  0  1  1 
Laws
identity  and  or 

commutativity  x /\ y = y /\ x  x \/ y = y \/ x 
associativity  (x /\ y) /\ z = x /\ (y /\ z)  (x \/ y) \/ z = x \/ (y \/ z) 
idempotency  x /\ x = x  x \/ x = x 
absoption laws  x \/ (x /\ y) = x  x /\ (x \/ y) = x 
distribution  (x \/ y) /\ z = (x /\ z) \/ (y /\ z)  
excluded middle  x /\ ¬x = false  x \/ ¬x = true 
De Morgan (duality principle) 
¬(x /\ y) = ¬x \/ ¬y  ¬(x \/ y) = ¬x /\ ¬y 
double negation  ¬¬x = x  
true and false  x /\ true = x 
x \/ true = true x \/ false = x ¬false = true 
Canonical Form
minterm form  ¬A¬B ƒ(00) + ¬AB ƒ(01) + A¬B ƒ(10) + AB ƒ(11) 
maxterm form  (¬A + ¬B + ƒ(00) )( ¬A + B + ƒ(01) )( A + ¬B + ƒ(10) )( A + B + ƒ(11)) 
example: exclusive or is:
Σ(1,2)=∏(0,3)
Karnaugh Maps
A\B  0  1  
EF\CD  EF\CD  
0 



EF\CD  EF\CD  
1 


Logic and Computing
There is a deep connection between: λcalculus, intuitionistic logic and cartesian closed categories.
Curry–Howard–Lambek correspondence:
Cartesian Closed Category  λcalculus  intuitionistic logic 

objects  types 
proposition p = proposition P = proof of p 
Operator Types 

function type 
implication A implies B 

product type <a,b>:A/\B 
conjunction if A is proof of 'a' and B is proof of 'b' then A/\B is proof of <a,b> 

sum type a+b:A\/B 
disjunction if A is proof of 'a' and B is proof of 'b' then A\/B is proof of a+b 

Dependant Types 

dependent product type The type of the result B(a) depends on the value a . 
universal quantification (a:A).B(a) 

dependent sum type 
existential quantification (a:A).B(a) 

unit type  true formula T 

bottom type  false formula __ 

Inductive Types 

recursive function  inductive proof  
morphisms  terms  proof 
variable  axiom  
constructor  introduction rule  
destructor  elimination rule  
normal form  normal deduction  
weak normalisation  normalisation of deductions  
type inhabitation problem  provability  
inhabited type  intuitionistic tautology  
function application  
substitution  
simply typed λcalculus
where:
 x,y... (lower case) = variables
 A,B ... (upper case, beginning alphabet) = types
 M,N ... (upper case, middle alphabet) = metavariables for terms
Formation rules for well typed terms (wtt):
 every variable x:A is a wtt.
 if x:A is a variable and M:B is a wtt then λ x:A.M: A>B is a wtt
 if M:A > B is a wtt and N:A is a wtt then M N: B is a wtt
 if M:A is a wtt and N:B is a wtt then <M,N>: A×B is a wtt
 if M:A×B is a wtt then fst(M): A is a wtt
 if M:A×B is a wtt then snd(M): B is a wtt
Given a wtt M:B the set FV(M) of the free variables of M, is defined as follows:
 if M=x, then FV(M) = {x}
 if M=λ x:A.N, then FV(M) = FV(N){x}
 if M=N P, then FV(M) = FV(N) U FV(P)
 if M=<N,P>, then FV(M) = FV(N) U FV(P)
 if M=fst(N), then FV(M) = FV(N)
 if M=snd(N), then FV(M) = FV(N)
The substitution [M/x]N:B of a proof M:A for a generic x:A in a proof N:B is defined in the following way:
 if N:B = x:A then [M/x]N:B = M:A
 if N:B = y:A,x≠y then [M/x]N:B = N:B
 if N:B = λ x:C.P:B then [M/x]N:B = λ x:C.P:B
 if N:B = λ y:C.P:B,x≠y,y∉FV(M) then [M/x]N:B = λ y:C.[M/x]P:B
 if N:B = P Q then [M/x]N:B = [M/x]P[M/x]Q:B
 if N:B = <P,Q> then [M/x]N:B = <[M/x]P[M/x]Q>:B
 if N:B = fst(P) then [M/x]N:B = fst([M/x]P)
 if N:B = snd(P) then [M/x]N:B = snd([M/x]P)
Reduction  rewriting system
 αreduction: λ x:A.M = λ y:A.[y/x]M
 β(>)reduction: (λ x:A.M)N = [N/x]M
 η(>)reduction: λ x:A.(M x) = M, if x∉FV(M)
 β(×)reduction: fst(<M,N>) = M
 β(×)reduction: snd(<M,N>) = N
 η(×)reduction: <fst(P),snd(P)>) = P
where:
= : minimal congruence relation