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

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

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

• 1 Интерпретации
• 2 Подобные графемы
• 3 Смотрите также
• 4 Примечания
• 5 использованная литература

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

• В гносеологии, Мартин-Лёф (1996) анализирует символ таким образом:»... [T] он сочетание Фреге Urteilsstrich, решение инсульт [|], и Inhaltsstrich, инсульт содержания [-], стал называть знак утверждения. " Обозначение Фреге для суждения некоторого содержания A${\ displaystyle \ vdash}$

${\ displaystyle \ vdash A}$

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

Я знаю, что А правда.

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

${\ displaystyle P \ vdash Q}$

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

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

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

${\ displaystyle P \ vdash Q}$

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

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

${\ displaystyle \ vdash Q}$

означает, что Q - теорема в системе.

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

${\ displaystyle T \ vdash S}$

означает, что S является доказуемо из T. Это использование демонстрируется в статье, посвященной исчислению высказываний. Синтаксическое следствие доказуемости должно быть противопоставлено семантическому следствию, обозначенному двойным символом турникета. Один говорит, что это семантическое следствие, или, когда все возможные оценки, в которых верны, также верны. Для логики высказываний можно показать, что семантическое следствие и выводимость эквивалентны друг другу. То есть логика высказываний является правильной ( подразумевает) и полной ( подразумевает).${\ 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}$

• В типизированном лямбда-исчислении турникет используется для отделения допущений при наборе текста от оценки набора.
• В теории категорий, инверсный турникет (), как и в, используются для указания того, что функтор F является левым сопряженным к функтору G. Реже, турникет (), как, используется, чтобы указать, что функтор G является сопряженным справа функтора F.${\ displaystyle \ dashv}$${\ displaystyle F \ dashv G}$ ${\ displaystyle \ vdash}$${\ displaystyle G \ vdash F}$
• В APL символ называется «правый галс» и представляет собой двойственную правильную функцию тождества, где оба Х ⊢ Y и ⊢ Y является Y. Обращенно символ «⊣» называется «левый галс» и представляет собой аналогичную левую идентичность, где Х ⊣ Y является Х и ⊣ Y является Y.
• В комбинаторике, означает, что λ является разбиение целого числа п.${\ displaystyle \ lambda \ vdash n}$
• В Hewlett-Packard «с HP-41C / CV / CX и HP-42S серии калькуляторов, символ (в точке 127 кода в FOCAL наборе символов ) называется„Append характер“и используется для указания того, что следующие символы быть добавленным к альфа-регистру, а не заменять существующее содержимое регистра. Символ также поддерживается (в кодовой точке 148) в модифицированном варианте осуществления HP Roman-8 набор символов, используемых другими вычислителей HP.
• На калькуляторах Casio fx-92 Collège 2D и fx-92 + Spéciale Collège символ представляет собой оператор по модулю ; ввод даст ответ, где Q - частное, а R - остаток. На других калькуляторах CASIO (например, на бельгийские вариантах-на FX-9 SPECIALE Collège и FX-92B Коллеж 2D вычислителях-где десятичный разделитель представлен как точку вместо запятой), оператор по модулю представлен ÷ R вместо.${\ displaystyle 5 \ vdash 2}$${\ Displaystyle Q = 2; R = 1}$

• ꜔ (U + A714) Буква-модификатор Средняя левая полоса тона
• ├ (U + 251C) Чертежи светлой рамки по вертикали и справа
• ㅏ (U + 314F) Корейский Ач
• Ͱ (U + 0370) Греческая заглавная буква хета
• ͱ (U + 0371) Греческая строчная буква хета
• Ⱶ (U + 2C75) Заглавная латинская буква половина H
• ⱶ (U + 2C76) Строчная латинская буква половина H
• ⎬ (U + 23AB) Правая фигурная скобка

• Двойной турникет ${\ displaystyle \ models}$
• Секвент
• Последовательное исчисление
• Список логических символов
• Список математических символов

• Фреге, Готтлоб (1879). "Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens". Галле. Цитировать журнал требует |journal=( помощь )
• Айверсон, Кеннет (1987). «Словарь АПЛ». Цитировать журнал требует |journal=( помощь )
• Мартин-Лёф, Пер (1996). «О значениях логических констант и обоснованиях логических законов» (PDF). Северный журнал философской логики. 1 (1): 11–60. (Конспект лекций к короткому курсу в Università degli Studi di Siena, апрель 1983 г.)
• Шмидт, Дэвид (1994). «Структура типизированных языков программирования». MIT Press. ISBN   0-262-19349-3. Цитировать журнал требует |journal=( помощь )
• Troelstra, AS ; Швихтенберг, Х. (2000). "Основная теория доказательств" (2-е изд.). Издательство Кембриджского университета. ISBN   978-0-521-77911-1. Цитировать журнал требует |journal=( помощь )