Просмотр кода страницы Турникет (символ)

{{Другие значения}}
{{Похожие символы|Ⱶ}}
{{Карточка графемы
|Название       = Турникет
|Изображение    = 
|Оригинал       = right tack
|HTML           = 8866
|Мнемоника      = RightTee;<br>&amp;vdash
}}
'''Турникет''' — в [[Математическая логика|математической логике]] и [[Информатика|информатике]] символ <math>\vdash</math> называется «турникетом» из-за его сходства с типичным [[турникет]]ом, если смотреть сверху. Он также упоминается как «тройник» и часто читается как «даёт», «доказывает», «удовлетворяет» или «влечёт за собой».

В [[TeX]] символ турникета <math>\vdash</math> получается из команды <tt>\vdash</tt>. В [[Юникод]]е символ турникета (<big>\vdash</big>) называется «кнопка вправо» и находится на кодовой позиции U+22A2<ref>{{Cite web |url=http://unicode.org/charts/PDF/U2200.pdf |title=Unicode standard |access-date=2021-05-16 |archive-date=2011-05-13 |archive-url=https://web.archive.org/web/20110513234345/http://www.unicode.org/charts/PDF/U2200.pdf |deadlink=no }}</ref>. Кодовая позиция U+22A6 называется «знак утверждения» (<big>\vdash</big>). На пишущей машинке турникет может состоять из вертикальной полосы (|) и тире (-). В [[LaTeX]] есть турникетный пакет, который выдаёт этот знак во многих случаях и способен помещать знаки ниже или выше него в нужных местах.<ref>{{Cite web |url=http://www.ctan.org/tex-archive/macros/latex/contrib/turnstile |title=CTAN Comprehensive TEX Archive Network, Directory - macros/latex/contrib/turnstile |access-date=2021-05-16 |archive-date=2021-05-17 |archive-url=https://web.archive.org/web/20210517012901/https://ctan.org/tex-archive/macros/latex/contrib/turnstile |deadlink=no }}</ref>

== Смысл ==
Турникет представляет собой [[бинарное отношение]]. Его {{iw|Интерпретация (логика)|интерпретация|en|Interpretation (logic)}} различна в разных контекстах:

* В [[Эпистемология|эпистемологии]] [[Мартин-Лёф, Пер|Пер Мартин-Лоф]] (1996) анализирует символ <math>\vdash</math> таким образом: «…Сочетание штриха суждения Фреге | и штриха содержания — стало называться знаком утверждения.»<ref>{{harvnb|Martin-Lof|1996|pp=6, 15}}</ref> Обозначение Фреге для [[Суждение (математическая логика)|суждения]] некоторого содержания {{mvar|A}}
:: <math>\vdash A</math>:
можно прочитать::"Я знаю, что {{mvar|A}}-это правда".
: В том же духе условное утверждение
:: <math>P \vdash Q</math>:
может быть прочитано как:
:: «Исходя из {{mvar|P}}, я знаю, что {{mvar|Q}}»
* В [[Металогика|металогике]], при построении [[Формальный язык|формальных языков]], турникет представляет собой [[умозаключение]] (или «выводимость»). Это означает, что он показывает, что одна строка может быть {{iw|Формальное доказательство|получена|en|Formal proof}} из другой за один шаг в соответствии с [[Правило вывода|правилами преобразования]] (то есть [[Синтаксис (логика)|синтаксисом]]) некоторой заданной [[Формальная система|формальной системы]].<ref>{{Cite web |url=http://dingo.sbs.arizona.edu/~hammond/ling178-sp06/mathCh6.pdf |title=Chapter 6, Formal Language Theory |access-date=2021-05-16 |archive-date=2018-04-04 |archive-url=https://web.archive.org/web/20180404070001/http://dingo.sbs.arizona.edu/~hammond/ling178-sp06/mathCh6.pdf |deadlink=no }}</ref> Как таковое, выражение
:: <math>P \vdash Q</math>
: означает, что {{mvar|Q}} выводимо из {{mvar|P}} в системе.
: В соответствии с его использованием для выводимости, <math>\vdash</math>, за которым следует выражение без чего-либо предшествующего ему, обозначает [[Теорема|теорему]], то есть выражение может быть выведено из правил с использованием [[Пустое множество|пустого множества]] [[Аксиома|аксиом]]. Как таковое, выражение
:: <math>\vdash Q</math>
: означает, что {{mvar|Q}} является теоремой в системе.
* В [[Теория доказательств|теории доказательств]] турникет используется для обозначения «доказуемости» или «выводимости». Например, если {{mvar|T}} — это {{iw|Теория (математическая логика)|формальная теория|en|Theory (mathematical logic)}}, а {{mvar|S}} — конкретное предложение на языке теории, то
:: <math>T \vdash S</math>
: означает, что {{mvar|S}} доказуемо из {{mvar|T}}.<ref>{{harvnb|Troelstra| Schwichtenberg| 2000}}</ref> Это использование продемонстрировано в статье о [[Логика высказываний|логике высказываний]]. Синтаксическое следствие доказуемости следует противопоставить семантическому следствию, обозначаемому символом {{iw|Двойной турникет (символ)|двойного турникета|en|Double turnstile}} <math>\models</math>. Он говорит, что <math>S</math> является семантическим следствием <math>T</math>, или <math>T \models S</math>, когда все возможные {{iw|Оценка (логика)|оценки|en|Valuation (logic)}}, в которых <math>T</math> истинны, <math>S</math> также истинны. Для пропозициональной логики можно показать, что семантическое следствие <math>\models</math> и выводимость <math>\vdash</math> эквивалентны друг другу. То есть пропозициональная логика является здравой (<math>\vdash</math> подразумевает <math>\models</math>) и полной (<math>\models</math> подразумевает <math>\vdash</math>).<ref>Dirk van Dalen, ''Logic and Structure'' (1980), Springer, {{ISBN|3-540-20879-8}}. ''See Chapter 1, section 1.5.''</ref>
* В [[Типизированное лямбда-исчисление|типизированном лямбда-исчислении]] турникет используется для отделения предположений о типизации от суждения о типизации.<ref>{{Cite web |url=http://www.mscs.dal.ca/~selinger/papers/lambdanotes.pdf |title=Peter Selinger, Lecture Notes on the Lambda Calculus |access-date=2021-05-16 |archive-date=2021-05-06 |archive-url=https://web.archive.org/web/20210506152957/https://www.mscs.dal.ca/~selinger/papers/lambdanotes.pdf |deadlink=no }}</ref><ref>{{harvnb|Schmidt|1994}}</ref>
* В [[Теория категорий|теории категорий]] обратный турникет (<math>\dashv</math>), как и в <math>F \dashv G</math>, используется для указания на то, что [[Функтор (математика)|функтор]] {{mvar|F}} остается [[Сопряжённые функторы|сопряженным]]
с функтором {{mvar|G}}.<ref>{{Cite web |url=https://ncatlab.org/nlab/show/adjoint+functor |title=adjoint functor in nLab |access-date=2021-05-16 |archive-date=2021-05-13 |archive-url=https://web.archive.org/web/20210513205037/https://www.ncatlab.org/nlab/show/adjoint+functor |deadlink=no }}</ref> В более редких случаях турникет (<math>\vdash</math>), как в <math>G \vdash F</math>, используется для указания на то, что функтор {{mvar|G}}
[[Сопряжённые функторы|непосредственно примыкает]] к функтору {{mvar|F}}.<ref>{{cite tweet |user=FunctorFact |number=750413999649546245 |date=2016-07-05 |title=Functor Fact on Twitter }}</ref>
* В [[APL (язык программирования)|APL]] символ называется «правый галс» и представляет амбивалентную функцию правой идентичности, где и <math>X \vdash Y</math>, и <math>\vdash Y</math> являются <math>Y</math>. Обратный символ <math>\dashv</math> называется «левый галс» и представляет аналогичное левое тождество, где <math>X \dashv Y</math> — это <math>X</math>, а <math>\dashv Y</math> — <math>Y</math>.<ref>{{Cite web |url=http://www.jsoftware.com/papers/APLDictionary.htm |title=Iverson, APL dictionary |access-date=2021-05-16 |archive-date=2020-04-25 |archive-url=https://web.archive.org/web/20200425181643/http://www.jsoftware.com/papers/APLDictionary.htm |deadlink=no }}</ref><ref>{{harvnb|Iverson|1987}}</ref>
* В [[Комбинаторика|комбинаторике]], <math>\lambda \vdash n</math> означает, что <math>\lambda</math> является [[Разбиение числа|разбиением]] числа <math>n</math>.<ref>{{cite book |page=287 |last=Stanley |first=Richard P. |title=Enumerative Combinatorics |edition=1st |volume=Vol. 2 |location=Cambridge |publisher=Cambridge University Press |year=1999 }}</ref>
* В калькуляторах фирмы [[Hewlett-Packard]] серий {{iw|HP-41C|HP-41C|en|HP-41C}} и {{iw|HP-42S|HP-42S|en|HP-42S}} символ (в кодовой точке 127) в {{iw|FOCAL character set|FOCAL character set|en|FOCAL character set}}) называется «Добавить символ» и используется для указания на то, что следующие символы будут добавлены в альфа-регистр, а не заменят существующее содержимое регистра. Этот символ также поддерживается (в кодовой точке 148) в модифицированном варианте шрифта {{iw|HP Roman|HP Roman|en|HP Roman}}, используемого в других калькуляторах HP.
* В калькуляторах фирмы [[Casio]] серий fx-92 College 2D и fx-92+ Speciale College,<ref>{{Cite book|url=https://support.casio.com/storage/fr/manual/pdf/FR/004/fx-92%20Speciale_College_FR.pdf|title=fx-92 Speciale College Mode d'emploi|publisher=[[CASIO]] COMPUTER CO., LTD.|year=2015|pages=12}} {{Wayback|url=https://support.casio.com/storage/fr/manual/pdf/FR/004/fx-92%20Speciale_College_FR.pdf |date=20210416161749 }}</ref> символ означает {{iw|Оператор модуля|оператор модуля|en|Modulo operation}}; на ввод <math>5\vdash2</math> будет выведено <math>Q=2;R=1
</math>, где {{Mvar|Q}} [[Деление (математика)|частное]] и {{Mvar|R}} [[остаток от деления|остаток]]. В других калькуляторах CASIO (таких как [[Бельгия|бельгийские]] варианты — калькуляторы fx-92B Speciale College и fx-92B College 2D<ref>{{Cite web|title=Remainder Calculations - Casio fx-92B User Manual [Page 13] {{!}} ManualsLib|url=https://www.manualslib.com/manual/564947/Casio-Fx-92b.html?page=13#manual|access-date=2020-12-24|website=www.manualslib.com|archive-date=2021-05-16|archive-url=https://web.archive.org/web/20210516191156/https://www.manualslib.com/manual/564947/Casio-Fx-92b.html?page=13#manual|deadlink=no}}</ref>— где [[десятичный разделитель]] представлен точкой вместо запятой), оператор модуля вместо него обозначается как <math>\div R</math>.

== См. также ==
* {{iw|Двойной турникет (символ)|Двойной турникет (символ)|en|Double turnstile}} <math>\models</math>
* [[Секвенция (теория доказательств)]]
* [[Исчисление секвенций]]
* [[Список логических символов]]
* [[Таблица математических символов]]

== Примечания ==
{{Примечания}}

== Ссылки ==
* {{cite journal |author-last=Frege |author-first=Gottlob |title=Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens |publisher=Halle |date=1879}}
* {{cite journal |author-last=Iverson |author-first=Kenneth |title=A Dictionary of APL |date=1987|ref=Iverson}}
* {{cite journal |author-last=Martin-Lof |author-first=Per |url=http://docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf |title=On the meanings of the logical constants and the justifications of the logical laws |journal=Nordic Journal of Philosophical Logic |volume=1 |issue=1 |date=1996 |pages=11–60|ref=Martin-Lof}} (Lecture notes to a short course at Universita degli Studi di Siena, April 1983.)
* {{cite journal |author-last=Schmidt |author-first=David |title=The Structure of Typed Programming Languages |url=https://archive.org/details/structureoftyped0000schm |publisher=[[MIT Press]] |date=1994 |isbn=0-262-19349-3|ref=Schmidt}}
* {{cite journal |author-last1=Troelstra |author-first1=A. S. |author-last2=Schwichtenberg |author-first2=H. |title=Basic Proof Theory |edition=2nd |publisher=[[Cambridge University Press]] |date=2000 |isbn=978-0-521-77911-1|ref=TroelstraSchwichtenberg}}

{{Математические знаки}}

[[Категория:Математическая логика]]
[[Категория:Логические символы]]
[[Категория:Дедуктивные рассуждения]]
[[Категория:Теория доказательств]]
[[Категория:Логическое следствие]]