置換（論理）

置換とは、形式表現に対する構文変換のことです。式に置換を適用するとは、その式の変数記号、またはプレースホルダー記号を、他の式で一貫して置き換えることを意味します。

結果として得られる式は、元の式の置換インスタンス、または略してインスタンスと呼ばれます。

命題論理

意味

ここで、ψとφは命題論理の式を表す。ψがφの置換インスタンスであるのは、φの命題変数を式で置き換え、同じ変数の出現箇所を同じ式の出現箇所に置き換えることによってψがφから得られる場合に限る。例：

ψ: (R → S) & (T → S)

置換インスタンス

φ: P & Q

つまり、ψはφ中のPとQをそれぞれ(R → S)と(T → S)に置き換えることで得られる。同様に：

ψ: (A ↔ A) ↔ (A ↔ A)

は、以下の置換インスタンスです。

φ: (A ↔ A)

ψはφ中の各Aを(A ↔ A)に置き換えることで得られる。

命題論理のいくつかの演繹システムでは、新しい式（命題）は、導出の前の行の置換インスタンスである場合に、導出の行に入力できます。^{[ 1 ]}これは、いくつかの公理系で新しい行が導入される方法です。変換規則を使用するシステムでは、規則には、特定の変数を導出に導入する目的で置換インスタンスを使用することが含まれる場合があります。

同義反復

命題論理式は、その述語記号のあらゆる評価（または解釈）の下で真である場合、トートロジーである。Φがトートロジーであり、ΘがΦの置換例である場合、Θもまたトートロジーである。この事実は、前節で述べた演繹規則の健全性を意味する。

一階述語論理

一階述語論理では、置換とは変数から項への全写像 $σ : V \to T$ のことである。多くの著者^[²^]^:⁷³^[³^]^:⁴⁴⁵だが、すべての著者^[⁴^]^:²⁵⁰は、有限個の変数xを除くすべての変数に対してσ ( x ) = x を要求している。表記{ x ₁↦ t ₁, …, x _k ↦ t _k } ^[^{注 1}^]は、 i =1,…, kに対して各変数x _iを対応する項t _iに、他のすべての変数をそれ自身に写像する置換を指す。x _{i は}ペアごとに異なっていなければならない。ほとんどの著者は、同じ置換に対して無限に多くの異なる表記を避けるため、各項t _iが構文的にx _iと異なっていることを要求している。項tにその置換を適用することは、後置記法でt { x ₁↦ t ₁, ..., x _k ↦ t _k }と表記されます。これは、 t内の各x _iのすべての出現箇所をt _iで（同時に）置き換えることを意味します。^[^{注 2}^]項tに置換σを適用した結果tσは、その項tのインスタンスと呼ばれます。たとえば、項に置換{ x ↦ z , z ↦ h ( a , y ) }を適用すると、

置換σのドメインdom ( σ )は、実際に置き換えられる変数の集合として一般的に定義されます。つまり、dom ( σ ) = { x ∈ V | xσ ≠ x }です。置換は、そのドメインのすべての変数を、基底、つまり変数を含まない項にマッピングする場合、基底置換と呼ばれます。基底置換の置換インスタンスtσは、 tのすべての変数がσのドメインにある場合、つまりvars ( t ) ⊆ dom ( σ ) の場合、基底項です。置換σは、 tσが、 σのドメインの変数を正確に含む(したがってすべての) 線形項tの線形項である場合、つまりvars ( t ) = dom ( σ )の場合、線形置換と呼ばれます。置換σは、すべての変数xに対してxσが変数である場合、フラット置換と呼ばれます。置換σは、すべての変数の集合に対する置換である場合、名前変更置換と呼ばれます。すべての順列と同様に、名前変更置換 σ には必ず逆置換σ ⁻¹が存在し、すべての項tに対してtσσ ⁻¹ = t = tσ ⁻¹σが成り立ちます。ただし、任意の置換に対して逆を定義することはできません。

