Логика предикатов: как вы самостоятельно проверяете логическую структуру своих собственных аргументов?

Таблиц истинности недостаточно для захвата логики первого порядка (с квантификаторами), поэтому вместо этого мы используем правила вывода. Каждое правило вывода выбрано так, чтобы оно было верным, а это означает, что если вы начнете с истинных утверждений и будете использовать правило, вы получите только истинные утверждения. Мы говорим, что эти правила сохраняют истину. Если вы выбираете достаточно тщательно, вы можете сделать так, чтобы правила не только сохраняли истинность, но и позволяли вам вывести каждое (правильно построенное) утверждение, которое обязательно истинно (во всех ситуациях).

То, что вы, вероятно, ищете (а именно, практический способ строго проверить логическую обоснованность ваших аргументов), — это естественная дедукция. Существует множество различных стилей, наиболее интуитивно понятным из которых является стиль Fitch , который отмечает подконтексты с помощью отступов или соответствующих визуальных разграничений. Следующая система использует отступы и, на мой взгляд, наиболее точно следует интуиции.$\def\block#1{\begin{array}{ll}\ &{#1}\end{array}} \def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}} \def\sub#1#2{\text{#1}:\\\block{#2}} \def\imp{\Rightarrow} \def\eq{\Leftrightarrow} \def\nn{\mathbb{N}} \def\none{\varnothing} \def\pow{\mathcal{P}}$

---

Контексты

Каждая строка является либо заголовком, либо оператором. Мы будем ставить двоеточие после каждого заголовка и точку после каждого утверждения. Каждый заголовок определяет некоторый подконтекст (содержащийся в текущем контексте), а строки, управляемые этим заголовком, обозначаются отступом. Полный контекст каждой строки определяется всеми управляющими ею заголовками (т. е. всеми ближайшими заголовками над ней на каждом более низком уровне отступа).

Например, вложенный анализ случаев может выглядеть так:

  $\sub{If $A$}{\sub{If $B$}{...} \\ \sub{If $¬B$}{...}} \\ \sub{If $\neg A$}{...}$

И рассуждения о произвольном члене коллекции$S$будет выглядеть так:

  $\sub{Given $x{∈}S$}{...}$

Обратите внимание, что то, что указано в одном контексте, может быть недействительным в другом контексте. Как только вы поймете принцип, лежащий в основе контекстов и отступов, следующие правила станут очень естественными. Также обратите внимание, что для логики первого порядка нужны только эти два типа заголовков контекста (для условных подконтекстов и универсальных подконтекстов соответственно).

Синтаксические правила

Утверждение должно быть атомарным (неделимым) предложением или составным утверждением, сформированным обычным образом с использованием логических операций или кванторов, с тем ограничением, что каждая переменная, связанная квантором, еще не используется для ссылки на какой-либо объект в текущем контексте. , и что нет вложенных квантификаторов, связывающих одну и ту же переменную.

Правила естественного вычета

Каждое правило вывода имеет вид:

  $\fitch{\text{X}}{\text{Y}}$

это означает, что если последние строки, которые вы написали, совпадают с «X», вы можете написать «Y» сразу после этого на том же уровне отступа. Каждое применение правила вывода также привязано к текущему контексту, а именно к контексту «X». Мы не будем постоянно упоминать «текущий контекст».

---

Логические операции

Возьмите любые заявления$A,B,C$(в текущем контексте).

restate : если мы что-то доказываем, мы можем подтвердить это снова в том же контексте.

  $\fitch{A.\\ ...}{A.}$

Обратите внимание, что "$...$" обозначают любое количество строк, которые находятся не менее чем на изображенном уровне отступа. В приведенном выше правиле это означает, что все строки, написанные с момента более раннего написания "$A.$" должен быть в том же контексте (или в каком-то подконтексте).

На практике мы никогда не пишем одну и ту же строку дважды. Чтобы указать, что мы можем опустить строку в доказательстве, я отмечу ее квадратными скобками следующим образом:

  $\fitch{A. \\ ...}{[A.]}$

⇒sub       ⇒restate     (мы можем создать условный подконтекст, где$A$держит.)

  $\fitch{}{\sub{If $A$}{[A.]}}$   $\fitch{B. \\ ... \\ \sub{If $A$}{...}}{\block{[B.]}}$

⇒вступление       ⇒элим

  $\fitch{\sub{If $A$}{... \\ B.}}{[A \imp B.]}$   $\fitch{A \imp B. \\ A.}{B.}$

∧вступление     ∧елим

  $\fitch{A. \\ B.}{A \land B.}$   $\fitch{A \land B.}{[A.] \\ [B.]}$

