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

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

Смысл

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

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

${\displaystyle \vdash A}$ :

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

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

${\displaystyle P\vdash Q}$ :

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

«Исходя из P , я знаю, что Q »

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

${\displaystyle P\vdash Q}$

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

В соответствии с его использованием для выводимости, ${\displaystyle \vdash }$ , за которым следует выражение без чего-либо предшествующего ему, обозначает теорему , то есть выражение может быть выведено из правил с использованием пустого множества аксиом . Как таковое, выражение

${\displaystyle \vdash Q}$

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

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

${\displaystyle T\vdash S}$

означает, что S доказуемо из T . Это использование продемонстрировано в статье о логике высказываний . Синтаксическое следствие доказуемости следует противопоставить семантическому следствию, обозначаемому символом ${\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 \dashv }$ ), как и в ${\displaystyle F\dashv G}$ , используется для указания на то, что функтор F остается сопряженным

с функтором G . В более редких случаях турникет ( ${\displaystyle \vdash }$ ), как в ${\displaystyle G\vdash F}$ , используется для указания на то, что функтор G непосредственно примыкает к функтору F .

• В APL символ называется «правый галс» и представляет амбивалентную функцию правой идентичности, где и ${\displaystyle X\vdash Y}$ , и ${\displaystyle \vdash Y}$ являются ${\displaystyle Y}$ . Обратный символ ${\displaystyle \dashv }$ называется «левый галс» и представляет аналогичное левое тождество, где ${\displaystyle X\dashv Y}$ — это ${\displaystyle X}$ , а ${\displaystyle \dashv Y}$ — ${\displaystyle Y}$ .
• В комбинаторике , ${\displaystyle \lambda \vdash n}$ означает, что ${\displaystyle \lambda }$ является разбиением числа ${\displaystyle n}$ .
• В калькуляторах фирмы Hewlett-Packard серий и символ (в кодовой точке 127) в ) называется «Добавить символ» и используется для указания на то, что следующие символы будут добавлены в альфа-регистр, а не заменят существующее содержимое регистра. Этот символ также поддерживается (в кодовой точке 148) в модифицированном варианте шрифта , используемого в других калькуляторах HP.
• В калькуляторах фирмы Casio серий fx-92 College 2D и fx-92+ Speciale College, символ означает ; на ввод ${\displaystyle 5\vdash 2}$ будет выведено ${\displaystyle Q=2;R=1}$ , где Q частное и R остаток . В других калькуляторах CASIO (таких как бельгийские варианты — калькуляторы fx-92B Speciale College и fx-92B College 2D — где десятичный разделитель представлен точкой вместо запятой), оператор модуля вместо него обозначается как ${\displaystyle \div R}$ .

См. также

• ${\displaystyle \models }$
• Секвенция (теория доказательств)
• Исчисление секвенций
• Список логических символов
• Таблица математических символов

Примечания

Ссылки

• Frege, Gottlob (1879). “Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens”. Halle.
• Iverson, Kenneth (1987). “A Dictionary of APL”.
• Martin-Lof, Per (1996). (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). . MIT Press . ISBN 0-262-19349-3 .
• Troelstra, A. S.; Schwichtenberg, H. (2000). “Basic Proof Theory” (2nd ed.). Cambridge University Press . ISBN 978-0-521-77911-1 .