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

Турникет — в математической логике и информатике символ $⊢<!--\; ⊢\; -->$$\vdash$ называется «турникетом» из-за его сходства с типичным турникетом, если смотреть сверху. Он также упоминается как «тройник» и часто читается как «даёт», «доказывает», «удовлетворяет» или «влечёт за собой».

Турникет
⊢
◄ ⊞ ⊟ ⊠ ⊡ ⊢ ⊣ ⊤ ⊥ ⊦ ►
Характеристики
Название	right tack
Юникод	U+22A2
HTML-код	⊢ или ⊢
UTF-16	0x22A2
URL-код	%E2%8A%A2
Мнемоника	⊢ ⊢

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

СмыслПравить

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

• В эпистемологии Пер Мартин-Лоф (1996) анализирует символ $⊢<!--\; ⊢\; -->$$\vdash$  таким образом: «…Сочетание штриха суждения Фреге | и штриха содержания — стало называться знаком утверждения.» Обозначение Фреге для суждения^[en] некоторого содержания A

$⊢<!--\; ⊢\; -->A$$\vdash A$ :

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

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

$P⊢<!--\; ⊢\; -->Q$$P\vdash Q$ :

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

«Исходя из P, я знаю, что Q»

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

$P⊢<!--\; ⊢\; -->Q$$P\vdash Q$ 

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

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

$⊢<!--\; ⊢\; -->Q$$\vdash Q$ 

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

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

$T⊢<!--\; ⊢\; -->S$$T\vdash S$ 

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

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

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

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

См. такжеПравить

• Двойной турникет (символ)^[en] $\models <!--\; \models \; -->$$\models$ 
• Секвенция (теория доказательств)
• Исчисление секвенций
• Список логических символов
• Таблица математических символов

СсылкиПравить

• Frege, Gottlob (1879). “Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens”. Halle.
• Iverson, Kenneth (1987). “A Dictionary of APL”.
• 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.
• Troelstra, A. S.; Schwichtenberg, H. (2000). “Basic Proof Theory” (2nd ed.). Cambridge University Press. ISBN 978-0-521-77911-1.