∨вступление     ∨элим

  $\fitch{A.}{[A \lor B.] \\ [B \lor A.]}$   $\fitch{A \lor B. \\ A \imp C. \\ B \imp C.}{C.}$

¬intro     ¬элим     ¬¬элим

  $\fitch{A \imp \bot.}{\neg A.}$   $\fitch{A. \\ \neg A.}{\bot.}$   $\fitch{\neg \neg A.}{A.}$

Обратите внимание, что, используя ¬intro и ¬¬elim, мы можем получить следующее дополнительное правило вывода:

  $\fitch{\neg A \imp \bot.}{A.}$

что соответствует тому, как можно было бы попытаться доказать$A$ от противного , а именно показать, что, полагая$\neg A$подразумевает ложь.

⇔интро     ⇔елим

  $\fitch{A \imp B. \\ B \imp A.}{A \eq B.}$   $\fitch{A \eq B.}{[A \imp B.] \\ [B \imp A.]}$

Кванторы и равенство

Правила здесь предназначены для ограниченных кванторов, потому что обычно мы думаем в их терминах. Сначала нам понадобятся некоторые определения.

Используемая переменная : переменная, которая объявлена ​​в заголовке некоторого содержащего ∀-контекста или объявлена ​​на каком-то предыдущем шаге ∃-исключения ("let") в некотором содержащем контексте.

Неиспользуемая переменная : переменная, которая не используется.

Свежая переменная : переменная, которая не появляется ни в одном предыдущем операторе ни в одном содержащем контексте.

Объектное выражение : выражение, которое ссылается на объект (например, используемую переменную или функциональный символ, применяемый к объектным выражениям).

Недвижимость с$k$параметры : строка$P$с некоторыми пробелами, где каждый пробел имеет некоторую метку из$1$к$k$, так что заменяя каждый пробел в$P$некоторым выражением объекта дает оператор. Если$k = 2$, затем$P(E,F)$является результатом замены каждого пробела с пометкой$1$к$E$и заменяя каждый пробел помеченным$2$к$F$. Аналогично для других$k$.

В этой секции,$E,F$(если задействовано) может быть любым выражением объекта (в текущем контексте).

Начнем со следующих правил, которые определяют тип всех объектов.

вселенная :$obj$является типом.

  $\fitch{}{[E{∈}obj.]}$

Теперь возьмите любой тип$S$и 1-параметрическое свойство$P$и неиспользуемая переменная$x$что не появляется в$S$или$P$.

∀sub           ∀restate         (мы можем создать ∀-подконтекст, в котором$x$имеет тип$S$.)

  $\fitch{}{\sub{Given $x{∈}S$}{[x{∈}S.]}}$   $\fitch{A. \\ ... \\ \sub{Given $x{∈}S$}{...}}{\block{[A.]}}$($x$не должен появляться в$A$)

∀интро           ∀елим

  $\fitch{\sub{Given $x{∈}S$}{... \\ P(x).}}{\forall x{∈}S\ ( \ P(x) \ ).}$   $\fitch{\forall x{∈}S\ ( \ P(x) \ ). \\ E{∈}S.}{P(E).}$($E$не должны делиться никакими неиспользуемыми переменными с$P$)

∃интро           ∃елим

  $\fitch{E{∈}S. \\ P(E).}{\exists x{∈}S\ ( \ P(x) \ ).}$   $\fitch{\exists x{∈}S\ ( \ P(x) \ ).}{\text{Let $y{∈}S$ such that $P(y)$}. \\ [y{∈}S.] \\ [P(y).]}$(где$y$это новая переменная)

= вступление       = элим

  $\fitch{}{[E=E.]}$   $\fitch{E=F. \\ P(E).}{P(F).}$($F$не должны делиться какой-либо неиспользуемой переменной с$P$)

Переименование переменных

Наконец, следующие правила переименования переменных являются излишними, но сокращают доказательства.

∀переименовать         ∃переименовать

  $\fitch{\forall x{∈}S\ ( \ P(x) \ ).}{[\forall y{∈}S\ ( \ P(y) \ ).]}$   $\fitch{\exists x{∈}S\ ( \ P(x) \ ).}{[\exists y{∈}S\ ( \ P(y) \ ).]}$

  (где$y$неиспользуемая переменная, которая не появляется в$P$)

Краткие формы

