Турникет — в математической логике и информатике символ называется «турникетом» из-за его сходства с типичным турникетом, если смотреть сверху. Он также упоминается как «тройник» и часто читается как «даёт», «доказывает», «удовлетворяет» или «влечёт за собой».
В TeX символ турникета получается из команды \vdash. В Юникоде символ турникета (\vdash) называется «кнопка вправо» и находится на кодовой позиции U+22A2. Кодовая позиция U+22A6 называется «знак утверждения» (\vdash). На пишущей машинке турникет может состоять из вертикальной полосы (|) и тире (-). В LaTeX есть турникетный пакет, который выдаёт этот знак во многих случаях и способен помещать знаки ниже или выше него в нужных местах.
Смысл Турникет представляет собой бинарное отношение. Его различна в разных контекстах:
В эпистемологии Пер Мартин-Лоф (1996) анализирует символ таким образом: «…Сочетание штриха суждения Фреге | и штриха содержания — стало называться знаком утверждения.» Обозначение Фреге для суждения некоторого содержания : можно прочитать: "Я знаю, что -это правда". В том же духе условное утверждение : может быть прочитано как: «Исходя из , я знаю, что » В металогике, при построении формальных языков, турникет представляет собой умозаключение (или «выводимость»). Это означает, что он показывает, что одна строка может быть из другой за один шаг в соответствии с правилами преобразования (то есть синтаксисом) некоторой заданной формальной системы. Как таковое, выражение
означает, что выводимо из в системе. В соответствии с его использованием для выводимости, , за которым следует выражение без чего-либо предшествующего ему, обозначает теорему, то есть выражение может быть выведено из правил с использованием пустого множества аксиом. Как таковое, выражение
означает, что является теоремой в системе. В теории доказательств турникет используется для обозначения «доказуемости» или «выводимости». Например, если — это , а — конкретное предложение на языке теории, то
означает, что доказуемо из . Это использование продемонстрировано в статье о логике высказываний. Синтаксическое следствие доказуемости следует противопоставить семантическому следствию, обозначаемому символом двойного турникета . Он говорит, что является семантическим следствием , или , когда все возможные , в которых истинны, также истинны. Для пропозициональной логики можно показать, что семантическое следствие и выводимость эквивалентны друг другу. То есть пропозициональная логика является здравой ( подразумевает ) и полной ( подразумевает ).Dirk van Dalen, Logic and Structure (1980), Springer, . See Chapter 1, section 1.5. В типизированном лямбда-исчислении турникет используется для отделения предположений о типизации от суждения о типизации. В теории категорий обратный турникет (), как и в , используется для указания на то, что функтор остается сопряженным с функтором . В более редких случаях турникет (), как в , используется для указания на то, что функтор непосредственно примыкает к функтору . В APL символ называется «правый галс» и представляет амбивалентную функцию правой идентичности, где и , и являются . Обратный символ называется «левый галс» и представляет аналогичное левое тождество, где — это , а — . В комбинаторике, означает, что является разбиением числа . В калькуляторах фирмы Hewlett-Packard серий и символ (в кодовой точке 127) в ) называется «Добавить символ» и используется для указания на то, что следующие символы будут добавлены в альфа-регистр, а не заменят существующее содержимое регистра. Этот символ также поддерживается (в кодовой точке 148) в модифицированном варианте шрифта , используемого в других калькуляторах HP. В калькуляторах фирмы Casio серий fx-92 College 2D и fx-92+ Speciale College, символ означает ; на ввод будет выведено , где частное и остаток. В других калькуляторах CASIO (таких как бельгийские варианты — калькуляторы fx-92B Speciale College и fx-92B College 2D— где десятичный разделитель представлен точкой вместо запятой), оператор модуля вместо него обозначается как .
См. также Двойной турникет (символ) Секвенция (теория доказательств) Исчисление секвенций Список логических символов Таблица математических символов
Примечания
Ссылки
(Lecture notes to a short course at Universita degli Studi di Siena, April 1983.)
Категория:Математическая логика Категория:Логические символы Категория:Дедуктивные рассуждения Категория:Теория доказательств Категория:Логическое следствие