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

Шаблон:Другие значения Шаблон:Похожие символы Шаблон:Карточка графемы Турникет — в математической логике и информатике символ $⊢$ называется «турникетом» из-за его сходства с типичным турникетом, если смотреть сверху. Он также упоминается как «тройник» и часто читается как «даёт», «доказывает», «удовлетворяет» или «влечёт за собой».

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

Смысл

Турникет представляет собой бинарное отношение. Его Шаблон:Iw различна в разных контекстах:

• В эпистемологии Пер Мартин-Лоф (1996) анализирует символ $⊢$ таким образом: «…Сочетание штриха суждения Фреге | и штриха содержания — стало называться знаком утверждения.» Обозначение Фреге для суждения некоторого содержания Шаблон:Mvar

$⊢A$:

можно прочитать::"Я знаю, что Шаблон:Mvar-это правда".

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

$P⊢Q$:

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

«Исходя из Шаблон:Mvar, я знаю, что Шаблон:Mvar»

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

$P⊢Q$

означает, что Шаблон:Mvar выводимо из Шаблон:Mvar в системе.

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

$⊢Q$

означает, что Шаблон:Mvar является теоремой в системе.

• В теории доказательств турникет используется для обозначения «доказуемости» или «выводимости». Например, если Шаблон:Mvar — это Шаблон:Iw, а Шаблон:Mvar — конкретное предложение на языке теории, то

$T⊢S$

означает, что Шаблон:Mvar доказуемо из Шаблон:Mvar. Это использование продемонстрировано в статье о логике высказываний. Синтаксическое следствие доказуемости следует противопоставить семантическому следствию, обозначаемому символом Шаблон:Iw $\models$. Он говорит, что $S$ является семантическим следствием $T$, или $T\models S$, когда все возможные Шаблон:Iw, в которых $T$ истинны, $S$ также истинны. Для пропозициональной логики можно показать, что семантическое следствие $\models$ и выводимость $⊢$ эквивалентны друг другу. То есть пропозициональная логика является здравой ($⊢$ подразумевает $\models$) и полной ($\models$ подразумевает $⊢$).

• В типизированном лямбда-исчислении турникет используется для отделения предположений о типизации от суждения о типизации.
• В теории категорий обратный турникет ($⊣$), как и в $F⊣G$, используется для указания на то, что функтор Шаблон:Mvar остается сопряженным

с функтором Шаблон:Mvar. В более редких случаях турникет ($⊢$), как в $G⊢F$, используется для указания на то, что функтор Шаблон:Mvar непосредственно примыкает к функтору Шаблон:Mvar.

• В APL символ называется «правый галс» и представляет амбивалентную функцию правой идентичности, где и $X⊢Y$, и $⊢Y$ являются $Y$. Обратный символ $⊣$ называется «левый галс» и представляет аналогичное левое тождество, где $X⊣Y$ — это $X$, а $⊣Y$ — $Y$.
• В комбинаторике, $\lambda ⊢n$ означает, что $\lambda$ является разбиением числа $n$.
• В калькуляторах фирмы Hewlett-Packard серий Шаблон:Iw и Шаблон:Iw символ (в кодовой точке 127) в Шаблон:Iw) называется «Добавить символ» и используется для указания на то, что следующие символы будут добавлены в альфа-регистр, а не заменят существующее содержимое регистра. Этот символ также поддерживается (в кодовой точке 148) в модифицированном варианте шрифта Шаблон:Iw, используемого в других калькуляторах HP.
• В калькуляторах фирмы Casio серий fx-92 College 2D и fx-92+ Speciale College, символ означает Шаблон:Iw; на ввод $5⊢2$ будет выведено $Q=2;R=1$, где Шаблон:Mvar частное и Шаблон:Mvar остаток. В других калькуляторах CASIO (таких как бельгийские варианты — калькуляторы fx-92B Speciale College и fx-92B College 2D— где десятичный разделитель представлен точкой вместо запятой), оператор модуля вместо него обозначается как $÷R$.

См. также

• Шаблон:Iw $\models$
• Секвенция (теория доказательств)
• Исчисление секвенций
• Список логических символов
• Таблица математических символов

Ссылки

• Шаблон:Cite journal
• Шаблон:Cite journal
• Шаблон:Cite journal (Lecture notes to a short course at Universita degli Studi di Siena, April 1983.)
• Шаблон:Cite journal
• Шаблон:Cite journal