Для удобства пишем "$\forall x,y{∈}S\ ( \ P(x,y) \ )$"как краткая форма"$\forall x{∈}S\ ( \ \forall y{∈}S\ ( \ P(x,y) \ ) \ )$", и аналогично для большего количества переменных и для "$\exists$". Мы также будем сжимать вложенные заголовки ∀-подконтекста в следующем виде:

  $\sub{Given $x{∈}S$}{\sub{Given $y{∈}S$}{...}}$

к:

  $\sub{Given $x,y{∈}S$}{...}$

Кроме того, "$\exists! x{∈}S\ ( \ P(x) \ )$"это краткая форма для"$\exists x{∈}S\ ( \ P(x) \land \forall y{∈}S\ ( \ P(y) \imp x=y \ ) \ )$".

---

Пример

Вот пример, где$S,T$любые виды и$P$любое свойство с двумя параметрами.

Сначала показаны все строки:

  Если$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$: [⇒sub]
    $\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$. [⇒sub]
    Пусть$a{∈}S$такой, что$\forall y{∈}T\ ( \ P(a,y) \ )$. [∃элим]
    $a{∈}S$. [∃элим]
    $\forall y{∈}T\ ( \ P(a,y) \ )$. [∃элим]
    $\forall z{∈}T\ ( \ P(a,z) \ )$. [∀переименовать]
    Дано$y{∈}T$: [∀sub]
      $y{∈}T$. [∀sub]
      $\forall z{∈}T\ ( \ P(a,z) \ )$. [∀переформулировать]
      $y{∈}T$. [переформулировать]
      $P(a,y)$. [∀элим]
      $a{∈}S$. [∀переформулировать]
      $\exists x{∈}S\ ( \ P(x,y) \ )$. [∃интро]
    $\forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [∀введение]
  $\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ ) \imp \forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [⇒ введение]

Наконец, со всеми удаленными строками в квадратных скобках:

  Если$\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ )$: [⇒sub]
    Пусть$a{∈}S$такой, что$\forall y{∈}T\ ( \ P(a,y) \ )$. [∃элим]
    Дано$y{∈}T$: [∀sub]
      $P(a,y)$. [∀элим]
      $\exists x{∈}S\ ( \ P(x,y) \ )$. [∃интро]
    $\forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [∀введение]
  $\exists x{∈}S\ ( \ \forall y{∈}T\ ( \ P(x,y) \ ) \ ) \imp \forall y{∈}T\ ( \ \exists x{∈}S\ ( \ P(x,y) \ ) \ )$. [⇒ введение]

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

Дефиниторное расширение

Для облегчения определений , которые могут значительно сократить доказательства, у нас также есть следующие дефиниторные правила расширения.

Для каждого$k$- свойство параметра$P$и свежий предикат-символ$Q$:

  $\fitch{}{\text{Let $Q(x_1,...x_k) ≡ P(x_1,...x_k)$ for each $x_1{∈}S_1$ and ... and $x_k{∈}S_k$.} \\ [∀x_1{∈}S_1\ \cdots ∀x_k{∈}S_k\ ( \ Q(x_1,...x_k) ⇔ P(x_1,...x_k) \ ).]}$

Для каждого$(k+1)$- свойство параметра$R$и свежий функциональный символ$f$:

  $\fitch{∀x_1{∈}S_1 \cdots ∀x_k{∈}S_k\ ∃!y{∈}T ( \ R(x_1,...x_k,y) \ ) } {\text{Let $f : S_1{×}{\cdots}{×}S_k{→}T$ such that $R(x_1,...x_k,f(x_1,...x_k))$ for each $x_1{∈}S_1$ and ... and $x_k{∈}S_k$.} \\ [∀x_1{∈}S_1\ \cdots ∀x_k{∈}S_k\ ( \ f(x_1,...x_k)∈T ∧ R(x_1,...x_k,f(x_1,...x_k)) \ ).]}$

Эти правила избыточны в том смысле, что любое утверждение, которое вы можете доказать, не используя никаких новых символов, может быть доказано без использования дефиниторного расширения.

Примечания

Вышеупомянутые правила позволяют избежать обычных проблем, с которыми сталкиваются многие другие системы, когда переменные, используемые для свидетелей экзистенциальных утверждений, необходимо отличать от переменных, используемых для произвольных объектов. Причина в том, что каждая переменная здесь определяется либо ∀-подконтекстом, либо оператором "let"; другими словами, свободных переменных нет. Тот факт, что каждая переменная связана, тесно связан с тем фактом, что эта система допускает пустую вселенную, если нет других аксиом.

