Словарь по логике

Рекурсивность по Смирнову: В работах по сравнению исчислений и формальных теорий В.А. Смирнов обычно характеризовал функции из языка одной теории в язык другой как рекурсивные. Поскольку под рекурсивными понимается особый класс арифметических функций (см. рекурсивные функции), т.е. с аргументами и значениями на множестве натуральных чисел, то непонятно, что Смирнов имел ввиду, называя так функции, определенные на формулах. В опубликованных работах это, вроде бы, нигде не определяется. Исходя из имеющихся примеров, можно предположить, что речь идет о возможности задания функции определенным образом. Во-первых, задание функция из языка L₁ в язык L₂ идет строго по пунктам индуктивного определения ППФ языка L₁. Второе требование (выполняется в известных примерах, но необходимо ли теоретически?) - чтобы функция была дистрибутивна относительно логических связок (по крайней мере, если алфавиты языков, т.е. наборы их логических связок, это позволяют).