The logical conclusion is a reasoning in which the passage through the rules from the utterance or the system of utterances. To the logical conclusion, the following requirements are usually presented (jointly or separately):

- transition rules should reproduce the relation of following the logical (one or another of its varieties);
- transitions in the logical inference should be carried out by only the syntactic characteristics of utterances or systems of utterance.

In modern logic, the concept of logical inference is defined for formal systems in which formulas represent utterances. Usually, three main types of formal systems are distinguished: axiomatic calculi, natural deduction calculus, sequent calculus. The standard definition of the logical derivation (from the set of formulas G) for the axiomatic calculus S is as follows: the logical deduction in S from the set of formulas G is a sequence A1…An of formulas of the language of the calculus S such that for each Ai (1 ≤ i ≤n) at least one of the following three conditions:

- Ai is a formula in T;
- Ai is the axiom of the calculus S;
- Ai is the formula obtained from the formula preceding it in the sequence A1…An or from the formulas preceding it in this sequence, according to one of the rules for deducing the calculus S. If α is a logical deduction in S from the set of formulas G, then the formulas in G are called the premisses of a, and the derivation α itself is called the deduction in S from the premisses of G; if, in addition, A is the last formula α, then α is called the logical deduction in S of formula A from the premises of G. The record “G ⊦ sA” means that there exists a logical deduction in S of formula A from the premises of G. The logical deduction in S from the empty set of formulas is called a proof in S. The notation “⊦sA” means that there exists a proof in S of the formula A. A formula A is said to be provable in S if ⊦A. As an example, consider the axiomatic calculus S1 with the standard derivation definition, which is a variant of the classical propositional logic. The alphabet of this calculus contains only the propositional variables p1, p2, …, pn, …, logical links ⊃, ⌉ and parentheses. The definition of a formula in this language is normal. Axioms S1 are formulas of the following six kinds (and only these formulas):

I. (A⊃A),

II. ((A⊃B) ⊃ ((B⊃C) ⊃ (A⊃C))),

III. ((A⊃ (B⊃C)) ⊃ (B⊃ (A⊃C))),

IV. (A⊃ (⌉B)) ⊃ (B⊃ (⌉A))),

V. ((⌉ (⌉A) ⊃A),

VI. ((((A⊃B) ⊃A) ⊃A).

The only rule for calculating the S1 modus ponens is A⊃B ⊦B.

The definition of the inference for S1 is an obvious specification of the definition given above. The following sequence of formulas F1-F6 is a logical deduction in S1 of the formula ((p1⊃p2) ⊃p2) from the premises {p1).

F1. ((p1⊃p2) ⊃ (p1⊃p2),

F2. (((p1⊃p2) ⊃ (p1⊃p2)) ⊃ (p1⊃ ((p1⊃p2) ⊃p2))),

F3. (p1⊃ ((p1⊃p2) ⊃p2)),

F4. p1,

F5. ((p1⊃p2) ⊃p2).

Analysis: F1 is an axiom of form 1, F2 is an axiom of form III, F3 is obtained by the modus ponens rule from F1 and F2, F4 is a premise, F5 is obtained by the modus ponens rule from F4 and F3. Thus, {p1} ⊦s1 ((p1⊃p2) ⊃p2). Considering the sequence of formulas F1, F2 F3, we see that ⊦s1 (p1⊃p2) ⊃p2)).

In some cases, the logical conclusion is defined in such a way that restrictions are imposed on the use of certain rules. For example, in axiomatic calculi that are variants of the classical logic of predicates of the first order and containing only the modus ponens and the generalization rule among the inference rules, the logical conclusion is often defined so that the use of the generalization rule is restricted: any application to generalization rules in α is such that a variable, on which the generalization rule is generalized in this application, does not enter into any premise preceding the generalization rule in the α lower formula of this application. The purpose of this restriction is to provide a number of useful terms of logic output properties (for example, execution for simple deduction forms of the theorem). There are definitions of logical inference (both for axiomatic and for calculi of other types):

- give a logical conclusion not only from the set of premises, but also allow other forms of organization of the parcels (for example, lists or sequences),
- structure the output not only linearly, but, for example, in the form of a tree,
- have a pronounced inductive character; the inductive determination of the output can be carried out either by one variable (for example, by the length of the output) or by several variables (e.g., by the length of the logical inference and by the number of its premises),
- contain the formalization of the relationship between formulas in the logical derivation, and many other definitions of logical inference, caused by other methods of formalization and axiomatization of classical and non-classical systems of logic.