Моделі

Подвійний турнікет виражає істинність у моделі або семантичний наслідок. Модель — це математична інтерпретація логічних символів. У записі A ⊧ φ структура A робить формулу φ істинною. У Γ ⊧ φ засновки Γ семантично тягнуть за собою φ: кожна модель, у якій істинна Γ, робить істинною і φ. Якщо ліворуч немає засновків, ⊧ φ означає, що φ істинна в кожній моделі.

Саймон Кохен широко використовував подвійний турнікет у теорії моделей у 1961 році. Він казав, що не пам’ятає, чи сам вигадав це позначення, чи запозичив його. Використання для логічного наслідку, ймовірно, з’явилося близько 1963 року й точно існувало до 1967 року.

Чим ⊧ відрізняється від ⊢?

⊧ виражає семантичну істинність, а ⊢ позначає формальне виведення. У записі Γ ⊢ φ система доведення виводить φ із засновків Γ. У Γ ⊧ φ кожна модель, у якій істинна Γ, робить істинною і φ. Ці знаки відповідають на різні запитання: що випливає з правил доведення і що істинне в усіх інтерпретаціях.

Що означає ⊧, коли його надсилають?

Зазвичай це вказує на контекст логіки або математики. У повідомленні подивіться на сусідні формули: розташування знака показує, чи пов’язує ⊧ модель із формулою, чи засновки з висновком.