Перейти к содержимому
Topos Uranos
Русский

Логика и выводы

Краткое содержание

Этот урок учит записывать логику средствами LaTeX так, чтобы это одинаково служило тем, кто изучает математику, информатику или философию. Он различает связку языка-объекта и стрелку метаязыка и представляет связки с их вариантами, обозначения других традиций (подкову, тильду, точку и польскую запись) и пользу собственной команды для каждой связки; устанавливает пробелы при кванторах; набирает множества, заданные характеристическим свойством, и объясняет, почему черта с клавиатуры и \mid получают разные пробелы; собирает символы металогики, секвенций и модальной логики вместе с пакетом, который определяет каждый из них; набирает таблицы истинности с помощью array; строит деревья натурального вывода с bussproofs, чья логика стека объясняет его ошибки, и ящики Фитча с logicproof; излагает рассуждения в стандартной форме с пронумерованными посылками и заключением; и завершается тем, чего делать не стоит, с настоящими журналами каждой ошибки.

Цели обучения

  1. Выбирать между связкой языка-объекта и стрелкой метаязыка, а также между \models, \vdash, \equiv и \Leftrightarrow, в зависимости от того, что утверждает формула.
  2. Предсказывать пробелы при кванторах, во множествах, заданных характеристическим свойством, и в отрицаниях с тильдой, и исправлять погрешности, о которых не выдаётся никакого предупреждения.
  3. Определять по команде на каждую связку и объяснять, какую смену традиции это позволяет, а какую нет.
  4. Строить деревья натурального вывода с bussproofs, следя за состоянием его стека, и диагностировать их ошибки по журналу.
  5. Набирать таблицу истинности и рассуждение в стандартной форме и выбирать между деревом и ящиком Фитча для данного доказательства.

Два уровня языка

Текст по логике всегда говорит на двух уровнях. Есть язык-объект, язык изучаемых формул, с его связками и кванторами; и есть метаязык, язык автора, который утверждает нечто об этих формулах: что одна выводится из других, что две равносильны, что одна истинна в любой модели. Обозначения должны держать оба уровня раздельно, потому что стрелка не на своём месте не типографская небрежность, а другое утверждение. Этот урок предполагает знакомство с символами и операторами из урока о символах и обозначениях и с окружениями из урока о теоремах и доказательствах; здесь изучается то, что свойственно логике. Кто хочет знать теорию, которую выражают эти обозначения, найдёт её в курсе Математическая логика I: логика высказываний.