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

Перейти к навигацииПерейти к поиску
Турникет
Характеристики
Названиеright tack
ЮникодU+22A2
HTML-код⊢ или ⊢
UTF-16 0x22A2
URL-код %E2%8A%A2
Мнемоника⊢
⊢

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

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

Смысл

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

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

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

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

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

«Исходя из P, я знаю, что Q»
означает, что Q выводимо из P в системе.
В соответствии с его использованием для выводимости, , за которым следует выражение без чего-либо предшествующего ему, обозначает теорему, то есть выражение может быть выведено из правил с использованием пустого множества аксиом. Как таковое, выражение
означает, что Q является теоремой в системе.
  • В теории доказательств турникет используется для обозначения «доказуемости» или «выводимости». Например, если T — это формальная теория[англ.], а S — конкретное предложение на языке теории, то
означает, что S доказуемо из T.[5] Это использование продемонстрировано в статье о логике высказываний. Синтаксическое следствие доказуемости следует противопоставить семантическому следствию, обозначаемому символом двойного турникета[англ.] . Он говорит, что является семантическим следствием , или , когда все возможные оценки[англ.], в которых истинны, также истинны. Для пропозициональной логики можно показать, что семантическое следствие и выводимость эквивалентны друг другу. То есть пропозициональная логика является здравой ( подразумевает ) и полной ( подразумевает ).[6]

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

  • В APL символ называется «правый галс» и представляет амбивалентную функцию правой идентичности, где и , и являются . Обратный символ называется «левый галс» и представляет аналогичное левое тождество, где  — это , а  — .[11][12]
  • В комбинаторике, означает, что является разбиением числа .[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] символ означает оператор модуля[англ.]; на ввод будет выведено , где Q частное и R остаток. В других калькуляторах CASIO (таких как бельгийские варианты — калькуляторы fx-92B Speciale College и fx-92B College 2D[15]— где десятичный разделитель представлен точкой вместо запятой), оператор модуля вместо него обозначается как .

См. также

Примечания

  1. Unicode standard. Дата обращения: 16 мая 2021. Архивировано 13 мая 2011 года.
  2. CTAN Comprehensive TEX Archive Network, Directory - macros/latex/contrib/turnstile. Дата обращения: 16 мая 2021. Архивировано 17 мая 2021 года.
  3. Martin-Lof, 1996, pp. 6, 15
  4. Chapter 6, Formal Language Theory. Дата обращения: 16 мая 2021. Архивировано 4 апреля 2018 года.
  5. Troelstra & Schwichtenberg, 2000
  6. Dirk van Dalen, Logic and Structure (1980), Springer, ISBN 3-540-20879-8. See Chapter 1, section 1.5.
  7. Peter Selinger, Lecture Notes on the Lambda Calculus. Дата обращения: 16 мая 2021. Архивировано 6 мая 2021 года.
  8. Schmidt, 1994
  9. adjoint functor in nLab. Дата обращения: 16 мая 2021. Архивировано 13 мая 2021 года.
  10. FunctorFact. Functor Fact on Twitter. [твит]. Твиттер (5 июля 2016).
  11. Iverson, APL dictionary. Дата обращения: 16 мая 2021. Архивировано 25 апреля 2020 года.
  12. Iverson, 1987
  13. Stanley, Richard P. Enumerative Combinatorics. — 1st. — Cambridge : Cambridge University Press, 1999. — Vol. Vol. 2. — P. 287.
  14. fx-92 Speciale College Mode d'emploi. — CASIO COMPUTER CO., LTD., 2015. — P. 12. Архивная копия от 16 апреля 2021 на Wayback Machine
  15. Remainder Calculations - Casio fx-92B User Manual [Page 13] | ManualsLib. www.manualslib.com. Дата обращения: 24 декабря 2020. Архивировано 16 мая 2021 года.

Ссылки

  • 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= ()