Reflexivity of %$=$%

%$\Gamma\vdash t=t$%, where %$t$% is a constant symbol or a variable.

Transitivity of %$=$%

%$\Gamma , r=s,s=t\vdash r=t$%, where %$r$%, %$s$%, and %$t$% are constant symbols or variables.

Substitution

If %$\phi$% is a formula according to either of the first two clauses of the definition of a formula, %$s$% and %$t$% are variables and constant symbols, and %$\psi$% is obtained from %$\phi$% by replacing some occurrences of %$s$% by %$t$%, then %$\Gamma ,s=t,\phi\vdash\psi$%.

Thinning

If %$\Sigma$% is a set of formulas and %$\Gamma\vdash\phi$%, then %$\Gamma\cup\Sigma\vdash\phi$%.

Cut

If %$\Gamma\vdash\sigma$% for every %$\sigma$% in %$\Sigma$% and %$\Sigma\vdash\phi$%, then %$\Gamma\vdash\phi$%.

Proofs and theorems

A derivation (or proof) of %$\phi$% from %$\Gamma$% is a finite sequence of inferences %$\Sigma_{i}\vdash\phi_{i}$% such that the last one is %$\Gamma\vdash\phi$% and such that each %$\Sigma_{i}\vdash\phi_{i}$% is shown to be a legitimate inference using only the rules above and %$\Sigma_{j}\vdash\phi_{j}$% for %$j<i$%. A sentence %$\phi$% is derivable from %$\Gamma$% or is a theorem of %$\Gamma$% if there is a proof of %$\phi$% from %$\Gamma$% or, equivalently, if %$\phi$% is a member of the smallest set %$\Sigma$% such that %$\Gamma\subseteq\Sigma$% and, for any formula %$\sigma$% if %$$\Sigma\vdash\sigma$%, then %$\sigma\in\Sigma$%.

Consistency

A set %$\Gamma$% of formulas is inconsistent if there is a formula %$\psi$% such that %$\Gamma\vdash\phi$% and %$\Gamma\vdash (\lnot\phi )$%. A set %$\Gamma$% of formulas is consistent if it is not inconsistent.

-- ShaughanLavine - 04 May 2009