例えば、{ x ↦ 2, y ↦ 3+4 }は基底置換であり、{ x ↦ x ₁, y ↦ y ₂+4 }は基底でも平坦でもないが線形であり、 { x ↦ y ₂, y ↦ y ₂+4 }は非線形かつ平坦ではなく、{ x ↦ y ₂, y ↦ y ₂}は平坦であるが非線形であり、{ x ↦ x ₁, y ↦ y ₂}は線形かつ平坦であるが、yとy _{2の両方を}y ₂に写像するため、名前変更ではない。これらの置換はそれぞれ集合{ x , y }を定義域とする。名前変更置換の例は{ x ↦ x ₁, x ₁↦ y , y ↦ y ₂, y ₂↦ x }であり、その逆は{ x ↦ y ₂, y ₂↦ y , y ↦ x ₁, x ₁↦ x }です。平面置換{ x ↦ z , y ↦ z }は逆を持ちません。なぜなら、例えば ( x + y ) { x ↦ z , y ↦ z } = z + zであり、後者の項は、 zの由来に関する情報が失われるため、x + yに戻すことができないからです。基底置換{ x ↦ 2 }も同様に、例えば ( x +2) { x ↦ 2 }のように、由来情報が失われるため、逆を持ちません。定数を変数に置き換えることが何らかの架空の「一般化された置換」によって許可されていたとしても、= 2+2 となる。

2 つの置換は、各変数を構文的に等しい結果項にマッピングする場合に等しいとみなされます。形式的には、各変数x ∈ Vに対してxσ = xτの場合、 σ = τとなります。2つの置換σ = { x 1 _↦t 1 _,…, x _k ↦ t _k }とτ = { y ₁↦ u ₁, …, y _l ↦ u _l }の合成は、置換{ x ₁↦ t ₁τ , …, x _k ↦ t _k τ , y ₁↦ u ₁, …, y _l ↦ u _l }から、y _i ∈ { x ₁, …, x _k }となるペアy _i ↦ u _iを取り除くことによって得られます。σとτの合成はστで表されます。合成は結合法則を満たす演算であり、置換の適用と互換性があります。つまり、すべての置換ρ、σ、τおよびすべての項tに対して、それぞれ( ρσ ) τ = ρ ( στ ) および ( tσ ) τ = t ( στ ) が成り立ちます。すべての変数をそれ自身に写像する恒等置換は、置換合成の中立要素です。置換σ は、 σσ = σの場合、冪等であると呼ばれ、したがってすべての項tに対してtσσ = tσとなります。すべてのiに対してx _i ≠ t _iの場合、置換{ x ₁↦ t ₁, …, x _{k }は、} ↦ t _k }は、変数x _{i が}どのt _jにも出現しない場合に限り冪等である。置換合成は可換ではない。つまり、σとτが冪等であっても、 στ はτσと異なる可能性がある。^[²^]^:^73–74^[³^]^:^445–446

例えば、{ 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 } = (( x + y )+ y ) { x ↦ x + y } = (( x + y )+ y )+ y となります。非可換置換の例としては、{ x ↦ y } { y ↦ z } = { x ↦ z , y ↦ z }ですが、{ y ↦ z } { x ↦ y } = { x ↦ y , y ↦ z } です。

数学

数学では、置換には 2 つの一般的な用途があります。変数を定数に置き換えること(その変数への代入とも呼ばれます) と、等式の置換特性^[⁵^]、ライプニッツの法則とも呼ばれます^[⁶^]。

数学を形式言語と考えると、変数はアルファベットの記号であり、通常は $x$ 、 $y$ 、 $zのような文字で、取りうる$ 値の範囲を表します。^[⁷^]与えられた式や数式の中で変数が自由変数である場合、その変数はその範囲内の任意の値に置き換えることができます。^[⁸^]束縛変数も置き換えることができます。例えば、式のパラメータ（多項式の係数など）や関数の引数などです。さらに、全称量化されている変数は、その範囲内の任意の値に置き換えることができ、その結果は真のステートメントになります。（これは全称インスタンス化と呼ばれます）

非形式化言語、つまり数理論理学以外のほとんどの数学テキストでは、個々の式について、どの変数が自由変数でどの変数が束縛変数であるかを常に識別できるとは限りません。たとえば、 ${\textstyle \sum _{i<k}a_{ik}}$ 文脈によっては、変数 ${\textstyle i}$ 無料であり、 ${\textstyle k}$ どちらかが束縛されているか、あるいはその逆で、両方が自由であることはできません。どちらの値が自由であるとみなされるかは、文脈と意味論に依存します。

等式の置換性質、あるいはライプニッツの法則（ただし後者の用語は通常、哲学的な文脈で用いられる）は、一般的に、二つのものが等しいならば、一方の性質は他方の性質でもある、と述べている。これは論理記号を用いて形式的に次のように表すことができる。 $(a=b)\implies {\bigl [}\phi (a)\Rightarrow \phi (b){\bigr ]}$ すべての ${\textstyle a}$ そして ${\textstyle b}$ 、そしてあらゆる整った公式 ${\textstyle \phi (x)}$ （自由変数 x を使用）。例: すべての実数 $a$ と $b$ について、 $a = b$ ならば、 $a \geq 0は$ $b \geq 0$ を意味します（ここで、 $\phi (x)$ $x \geq 0$ である。これは代数学、特に連立方程式を解く際に最もよく使われる性質だが、等号を用いる数学のほぼすべての分野に適用される。これは等号の反射的性質と合わせて、一階述語論理における等号の公理を形成する。 ^{[ 9 ]}

置換は関数合成と関連しているが、同一ではない。ラムダ計算におけるβ還元と密接に関連している。しかし、これらの概念とは対照的に、代数学では置換演算による代数構造の保存、すなわち置換によって対象となる構造（多項式の場合は環構造）の準同型写像が得られるという事実に重点が置かれている。

代数

代入は代数学、特にコンピュータ代数学における基本的な演算である。^{[ 10 ]}^{[ 11 ]}

置換の一般的な例として多項式が挙げられます。1変数多項式の不定元に数値（または別の式）を代入することは、その値で多項式を評価することに相当します。実際、この操作は非常に頻繁に行われるため、多項式の表記法はしばしばこの操作に合わせて調整されます。他の数学的対象と同様に、多項式をPのような名前で指定する代わりに、次のように定義することができます。

P(X)=X^{5}-3X^{2}+5X-17

したがって、Xの置換は「 P ( X )」内の置換によって指定できます。

P(2)=13

または

P(X+1)=X^{5}+5X^{4}+10X^{3}+7X^{2}+4X-14.

置換は、記号から構成される他の種類の形式的対象、例えば自由群の要素にも適用できる。置換を定義するためには、不定元を特定の値に写像する一意の準同型写像の存在を主張する、適切な普遍性を持つ代数構造が必要である。置換とは、そのような準同型写像による要素の像を見つけることに相当する。

ZFCにおける置換の証明

以下は、ZFC における等号の置換特性 (等号のない一階述語論理で定義されている) の証明であり、 Gaisi Takeuti と Wilson M. Zaring によるIntroduction to Axiomatic Set Theory (1982) から改変したものである。^{[ 12 ]}

定理—もし $a=b$ すると、任意の整形式式に対して $\phi$ 、 $\phi (a)\Rightarrow \phi (b)$ 。

ツェルメロ・フレンケル集合論 § ZFC における論理式の定義のための形式言語を参照。定義は再帰的であるため、帰納法による証明が用いられる。等号のない一階述語論理の ZFC では、「集合の等価性」は、2 つの集合が同じ要素を持つことを意味し、記号的には「すべての z について、z が x に含まれるのは、z が y に含まれる場合かつその場合に限る」と記述される。そして、外延性の公理は、2 つの集合が同じ要素を持つならば、それらは同じ集合に属すると主張する。

意味- $(x=y):=\forall z[z\in x\Leftrightarrow z\in y]$

公理— $(x=y)\Rightarrow \forall z(x\in z\Leftrightarrow y\in z)$

基本式

させて $X,Y,Z$ は、任意の変数または集合のメタ変数であり、 $X=Y$

ケース1： $\phi (X):(Z\in X)$

仮定する $Z\in X$ すると、平等の定義により、 $Z\in Y$ 、したがって $(X=Y)\implies {\bigl [}Z\in X\Rightarrow Z\in Y{\bigr ]}$

ケース2： $\phi (X):(X\in Z)$

仮定する $X\in Z$ そして外延性の公理により、 $Y\in Z$ 、したがって $(X=Y)\implies {\bigl [}X\in Z\Rightarrow Y\in Z{\bigr ]}$

再帰式

させて $\psi ,\varphi$ 次のような特性を持つ任意の数式のメタ変数である $(a=b)\implies {\bigl [}\phi (a)\Rightarrow \phi (b){\bigr ]}$ 。させて $X,Y$ は、任意の変数または集合のメタ変数であり、 $X=Y$ 、そして $z$ 任意の変数のメタ変数となる。

ケース1： $\neg (\psi )$

