Свидетель (математика)

В математической логике свидетель — это конкретное значение t, которое необходимо заменить на переменную x экзистенциального утверждения формы ∃ x φ ( x ), такого, что φ ( t ) истинно.

Примеры

Например, теория арифметики T называется несовместимой, если существует доказательство в T формулы «0 = 1». Формула I( T ), которая говорит, что T несовместима, является, таким образом, экзистенциальной формулой. Свидетельством несогласованности T является частное доказательство «0 = 1» в T .

Булос, Берджесс и Джеффри (2002:81) определяют понятие свидетеля на примере, в котором S — это n- местное отношение для натуральных чисел, R — (n+1) -местное рекурсивное отношение , а ↔ указывает логическая эквивалентность (тогда и только тогда, когда):

S ( Икс ₁ , ..., Икс _п ) ↔ ∃ y р ( Икс ₁ , ..., Икс _п , y )

« Любой такой, что R имеет отношение к xi _, может быть назван «свидетелем» отношения S имеющим xi _, (при условии, что мы понимаем, что, когда свидетелем является число, а не человек, свидетель свидетельствует только о том, что является истинный)."

В этом конкретном примере авторы определили s как (положительно) рекурсивно полуразрешимый или просто полурекурсивный .

Хенкин

В исчислении предикатов Хенкин является свидетелем приговора. $\exists x\,\varphi (x)$ в теории T — это термин c такой, что T доказывает φ ( c ) (Hinman 2005:196). Использование таких свидетелей является ключевым методом доказательства теоремы Гёделя о полноте, представленной Леоном Хенкиным в 1949 году.

Связь с семантикой игры

Понятие свидетеля приводит к более общей идее семантики игры . В случае приговора $\exists x\,\varphi (x)$ выигрышная стратегия для проверяющего — выбрать свидетеля для $\varphi$. Для более сложных формул, включающих кванторы универсальности , существование выигрышной стратегии для проверяющего зависит от существования соответствующих скулемовских функций . Например, если S обозначает $\forall x\,\exists y\,\varphi (x,y)$ тогда эквивыполнимое утверждение для S есть $\exists f\,\forall x\,\varphi (x,f(x))$. Функция Скулема f (если она существует) фактически кодифицирует выигрышную стратегию для проверяющего S , возвращая свидетель экзистенциальной подформулы для каждого выбора x, который может сделать фальсификатор.

См. также

• Сертификат (сложность) — аналогичное понятие в теории сложности вычислений.

Ссылки

• Джордж С. Булос, Джон П. Берджесс и Ричард К. Джеффри, 2002, Вычислимость и логика: четвертое издание , Cambridge University Press, ISBN   0-521-00758-5 .
• Леон Хенкин, 1949, « Полнота функционального исчисления первого порядка », Журнал символической логики , т. 14 н. 3, стр. 159–166.
• Питер Г. Хинман, 2005, Основы математической логики , А. К. Петерс, ISBN   1-56881-262-0 .
• Дж. Хинтикка и Г. Санду, 2009, «Теоретико-игровая семантика» в книге Кита Аллана (ред.), Краткая энциклопедия семантики , Elsevier, ISBN   0-08095-968-7 , стр. 341–343.