Главная страница Случайная страница
КАТЕГОРИИ:
АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника
Г) в результате подстановки ни одна свободная переменная не должна становиться связанной1.
|
|
Поясним сказанное примерами.
Пусть выражение $x R(x, y) означает фразу «Существует целое число х, не равное произвольному числу у».
Данное выражение будет оставаться истинным при любой подстановке, кроме случая, когда вместо переменной у подставим связанную переменную х:
$x R(x, x).
Получим ложное высказывание «Существует целое число х, не равное самому себе».
Или возьмем ту же формулу, но с предикатом R – «отец», а переменные х и у пусть будут определены на области людей. Тогда формула $х R(x, y) будет представлять истинные выражения до тех пор, пока на место свободной переменной у не подставим связанную переменную х. Подобная подстановка приведет к появлению нелепого высказывания «Существует человек, являющийся отцом самого себя».
После сделанных замечаний перейдем к формулировке правил введения и удаления кванторов.
Правило удаления квантора общности (У"):
" x A
A(x/t)
Буквально данное правило означает, что если все предметы универсума рассуждения удовлетворяют некоторому условию (простому или сложному) A, то этому условию удовлетворяетлюбой предмет, выбранный из данного универсума.
Правило введения квантора общности (В"):
Если формула В(х) содержит свободные вхождения предметной переменной х, а формула А не содержит свободных вхождений х, то из формулы А É В(х) выводима формула А É " х В(х).
А É В(х) |- А É " х В(х)
Либо в такой записи:
А É В(х) ___
А É " х В(х)
Суть данного правила заключается в том, что если из некоторых посылок и допущения А со связанной переменной х выводится формула В(х), то из тех же посылок и допущения А выводится формула " х В(х).
Другими словами, если в процессе выведения получаем утверждение о том, что произвольный предмет некоторой предметной области обладает определенным признаком, то можно утверждать, что все предметы данной области обладают этим признаком.
Заметим, что правило (В") можно применять только в тех случаях, когда все вхождения х в А являются связанными. В противном случае формула В(х) превратится в истинное высказывание только для тех значений х, для которых A истинно. Однако подобной особенностью могут обладать не все значения переменной x, так что формула В(х) не будет истинной для всех значений х. В последнем случае высказывание " х В(х) окажется ложным.
Правило введения квантора существования (В$):
A(x/t)
$x A
Из этого првила вытекает, что если некоторый выбранный из предметной области предмет t удовлетворяет условию A, то существует по крайней мере один предмет, удовлетворяющий данному условию.
Правило удаления квантора существования (У$):
$x A
A(x/t)
Из этого правила вытекает, что из истинного экзистенциального высказывания $x A следует истинность высказывания A(t), которое является результатом подстановки пост константы (замкнутого терма) t вместосвободной переменной x.
Правила (У") и (В$) являются более сильными, чем правила (В") и (У$), поскольку в их основе лежит отношение логического следования. Дело в том, что переход от формулы " x A к формуле A(x/t) и от формулы A(x/t) к формуле $x A оправдан наличием между ними отношения логического следования: " x A |= A(x/t), A(x/t) |= $х A.
Совсем другая ситуация для правилА (У$). В его основе отсутствует отношение логического следования. И тем не менее в исчислении предикатов данное правило все же принимается. Однако, чтобы не допустить выведения из истинных посылок ложных следствий, необходимо, в случае применения данного правила, придерживаться в процессе формального вывода некоторых ограничений, о которых будет сказано ниже.
Доказательством (выводом) формулы A называется последовательность формул В1, В2 ,... Вn = A такая, что для любого Bi (1 Ô iÔ n) формула Вi является: