2. Клини Стефан Коул

5.1.1909	Родился в Хартфорд, штат Коннектикут
1969	член Национальной Академии Наук США
1930	Окончил Принстонский университет
В 1934	получил степень доктора философии в Принстонском университете
С 1935	работает в Висконсинском университете
С 1948	профессор
1952	В книге «Введение в математику» дал очерк состояния оснований математики и возникших в середине 20 века в этой связи основных направлений в математической логике. В ней подробно рассмотрены интуиционские системы.
1943	Введена классификация Клини-Мостовского для теоретико-числовых предикатов,независимо С.Клини и А.Мостовским

Клини Стивен Коул (Kleene Stephen Cole)– известный американский логик и математик. Основные труды по теории алгоритмов и рекурсивных функций, а также проблемам интуиционистской логики и математики. В частности, им доказана эквивалентность, введенного А.Чёрчем понятия λ-определимости функции с общерекурсивностью. Введенное Клини понятие (рекурсивной реализуемости формул лежит в основе интуиционистской интерпретации арифметических суждений. Клини – автор ряда широко известных монографий по математической логике, основаниям математики и теории рекурсивных функций. Ввёл понятие рекурсивной реализуемости формул.

2.3. Чёрч Алоизо

Чёрч Алоизо (Church Alonzo) (родился 14.6.1903, Вашингтон) – крупный американский логик и математик, профессор математики Принстонского и Калифорнийского универститетов. С 1936 года редактор журнала «The Journal of Symbolic Logic». Занимался исследованиями проблемы логической семантики. Внес большой вклад в развитие математической логики и теории автоматов. Он знаменит тем, что в 1935 году построил первый пример неразрешимой массовой проблемы, которая состоит в требовании найти алгоритм для решения некоторой серии «единичных» проблем. Массовая проблема неразрешима, если ее решения, то есть требуемого алгоритма, е существует.

Им же дано доказательство неразрешимости проблемы для узкого исчисления предикатов, то есть доказательство того, что не существует алгоритма, который по виду формулы этого исчисления определял бы, выражает эта формула общелогическую истину или нет.

Алоизо Чёрч автор книги «Введение в математическую логику» (1956), в которой разъяснил свое понимание метода математической логики, определил ее первичные понятия и изложил исчисление высказываний или пропорциональное исчисление, функциональные исчисления первого порядка, чистое функциональное исчисление первого порядка и функциональные исчисления второго порядка. А.Чёрч дает определения таких категорий, как имя, константы и переменные функции, символы, связки, операторы, кванторы, проблема разрешения, непротиворечивость и полнота системы аксиом.

Математическую логику А.Чёрч называет формальной логикой, предмет которой изучается методом построения формализованных языков. «Обычно (формальная) логика, – пишет он, – занимается анализом предложений и доказательств; при этом основное внимание обращается на форму в отвлечении от содержания…»¹ Поскольку естественные языки на протяжении длительных исторических периодов развивались под влиянием практических потребностей легкости общения, постольку они не отличаются точностью и надежностью, что приводит к ошибкам в рассуждениях. Чтобы избежать возможных ошибок, А.Черч предлагает употреблять для логических целей специально созданный язык – формализованный язык, в который из обычных языков будут перенесены собственные имена. При этом он подчеркивает, что в хорошо построенном языке каждое имя должно иметь точно один смысл, если ставится задача обеспечить однозначность в формализованных языках. Суждение А.Чёрч определяет так: «Всякий концепт истинного значения называется суждением независимо от того, является ли он смыслом какого-либо предложения».²

В математической логике большую роль играет тезис Чёрча, принцип, согласно которому класс функций, вычислимых с помощью алгоритмов в широком интуитивном смысле, совпадает с классом частично рекурсивных функций. Тезис Чёрча – это естественнонаучный факт, подтверждаемый опытом, накопленным в математике за всю ее историю. Все известные в математике примеры алгоритмов удовлетворяют ему. Различным уточнениям интуитивного понятия алгоритма соответствуют свои формулировки тезиса Чёрча. Тезис Тьюринга заключается в том, что всякая вычислимая в интуитивном смысле функция вычислима с помощью машины Тьюринга, а принцип нормализации Маркова – в том, что всякая вычислимая в интуитивном смысле функция вычислима с помощью некоторого нормального алгоритма. Из эквивалентности известных уточнений понятия алгоритма следует эквивалентность соответствующих вариантов тезиса Чёрча. Этот факт является еще одним подтверждением тезиса Чёрча. Тезис Чёрча не может быть строго доказан, так как в его формулировке участвует неточное понятие «алгоритм в интуитивном смысле». Были попытки опровергнуть тезис Чёрча, однако они к успеху не привели. Принятие тезиса Чёрча полезно в теории алгоритмов и ее приложениях. Во-первых, при доказательстве существования тех или иных конкретных алгоритмов – машин Тьюринга, рекурсивных функций, нормальных алгоритмов – можно, опираясь на тезис Чёрча, ограничиваться интуитивно ясными построениями и не выписывать соответствующие формальные схемы. Кроме того, тезис Чёрча является основанием для вывода о неразрешимости данной алгоритмической проблемы после того, как строго доказано, что эта проблема не может быть решена в рамках того или иного уточнения понятия алгоритма.