Логический анализ дефинициальной дедукции

Abstract

The article is devoted to analisis of definitions and their properties in type-free languages. In order to achieve this aim we define logic of definitional deduction. The single rule of this logic is replacement of terms according to their definitions. The resulting logic is definitionally equivalent to combinatory logic of Sch_nfinkel-Curry.