Турникет (символ)

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

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

• В эпистемологии Пер Мартин - Лёф (1996) анализирует символ следующим образом: «...[Т]о сочетании Urteilsstrich Фреге , штриха суждения [|], и Inhaltsstrich , штриха содержания [—], стало называться знаком утверждения». ^[1] Обозначение Фреге для суждения некоторого содержания A${\displaystyle \vdash}$

${\displaystyle \vdash А}$

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

Я знаю, что А — правда . ^[2]

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

${\displaystyle P\vdash Q}$

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

Из P я знаю, что Q

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

${\displaystyle P\vdash Q}$

означает, что Q выводится из P в системе.

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

${\displaystyle \vdash Q}$

означает, что Q является теоремой в системе.

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

${\displaystyle T\vdash S}$

означает, что S доказуемо из T . ^[4] Такое использование продемонстрировано в статье о пропозициональном исчислении . Синтаксическое следствие доказуемости следует противопоставить семантическому следствию, обозначенному символом двойного турникета . Говорят, что является семантическим следствием , или , когда все возможные оценки , в которых является истинным, также являются истинными. Для пропозициональной логики можно показать, что семантическое следствие и выводимость эквивалентны друг другу. То есть пропозициональная логика является обоснованной ( подразумевает ) и полной ( подразумевает ) ^[5]${\displaystyle \модели}$${\displaystyle S}$${\displaystyle Т}$${\displaystyle T\models S}$${\displaystyle Т}$${\displaystyle S}$${\displaystyle \модели}$${\displaystyle \vdash}$${\displaystyle \vdash}$${\displaystyle \модели}$${\displaystyle \модели}$${\displaystyle \vdash}$

• В исчислении последовательностей турникет используется для обозначения секвенции . Секвенция утверждает, что если все антецеденты истинны, то по крайней мере один из консеквентов должен быть истинным.${\displaystyle A_{1},\,\точки ,A_{м}\,\vdash \,B_{1},\,\точки ,B_{н}}$${\displaystyle A_{1},\,\точки ,A_{м}}$${\displaystyle B_{1},\,\точки ,B_{n}}$
• В типизированном лямбда-исчислении турникет используется для отделения предположений о типизации от суждений о типизации. ^{[6] [7]}
• В теории категорий перевернутый турникет ( ), как в , используется для указания того, что функтор F является левым сопряженным к функтору G . ^[8] Реже турникет ( ), как в , используется для указания того, что функтор G является правым сопряженным к функтору F . ^[9]${\displaystyle \dashv}$${\displaystyle F\dashv G}$ ${\displaystyle \vdash}$${\displaystyle G\vdash F}$
• В APL символ называется «правый галс» и представляет собой амбивалентную правую тождественную функцию, где и X ⊢ Y и ⊢ Y являются Y. Обратный символ «⊣» называется «левый галс» и представляет собой аналогичную левую тождественность, где X ⊣ Y является X , а ⊣ Y является Y. ^{[10] [11} ]
• В комбинаторике означает, что λ является разбиением целого числа n . ^[12]${\displaystyle \lambda \vdash n}$
• В калькуляторах серий HP-41C / CV / CX и HP-42S компании Hewlett-Packard этот символ (в кодовой точке 127 в наборе символов FOCAL ) называется «Append character» и используется для указания того, что следующие символы будут добавлены в альфа-регистр, а не заменят существующее содержимое регистра. Этот символ также поддерживается (в кодовой точке 148) в модифицированном варианте набора символов HP Roman-8 , используемого другими калькуляторами HP.
• На калькуляторах Casio fx-92 Collège 2D и fx-92+ Spéciale Collège ^[13] символ представляет оператор деления по модулю ; ввод даст ответ , где Q — частное , а R — остаток .${\displaystyle 5\vdash 2}$${\displaystyle Q=2;R=1}$
• В теории моделей означает , что каждая модель является моделью .${\displaystyle \varphi \vdash \psi}$${\displaystyle \varphi}$${\displaystyle \пси}$${\displaystyle \varphi}$${\displaystyle \пси}$

В TeX символ турникета получается из команды \vdash . ${\displaystyle \vdash}$

В Unicode символ турникета ( ⊢ ) называется правым галсом и находится в кодовой точке U+22A2. ^[14] (Кодовая точка U+22A6 называется знаком утверждения ( ⊦ ).)

• U+22A2 ⊢ ПРАВЫЙ ТАК ( ⊢, ⊢ )
  • = турникет
  • = доказывает, подразумевает, дает
  • = сокращаемый
• U+22A3 ⊣ ЛЕВЫЙ ГАЛК ( ⊣, ⊣ )
  • = обратный турникет
  • = не теорема, не приводит к
• U+22AC ⊬ НЕ ДОКАЗЫВАЕТ ( ⊬ )
  • ≡ 22A2⊢ 0338$̸

На пишущей машинке турникет может быть составлен из вертикальной черты (|) и тире (–).

В LaTeX есть пакет турникета, который выдает этот знак разными способами и способен размещать метки под ним или над ним в нужных местах. ^[15]

• ꜔ (U+A714) Модификатор Буква Середина Левого Штиля Тоновая полоса
• ├ (U+251C) Рисунки ящиков светлые вертикальные и правые
• ㅏ (U+314F) Хангыль, буква A
• Ͱ (U+0370) Греческая заглавная буква Хета
• ͱ (U+0371) Греческая строчная буква Хета
• Ⱶ (U+2C75) Латинская заглавная буква половина H
• ⱶ (U+2C76) Латинская строчная буква половина H
• ⎬ (U+23AC) Средняя часть правой фигурной скобки

• Двойной турникет ⊨
• Список логических символов
• Список математических символов

• Фреге, Готтлоб (1879). Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens . Галле.
• Айверсон, Кеннет (1987). Словарь APL .
• Мартин-Лёф, Пер (1996). «О значениях логических констант и обоснованиях логических законов» (PDF) . Nordic Journal of Philosophical Logic . 1 (1): 11– 60.(Конспект лекций к краткому курсу в Университете Студи ди Сиены, апрель 1983 г.)
• Шмидт, Дэвид (1994). Структура типизированных языков программирования . MIT Press . ISBN 0-262-19349-3.
• Troelstra, AS ; Schwichtenberg, H. (2000). Базовая теория доказательств (2-е изд.). Cambridge University Press . ISBN 978-0-521-77911-1.