Кроме того, каждая переменная определяется уникальным заголовком или оператором «let» в текущем контексте; другими словами, нет переменного затенения. Это задумано, и в реальной математической практике мы также соблюдаем это, хотя большинство других формальных систем этого не делают. Как следствие, такие предложения, как «$\exists x\ \forall x\ ( x=x )$.» просто не может быть записано в этой системе. Если вы хотите разрешить такие ужасные предложения, вам придется соответствующим образом изменить правила, но это, скорее всего, вызовет головную боль.

Наконец, были некоторые тонкие технические решения. Для правил квантификатора причина, по которой я требовал, чтобы$x$не появляется в$S,P$заключается в том, что если мы позже включим правила для указания типов, у нас обычно будут имена переменных в его синтаксисе, что вызовет проблемы. Например, если мы написали в текущем контексте "$x∈\{y:y∈S∧y∈T\}$" и "$x∈U$", будет неразумно разрешать писать"$∃y∈U\ ( y∈\{y:y∈S∧y∈T\} )$". Аналогично, если бы мы написали "$x=\{y:P(y)\}$" и "$∃y∈U\ ( Q(x,y) )$", мы не хотим разрешать писать"$∃y∈U\ ( Q(\{y:P(y)\},y) )$".

Кроме того, чтобы позволить переменной снова стать свежей после выхода из подконтекста, в котором она была объявлена, я потребовал, чтобы правила ⇒intro и ∀intro могли применяться только сразу после соответствующего ⇒-подконтекста или ∀-подконтекста. Было бы проще просто определить новую переменную как переменную, которая не появляется ни в одной предыдущей строке, но тогда мы можем легко исчерпать новые имена переменных в длинном доказательстве.

~ ~ ~ ~ ~ ~ ~

Чтобы проиллюстрировать гибкость этой системы, я представлю и арифметику Пеано, и теорию множеств в виде дополнительных правил, которые можно просто добавить в систему.

Арифметика Пеано

Добавьте тип$\nn$и символы PA, а именно символы-константы$0,1$и$2$-входные функции-символы$+,·$и$2$-input предикат-символ$<$.

Добавьте аксиомы PA$^-$, адаптировано отсюда :

• $\forall x,y{∈}\nn\ ( \ x+y ∈ \nn \ )$.
• $\forall x,y{∈}\nn\ ( \ x·y ∈ \nn \ )$.
• $\forall x,y{∈}\nn\ ( \ x+y=y+x \ )$.
• $\forall x,y{∈}\nn\ ( \ x·y=y·x \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x+(y+z)=(x+y)+z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x·(y·z)=(x·y)·z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x·(y+z)=x·y+x·z \ )$.
• $\forall x{∈}\nn\ ( \ x+0=x \ )$.
• $\forall x{∈}\nn\ ( \ x·1=x \ )$.
• $\forall x{∈}\nn\ ( \ \neg x<x \ )$.
• $\forall x,y{∈}\nn\ ( \ x<y \lor y<x \lor x=y \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x<y \land y<z \imp x<z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x<y \imp x+z<y+z \ )$.
• $\forall x,y,z{∈}\nn\ ( \ x<y \land 0<z \imp x·z<y·z \ )$.
• $\forall x,y{∈}\nn\ ( \ x<y \imp \exists z{∈}\nn\ ( \ x+z=y \ ) \ )$.
• $0<1$.
• $\forall x{∈}\nn\ ( \ 0=x \lor 1=x \lor 1<x \ )$.

Добавьте аксиомы индукции, а именно для каждого свойства$P$с участием только символов PA и кванторов над$\nn$добавить следующую аксиому (где$k$не появляется в$P$):

• $P(0) \land \forall k{∈}\nn\ ( \ P(k) \imp P(k+1) \ ) \imp \forall k{∈}\nn\ ( \ P(k) \ )$.

Теория множеств

Добавьте тип$set$и правило, согласно которому каждый член$set$тоже тип.

Добавьте унарные функциональные символы$\pow,\bigcup$, бинарные функции-символы$×,→$, а постоянный символ$\none$. Мы повторно используем бинарный предикат-символ$\in$, так как не будет двусмысленности. Также добавьте следующие правила (в каждом контексте) для других обозначений:

• Если$E,F \in obj$, затем$(E,F) \in obj$и$\{E,F\} \in set$.
• Если$S,T \in set$, затем$S×T \in set$и$(S{→}T) \in set$и$\pow(S) \in set$.
• Если$S,T \in set$и$f \in (S{→}T)$и$x \in S$, затем$f(x) \in T$.
• Если$S \in set$и$\forall x{∈}S\ ( \ x \in set \ )$, затем$\bigcup(S) \in set$.

Добавьте следующие аксиомы:

