Логика комбинаторная

Комбинаторная логика — это направление в основаниях логики и математики, занимающееся анализом понятий, которые в рамках классической математической логики (см. Логика математическая) принимаются без дальнейшего изучения (например, понятия «переменная», «функция», «правила подстановки» и другие). В комбинаторной логике в качестве основных понятий выбираются: функция (оператор) и операция аппликации (application) — применение (приложение) функции f к аргументу g, пишут: (fg). Функции понимаются теоретико-операторно, бестипово, то есть допустимы: (gf), (gg), (g(ff)), (gg) (fg) и так далее. Выражение вида f(x₁, … x_n), является лишь записью для (…(fx₁) x₂)x_n). Тем самым многоместные функции сводятся к одноместным. Опуская скобки, пишут: fx₁x₂ … x_n вместо x₁, … x_n можно поставить f, получая fff … f. Здесь n ≥ 0 (если n = 0, то f — нульместная функция).

Исходными объектами (сокращённо, по X. Карри, называемыми обами) в комбинаторной логике служат константы и переменные (множество переменных может быть пустым). Новые обы строятся из исходных и полученных ранее по правилу: если a и b — обы, то (ab) считается обом. Выделяются три константы, обозначающие индивидуальные функции (комбинаторы): два собственных комбинатора К и S, удовлетворяющих равенствам Kab = a и Sabc = ac (bc), где a, b и c — произвольные обы (скобки в обах восстанавливаются по ассоциации влево) и один дедуктивный комбинатор U как некоторый аналог формальной импликации или оператора функциональности. Эти три комбинатора позволяют заменить любое предложение логико-математических языков комбинацией (обом) из К, S и U и скобок, откуда и название «комбинаторная логика» (введённое Карри). Употребление же переменных вообще может быть исключено, что соответствует первоначальному замыслу М. И. Шейнфинкеля, X. Карри и А. Чёрча. К примеру, если A комбинатор такой, что Аху = x + y, а C комбинатор такой, что Cfxy = fyx [или в более обычных обозначениях: приложение комбинатора A к аргументам x, y даёт x + y; приложение комбинатора C к fxу) даёт f(yx)], то сумму y + x в этом случае можно выразить как САху. Тождество x + y = y + x выражается при этом в виде Аху = САху. И если [как это делается обычно в математике] трактовать тождественное равенство f(x₁, … x_n) = g(x₁…, x_n) как другое выражение для f = g (то есть считать, что функции f и g, относящие обе одни и те же объекты к одним и тем же значениям аргументов, отождествляются нами), то другим выражением для тождества x + y = y + x будет формула A = CA, не содержащая переменных.

Создателем комбинаторной логики является московский математик Моисей Ильич Шейнфинкель (1920). Он ввёл комбинаторы К, S и U, сформулировал и обосновал, используя указанные равенства для К и S, принцип комбинаторной полноты, более общий, чем канторовское неограниченное теоретико-множественное свёртывание. Шейнфинкель предложил один из первых способов уточнения интуитивного понятия алгоритма, определив по существу комбинаторные алгоритмы как вариант реализации вычислительной (алгоритмической) части дискретно-комбинаторной программы Г. В. Лейбница.

Независимо от Шейнфинкеля американские математики Карри и Чёрч получили аналогичные результаты. В их трудах комбинаторные алгоритмы представлены дедуктивно в виде доказуемо непротиворечивых исчислений негилбертовского типа. Таковы, в частности, ламбда-исчисления (λ-исчисления) Чёрча, эквивалентные чистой (без логических законов) комбинаторной логике Шейнфинкеля — Карри. Исчисления Шейнфинкеля — Чёрча — Карри оказались удачными теориями вычислений. Они дали толчок развитию теории рекурсий, различных видов алгоритмов, а в последнее время и информатики. Известны применения комбинаторной логики в теории доказательств, в семантике языков программирования, алгебре, топологии, теории категорий и других разделах современного знания.

Бестиповые исчисления Шейнфинкеля — Чёрча — Карри были введены прежде всего в расчёте на то, что их дедуктивные расширения станут основаниями математики и других наук. Пытаясь реализовать синтаксически дедуктивный комбинатор U, Карри и Чёрч построили также логико-математические исчисления гилбертовского типа, которые, однако, оказались противоречивыми: парадокс Клини — Россера (1936), парадокс Карри (1941). Следует отметить, что в парадоксе Карри из логических средств используются только имшшкативные, а правило modus ponens выступает как единственный логический источник противоречивости. Поскольку все известные дедуктивные системы гилбертовского типа либо бедны выразительными возможностями, либо противоречивы, обращаются к идее ступенчатых расширений. Ступенчатые системы комбинаторной логики строятся на основе комбинаторных алгоритмов путём последовательных расширений бестиповых непротиворечивых исчислений Шейнфинкеля — Чёрча — Карри, опираясь на принципы дедуктивной полноты — правила введения операторов (прежде всего логических) в сукцедент (в заключение выводимостей) и в антецедент (в посылки выводимостей).

Такая трактовка выводимостей позволила ограничить иерархии двумя ярусами. Первый — исчисления Шейнфинкеля — Чёрча — Карри. Второй вводится как расширение первого на базе исчисления секвенций — классической логики предикатов первого порядка, распространённой на обы комбинаторной логики, без постулируемого (в силу известного результата Г. Генцена 1934 года) правила сечения. Логические связки и кванторы представляются в виде обов, составленных из символов алфавита комбинаторной логики, являющихся константами первого яруса.

Среди всех двухярусных систем выделяется A-система со всеми логическими операторами и оператором λ. Её правила объединяют два яруса в формальное исчисление (в соответствии с программой Гилберта), для которого доказываются теоремы о полноте (в смысле К. Гёделя, ср. его теоремы 1931 года о неполноте известных исчислений гилбертовского типа) и непротиворечивости (в классическом секвенциальном смысле). Эти правила выражаются следующим образом:

Где a и b — обы, Г, Θ — это наборы обов, → и ⇒ — это символы секвенций первого и второго ярусов, алгоритмической (вычислительной) и дедуктивной (генценовской) соответственно. Говорят, что об a конвертируется в об b, если секвенция a → b выводима в чистой комбинаторной логике (в исчислении Шейнфинкеля — Чёрча — Карри).

Все элементы языка теории множеств записываются как обы комбинаторной логики с точностью до конвертируемости. Так, атомарная формула b ∈ a представляется обом ba, по формуле C и переменной x строится новый терм (новое множество) как об λ хС, отражая тем самым исходный принцип Кантора: неограниченное образование новых множеств.

В классе всех выводов A-системы выделяется подкласс M всех выводов, в которых применения структурных и логических правил второго яруса ограничены описанными элементами теории множеств. В основе M лежат два принципа, характеризующие канторовскую («наивную») теорию множеств: неограниченное теоретико-множественное свёртывание и классическая логика предикатов первого порядка без ограничений, соответствующие двум ярусам A-системы. Класс M выступает как вариант непротиворечивой формализации канторовской теории множеств.

Широко известный парадокс Рассела (1902) отражается в классе M в виде выводов двух дедуктивных секвенций ⇒ D) и ⇒ ⌉D, где ⌉ — знак отрицания, a D — об: ∃λу П λx = (x ∈ y) (⌉(x ∈ x), представляющий частный случай известной схемы теоретико-множественного свёртывания, записанной на языке комбинаторной логики.