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

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

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

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

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

• В гносеологии , Мартин-Лёф (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=( помощь )