Classical or traditional system of determining the validity or invalidity of a conclusion (inference) deduced from two or more statements (premises). Based on the theory of syllogism of the Greek philosopher Aristotle (384-322 BC) systematized in his book 'Organon,' its focus is not on what is stated (the content) but on the structure (form) of the argument and the validity of the inference drawn from the premises of the argument-if the premises are true then the inference (also called logical consequence) must also be true. The basic principles of formal logic are (1) Principle of identity: if a statement is true then it is true. (2) Principle of excluded middle: a statement is either true or false. (3) Principle of contradiction: no statement can be both true and false at the same time. Also called Aristotelian logic.
An inference rule is a method of deriving conclusions from premises. When inference rules for a formal language are codified it becomes a formal logic.

Sentences

For a language to become a logic it must be capable of expressing propositions, for which purpose there must be an appropriate syntactic category, e.g. sentences, or formulae. Examples of languages which fail to be suitable for logics for lack of such a category are the lambda calculus and most programming languages, which are designed for defining algorithms or functions, not for making or proving assertions. In the case of a typed language a distinguished type may suffice, a type of propositions or truth values, e.g. BOOL in HOL. This technique was used by Alonzo Church to make a logic (his simple theory of types) from the typed lambda calculus.

Axioms

To define the logic it is next necessary to determine the axioms of the logic. The axioms are those sentences which are to be considered true without proof.

Inference rules

Next the inference rules must be defined. Inference rules determine how new theorems can be derived from one or more previously proven theorems.

Effectiveness

It is normal that the definitions of the axioms and inference rules be effective in the sense that a computer could be used to check what is an axiom or to check the correctness of an application of an inference rule.

Consistency

The logic is consistent (in the sense of Emil Post) if there are some sentences of the language which are not provable from the axioms using the inference rules.

Truth

If the language has a semantics this will usually determine a subset of the sentences of the language which are "true", these are the sentences which should be provable in the logic.
If all the sentences which can be proven using the logic are true then the logic is sound.
If all the true sentences are provable then the logic is complete.