Расширения первого и более высокого порядка
Краткое описание системы первого порядка
Логика предыдущего раздела является примером односортированной логики, то есть логики с единственным видом объекта: высказываний. Было предложено множество расширений этой простой структуры; в этом разделе мы расширим ее с помощью второго рода индивидуумов или терминов . Точнее, мы добавим новый вид суждения " t - термин " (или " t термин "), где t является схематичным. Мы зафиксируем счетный набор V переменных , другой счетный набор F функциональных символов и построим термины со следующими правилами формирования:
v ∈ V v term var F {\displaystyle {\frac {v\in V}{v{\hbox{ term}}}}{\hbox{ var}}_{F}}
и
f ∈ F t 1 term t 2 term ⋯ t n term f ( t 1 , t 2 , ⋯ , t n ) term app F {\displaystyle {\frac {f\in F\qquad t_{1}{\hbox{ term}}\qquad t_{2}{\hbox{ term}}\qquad \cdots \qquad t_{n}{\hbox{ term}}}{f(t_{1},t_{2},\cdots ,t_{n}){\hbox{ term}}}}{\hbox{ app}}_{F}}
Для предложений мы рассматриваем третье счетное множество P предикатов и определяем атомарные предикаты над терминами со следующим правилом формирования:
ϕ ∈ P t 1 term t 2 term ⋯ t n term ϕ ( t 1 , t 2 , ⋯ , t n ) prop pred F {\displaystyle {\frac {\phi \in P\qquad t_{1}{\hbox{ term}}\qquad t_{2}{\hbox{ term}}\qquad \cdots \qquad t_{n}{\hbox{ term}}}{\phi (t_{1},t_{2},\cdots ,t_{n}){\hbox{ prop}}}}{\hbox{ pred}}_{F}}
Первые два правила формирования дают определение термина, которое фактически совпадает с определением в алгебре терминов и теории моделей , хотя фокус этих областей исследования сильно отличается от естественной дедукции. Третье правило формирования эффективно определяет атомарную формулу , как в логике первого порядка , так и в теории моделей.
К ним добавлена пара правил формирования, определяющих обозначения для квантифицированных предложений; по одному для универсальной ( ∀ ) и экзистенциальной ( ∃ ) квантификации :
x ∈ V A prop ∀ x . A prop ∀ F x ∈ V A prop ∃ x . A prop ∃ F {\displaystyle {\frac {x\in V\qquad A{\hbox{ prop}}}{\forall x.A{\hbox{ prop}}}}\;\forall _{F}\qquad \qquad {\frac {x\in V\qquad A{\hbox{ prop}}}{\exists x.A{\hbox{ prop}}}}\;\exists _{F}}
Универсальный квантификатор содержит правила введения и исключения:
a term u ⋮ [ a / x ] A true ∀ x . A true ∀ I u , a ∀ x . A true t term [ t / x ] A true ∀ E {\displaystyle {\cfrac {\begin{array}{c}{\cfrac {}{a{\text{ term}}}}{\text{ u}}\\\vdots \\{}[a/x]A{\text{ true}}\end{array}}{\forall x.A{\text{ true}}}}\;\forall _{I^{u,a}}\qquad \qquad {\frac {\forall x.A{\text{ true}}\qquad t{\text{ term}}}{[t/x]A{\text{ true}}}}\;\forall _{E}}
У экзистенциального квантора есть правила введения и исключения:
[ t / x ] A true ∃ x . A true ∃ I a term u [ a / x ] A true v ⏟ ⋮ ∃ x . A true C true C true ∃ E a , u , v {\displaystyle {\frac {[t/x]A{\hbox{ true}}}{\exists x.A{\hbox{ true}}}}\;\exists _{I}\qquad \qquad {\cfrac {\begin{array}{cc}&\underbrace {\,{\cfrac {}{a{\hbox{ term}}}}{\hbox{ u}}\quad {\cfrac {}{[a/x]A{\hbox{ true}}}}{\hbox{ v}}\,} \\&\vdots \\\exists x.A{\hbox{ true}}\quad &C{\hbox{ true}}\\\end{array}}{C{\hbox{ true}}}}\exists _{E^{a,u,v}}}
В этих правилах обозначение [ t / x ] A обозначает замену t для каждого (видимого) экземпляра x в A , избегая захвата. [8] Как и прежде, верхние индексы в названии обозначают компоненты, которые разряжаются: термин a не может встречаться в выводе из ∀ I ( такие термины известны как собственные переменные или параметры), а гипотезы, названные u и v в ∃ E , локализованы на второй посылке гипотетического вывода . Хотя пропозициональная логика предыдущих разделов была разрешима , добавление кванторов делает логику неразрешимой.
Пока что квантифицированные расширения являются первого порядка: они отличают предложения от видов объектов, определяемых количественно. Логика высшего порядка использует другой подход и имеет только один вид предложений. Кванторы имеют в качестве области квантификации те же самые утверждения, что и отраженные в правилах формирования:
p prop u ⋮ A prop ∀ p . A prop ∀ F u p prop u ⋮ A prop ∃ p . A prop ∃ F u {\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{p{\hbox{ prop}}}}{\hbox{ u}}\\\vdots \\A{\hbox{ prop}}\\\end{matrix}}{\forall p.A{\hbox{ prop}}}}\;\forall _{F^{u}}\qquad \qquad {\cfrac {\begin{matrix}{\cfrac {}{p{\hbox{ prop}}}}{\hbox{ u}}\\\vdots \\A{\hbox{ prop}}\\\end{matrix}}{\exists p.A{\hbox{ prop}}}}\;\exists _{F^{u}}}
Обсуждение форм введения и исключения для логики высшего порядка выходит за рамки этой статьи. Возможно находиться между логиками первого и более высокого порядка. Например, в логике второго порядка есть два вида предложений: один вид, определяющий количество терминов, а второй вид, определяющий количество предложений первого рода.