Нормализованные выводы и обобщение теоремы дедукции.

Аннотация

The main aim of the paper is to formulate both a general definition of the normalized inference from hypotheses and a general definition of the deduction theorem which at the same time would be valid for any logical theory T (D-theory) being not weaker than a system $D_{min}$ with the following axiom schemes:

(1) $A\rightarrow A$ (2) $A\rightarrow B\rightarrow _.C\rightarrow A \rightarrow _.C\rightarrow B$ (3) $(A_T\rightarrow B)\rightarrow B$

(2) (where $A_T$ is any theorem of $T$), and the only rule of inference:

MP (modus ponens).

Let $B_l,..., B_m$ is a consequence of inference $В$ from hypotheses $\varGamma$ We say that a member $B_i$ of $B_l,..., B_m$ depends from $B_k$ iff (1) $B_i$ is the same as $B_k$ , or (2) $B_k$ was used to obtained $B_i$ by a rule of inference, or (3) $B_i$ depends from $B_j$and $B_j$depends from $B_k$.

The using of $MP$ in a consequence $B_l,..., B_m$ of inference $В$ from hypotheses $\varGamma$ in a theory $T$ is said to be normalized iff for each member of the consequence $B_i$ $(i\leq m)$, obtained from $B_k$ (the major premise) and $B_l$ (the minor premise) by $MP$, the following conditionals are satisfied:

(a) the major premise $B_k$ precedes the minor one $B_l$ , i.e. $(k