Предикаты. Помогите c решением.

[Pavlovsky]

∀x(x четно) v ∀x(x нечетно) = 0 x принадлежит множеству натуральных чисел

[Natrix]

Source of the post
x(x четно) v ∀x(x нечетно) = 0 x принадлежит множеству натуральных чисел

Напомню, что дизъюнкция истинна, когда хотя бы одно из высказываний истинно.
Для любого натурального х, х либо четно, либо нечетно.

[Pavlovsky]

Для любого натурального х, х либо четно, либо нечетно.
эквивалентно
∀x((x четно) v (x нечетно))
и преобразование в
∀x(x четно) v ∀x(x нечетно) некорректно. Нет такого правила!

[Natrix]

Source of the post
Для любого натурального х, х либо четно, либо нечетно.
эквивалентно
∀x((x четно) v (x нечетно))
и преобразование в
∀x(x четно) v ∀x(x нечетно) некорректно. Нет такого правила!

Пшепрашем пана! У меня такого преобразования нет! B последней строке прописано:
Для каждого х B-истинно
или
для каждого х A-истинно
или
для каждого х неВ-истинно.

Очевидно, что в этой тройке высказываний есть истинное. B этом случае дизъюнкция этих высказываний истинна.

[Slayer D]

O, оно все таки доказывается ?!?!?!!!! (я просто давно не заходил)

[Slayer D]

Есть еще один пример, посложнее. Его надо привести к ССФ (Сколемовская стандартная форма). Из алгоритма приведения к ССФ следует, что формулу сначала необходимо привести к ПНФ (Предваренная нормальная форма). Так вот, я c этим застрял немного, помогите пж-та.

Исходный пример:
∀x(¬A(x)->∃y(¬B(y)))->(B(x)->A(x))

Мои действия:
∀x(¬A(x)->∃y(¬B(y)))->(B(x)->A(x))
∀x(A(x)v∃y(¬B(y)))->(¬B(x)vA(x))
∀x(A(x)v∀y(B(y)))->(¬B(x)vA(x))
¬(∀x(A(x)v∀y(B(y))))v(¬B(x)vA(x))
дальше немогу

[Pavlovsky]

Где то так (Если ничего не напутал)

Приведение к ПНФ

1) ¬∀x(A(x)v∃y(¬B(y)))v( ¬B(x)vA(x))
2) ∃x[¬A(x)& ∀y(B(y))]v[¬B(x)vA(x)]
3) ∃x[¬A(x) & ∀yB(y)]v[¬B(z)vA(z)]
4) ∃x∀y [(¬A(x) & B(y))v(¬B(z)vA(z))]
5) ∃x∀y [(¬A(x)v¬B(z)vA(z)) & (B(y)v¬B(z)vA(z))]

Приведение к ССФ

1) ∀y [(¬A(a)v¬B(z)vA(z)) & (B(y)v¬B(z)vA(z))]
При решении использовано: [url=http://www.univer.omsk.su/departs/compsci/...gic/logika1.doc]http://www.univer.omsk.su/departs/compsci/...gic/logika1.doc[/url]

[Slayer D]

Source of the post
Где то так (Если ничего не напутал)

Приведение к ПНФ

1) ¬∀x(A(x)v∃y(¬B(y)))v( ¬B(x)vA(x))
2) ∃x[¬A(x)& ∀y(B(y))]v[¬B(x)vA(x)]
3) ∃x[¬A(x) & ∀yB(y)]v[¬B(z)vA(z)]
4) ∃x∀y [(¬A(x) & B(y))v(¬B(z)vA(z))]
5) ∃x∀y [(¬A(x)v¬B(z)vA(z)) & (B(y)v¬B(z)vA(z))]

Приведение к ССФ

1) ∀y [(¬A(a)v¬B(z)vA(z)) & (B(y)v¬B(z)vA(z))]
При решении использовано: [url=http://www.univer.omsk.su/departs/compsci/...gic/logika1.doc]http://www.univer.omsk.su/departs/compsci/...gic/logika1.doc[/url]

Большое спасибо. У меня возник один вопрос при решении аналогичного примера: после приведения к ССФ ведь может остаться отрицание над каким-нибудь предикатом?

[Slayer D]

Пож-та проверьте правильность решения и исправьте, если будут ошибки, желательно поскорее. Приведение к ССФ:

(∀x(B(x))->∀y(A(y)))^(∀y(B(y)->A(x)->C(z)))->∃z(C(z))
¬((¬(∀x(B(x)))v∀y(A(y)))^(∀y(¬B(y)v¬A(x)->C(z))))v∃z(C(z))
(∀x(B(x))^∃y(¬A(y)))v(∃y(B(y)^A(x)^¬C(z)))v∃z(C(z))
(∀n(B(n))^∃m(¬A(m)))v(∃y(B(y)^A(x)^¬C(z)))v∃t(C(t))
∀n∃m∃y∃t(B(n)^¬A(m)vB(y)^A(x)^C(z)vC(t))
∀n(B(k)^¬(A(f(m)))vB(f(y))^A(x)^C(z)vC(f(t)))

[Pavlovsky]

1. B(y)->A(x)->C(z)
Это как? Надо.
(B(y)->A(x))->C(z) или B(y)->(A(x)->C(z))

2. ∀n(B(k)^¬(A(f(m)))vB(f(y))^A(x)^C(z)vC(f(t)))
замена неверно. Надо
∀n(B(n)^¬(A(fm(n)))vB(fy(n))^A(x)^C(z)vC(ft(n)))

Остальное тщательно не смотрел