Из Википедии, свободной энциклопедии
Перейти к навигации Перейти к поиску

В математической логике , термы из формальной системы является термином , который не содержит какие - либо переменный . Точно так же основная формула - это формула , не содержащая никаких переменных.

В логике первого порядка с идентичностью предложение Q ( a ) ∨ P ( b ) является основной формулой, где a и b являются постоянными символами. Выражение заземления является термами или молотой формула.

Примеры [ править ]

Рассмотрим следующие выражения в логике первого порядка над подписью, содержащей постоянный символ 0 для числа 0, унарный функциональный символ s для функции-преемника и двоичный функциональный символ + для сложения.

  • s (0), s ( s (0)), s ( s ( s (0))), ... основные термины,
  • 0 + 1, 0 + 1 + 1, ... - основные термины,
  • x  +  s (1) и s ( x ) - термины, но не основные,
  • s (0) = 1 и 0 + 0 = 0 - основные формулы,

Формальное определение [ править ]

Ниже приводится формальное определение языков первого порядка . Пусть задан язык первого порядка, где C - набор постоянных символов, V - набор (индивидуальных) переменных, F - набор функциональных операторов, а P - набор предикатных символов .

Основные условия [ править ]

Основные термины - это термины , не содержащие переменных. Их можно определить логической рекурсией (формула-рекурсия):

  1. Элементы C являются основными терминами;
  2. Если f ∈ F является n- мерным функциональным символом и α 1 , α 2 , ..., α n являются основными членами, то f (α 1 , α 2 , ..., α n ) является основным членом.
  3. Каждый основной термин может быть задан конечным применением двух вышеупомянутых правил (других основных терминов нет; в частности, предикаты не могут быть основными терминами).

Грубо говоря, вселенная Хербранда - это совокупность всех основных терминов.

Земной атом [ править ]

Основной предикат , основной атом или основной литерал - это атомарная формула, все аргументы которой являются основными.

Если p ∈ P является n- мерным предикатным символом и α 1 , α 2 , ..., α n являются основными членами, то p (α 1 , α 2 , ..., α n ) является основным предикатом или основанием атом.

Грубо говоря, база Herbrand - это набор всех основных атомов, в то время как интерпретация Herbrand присваивает значение истинности каждому основному атому в базе.

Формула основания [ править ]

Основная формула или основное предложение - это формула без переменных.

Формулы со свободными переменными могут быть определены с помощью синтаксической рекурсии следующим образом:

  1. Свободные переменные неотделанного атома - это все переменные, входящие в него.
  2. Свободные переменные ¬ p такие же, как переменные p . Свободные переменные p ∨ q , p ∧ q , p → q - это свободные переменные p или свободные переменные q .
  3. Свободные переменные x  p и ∃ x  p являются свободными переменными p, кроме x .

Ссылки [ править ]