Сведок (математика)

Во математичката логика, сведок е специфична вредност t да се замени со променливата x на егзистенцијална изјава на обликот x φ (x) така што φ (t) е точен.

Примери

На пример, се вели дека теоријата Т за аритметика е недоследна доколку постои доказ во Т со формулата „0 = 1“. Формулата I ( T ), која вели дека Т е недоследна, е така егзистенцијална формула. Сведок за недоследност на Т е посебен доказ за „0 = 1 “ во Т.

Булос, Бургес и Џефри (2002: 81) го дефинираат поимот сведок со примерот, во кој S е n -врска на место со природни броеви, R е (n + 1) -просторен рекурзивен однос и ↔ означува логичка еквивалентност (ако и само ако):

S (x _1, ..., x _n) ↔ y R (x _{1,..., N} x, y)

"А y, така што R држи на x _i може да се нарече" сведок "на односот S одржување на x _i (под услов да се разбере дека кога сведокот е голем број, а не човек, сведок само сведочи за она што е точно).”

Во овој конктретен пример, авторите го дефинирале s да биде (позитивно) рекурзивно полуодлучливо, или едноставно полурекурзивно.

Хенкинов сведок

Во предикативни пресметки, Хенкиновиот сведок за реченица $\exists x\,\varphi (x)$ во теоријата Т е термин c таков што Т докажува φ ( в ) (Хинман 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 година, Computability and Logic: Fourth Edition, Универзитетски печат Кембриџ, ISBN 0-521-00758-5 .
• Леон Хенкин, 1949 година, „The completeness of the first-order functional calculus“, Journal of Symbolic Logic т. 14 б. 3, стр. 159 – 166.
• Питер Г. Хинман, 2005 година, Fundamentals of mathematical logic, A.K. Peters, ISBN 1-56881-262-0 .
• X. Хинтика и Г. Санду, 2009 година, „Game-Theoretical Semantics“ во изданието на Кит Алан - „Concise Encyclopedia of Semantics, Елсевиер, ISBN 0-08095-968-7, стр. 341 – 343