• экстенсиональность :   $\forall S,T{∈}set\ ( \ S=T \eq \forall x{∈}obj\ ( \ x \in S \eq x \in T \ ) \ ).$
• пустой набор :   $\forall x{∈}obj\ ( \ \neg x \in \none \ ).$
• натуралы :   $\nn{∈}set$.
• набор мощности :   $\forall S{∈}set\ ( \ \pow(S) = \{ T : T \in set \land \forall x{∈}T\ ( \ x \in S \ ) \} ).$
• пара :   $\forall x,y{∈}obj\ ( \ \{x,y\} = \{ z : z=x \lor z=y \} ).$
• упорядоченная пара :   $\forall x,y{∈}obj\ \forall z,w{∈}obj\ ( \ (x,y)=(z,w) \eq x=z \land y=w \ ).$
• тип продукта :   $\forall S,T{∈}set\ ( \ S×T = \{ t : \exists x{∈}S\ \exists y{∈}T\ ( \ t=(x,y) \ ) \} \ ).$
• тип функции :   $\forall S,T{∈}set\ ( \ (S→T) = \\ \{ F : F \in \pow(S×T) \land \forall x{∈}S\ \exists! y{∈}T\ ( \ (x,y) \in F \ ) \} \ ).$
• функция-приложение :   $\forall S,T{∈}set\ \forall f{∈}(S{→}T)\ \forall x{∈}S\ ( \ (x,f(x)) \in f \ ).$
• союз :   $\forall S{∈}set\ ( \ \bigcup(S) = \{ x : \exists T{∈}set\ ( \ x \in T \land T \in S \ ) \} \ ).$
• выбор :   $\forall S,T{∈}set\ \forall R{∈}\pow(S×T)\ ( \ \forall x{∈}S\ \exists y{∈}T\ ( \ (x,y) \in R \ ) \\ \imp \exists f{∈}(S{→}T)\ \forall x{∈}S\ ( \ (x,f(x)) \in R \ ) \ ).$

Добавьте следующие правила:

обозначение типа

Возьмите (в текущем контексте) любое свойство$P$и выражение объекта$E$и неиспользуемая переменная$x$.

Затем$\{ x : P(x) \}$является типом, и его членство регулируется:

  $\fitch{}{E \in \{ x : P(x) \} \eq P(E).}$. ($x$не должен появляться в$E$или$P$)

понимание

Возьмите любое имущество$P$и неиспользуемая переменная$x$.

  $\fitch{S \in set.}{\{ x : x \in S \land P(x) \} \in set.}$. ($x$не должен появляться в$S$или$P$)

замена

Возьми любой$2$- свойство параметра$P$и неиспользуемые переменные$x,y$.

  $\fitch{S \in set. \\ \forall x{∈}S\ \exists! y{∈}obj\ ( \ P(x,y) \ ).}{\{ y : \exists x{∈}S\ ( \ P(x,y) \ ) \} \in set.}$($x,y$не должен появляться в$S$или$P$)

индукция

Возьмите любое имущество$P$с$1$параметр из$\nn$.

  $\fitch{P(0). \\ \forall k{∈}\nn\ ( \ P(k) \imp P(k+1) \ ).}{\forall k{∈}\nn\ ( \ P(k) \ ).}$($k$не должен появляться в$P$)

Правило индукции включает в себя аксиомы индукции для PA, и, по сути, единственное отличие состоит в том, что свойство$P$может включать операции над множествами и количественную оценку над множествами.

функция-обозначение

Это правило теоретически не нужно, но прагматически очень удобно (также известное как лямбда-выражения в информатике).

Возьми любой набор$S$и любое объектное выражение$E$с$1$параметр из$S$и неиспользуемая переменная$x$.

Затем$( S\ x \mapsto E(x) )$является объектом, и его поведение регулируется:

  $\fitch{\forall x{∈}S\ ( \ E(x) \in T \ ). \\ f = ( S\ x \mapsto E(x) ).}{f \in (S→T) \land \forall x{∈}S ( \ f(x) = E(x) \ ).}$

Фундаментальная система

Сочетание вышеупомянутой арифметики Пеано с теорией множеств дает фундаментальную систему, которая по существу не уступает ZFC, но гораздо более удобна для пользователя. Он также агностичен к существованию объектов, не являющихся множествами, и даже не предполагает, что члены$\nn$являются множествами. Он также рассматривает декартовы произведения и упорядоченные пары как встроенные абстрактные понятия. Вот как мы используем их в реальной математике. (Точнее, приведенная выше система напрямую интерпретирует ZFC за вычетом регулярности.)