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

В логике символ ⊨ , ⊧ или $\models$ называется двойным турникетом . Его часто читают как « влечет за собой », « моделирует », «является семантическим следствием » или «сильнее». ^[1] Он тесно связан с турникета . символом $\vdash$ , который имеет одну черту посередине и обозначает синтаксическое последствие (в отличие от семантического ).

Значение [ править ]

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

Чтобы показать семантическую последовательность с набором предложений слева и одним предложением справа, чтобы обозначить, что если каждое предложение слева истинно, то предложение справа должно быть истинным, например $\Gamma \vDash \varphi$ . Это использование тесно связано с символом турникета с одной перемычкой , который обозначает синтаксическое последствие .
Чтобы показать удовлетворение , с моделью (или структурой истинности) слева и набором предложений справа, чтобы обозначить, что структура является моделью (или удовлетворяет) набору предложений, например ${\mathcal {A}}\models \Gamma$ ${\mathcal {A}}\модели \Гамма$ . Обычно это делается индуктивно вместе с ограничением диапазона присваивания переменной : функция сопоставляет каждый символ переменной со значением в ${\mathcal {A}}$ ${\mathcal {A}}$ это может выдержать. ^[2]
- В этом контексте семантическое следствие в предыдущем списке можно сформулировать как «Для данной модели ${\mathcal {A}}$ , если ${\mathcal {A}}\models \Gamma$ затем ${\mathcal {A}}\vDash \varphi$ ".
Чтобы обозначить тавтологию , $\vDash \varphi$ . то есть выражение $\varphi$ является семантическим следствием пустого множества.
Вы также можете использовать этот символ следующим образом: ⊭ для обозначения утверждения «не влечет за собой».

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

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

В Юникоде он кодируется как U+22A8 ⊨ ИСТИНА ( &DoubleRightTee;, &vDash; ) , а противоположность этому U+22AD ⊭ НЕ ВЕРНО ( &nvDash; ) .

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

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

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

^ Недерпельт, Роб (2004). «Глава 7: Усиление и ослабление». Логическое рассуждение: первый курс (3-е исправленное изд.). Публикации Королевского колледжа. п. 62. ИСБН 0-9543006-7-Х .
^ Проект Open Logic, Логика первого порядка (стр.7). По состоянию на 4 января 2022 г.

Эта математической логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее .

Эта логике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее .

Эта типографике статья, посвященная , незавершена . Вы можете помочь Википедии, расширив ее .

[1] Недерпельт, Роб (2004). «Глава 7: Усиление и ослабление». Логическое рассуждение: первый курс (3-е исправленное изд.). Публикации Королевского колледжа. п. 62. ИСБН 0-9543006-7-Х .

[2] Проект Open Logic, Логика первого порядка (стр.7). По состоянию на 4 января 2022 г.

[1]

[2]