Войти
Подстановка - фундаментальное понятие в логике. Замещение является синтаксическим преобразованием в формальных выражениях. Чтобы применить подстановку к экспрессии средства, чтобы последовательно заменить его переменной, или заполнитель, символы другими выражениями. Результирующее выражение называется экземпляром подстановки или коротким экземпляром исходного выражения.
Там, где ψ и ф представляют формулы логики высказываний, ψ является замена экземпляра из ф тогда и только тогда, когда ψ могут быть получены из ф путем подстановки формулы для символов в ф, заменяя каждое вхождение одного и того же символа путем вхождения той же формулы. Например:
является экземпляром подстановки:
а также
является экземпляром подстановки:
В некоторых системах дедукции для логики высказываний новое выражение ( пропозиция ) может быть введено в строку вывода, если это подстановка предыдущей строки вывода (Hunter 1971, стр. 118). Так вводятся новые линии в некоторых аксиоматических системах. В системах, использующих правила преобразования, правило может включать использование экземпляра подстановки с целью введения определенных переменных в производную.
В логике первого порядка каждая закрытая пропозициональная формула, которая может быть получена из открытой пропозициональной формулы a путем подстановки, называется экземпляром подстановки a. Если a - замкнутая пропозициональная формула, мы считаем само a как ее единственный пример подстановки.
Пропозициональная формула является тавтологией, если она истинна при любой оценке (или интерпретации ) ее предикатных символов. Если Φ - тавтология, а Θ - подстановка Φ, то Θ снова является тавтологией. Этот факт подразумевает обоснованность правила дедукции, описанного в предыдущем разделе.
В логике первого порядка, А замена является полным отображением σ: V → T из переменных в терминах ; многие, но не все авторы дополнительно требуют σ ( x) = x для всех переменных x, кроме конечного числа. Обозначение { x 1 ↦ t 1,…, x k ↦ t k } относится к замене, отображающей каждую переменную x i в соответствующий терм t i, для i = 1,…, k, и каждую другую переменную в себя; х я должен быть попарно различны. Применение этой замены к терму t записывается в постфиксной записи как t { x 1 ↦ t 1,..., x k ↦ t k }; это означает (одновременно) заменить каждое вхождение каждого x i в t на t i. Результат tσ применения подстановки σ к термину t называется экземпляром этого члена t. Например, применяя замену { x ↦ z, z ↦ h ( a, y)} к члену
| f ( | z | , а, г ( | Икс | ), у) | дает |
| f ( | ч ( а, у) | , а, г ( | z | ), у) | . |
Область определения dom ( σ) подстановки σ обычно определяется как набор фактически заменяемых переменных, т. Е. Dom ( σ) = { x ∈ V | xσ ≠ x }. Подстановка называется базовой заменой, если она отображает все переменные своего домена на основные, то есть свободные от переменных, термины. Экземпляр замену tσ подстановки земли является терм, если все Т « переменных s в сг » домена с, то есть, если вары ( т) ⊆ дом ( σ). Подстановка σ называется линейное замещение, если tσ является линейным термином для некоторого (и, следовательно, каждый) линейный член т, содержащий именно переменные сг ' ы домена, т.е. с VARS ( т) = дом ( сг). Подстановка σ называется плоской заменой, если xσ является переменной для каждой переменной x. Подстановка σ называется подстановкой переименования, если это перестановка на множестве всех переменных. Как и любая перестановка, переименование σ всегда имеет обратную замену σ −1, такую что tσσ −1 = t = tσ −1σ для каждого члена t. Однако невозможно определить обратное для произвольной замены.
Например, { x ↦ 2, y ↦ 3 + 4} является основной заменой, { x ↦ x 1, y ↦ y 2 +4} не является основной и неплоской, но линейной, { x ↦ y 2, y ↦ y 2 +4} является нелинейным и неплоским, { x ↦ y 2, y ↦ y 2 } является плоским, но нелинейным, { x ↦ x 1, y ↦ y 2 } одновременно линейным и плоский, но не переименование, поскольку он отображает y и y 2 в y 2 ; каждая из этих замен имеет набор { x, y } в качестве области определения. Пример подстановки переименования: { x ↦ x 1, x 1 ↦ y, y ↦ y 2, y 2 ↦ x }, он имеет обратное { x ↦ y 2, y 2 ↦ y, y ↦ x 1, x 1 ↦ x }. Плоская подстановка { x ↦ z, y ↦ z } не может иметь обратного, так как, например, ( x + y) { x ↦ z, y ↦ z } = z + z, и последний член не может быть преобразован обратно в x + y, поскольку информация о происхождении z теряется. Основная подстановка { x ↦ 2} не может иметь инверсию из-за аналогичной потери информации о происхождении, например, в ( x +2) { x ↦ 2} = 2 + 2, даже если замена констант на переменные была разрешена каким-то фиктивным видом «обобщенные замены».
Две замены считаются равными, если они отображают каждую переменную в структурно равных условиях результата, формально: σ = τ, если xσ = хт для каждой переменной х ∈ V. Композицию из двух замен σ = { х 1 ↦ т 1,..., х к ↦ т к } и τ = { у 1 ↦ U 1,..., у л ↦ у л } получается удалением из подстановки { х 1 ↦ t 1 τ,…, x k ↦ t k τ, y 1 ↦ u 1,…, y l ↦ u l } те пары y i ↦ u i, для которых y i ∈ { x 1,…, x k }. Композиция σ и τ обозначается στ. Композиция является ассоциативной операцией и совместима с применением замены, т. Е. ( Ρσ) τ = ρ ( στ) и ( tσ) τ = t ( στ), соответственно, для каждой замены ρ, σ, τ и каждого члена t. Замена идентичности, которая отображает каждую переменную в себе, является нейтральным элементом замещения композиции. Подстановка σ называется идемпотентной, если σσ = σ, и, следовательно, tσσ = tσ для каждого члена t. Подстановка { x 1 ↦ t 1,…, x k ↦ t k } идемпотентна тогда и только тогда, когда ни одна из переменных x i не встречается ни в одном t i. Подстановочная композиция не коммутативна, то есть στ может отличаться от τσ, даже если σ и τ идемпотентны.
Например, { x ↦ 2, y ↦ 3 + 4} равно { y ↦ 3 + 4, x 2}, но отличается от { x ↦ 2, y ↦ 7}. Подстановка { x ↦ y + y } идемпотентна, например (( x + y) { x ↦ y + y }) { x ↦ y + y } = (( y + y) + y) { x ↦ y + y } = ( y + y) + y, в то время как подстановка { x ↦ x + y } неидемпотентна, например (( x + y) { x ↦ x + y }) { x ↦ x + y } = (( х + у) + у) { х ↦ х + у } = (( х + у) + у) + у. Пример для неперестановочных замен { х ↦ у } { у ↦ г } = { х ↦ г, у ↦ г }, а { у ↦ г } { х ↦ у } = { х ↦ у, у ↦ г }.
