Що означає ⊬
Ні: знак стосується вивідності, а не істинності.
У записі P ⊬ Q літера P позначає засновки, а Q — висновок; знак заперечує синтаксичне слідування. Натомість P ⊭ Q означає, що існує модель (математична інтерпретація), у якій P істинне, а Q хибне.
«Поняттєва нотація» Ґотлоба Фреге, видана 1879 року, була двовимірною системою логічного запису й містила історичного попередника знака вивідності. Значення знака з часом змінилося: у багатьох системах доведень ⊢ позначає вивідність, а ⊬ її заперечує.
Технічний, формальний і нейтральний знак.
Сам по собі він не означає, що Q хибне.
Не плутайте з
1Як набрати ⊬
Windows (Word)
Alt+XВведіть 22AC, потім натисніть Alt+X, щоб отримати ⊬.
Windows
Win+RЗапустіть charmap для повної таблиці або скористайтеся вкладкою Ω у панелі емодзі (Win + .).
macOS
Control+Command+SpaceВідкрийте переглядач символів і знайдіть «does not prove».
Linux
Ctrl+Shift+UВведіть 22ac, потім натисніть Enter або пробіл.
HTML
⊬CSS
\22ACLaTeX
У математичному режимі LaTeX для перекресленого знака вивідності використовуйте `\nvdash`.
Коди й кодуванняКодових точок: 1
HTML десятковий
⊬
HTML шістнадцятковий
⊬
Вміст CSS
content: "\22AC";
Кожна escape-послідовність закінчується наступною зворотною скісною рискою; перед звичайною шістнадцятковою цифрою потрібен пробіл.
Кодування URL
%E2%8A%AC
1
На екрані
1
Кодові точки
1
JS .length
3
Байти UTF-8
Видимий символ може містити кілька кодових точок. JS .length рахує одиниці UTF-16, а UTF-8 — байти.