Predicate Logic (or also called Predicate Calculus) is the term for a formal and symbolic system of logic like firstorder logic, secondorder logic and so on.
It is defined over some (possibly infinite) set. It requires some form of assignment or relationship of the elements of the set to give true or false values.
Terms
Constants
Values have two values ether true of false, we may use alternative names as follows:
true  1 
T  
false  0 
__ 
Variables
A variable is a letter or symbol used to represent a value (an object, not a proposition). A predicate containing variables can be made into a valid proposition if the variables are either:
 assigned a value.
 or quanitified using a quantifier.
Functions
Composite terms are formed by applying function symbols to other terms. Each function symbol has an 'arity' that is it takes in 'n' parameters and returns 'm' parameters.
Quantifiers
universal quantifier:  for all  
existential quantifier:  there exists (for some) 
For universal quantifier we will use the notation x:σ.A(x) which is true if A(x) is true for every 'x' in type 'σ', where:
 is start of this universal quantifier syntax.
 x is a variable which ranges over given type.
 : means 'has type'.
 σ indicates the type.
 . seperator.
 A(x) is a predicate that is a function of x.
So,
x:σ.A(x) = A(a) /\ A(b) /\ ...
where a:σ, b:σ ... are all objects in discourse.
Simarly for existential quantifier we will use the notation x:σ.A(x) which is true if A(x) is true for at least one 'x' in type 'σ'
x:σ.A(x) = A(a) \/ A(b) \/ ...
where a:σ, b:σ ... are all objects in discourse.
Introduction Rules


Elimination Rules


Formulas
If x_{1}, … ,x_{n} are elements of the set and P is an nplace predicate symbol, then
P(x_{1}, … ,x_{n}) is an elementry formula
If A and B are formulas, then
 A /\ B
 A \/ B
 A ¬ B
 A ==> B
 A <=> B
 x A
 x A
are also formulas.
Connectives
Commonly used logical connectives include:
 Negation (not) ( or ~)
 Conjunction (and) (/\,wedge, &, or )
 Disjunction (or) (/\ or vee )
 Material implication (if...then) (> or supset)
 Biconditional (if and only if) (iff) (xnor) (<> , equiv, or = )
Programming
Formation Rules


Introduction Rules


Elimination Rules


Computation Rules
((λ x:A).p a > p[a/x]  fst (p,q) > p snd (p,q) > q 