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

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

Интерпретации [ править ]

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

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

\vdash A

тогда можно будет прочитать

Я знаю, $что А$ верно . ^[2]

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

P\vdash Q

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

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

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

P\vdash Q

означает, что

Q

выводится из

P

в системе.

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

\vdash Q

означает, что

Q

является теоремой в системе.

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

T\vdash S

означает,

S

доказуемо что из

T

. ^[4]Это использование продемонстрировано в статье об исчислении высказываний . Синтаксическому последствию доказуемости следует противопоставить семантическое следствие, обозначаемое турникета. двойным символом

\models

. Один говорит, что

S

является смысловым следствием

T

, или

T\models S

, когда все возможные оценки , в которых

T

правда,

S

это тоже правда. Для пропозициональной логики можно показать, что семантическое следствие

\models

и выводимость

\vdash

эквивалентны друг другу. То есть пропозициональная логика верна (

\vdash

подразумевает

\models

) и полный (

\models

подразумевает

\vdash

) ^[5]

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

Типография [ править ]

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

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

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

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

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

Подобные графемы [ править ]

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

См. также [ править ]

Примечания [ править ]

^ Мартин-Лёф 1996 , стр. 6, 15
^ Мартин-Лёф 1996 , стр. 15.
^ «Глава 6, Теория формального языка» (PDF) .
^ Троэльстра и Швихтенберг 2000
^ Дирк ван Дален, Логика и структура (1980), Springer, ISBN 3-540-20879-8 . См. главу 1, раздел 1.5.
^ «Питер Селинджер, Конспект лекций по лямбда-исчислению» (PDF) .
^ Шмидт 1994 г.
^ «сопряженный функтор в nLab» . ncatlab.org .
^ @FunctorFact (5 июля 2016 г.). «Факт о функторе в Твиттере» ( Tweet ) — через Twitter .
^ «Словарь АПЛ» . www.jsoftware.com .
^ Айверсон 1987
^ Стэнли, Ричард П. (1999). Перечислительная комбинаторика . Том. 2 (1-е изд.). Кембридж: Издательство Кембриджского университета. п. 287.
^ Руководство по эксплуатации специального колледжа fx-92 (PDF) . Касио . 2015. с. 12.
^ «Вычисления остатка — Руководство пользователя Casio fx-92B [страница 13] | ManualsLib» . www.manualslib.com . Проверено 24 декабря 2020 г.
^ «Стандарт Юникод» (PDF) .
^ «CTAN: /tex-archive/macros/latex/contrib/turnstile» . ctan.org .

Ссылки [ править ]

Фреге, «Хвала Богу» (1879). Концептуальное письмо: формульный язык чистого мышления, основанный на арифметике . Зал.
Айверсон, Кеннет (1987). Словарь APL .
Мартин-Лёф, Пер (1996). «О значениях логических констант и обоснованиях логических законов» (PDF) . Северный журнал философской логики . 1 (1): 11–60. (Конспект лекций к краткому курсу в Университете Студи ди Сиены, апрель 1983 г.)
Шмидт, Дэвид (1994). Структура типизированных языков программирования . МТИ Пресс . ISBN 0-262-19349-3 .
Троэльстра, AS ; Швихтенберг, Х. (2000). Основная теория доказательств (2-е изд.). Издательство Кембриджского университета . ISBN 978-0-521-77911-1 .

[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 г.). «Факт о функторе в Твиттере» ( Tweet ) — через Twitter .

[10] «Словарь АПЛ» . www.jsoftware.com .

[11] Айверсон 1987

[12] Стэнли, Ричард П. (1999). Перечислительная комбинаторика . Том. 2 (1-е изд.). Кембридж: Издательство Кембриджского университета. п. 287.

[13] Руководство по эксплуатации специального колледжа fx-92 (PDF) . Касио . 2015. с. 12.

[14] «Вычисления остатка — Руководство пользователя Casio fx-92B [страница 13] | ManualsLib» . www.manualslib.com . Проверено 24 декабря 2020 г.

[15] «Стандарт Юникод» (PDF) .

[16] «CTAN: /tex-archive/macros/latex/contrib/turnstile» . ctan.org .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]