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

Символ в математической логике

В математической логике и информатике символ ⊢ ( ) получил название «турникет » из-за сходства с типичным турникетом , если смотреть сверху. Его также называют « тройник » и часто читают как «приводит», «доказывает», «удовлетворяет» или «влечет». ${\displaystyle \vdash }$

Интерпретации

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

• В эпистемологии Пер Мартин - Лёф (1996) анализирует символ следующим образом: «...[Т]о сочетании Urteilsstrich Фреге , штриха суждения [|], и Inhaltsstrich , штриха содержания [—], стало называться знаком утверждения». ^[1] Обозначение Фреге для суждения некоторого содержания A ${\displaystyle \vdash }$

${\displaystyle \vdash A}$

затем можно прочитать

Я знаю, что А — правда . ^[2]

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

${\displaystyle P\vdash Q}$

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

Из P я знаю, что Q

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

${\displaystyle P\vdash Q}$

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

В соответствии с его использованием для выводимости, «⊢», за которым следует выражение без чего-либо предшествующего, обозначает теорему , то есть выражение может быть выведено из правил с использованием пустого набора аксиом . Таким образом, выражение

${\displaystyle \vdash Q}$

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

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

${\displaystyle T\vdash S}$

означает, что S доказуемо из T . ^[4] Такое использование продемонстрировано в статье о пропозициональном исчислении . Синтаксическое следствие доказуемости следует противопоставить семантическому следствию, обозначенному символом двойного турникета . Говорят, что является семантическим следствием , или , когда все возможные оценки , в которых является истинным, также являются истинными. Для пропозициональной логики можно показать, что семантическое следствие и выводимость эквивалентны друг другу. То есть пропозициональная логика является обоснованной ( подразумевает ) и полной ( подразумевает ) ^[5] ${\displaystyle \models }$ ${\displaystyle S}$ ${\displaystyle T}$ ${\displaystyle T\models S}$ ${\displaystyle T}$ ${\displaystyle S}$ ${\displaystyle \models }$ ${\displaystyle \vdash }$ ${\displaystyle \vdash }$ ${\displaystyle \models }$ ${\displaystyle \models }$ ${\displaystyle \vdash }$

• В исчислении последовательностей турникет используется для обозначения секвенции . Секвенция утверждает, что если все антецеденты истинны, то по крайней мере один из консеквентов должен быть истинным. ${\displaystyle A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}}$ ${\displaystyle A_{1},\,\dots ,A_{m}}$ ${\displaystyle B_{1},\,\dots ,B_{n}}$
• В типизированном лямбда-исчислении турникет используется для отделения предположений о типизации от суждений о типизации. ^{[6] [7]}
• В теории категорий перевернутый турникет ( ), как в , используется для указания того, что функтор F является левым сопряженным к функтору G . ^[8] Реже турникет ( ), как в , используется для указания того, что функтор G является правым сопряженным к функтору F . ^[9] ${\displaystyle \dashv }$ ${\displaystyle F\dashv G}$ ${\displaystyle \vdash }$ ${\displaystyle G\vdash F}$
• В APL символ называется «правый галс» и представляет собой амбивалентную правую тождественную функцию, где и X ⊢ Y и ⊢ Y являются Y. Обратный символ «⊣» называется «левый галс» и представляет собой аналогичную левую тождественность, где X ⊣ Y является X , а ⊣ Y является Y. ^{[10] [11} ]
• В комбинаторике означает, что λ является разбиением целого числа n . ^[12] ${\displaystyle \lambda \vdash n}$
• В калькуляторах серий HP-41C / CV / CX и HP-42S компании Hewlett-Packard этот символ (в кодовой точке 127 в наборе символов FOCAL ) называется «Append character» и используется для указания того, что следующие символы будут добавлены в альфа-регистр, а не заменят существующее содержимое регистра. Этот символ также поддерживается (в кодовой точке 148) в модифицированном варианте набора символов HP Roman-8 , используемого другими калькуляторами HP.
• На калькуляторах Casio fx-92 Collège 2D и fx-92+ Spéciale Collège ^[13] символ представляет оператор остатка ; ввод даст ответ , где Q — частное , а R — остаток . На других калькуляторах Casio (например, на бельгийских вариантах — калькуляторах fx-92B Spéciale Collège и fx-92B Collège 2D ^[14] — где десятичный разделитель представлен точкой вместо запятой), оператор остатка представлен как ÷R . ${\displaystyle 5\vdash 2}$ ${\displaystyle Q=2;R=1}$
• В теории моделей означает , что каждая модель является моделью . ${\displaystyle \varphi \vdash \psi }$ ${\displaystyle \varphi }$ ${\displaystyle \psi }$ ${\displaystyle \varphi }$ ${\displaystyle \psi }$

Типографика

В TeX символ турникета получается из команды \vdash . ${\displaystyle \vdash }$

В Unicode символ турникета ( ⊢ ) называется правым галсом и находится в кодовой точке U+22A2. ^[15] (Кодовая точка U+22A6 называется знаком утверждения ( ⊦ ).)

• U+22A2 ⊢ ПРАВЫЙ ТАК ( ⊢, ⊢ )
  • = турникет
  • = доказывает, подразумевает, дает
  • = сокращаемый
• U+22A3 ⊣ ЛЕВЫЙ ГАЛК ( ⊣, ⊣ )
  • = обратный турникет
  • = не теорема, не приводит к
• U+22AC ⊬ НЕ ДОКАЗЫВАЕТ ( ⊬ )
  • ≡ 22A2⊢ 0338$̸

На пишущей машинке турникет может быть составлен из вертикальной черты (|) и тире (–).

В LaTeX есть пакет турникета, который выдает этот знак разными способами и способен размещать метки под ним или над ним, в нужных местах. ^[16]

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

• ꜔ (U+A714) Модификатор Буква Середина Левого Штиля Тоновая полоса
• ├ (U+251C) Рисунки ящиков светлые вертикальные и правые
• ㅏ (U+314F) Хангыль, буква A
• Ͱ (U+0370) Греческая заглавная буква Хета
• ͱ (U+0371) Греческая строчная буква Хета
• Ⱶ (U+2C75) Латинская заглавная буква половина H
• ⱶ (U+2C76) Латинская строчная буква половина H
• ⎬ (U+23AC) Средняя часть правой фигурной скобки

Смотрите также

• Двойной турникет ⊨
• Список логических символов
• Список математических символов

Примечания

1. Мартин-Лёф 1996, стр. 6, 15
2. Мартин-Лёф 1996, стр. 15
3. "Глава 6, Формальная теория языка" (PDF) .
4. Троэльстра и Швихтенберг 2000
5. Дирк ван Дален, Логика и структура (1980), Springer, ISBN 3-540-20879-8 . См. Главу 1, раздел 1.5. 
6. «Питер Селинджер, Конспект лекций по лямбда-исчислению» (PDF) .
7. Шмидт 1994
8. "сопряжённый функтор в nLab". ncatlab.org .
9. @FunctorFact (5 июля 2016 г.). «Functor Fact в Twitter» ( Tweet ) – через Twitter .
10. «Словарь APL». www.jsoftware.com .
11. Айверсон 1987
12. Стэнли, Ричард П. (1999). Перечислительная комбинаторика . Т. 2 (1-е изд.). Кембридж: Cambridge University Press. С. 287.
13. fx-92 Специальный режим работы колледжа (PDF) . Касио . 2015. с. 12.
14. «Вычисление остатков — Руководство пользователя Casio fx-92B». стр. 13]. {{cite web}}: Отсутствует или пусто |url=( помощь )
15. "Стандарт Unicode" (PDF) .
16. "CTAN: /tex-archive/macros/latex/contrib/turnstile". ctan.org .

Ссылки

• Фреге, Готтлоб (1879). Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens . Галле.
• Айверсон, Кеннет (1987). Словарь APL .
• Мартин-Лёф, Пер (1996). «О значениях логических констант и обоснованиях логических законов» (PDF) . Nordic Journal of Philosophical Logic . 1 (1): 11–60.(Конспект лекций к краткому курсу в Университете Студи ди Сиены, апрель 1983 г.)
• Шмидт, Дэвид (1994). Структура типизированных языков программирования . MIT Press . ISBN 0-262-19349-3.
• Troelstra, AS ; Schwichtenberg, H. (2000). Базовая теория доказательств (2-е изд.). Cambridge University Press . ISBN 978-0-521-77911-1.