Логика — наука о правильном рассуждении и фундамент корректности. Чтобы знать, что программа или довод верны, недостаточно интуиции: нужны точные высказывания и строгий вывод. Здесь — связки, кванторы и доказательство, на которых позже вырастут типы-как-теоремы.
Алгебра из главы I дала язык структур. Логика добавляет к нему правила вывода: как из истинных утверждений строго получать новые истинные. Это и есть фундамент корректности — ведь «верно» означает, что заключение следует из посылок, а не просто кажется правдоподобным.
Для инженера логика — рабочий инструмент: ею формулируют условия (что должно быть истинно до и после действия), ею доказывают, что программа делает обещанное. На этой главе позже вырастет соответствие Карри-Ховарда: типы как теоремы.
Основные связки и их смысл:
$p\wedge q,\quad p\vee q,\quad \neg p,\quad p\to q,\quad p\leftrightarrow q$
Высказывание, истинное при любых значениях частей, — тавтология (логический закон). Например, закон де Моргана связывает отрицание с «и»/«или»:
$\neg(p\wedge q)\;\equiv\;\neg p\vee\neg q$
Такие эквивалентности — это уже алгебра логики; ей посвящено отдельное углубление.
Углубление: булева алгебра и логические схемычитать →Связок мало, чтобы говорить о свойствах объектов. Нужны предикаты — высказывания с переменной, $P(x)$, — и кванторы: всеобщности $\forall$ («для всех») и существования $\exists$ («найдётся»).
$\forall x\,P(x)\quad\text{— верно для каждого}\qquad\exists x\,P(x)\quad\text{— верно хотя бы для одного}$
Кванторы — это язык спецификаций. «Функция корректна для всех допустимых входов» — это $\forall$; «существует контрпример» — это $\exists$. Отрицание меняет один на другой: $\neg\forall x\,P(x)\equiv\exists x\,\neg P(x)$ — чтобы опровергнуть «всё верно», достаточно одного контрпримера.
Хорошая система вывода обладает двумя свойствами: непротиворечивость (доказуемо только истинное) и полнота (всё истинное доказуемо). Доказательство — это формальная, проверяемая цепочка; именно её машинную проверку мы видели в главе о корректных программах. А пределам формальных систем посвящён сюжет о неполноте — но это уже другая история.
Это и есть стык логики с программированием — формальное доказательство программ. Как именно проводят такие доказательства (правила, инварианты циклов), разобрано в отдельном углублении. А дальше, в главе о корректных программах, та же идея проявится через типы.
Углубление: логика Хоара — доказательство программчитать →Логика дала точные высказывания, связки и кванторы, правила вывода и понятие доказательства; на этом стоит корректность — предусловия, постусловия, инварианты и вывод постусловия из предусловия. Алгебра дала язык структур, логика — язык истины и следования.
Логика работает с определённостью: истинно или ложно. Но мир ИИ полон неопределённости — там нужен другой язык. Им займётся следующая глава: вероятность.