SHPORA.net :: PDA

Login:
регистрация

Main
FAQ

гуманитарные науки
естественные науки
математические науки
технические науки
Search:
Title: | Body:

Правило подстановки


Пусть U формула, содержащая переменную А. Тогда, если U - выводимая формула исчисления высказывания, то, заменив в ней



переменную А произвольной формулой b,получим так же выводимую формулу .

Правило заключения (modUs pones)

Если U и U->b выводимые формулы, то b так же выводима (правило отделения). (U, U->b b ).

Выводом формулы G из формул F1, …,Fn называется такая последовательность формул E1,…, En, где Ек=G и любая формула Ei(i<*>к)



является:

• либо аксиомой;

• либо формулой FJ(Ei=FJ);

• либо Ei получается из каких-либо предыдущих E1,…, Ei-1, одним из правил выведения ;

Сама формула G называется выводимой из формул F1,…,Fn .

F1,…,Fn ¬├ G.

Формула G выводимая только из аксиом называется теоремой, а вывод - доказательство этих теорем.



При построении вывода можно пользоваться уже полученными результатами, в частности, полученными теоремами и очень важной



теоремой: