WikiDer > Турникет (символ) - Википедия

Turnstile (symbol) - Wikipedia

В математическая логика и Информатика символ ${ displaystyle vdash}$ взял имя турникет из-за его сходства с типичным турникет если смотреть сверху. Его также называют тройник и часто читается как «дает», «доказывает», «удовлетворяет» или «влечет за собой».

В TeX, символ турникета ${ displaystyle vdash}$ получается из команды vdash. В Unicode, символ турникета (⊢) называется правильный галс и находится в кодовой точке U + 22A2.^[1] (Кодовый пункт U + 22A6 называется знак утверждения (⊦).) На печатная машинка, турникет может быть составлен из вертикальная полоса (|) и бросаться (-). В Латекс существует пакет турникета, который по-разному выдает этот знак и позволяет наклеивать ярлыки ниже или выше в нужных местах.^[2]

Интерпретации

Турникет представляет собой бинарное отношение. В нем есть несколько разных интерпретации в разных контекстах:

В эпистемология, Пер Мартин-Лёф (1996) анализирует ${ displaystyle vdash}$ символ таким образом: "... [T] комбинация Фреге Urteilsstrich, инсульт суд [| ], и Инхальцстрих, черта содержания [-], стала называться знаком утверждения ".^[3] Обозначение Фреге для суждение некоторого содержания $А$

{ displaystyle vdash A}

затем можно прочитать

Я знаю $А$ правда.^[4]

В том же духе условное утверждение

{ displaystyle P vdash Q}

можно читать как:

Из $п$ , Я знаю это $Q$

В металогика, изучение формальные языки; турникет представляет синтаксическое следствие (или «выводимость»). Это означает, что это показывает, что одна строка может быть полученный от другого за один шаг, согласно правила трансформации (т.е. синтаксис) некоторых данных формальная система.^[5] Таким образом, выражение

{ displaystyle P vdash Q}

Значит это

Q

выводится из

п

в системе.

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

{ displaystyle vdash Q}

Значит это

Q

это теорема в системе.

В теория доказательств, турникет используется для обозначения «доказуемость» или «выводимость». Например, если $Т$ это формальная теория и $S$ является конкретным предложением на языке теории, тогда

{ displaystyle T vdash S}

Значит это

S

является доказуемо из

Т

.^[6] Это использование продемонстрировано в статье о пропозициональное исчисление. Синтаксическое следствие доказуемости следует противопоставить семантическому следствию, обозначенному двойной турникет символ

{ displaystyle models}

. Один говорит, что

{ displaystyle S}

является семантическим следствием

{ displaystyle T}

, или же

{ displaystyle T models S}

, когда все возможно оценки в котором

{ displaystyle T}

правда,

{ displaystyle S}

тоже верно. Для логики высказываний можно показать, что семантическое следствие

{ displaystyle models}

и выводимость

{ displaystyle vdash}

эквивалентны друг другу. То есть логика высказываний верна (

{ displaystyle vdash}

подразумевает

{ displaystyle models}

) и заполнить (

{ displaystyle models}

подразумевает

{ displaystyle vdash}

)^[7]

в типизированное лямбда-исчисление, турникет используется для отделения допущений при наборе текста от суждения о вводе.^[8]^[9]
В теория категорий, реверсивный турникет ( ${ displaystyle dashv}$ ), как в ${ displaystyle F dashv G}$ , используется, чтобы указать, что функтор $F$ является левый смежный к функтору $грамм$ .^[10] Реже турникет ( ${ displaystyle vdash}$ ), как в ${ displaystyle G vdash F}$ , используется для обозначения того, что функтор $грамм$ является правый смежный к функтору $F$ .^[11]
В APL этот символ называется "правильная линия" и представляет двойственную функцию правого тождества, где оба $Икс$ ⊢ $Y$ и ⊢ $Y$ находятся $Y$ . Перевернутый символ «» называется «левый галс» и представляет аналогичную левую идентичность, где $Икс$ ⊣ $Y$ является $Икс$ и ⊣ $Y$ является $Y$ .^[12]^[13]
В комбинаторика, ${ displaystyle lambda vdash n}$ Значит это $λ$ это раздел целого числа $п$ .^[14]
В Hewlett Packardс HP-41C/резюме/CX и HP-42S серии калькуляторов символ (в кодовой точке 127 в Набор символов FOCAL) называется "символом добавления" и используется для обозначения того, что следующие символы будут добавлены к альфа-регистру, а не заменят существующее содержимое регистра. Этот символ также поддерживается (в кодовой точке 148) в модифицированный вариант из HP Роман-8 набор символов, используемый другими калькуляторами HP.