Claw.ru | Рефераты по математике | Структура исчисления предикатов - построение логического вывода Структура исчисления предикатов - построение логического вывода | Категория реферата: Рефераты по математике | Теги реферата: как лечить шпоры, реферат на тему земля | Добавил(а) на сайт: Ленин. Предыдущая страница реферата | 1  2  3  4  5  6  7  8 | Следующая страница реферата A(t) [Г] ∃x A(x) [Г]

	Здесь ∃x A(x) – имеющееся в выводе допущение, а В и никакое допущение из Г не содержат x свободно.

B[Г, A(x)] B[Г, ∃x A(x)]

∃и :

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

Если в выводе получена формула ∃х А(х} и нужно вывести В, не выводимую непосредственно из имеющихся формул, вводим допущение А(х), применяя способ рассуждения согласно ∃и.

Рассмотрим несколько примеров выводов.

Схема доказательства формул вида: ¬∃x A(x) ⊃∀x¬A(x):

+ 1. ¬∃x A(x) [1].

+ 2. A(x) [2].

   3. ∃x A(x) [2] – из 2, ∃в.

   4. ¬ A(x) [1] – из 1,3, ¬в.

   5. ∀x¬A(x) [1] – из 4, ∀в.

   6. ¬∃x A(x) ⊃∀x¬A(x) [ - ] – из 5, ⊃в.

Схемы доказательств рассмотренных в аксиоматической системе аксиом «введения ∀ в консеквент» и «введения ∃ в антецедент»:

Предполагается, что А не содержит х свободно.

+  1. ∀x (A ⊃ B(x)) [1].

+  2. А [2].

3. A ⊃ В(х) [1] —из 1, ∀и.

4. В(х) [1, 2] —из3 и 2, ⊃и.

5. ∀x B(x) [1, 2] —из 4, ∀в.

6. A⊃∀x B(x) [1] —из5, ⊃в.

7. ∀x (A ⊃ B(x)) ⊃ (A ⊃∀x B(x)) [ - ] —из 6, ⊃в.

Рекомендуем скачать другие рефераты по теме: курсовик, реферат по биологии 7 класс.





Предыдущая страница реферата | 1  2  3  4  5  6  7  8 | Следующая страница реферата