Чем лямбда-исчисление сильнее логики первого порядка?

1: В чем они превосходят выразительную силу логики первого порядка?

Я не знаю, можно ли напрямую сравнивать нетипизированное лямбда-исчисление и логику первого порядка, но простая теория типов — это типизированное лямбда-исчисление и в то же время формализация логики высшего порядка. Согласно википедии:

Лямбда-исчисление было введено математиком Алонзо Черчем в 1930-х [...]. Было показано, что исходная система логически непоследовательна в 1935 году [...] в 1936 году Черч выделил и опубликовал только ту часть, которая имеет отношение к вычислениям, то, что сейчас называется нетипизированным лямбда-исчислением. В 1940 году он также представил более слабую в вычислительном отношении, но логически непротиворечивую систему, известную как просто типизированное лямбда-исчисление.

Как я узнал из «Семи достоинств теории простых типов», обычно используемая система доказательств для теории простых типов равносильна теории множеств Маклейна . Это, в свою очередь, считается «хорошей моделью» «предикативной математики». Ходят слухи , что у Рэндалла Холмса есть доказательство того, что «Новые основы» Куайна равносильны теории множеств Маклейна.

2: Есть ли у нас теоремы полноты и обоснованности для лямбда/комбинаторной логики?

В статье, в которой вводилась семантика Хенкина для логики высшего порядка, явно рассматривалась теория простых типов, и содержалась теорема Хенкина. Таким образом, полнота и обоснованность в определенном смысле подобны логике первого порядка. Однако то, что оно непротиворечиво с теорией множеств Маклейна, означает, что непротиворечивость теории простых типов не может быть доказана в абсолютном смысле.

В статье на самом деле говорится, что они «обычно» превосходят возможности логики первого порядка. Логика первого порядка над языком арифметики, включающим сложение и умножение, является полной по Тьюрингу, поскольку вы можете арифметически определить каждую рекурсивную функцию:

http://www.cogsci.rpi.edu/~heuveb/teaching/Logic/CompLogic/Web/Presentations/Arithmetical%20Definability.pdf

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

Я не хочу здесь никого обидеть. Я могу прокомментировать только как неспециалист, у которого есть только непрофессиональное понимание университетской математики.

Примечательно, что не все здесь считают, что логика первого порядка не является полной по Тьюрингу. Машина Тьюринга — это конечный автомат с бесконечной лентой. Это всего лишь элементарное (т.е. выполнимое) упражнение по компьютерному кодированию для реализации этого.

Для полной системы Тьюринга требуется только крошечное подмножество Dartmouth Basic или Applesoft Basic. В последние годы Терри Тао спросил (возможно, на этом сайте), есть ли группа, которая была завершена по Тьюрингу. Возможно, мы могли бы выполнить упражнение по галочке, отметив, что любой из объектов, с которыми мы сталкиваемся на вводном курсе математики в университете, сам по себе достаточен для построения полной системы Тьюринга.

Запись в Википедии для логики первого порядка довольно подробная (многие сотни строк).

В нем говорится: логика первого порядка способна формализовать многие простые кванторные конструкции на естественном языке, например, «каждый человек, живущий в Перте, живет в Австралии». Но есть много более сложных особенностей естественного языка, которые не могут быть выражены в (односортной) логике первого порядка. «Любая логическая система, подходящая в качестве инструмента для анализа естественного языка, нуждается в гораздо более богатой структуре, чем логика предикатов первого порядка» (Gamut 1991, стр. 75).

В статье в Википедии также говорится:

Обычные интерпретации первого порядка имеют единую область дискурса, в которой распространяются все кванторы. Многосортная логика первого порядка позволяет переменным иметь разные сорта, которые имеют разные домены. ... Когда в теории имеется только конечное число сортов, многосортная логика первого порядка может быть сведена к односортной логике первого порядка. В односортную теорию вводится унарный предикатный символ для каждого вида в многосортной теории и добавляется аксиома, утверждающая, что эти унарные предикаты разделяют область дискурса.

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

Я буду следить за статьей Gamut, пытаясь пролить свет на это. Но prima facie статья Gamut неверна, потому что она вызывает вопрос — она говорит, что вы не можете выразить естественный язык в односортном исчислении предикатов. Но статья в Википедии ясно дает понять, что это не может быть ограничением — по крайней мере, она показывает, что многосортное исчисление предикатов может быть закодировано в односортированное исчисление предикатов.