Method of invariant transformations and logical deduction (Q759745)

It is well known that any derivable formula of the classical predicate calculus can be obtained by means of contractions \((A\vee A\to A,\quad A\&A\to A)\) from a formula derivable without using contraction rule. The notion of strong embedding of B in A used by the author is close to derivability of \(A\to B\) without using contraction rule (but does not coincide with it in view of nonsymmetric treatment of conjunction and disjunction). The deduction rules of the author's system (for which a long soundness argument is presented) are formulated in a complicated way using analogue of contraction rule combined with strong embedding into assumption formulas. This form is needed to incorporate axioms of specific theories in the process of automatic deductions.