Древесное доказательство и древесный вывод из множества гипотез

До сих пор мы имели дело с выводами в виде последовательности формул, но часто вместо этого «полезно рассматривать (вхождения) формул в некотором частичном упорядочении, которое прямо представляет логическую структуру вывода» [19, с. 98—99].

В таком упорядочении посылки каждого вывода пишутся «непосредственно над» заключением и никакое (вхождение) формулы не служит посылкой более чем для одного вывода.

Определение.

Понятие «древесное доказательство формулы А в гилъбертовеком исчислении» определим индуктивно:

  • 1) древесным доказательством аксиомы гилъбертовского исчисления является она сама;
  • 2) если Db ..., Dn — древесные доказательства формул Аь ..., Ап соответственно, а формула Л является непосредственным следствием формул А ..., Ап, по одному из основных правил вывода 1, 2, 3, то слово вида

является древесным доказательством формулы А.

Определение.

Понятие «древесный вывод формулы А из множества формул Я в гилъбертовском исчислении» определим индуктивно:

  • 1) древесным выводом аксиомы А из множества Я является А;
  • 2) древесным выводом формулы Ае Низ множества Я является А;
  • 3) если Db ...,Dn — древесные выводы формул Аь ...,Ап из множества Я соответственно, а формула Л является непосредственным следствием формул Аг, ..., Ап по одному из основных правил вывода 1, 2, 3, причём при применении правил вывода 2 и 3 предметная переменная х не входит ни в одну формулу из множества Я свободно, то слово вида

является древесным выводом формулы А из множества формул Я.

Теперь можно сокращённо обозначать древесный вывод форму-

def

лы А из множества формул Я = },..., Ап} следующим образом:

Индукция по построению доказательства

Индуктивные определения оправдывают соответствующие виды доказательств «с помощью математической индукции». Примером является следующий способ доказательства, называемый индукцией по построению доказательства формулы.

Определение.

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

Пусть доказано, что:

  • 1) каждая аксиома обладает некоторым свойством;
  • 2) если посылки какого-либо основного правила вывода обладают этим свойством, то и непосредственное следствие обладает этим свойством.

Тогда каждая доказуемая формула обладает указанным свойством.

Определение.

  • 1. (По [44, с. 52].) Анализом (линейного) вывода (доказательства), имеющего вид Al5 ...,Ап, будем называть явное указание на то, на каком основании каждая формула A,-, i = 1, ..., п, входит в линейный вывод (доказательство): как аксиома, в качестве гипотезы или как формула, непосредственно выводимая из предшествующих формул по определенному основному правилу вывода.
  • 2. (По [120, с. 29].) Определение понятия «вывод»доказательство») в логистическом исчислении будем называть эффективным определением, если относительно любой последовательности формул мы, проведя анализ вывода (доказательства), можно однозначно установить, является она выводом (доказательством) или нет.

Определение.

Определим индуктивно функцию h, которую назовем высотой древесного вывода и которая отображает множество всевозможных древесных выводов в множество N:

def

  • 1) fr(D) = 0, если D — древесный вывод аксиомы или формулы, принадлежащей Н;
  • ( n п Л def
  • 2) h 1n Ul + max(h(D1),...,/i(D1)),

I Л )

если D1}Dn — древесные выводы формул Аь ...,Ап из множества Н соответственно, формула Л является непосредственным следствием формул А1} ...,Ап по одному из основных правил вывода, а шах (а1? ..., ап) — функция, значением которой является наибольшее из аь апе N.

 
Посмотреть оригинал
< Пред   СОДЕРЖАНИЕ   ОРИГИНАЛ     След >