以来 $X=Y$ 、それから $Y=X$ 等式の対称性により、 ${\bigl [}\psi (Y)\Rightarrow \psi (X){\bigr ]}$ 帰納仮説によれば、 ${\bigl [}\neg \psi (X)\Rightarrow \neg \psi (Y){\bigr ]}$ 対位法によって、 $(X=Y)\implies {\bigl [}\neg \psi (X)\Rightarrow \neg \psi (Y){\bigr ]}$

ケース2： $\psi \land \varphi$

以来 $X=Y$ 、それから ${\bigl [}\psi (X)\Rightarrow \psi (Y){\bigr ]}$ そして ${\bigl [}\varphi (X)\Rightarrow \varphi (Y){\bigr ]}$ これは、 ${\bigl [}{\bigl (}\psi (X)\land \varphi (X){\bigr )}\Rightarrow \psi (Y)\land \varphi (Y){\bigr )}{\bigr ]}$ 、したがって $(X=Y)\implies {\bigl [}{\bigl (}\psi (X)\land \varphi (X){\bigr )}\Rightarrow \psi (Y)\land \varphi (Y){\bigr )}{\bigr ]}$

ケース3： $\exists z(\psi )$

以来 $X=Y$ 、 $\psi (X,z)\Rightarrow \psi (Y,z)$ 矛盾法則により、結果が偽であると仮定する。 $\exists z(\psi (X,z))$ それは本当だが $\exists z(\psi (Y,z))$ は偽である。存在インスタンス化により、 $z_{0}$ 値を表す $\psi (X,z_{0})$ それは本当です。 $\psi (Y,z_{0})$ 仮定により誤りであるため、 $\psi (X,z_{0})\Rightarrow \psi (Y,z_{0})$ これは偽であり、我々の帰納的仮説と矛盾するため、結果が導かれる。

注記

↑一部の著者は、置換を表すために[ t ₁ / x ₁ , …, t _k / x _k ] を使用しています。たとえば、M. Wirsing (1990)。Jan van Leeuwen (編)。代数仕様。理論計算機科学ハンドブック。Vol. B。Elsevier。pp. 675–788。、ここ：682ページ。
↑項代数の観点から項の集合Tは変数の集合V上の自由項代数であり、したがって各置換写像 σ: V → Tに対して、 V ⊆ T上で σ と一致する一意の準同型写像σ : T → Tが存在します。上記で定義されたσを項tに適用することは、関数σを引数tに適用することとみなされます。

引用文献

↑ハンター、ジェフリー(1996) [1971].メタロジック：標準一階述語論理のメタ理論入門. カリフォルニア大学出版局 (1973 年刊行). p. 118. ISBN 9780520023567OCLC 36312727 （視覚障害のある利用者も利用可能）
1 2 David A. Duffy (1991). Principles of Automated Theorem Proving . Wiley.
1 2 Franz Baader、Wayne Snyder (2001)。Alan Robinson、Andrei Voronkov (編)。統一理論(PDF)。Elsevier。pp. 439–526 。 2015年6月8日にオリジナル(PDF)からアーカイブ。 2014年9月24日に取得。
↑ N. Dershowitz; J.-P. Jouannaud (1990). "書き換えシステム". Jan van Leeuwen (編).形式モデルと意味論. 理論計算機科学ハンドブック. Vol. B. Elsevier. pp. 243–320 .
↑ソボレフ、SK (2001) [1994]、「等号公理」、数学百科事典、EMS Press
↑ハリー・ドイチュ、パヴェル・ガルバッツ、「相対的同一性」、スタンフォード哲学百科事典（2024年秋版）、エドワード・N・ザルタ、ウリ・ノーデルマン編、近日公開予定 URL: https://plato.stanford.edu/entries/identity-relative/#StanAccoIden
↑ Sobolev, SK (2001) [1994]、「個体変数」、数学百科事典、EMS Press
↑ Sobolev, SK (2001) [1994]、「自由変数」、数学百科事典、EMS Press
↑ Fitting, M. , First-Order Logic and Automated Theorem Proving (Berlin/Heidelberg: Springer, 1990), pp. 198–200 .
↑マーガレット・H・ホフト;ハルトムートFWホフト（2002年11月6日）。Mathematica を使った計算。エルゼビア。ISBN 978-0-08-048855-4。
↑ Andre Heck (2012年12月6日). Maple入門. Springer Science & Business Media. ISBN 978-1-4684-0484-5置換。
↑ Takeuti, Gaisi; Zaring, Wilson M. (1982). "Introduction to Axiomatic Set Theory" . Graduate Texts in Mathematics : 6– 9. doi : 10.1007/978-1-4613-8168-6 . ISSN 0072-5285 . 2014年8月6日にオリジナルからアーカイブ済み。

