Двойной турникет

В логика, символ ⊨, ⊧ или $\models \; \{\backslash \; displaystyle\; \backslash \; models\}$называется двойным турникетом . Его часто читают как «влечет за собой », «модели », «является семантическим следствием или« сильнее, чем ». Он тесно связан с символом турникет $⊢\; \{\backslash \; displaystyle\; \backslash \; vdash\}$, который имеет одну полосу посередине и обозначает синтаксический. следствие (в отличие от семантического).

• 1 Значение
• 2 Типографика
• 3 См. Также
• 4 Ссылки

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

• Чтобы показать семантическое следствие, с набором предложений слева и одним предложением справа, чтобы обозначить, что если каждое предложение слева истинно, предложение справа должно быть верным, например $\Gamma \; \models \; \phi \; \{\backslash \; displaystyle\; \backslash \; Gamma\; \backslash \; vDash\; \backslash \; varphi\}$. Это использование тесно связано с одинарным зарешеченным символом турникет, который обозначает синтаксическое следствие.
• , чтобы показать удовлетворение, с моделью (или структурой истинности) слева. и набор предложений справа, чтобы обозначить, что структура является моделью (или удовлетворяет) набору предложений, например $A\; \models \; \Gamma \; \{\backslash \; displaystyle\; \{\backslash \; mathcal\; \{A\}\}\; \backslash \; models\; \backslash \; Gamma\}$.
  • В этом контексте семантическое следствие в предыдущем списке может быть указано как «Для данной модели $A\; \{\backslash \; displaystyle\; \{\backslash \; mathcal\; \{A\}\}\}$, если $A\; \models \; \Gamma \; \{\backslash \; displaystyle\; \{\backslash \; mathcal\; \{A\}\}\; \backslash \; models\; \backslash \; Gamma\}$, то $A\; \models \; \phi \; \{\backslash \; displaystyle\; \{\backslash \; mathcal\; \{A\}\}\; \backslash \; vDash\; \backslash \; varphi\}$".
• Для обозначения тавтологии, $\models \; \phi \; \{\backslash \; displaystyle\; \backslash \; vDash\; \backslash \; varphi\}$. то есть выражение $\phi \; \{\backslash \; displaystyle\; \backslash \; varphi\}$является семантическим следствием пустого набора.

в TeX символы турникета $\models \; \{\backslash \; displaystyle\; \backslash \; vDash\}$и $\models \; \{\backslash \; displaystyle\; \backslash \; models\}$получаются с помощью команд \ vDashи \ modelsсоответственно. В Unicode он кодируется как U + 22A8 ⊨ TRUE (HTML ⊨·⊨, ⊨)

В LaTeX есть пакет турникета, который выдает этот знак разными способами, в том числе двойной турникет, и позволяет наклеивать ярлыки под или над ним, в правильных местах. Статья Инструмент для логиков представляет собой руководство по использованию этого пакета.

• Список логических символов
• Список математических символов

1. ^Nederpelt, Rob (2004). «Глава 7: Усиление и ослабление». Логическое рассуждение: первый курс (3-е пересмотренное издание). Публикации Королевского колледжа. п. 62. ISBN 0-9543006-7-X.

.