Турникет (символ)
| Турникет | ||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| ⊢ | ||||||||||||
|
||||||||||||
| Характеристики | ||||||||||||
| Название | right tack | |||||||||||
| Юникод | U+22A2 | |||||||||||
| HTML-код |
⊢ или ⊢ |
|||||||||||
| UTF-16 | 0x22A2 | |||||||||||
| URL-код | %E2%8A%A2 | |||||||||||
| Мнемоника |
⊢ |
|||||||||||
Турникет — в математической логике и информатике символ [math]\displaystyle{ \vdash }[/math] называется «турникетом» из-за его сходства с типичным турникетом, если смотреть сверху. Он также упоминается как «тройник» и часто читается как «даёт», «доказывает», «удовлетворяет» или «влечёт за собой».
В TeX символ турникета [math]\displaystyle{ \vdash }[/math] получается из команды \vdash. В Юникоде символ турникета (\vdash) называется «кнопка вправо» и находится на кодовой позиции U+22A2[1]. Кодовая позиция U+22A6 называется «знак утверждения» (\vdash). На пишущей машинке турникет может состоять из вертикальной полосы (|) и тире (-). В LaTeX есть турникетный пакет, который выдаёт этот знак во многих случаях и способен помещать знаки ниже или выше него в нужных местах.[2]
Смысл
Турникет представляет собой бинарное отношение. Его интерпретация различна в разных контекстах:
- В эпистемологии Пер Мартин-Лоф (1996) анализирует символ [math]\displaystyle{ \vdash }[/math] таким образом: «…Сочетание штриха суждения Фреге | и штриха содержания — стало называться знаком утверждения.»[3] Обозначение Фреге для суждения некоторого содержания A
- [math]\displaystyle{ \vdash A }[/math]:
можно прочитать::"Я знаю, что A-это правда".
- В том же духе условное утверждение
- [math]\displaystyle{ P \vdash Q }[/math]:
может быть прочитано как:
- «Исходя из P, я знаю, что Q»
- В металогике, при построении формальных языков, турникет представляет собой умозаключение (или «выводимость»). Это означает, что он показывает, что одна строка может быть получена из другой за один шаг в соответствии с правилами преобразования (то есть синтаксисом) некоторой заданной формальной системы.[4] Как таковое, выражение
- [math]\displaystyle{ P \vdash Q }[/math]
- означает, что Q выводимо из P в системе.
- В соответствии с его использованием для выводимости, [math]\displaystyle{ \vdash }[/math], за которым следует выражение без чего-либо предшествующего ему, обозначает теорему, то есть выражение может быть выведено из правил с использованием пустого множества аксиом. Как таковое, выражение
- [math]\displaystyle{ \vdash Q }[/math]
- означает, что Q является теоремой в системе.
- В теории доказательств турникет используется для обозначения «доказуемости» или «выводимости». Например, если T — это формальная теория, а S — конкретное предложение на языке теории, то
- [math]\displaystyle{ T \vdash S }[/math]
- означает, что S доказуемо из T.[5] Это использование продемонстрировано в статье о логике высказываний. Синтаксическое следствие доказуемости следует противопоставить семантическому следствию, обозначаемому символом двойного турникета [math]\displaystyle{ \models }[/math]. Он говорит, что [math]\displaystyle{ S }[/math] является семантическим следствием [math]\displaystyle{ T }[/math], или [math]\displaystyle{ T \models S }[/math], когда все возможные оценки, в которых [math]\displaystyle{ T }[/math] истинны, [math]\displaystyle{ S }[/math] также истинны. Для пропозициональной логики можно показать, что семантическое следствие [math]\displaystyle{ \models }[/math] и выводимость [math]\displaystyle{ \vdash }[/math] эквивалентны друг другу. То есть пропозициональная логика является здравой ([math]\displaystyle{ \vdash }[/math] подразумевает [math]\displaystyle{ \models }[/math]) и полной ([math]\displaystyle{ \models }[/math] подразумевает [math]\displaystyle{ \vdash }[/math]).[6]
- В типизированном лямбда-исчислении турникет используется для отделения предположений о типизации от суждения о типизации.[7][8]
- В теории категорий обратный турникет ([math]\displaystyle{ \dashv }[/math]), как и в [math]\displaystyle{ F \dashv G }[/math], используется для указания на то, что функтор F остается сопряженным
с функтором G.[9] В более редких случаях турникет ([math]\displaystyle{ \vdash }[/math]), как в [math]\displaystyle{ G \vdash F }[/math], используется для указания на то, что функтор G непосредственно примыкает к функтору F.[10]
- В APL символ называется «правый галс» и представляет амбивалентную функцию правой идентичности, где и [math]\displaystyle{ X \vdash Y }[/math], и [math]\displaystyle{ \vdash Y }[/math] являются [math]\displaystyle{ Y }[/math]. Обратный символ [math]\displaystyle{ \dashv }[/math] называется «левый галс» и представляет аналогичное левое тождество, где [math]\displaystyle{ X \dashv Y }[/math] — это [math]\displaystyle{ X }[/math], а [math]\displaystyle{ \dashv Y }[/math] — [math]\displaystyle{ Y }[/math].[11][12]
- В комбинаторике, [math]\displaystyle{ \lambda \vdash n }[/math] означает, что [math]\displaystyle{ \lambda }[/math] является разбиением числа [math]\displaystyle{ n }[/math].[13]
- В калькуляторах фирмы Hewlett-Packard серий HP-41C и HP-42S символ (в кодовой точке 127) в FOCAL character set) называется «Добавить символ» и используется для указания на то, что следующие символы будут добавлены в альфа-регистр, а не заменят существующее содержимое регистра. Этот символ также поддерживается (в кодовой точке 148) в модифицированном варианте шрифта HP Roman, используемого в других калькуляторах HP.
- В калькуляторах фирмы Casio серий fx-92 College 2D и fx-92+ Speciale College,[14] символ означает оператор модуля; на ввод [math]\displaystyle{ 5\vdash2 }[/math] будет выведено [math]\displaystyle{ Q=2;R=1 }[/math], где Q частное и R остаток. В других калькуляторах CASIO (таких как бельгийские варианты — калькуляторы fx-92B Speciale College и fx-92B College 2D[15]— где десятичный разделитель представлен точкой вместо запятой), оператор модуля вместо него обозначается как [math]\displaystyle{ \div R }[/math].
См. также
- Двойной турникет (символ) [math]\displaystyle{ \models }[/math]
- Секвенция (теория доказательств)
- Исчисление секвенций
- Список логических символов
- Таблица математических символов
Примечания
- ↑ Unicode standard. Дата обращения: 16 мая 2021. Архивировано 13 мая 2011 года.
- ↑ CTAN Comprehensive TEX Archive Network, Directory - macros/latex/contrib/turnstile. Дата обращения: 16 мая 2021. Архивировано 17 мая 2021 года.
- ↑ Martin-Lof, 1996, pp. 6, 15
- ↑ Chapter 6, Formal Language Theory. Дата обращения: 16 мая 2021. Архивировано 4 апреля 2018 года.
- ↑ Troelstra & Schwichtenberg, 2000
- ↑ Dirk van Dalen, Logic and Structure (1980), Springer, ISBN 3-540-20879-8. See Chapter 1, section 1.5.
- ↑ Peter Selinger, Lecture Notes on the Lambda Calculus. Дата обращения: 16 мая 2021. Архивировано 6 мая 2021 года.
- ↑ Schmidt, 1994
- ↑ adjoint functor in nLab. Дата обращения: 16 мая 2021. Архивировано 13 мая 2021 года.
- ↑ FunctorFact. Functor Fact on Twitter. [твит]. Твиттер (5 July 2016).
- ↑ Iverson, APL dictionary. Дата обращения: 16 мая 2021. Архивировано 25 апреля 2020 года.
- ↑ Iverson, 1987
- ↑ Stanley, Richard P. Enumerative Combinatorics. — 1st. — Cambridge : Cambridge University Press, 1999. — Vol. Vol. 2. — P. 287.
- ↑ fx-92 Speciale College Mode d'emploi. — CASIO COMPUTER CO., LTD., 2015. — P. 12. Архивная копия от 16 апреля 2021 на Wayback Machine
- ↑ Remainder Calculations - Casio fx-92B User Manual [Page 13 | ManualsLib]. www.manualslib.com. Дата обращения: 24 декабря 2020. Архивировано 16 мая 2021 года.
Ссылки
- (1879) «Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens» (Halle).
- (1987) «A Dictionary of APL».
- (1996) «On the meanings of the logical constants and the justifications of the logical laws». Nordic Journal of Philosophical Logic 1 (1): 11–60. (Lecture notes to a short course at Universita degli Studi di Siena, April 1983.)
- (1994) «The Structure of Typed Programming Languages» (MIT Press).
- (2000) «Basic Proof Theory» (Cambridge University Press).
| |