参考文献

Crabbé, M. (2004).置換の概念について. Logic Journal of the IGPL, 12, 111–124.
Curry, HB (1952)抽象的な形式体系における置換、置き換え、および関連概念の定義について. Revue philosophique de Louvain 50, 251–269.
クリーネ、SC（1967）。数理論理学。2002年再版、ドーバー出版。ISBN 0-486-42533-9
Robinson, Alan JA; Voronkov, Andrei (2001-06-22). Handbook of Automated Reasoning . Elsevier. ISBN 978-0-08-053279-0

外部リンク

n ラボにおける置換

[5] 一部の著者は、置換を表すために[ t ₁ / x ₁ , …, t _k / x _k ] を使用しています。たとえば、M. Wirsing (1990)。Jan van Leeuwen (編)。代数仕様。理論計算機科学ハンドブック。Vol. B。Elsevier。pp. 675–788。、ここ：682ページ。

[6] 項代数の観点から項の集合Tは変数の集合V上の自由項代数であり、したがって各置換写像 σ: V → Tに対して、 V ⊆ T上で σ と一致する一意の準同型写像σ : T → Tが存在します。上記で定義されたσを項tに適用することは、関数σを引数tに適用することとみなされます。

[1] ハンター、ジェフリー(1996) [1971].メタロジック：標準一階述語論理のメタ理論入門. カリフォルニア大学出版局 (1973 年刊行). p. 118. ISBN 9780520023567OCLC 36312727 （視覚障害のある利用者も利用可能）

[Duffy.1991-2] 1 2 David A. Duffy (1991). Principles of Automated Theorem Proving . Wiley.

[Baader.Snyder.2001-3] 1 2 Franz Baader、Wayne Snyder (2001)。Alan Robinson、Andrei Voronkov (編)。統一理論(PDF)。Elsevier。pp. 439–526 。 2015年6月8日にオリジナル(PDF)からアーカイブ。 2014年9月24日に取得。

[Dershowitz.Jouannaud.1990-4] N. Dershowitz; J.-P. Jouannaud (1990). "書き換えシステム". Jan van Leeuwen (編).形式モデルと意味論. 理論計算機科学ハンドブック. Vol. B. Elsevier. pp. 243–320 .

[7] ソボレフ、SK (2001) [1994]、「等号公理」、数学百科事典、EMS Press

[8] ハリー・ドイチュ、パヴェル・ガルバッツ、「相対的同一性」、スタンフォード哲学百科事典（2024年秋版）、エドワード・N・ザルタ、ウリ・ノーデルマン編、近日公開予定 URL: https://plato.stanford.edu/entries/identity-relative/#StanAccoIden

[:0-9] Sobolev, SK (2001) [1994]、「個体変数」、数学百科事典、EMS Press

[10] Sobolev, SK (2001) [1994]、「自由変数」、数学百科事典、EMS Press

[11] Fitting, M. , First-Order Logic and Automated Theorem Proving (Berlin/Heidelberg: Springer, 1990), pp. 198–200 .

[HoftHoft2002-12] マーガレット・H・ホフト;ハルトムートFWホフト（2002年11月6日）。Mathematica を使った計算。エルゼビア。ISBN 978-0-08-048855-4。

[HECK2012-13] Andre Heck (2012年12月6日). Maple入門. Springer Science & Business Media. ISBN 978-1-4684-0484-5置換。

[14] Takeuti, Gaisi; Zaring, Wilson M. (1982). "Introduction to Axiomatic Set Theory" . Graduate Texts in Mathematics : 6– 9. doi : 10.1007/978-1-4613-8168-6 . ISSN 0072-5285 . 2014年8月6日にオリジナルからアーカイブ済み。

[ 1 ]

[

[

[

[

[

[

[

[

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

置換（論理）

命題論理

意味

同義反復

一階述語論理

数学

代数

ZFCにおける置換の証明

関連項目

注記

引用文献

参考文献

外部リンク

関連するトピック

形式

構文

式

命題論理