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

Турникет (символ) — в математической логике и информатике символ $\vdash$ называется "турникетом" из-за его сходства с типичным турникетом, если смотреть сверху. Он также упоминается как "тройник" и часто читается как "дает", "доказывает", "удовлетворяет" или "влечет за собой".

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

Смысл

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

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

$\vdash A$:

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

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

$P\vdash Q$:

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

"От P, я знаю, что Q"

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

(т. е. синтаксисом) некоторой заданной формальной системы. Как таковое, выражение

$P\vdash Q$

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

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

$\vdash Q$

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

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

$T\vdash S$

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

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

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

• В APL символ называется "правый галс" и представляет амбивалентную функцию правой идентичности, где и $X\vdash Y$, и $\vdash Y$ являются $Y$. Обратный символ $\dashv$ называется "левый галс" и представляет аналогичное левое тождество, где $X\dashv Y$ - это $X$, а $\dashv Y$ - $Y$.
• В комбинаторике, $\lambda \vdash n$ означает, что $\lambda$ является разбиением числа $n$.
• В калькуляторах фирмы Hewlett-Packard серий HP-41C и HP-42S символ (в кодовой точке 127) в FOCAL character set) называется "Добавить символ" и используется для указания на то, что следующие символы будут добавлены в альфа-регистр, а не заменят существующее содержимое регистра. Этот символ также поддерживается (в кодовой точке 148) в модифицированном варианте шрифта HP Roman, используемого в других калькуляторах HP.
• В калькуляторах фирмы Casio серий fx-92 College 2D и fx-92+ Speciale College, символ означает оператор модуля; на ввод $5\vdash 2$ будет выведено $Q=2;R=1$, где Q частное и R остаток. В других калькуляторах CASIO (таких как бельгийские варианты — калькуляторы fx-92B Speciale College и fx-92B College 2D— где десятичный разделитель представлен точкой вместо запятой), оператор модуля вместо него обозначается как $\div R$.

Похожие графемы

• (U+A714) Modifier Letter Mid Left-Stem Tone Bar
• (U+251C) Box Drawings Light Vertical And Right
• (U+314F) Korean Ah
• (U+0370) Greek Capital Letter Heta
• (U+0371) Greek Small Letter Heta
• (U+2C75) Latin Capital Letter Half H
• (U+2C76) Latin Small Letter Half H
• (U+23AB) Right curly bracket

См. также

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

Ссылки

• Frege, Gottlob (1879). "Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens". Halle. {{cite journal}}: Cite journal требует |journal= (справка)
• Iverson, Kenneth (1987). "A Dictionary of APL". {{cite journal}}: Cite journal требует |journal= (справка)
• Martin-Lof, Per (1996). "On the meanings of the logical constants and the justifications of the logical laws" (PDF). Nordic Journal of Philosophical Logic. 1 (1): 11—60. (Lecture notes to a short course at Universita degli Studi di Siena, April 1983.)
• Schmidt, David (1994). "The Structure of Typed Programming Languages". MIT Press. ISBN 0-262-19349-3. {{cite journal}}: Cite journal требует |journal= (справка)
• Troelstra, A. S.; Schwichtenberg, H. (2000). "Basic Proof Theory" (2nd ed.). Cambridge University Press. ISBN 978-0-521-77911-1. {{cite journal}}: Cite journal требует |journal= (справка)