การแทนที่ (ตรรกศาสตร์)

Q: ข้อมูลสำคัญเกี่ยวกับ การแทนที่ (ตรรกศาสตร์)

การ แทนที่ คือ การแปลง ทางไวยากรณ์ ของนิพจน์ เชิงรูป แบบ การใช้ การแทนที่กับ นิพจน์ หมายถึงการแทนที่สัญลักษณ์ตัวแปรหรือสัญลักษณ์แทนตำแหน่งด้วยนิพจน์อื่นอย่างสม่ำเสมอ

Q: คำนิยาม

โดยที่ ψ และ φ แทน สูตร ของ ตรรกศาสตร์เชิงประพจน์ ψ เป็น ตัวอย่างการแทนที่ ของ φ ก็ต่อเมื่อ ψ สามารถได้มาจาก φ โดยการแทนที่สูตรด้วย ตัวแปรเชิงประพจน์ ใน φ โดยแทนที่ตัวแปรเดียวกันทุกครั้งด้วยสูตรเดียวกันทุก ครั้ง ตัวอย่างเช่น:

การแทนที่คือ การแปลง ทางไวยากรณ์ของนิพจน์เชิงรูป แบบ การใช้การแทนที่กับนิพจน์หมายถึงการแทนที่สัญลักษณ์ตัวแปรหรือสัญลักษณ์แทนตำแหน่งด้วยนิพจน์อื่นอย่างสม่ำเสมอ

นิพจน์ที่ได้เรียกว่าตัวอย่างการแทนที่หรือ เรียกสั้น ๆ ว่า ตัวอย่างของนิพจน์ดั้งเดิม

ตรรกศาสตร์เชิงประพจน์

คำนิยาม

โดยที่ψและφแทนสูตรของตรรกศาสตร์เชิงประพจน์ ψ เป็นตัวอย่างการแทนที่ของφ ก็ต่อเมื่อψสามารถได้มาจากφโดยการแทนที่สูตรด้วยตัวแปรเชิงประพจน์ในφ โดยแทนที่ตัวแปรเดียวกันทุกครั้งด้วยสูตรเดียวกันทุก ครั้งตัวอย่างเช่น:

ψ: (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$ จากตัวแปรไปยังเทอม ผู้เขียน หลายคน^{[ 2 ]}^{: 73}^{[ 3 ]}^{: 445}แต่ไม่ใช่ทั้งหมด^{[ 4 ]}^{: 250}ยังกำหนดให้σ ( x ) = x สำหรับตัวแปร xทั้งหมด ยกเว้นตัวแปร x จำนวนจำกัดสัญกรณ์ { x ₁ ↦ t ₁ , …, x _k ↦ t _k } ^{[หมายเหตุ 1 ]} หมายถึงการแมปการแทนที่ที่แมปตัวแปรx _i แต่ละตัวไปยังเทอม t _iที่สอดคล้องกันสำหรับi =1,…, kและตัวแปรอื่นๆ ทุกตัวไปยังตัวมันเอง โดยx _iต้องแตกต่างกันเป็นคู่ๆ ผู้เขียนส่วนใหญ่ยังกำหนดให้เทอมt _i แต่ละตัว ต้องแตกต่างกันทางไวยากรณ์จากx _iเพื่อหลีกเลี่ยงสัญกรณ์ที่แตกต่างกันเป็นอนันต์สำหรับการแทนที่เดียวกันการใช้การแทนที่ดังกล่าวกับเทอมtจะเขียนในรูปแบบสัญกรณ์โพสต์ฟิกเป็นt { x ₁ ↦ t ₁ , ..., x _k ↦ t _k }; ซึ่งหมายถึงการแทนที่x _i ทุกครั้งที่ปรากฏ ในtด้วยt _iพร้อม กัน ^{[หมายเหตุ 2 ]}ผลลัพธ์tσของการใช้การแทนที่σกับเทอมtเรียกว่าอินสแตนซ์ของเทอมt นั้น ตัวอย่างเช่น การใช้การแทนที่ { x ↦ z , z ↦ h ( a , y ) } กับเทอม

ฟ (	z	, a , g (	x	), y )	ผลผลิต
ฟ (	h ( a , y )	, a , g (	z	), y )	.

โดเมนdom ( σ ) ของการแทนที่σโดยทั่วไปจะถูกกำหนดให้เป็นเซตของตัวแปรที่ถูกแทนที่จริง ๆ กล่าวคือdom ( σ ) = { x ∈ V | xσ ≠ x } การแทนที่เรียกว่า การแทนที่แบบพื้นฐาน ( ground substitution) ถ้ามันแมปตัวแปรทั้งหมดในโดเมนของมันไปยังเทอมพื้นฐาน กล่าวคือเทอมที่ไม่มีตัวแปร เทอม แทนที่ tσของการแทนที่แบบพื้นฐานเป็นเทอมพื้นฐาน (ground term) ถ้าตัวแปรทั้งหมดของt อยู่ในโดเมนของ σ กล่าวคือถ้าvars ( t ) ⊆ dom ( σ )การแทนที่σเรียกว่า การแทนที่ เชิงเส้น (linear substitution) ถ้าtσเป็น เทอม เชิงเส้น สำหรับเทอมเชิงเส้น tบางเทอม (และดังนั้นทุกเทอม) ที่มีตัวแปรของ โดเมน ของσ อย่างแม่นยำ กล่าวคือvars ( t ) = dom ( σ ) การแทนที่σเรียกว่า การแทนที่ แบบราบ (flat substitution ) ถ้า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 ₂ไปยัง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และพจน์หลังไม่สามารถแปลงกลับไปเป็นx + yได้ เนื่องจากข้อมูลเกี่ยวกับจุดกำเนิด ของ zหายไป การแทนที่พื้นฐาน { x ↦ 2 } ไม่สามารถมีตัวผกผันได้เนื่องจากการสูญเสียข้อมูลต้นกำเนิดที่คล้ายกัน เช่น ใน ( x +2) { x ↦ 2 } = 2+2 แม้ว่าจะอนุญาตให้แทนที่ค่าคงที่ด้วยตัวแปรโดย "การแทนที่แบบทั่วไป" สมมุติบางประเภทก็ตาม

การแทนที่สองแบบจะถือว่าเท่ากันก็ต่อเมื่อการแทนที่เหล่านั้นแปลงตัวแปรแต่ละตัวไปเป็นผลลัพธ์ที่มีโครงสร้างทางไวยากรณ์เท่า กัน กล่าวคือ σ = τถ้าxσ = xτสำหรับแต่ละตัวแปรx ∈ Vการประกอบของการแทนที่สองแบบσ = { x ₁ ↦ t ₁ , …, x _k ↦ t _k } และτ = { y ₁ ↦ u ₁ , …, y _l ↦ u _l } ได้มาจากการลบคู่ y i ↦ u i ที่ y i ∈ { _x₁ , … , x k _}ออก จาก การแทนที่{ x ₁ ↦ t ₁τ , …, x k _↦ t _k τ _,y ₁ ↦ u 1 _, …, y _l ↦ u _l_}การประกอบกันของσและτจะใช้สัญลักษณ์στการประกอบกันเป็นการดำเนินการแบบสมาคมและเข้ากันได้กับการประยุกต์ใช้การแทนที่ กล่าวคือ ( ρσ ) τ = ρ ( στ ) และ ( tσ ) τ = t ( στ ) ตามลำดับ สำหรับการแทนที่ρ , σ , τและทุกพจน์tการแทนที่เอกลักษณ์ซึ่งแมปตัวแปรทุกตัวไปยังตัวมันเอง เป็นองค์ประกอบที่เป็นกลางของการประกอบการแทนที่ การแทนที่σเรียกว่าเป็นตัวประกอบเอกลักษณ์ถ้าσσ = σและดังนั้นtσσ = tσสำหรับทุกพจน์tเมื่อx _i ≠ t _iสำหรับทุกiการแทนที่ { x ₁ ↦ t ₁ , …, x _k ↦ t _k } เป็นตัวประกอบเอกลักษณ์ก็ต่อเมื่อไม่มีตัวแปรใดx _iเกิดขึ้นในt _j ใดๆ การประกอบการแทนที่ไม่เป็นไปตามการสลับที่ นั่นคือστอาจแตกต่างจากτσแม้ว่าσและτจะเป็น idempotent ก็ตาม^{[ 2 ]}^{: 73–74}^{[ 3 ]}^{: 445–446}

ตัวอย่างเช่น { x ↦ 2, y ↦ 3+4 } เท่ากับ { y ↦ 3+4, x ↦ 2 } แต่แตกต่างจาก { x ↦ 2, y ↦ 7 } การแทนที่ { x ↦ y + y } เป็นแบบ idempotent เช่น (( x + y ) { x ↦ y + y }) { x ↦ y + y } = (( y + y )+ y ) { x ↦ y + y } = ( y + y )+ yในขณะที่การแทนที่ { x ↦ x + y } เป็นแบบ non-idempotent เช่น (( 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 }

คณิตศาสตร์

ในคณิตศาสตร์มีการใช้การแทนที่สองแบบที่พบได้ทั่วไป ได้แก่การแทนที่ตัวแปรด้วยค่าคงที่ (เรียกอีกอย่างว่าการกำหนดค่าให้กับตัวแปรนั้น) และคุณสมบัติการแทนที่ของความเท่าเทียมกัน [ ^{5 ] หรือ}ที่เรียกว่ากฎของไลบ์นิซ^{[ 6 ]}

เมื่อพิจารณาคณิตศาสตร์ในฐานะภาษาที่เป็นทางการตัวแปรคือสัญลักษณ์จากตัวอักษรซึ่งโดยปกติจะเป็นตัวอักษร เช่น $x$ , $y$ และ $z$ ซึ่งแสดงถึงช่วงของค่า ที่เป็นไป ได้^{[ 7 ]}หากตัวแปรเป็นอิสระในนิพจน์หรือสูตรที่ กำหนด ตัวแปร นั้นสามารถแทนที่ด้วยค่าใดๆ ในช่วงของมันได้^{[ 8 ]}ตัวแปรที่ถูกผูกไว้บางประเภทก็สามารถแทนที่ได้เช่นกัน ตัวอย่างเช่นพารามิเตอร์ของนิพจน์ (เช่นสัมประสิทธิ์ของพหุนาม ) หรืออาร์กิวเมนต์ของฟังก์ชันยิ่งไปกว่านั้น ตัวแปรที่มีปริมาณสากล สามารถแทนที่ด้วยค่าใดๆ ในช่วงของมันได้ และผลลัพธ์จะเป็น ข้อความที่เป็นจริง(เรียกว่าการกำหนดค่าสากล )

สำหรับภาษาที่ไม่เป็นทางการ กล่าวคือ ในตำราคณิตศาสตร์ส่วนใหญ่ที่อยู่นอกเหนือตรรกศาสตร์ทางคณิตศาสตร์สำหรับนิพจน์แต่ละตัวนั้น ไม่สามารถระบุได้เสมอไปว่าตัวแปรใดเป็นตัวแปรอิสระและตัวแปรใดเป็นตัวแปรที่ถูกผูกไว้ ตัวอย่างเช่น ในขึ้นอยู่กับบริบท ตัวแปร อาจเป็นทั้งตัวแปรอิสระและตัวแปรที่ถูกผูกไว้ หรือในทางกลับกัน แต่ไม่สามารถเป็นตัวแปรอิสระพร้อมกันได้ การพิจารณาว่าจะถือว่าค่าใดเป็นตัวแปรอิสระนั้นขึ้นอยู่กับบริบทและความหมาย ${\textstyle \sum _{i<k}a_{ik}}$ ${\textstyle i}$ ${\textstyle k}$

คุณสมบัติการแทนที่ของความเท่าเทียมกันหรือกฎของไลบ์นิซ (แม้ว่าคำหลังมักจะสงวนไว้สำหรับบริบททางปรัชญา ) โดยทั่วไประบุว่า ถ้าสิ่งสองสิ่งเท่ากัน คุณสมบัติใดๆ ของสิ่งหนึ่งจะต้องเป็นคุณสมบัติของอีกสิ่งหนึ่งด้วย สามารถระบุอย่างเป็นทางการใน สัญกรณ์ตรรกะได้ดังนี้: สำหรับทุกและและสูตรที่สร้างขึ้นอย่างดี (โดยมีตัวแปรอิสระ x) ตัวอย่างเช่น: สำหรับจำนวนจริง $a$ และ $b$ ทั้งหมด ถ้า $a$ $=$ $b$ แล้ว $a$ $\geq 0$ หมายความว่า $b$ $\geq 0$ (ในที่นี้คือ $x$ $\geq 0$ ) นี่เป็นคุณสมบัติที่ใช้บ่อยที่สุดในพีชคณิตโดยเฉพาะอย่างยิ่งในการแก้ระบบสมการแต่ถูกนำไปใช้ในเกือบทุกสาขาของคณิตศาสตร์ที่ใช้ความเท่าเทียมกัน สิ่งนี้ เมื่อรวมกับคุณสมบัติการสะท้อนของความเท่าเทียมกัน จะก่อให้เกิดสัจพจน์ของความเท่าเทียมกันในตรรกะลำดับที่หนึ่ง^[⁹^] $(a=b)\implies {\bigl [}\phi (a)\Rightarrow \phi (b){\bigr ]}$ ${\textstyle a}$ ${\textstyle b}$ ${\textstyle \phi (x)}$ $\phi (x)$

การแทนที่นั้นเกี่ยวข้องกับ แต่ไม่เหมือนกับการประกอบฟังก์ชันมันมีความเกี่ยวข้องอย่างใกล้ชิดกับβ -reduction ในแคลคูลัสแลมบ์ดาอย่างไรก็ตาม เมื่อเปรียบเทียบกับแนวคิดเหล่านี้ จุดเน้นในพีชคณิตอยู่ที่การรักษาโครงสร้างทางพีชคณิตโดยการดำเนินการแทนที่ ซึ่งก็คือข้อเท็จจริงที่ว่าการแทนที่ให้โฮโมมอร์ฟิซึมสำหรับโครงสร้างที่ต้องการ (ในกรณีของพหุนาม คือโครงสร้าง วงแหวน )

พีชคณิต

การแทนที่เป็นการดำเนินการพื้นฐานในพีชคณิตโดยเฉพาะอย่างยิ่งในพีชคณิตคอมพิวเตอร์^{[ 10 ]}^{[ 11 ]}

ตัวอย่างทั่วไปของการแทนที่เกี่ยวข้องกับพหุนามโดยการแทนที่ค่าตัวเลข (หรือนิพจน์อื่น) ลงในค่าที่ไม่กำหนดของพหุนามตัวแปรเดียว จะเท่ากับการประเมินค่าพหุนามที่ค่านั้น อันที่จริง การดำเนินการนี้เกิดขึ้นบ่อยมากจนสัญลักษณ์สำหรับพหุนามมักถูกปรับให้เข้ากับการดำเนินการนี้ แทนที่จะกำหนดชื่อพหุนาม เช่น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 (ตามที่กำหนดไว้ในตรรกะลำดับแรกโดยไม่มีความเท่าเทียมกัน) ซึ่งดัดแปลงมาจากIntroduction to Axiomatic Set Theory (1982) โดย Gaisi Takeuti และ Wilson M. Zaring ^{[ 12 ]}

ทฤษฎีบท—ถ้า แล้ว สำหรับสูตร ที่ ถูกต้องใดๆ. $a=b$ $\phi$ $\phi (a)\ลูกศรขวา \phi (b)$

ดูทฤษฎีเซตของ Zermelo–Fraenkel § ภาษาเชิงรูปธรรมสำหรับการนิยามสูตรใน ZFC การนิยามเป็นแบบเวียนเกิดดังนั้นจึงใช้การพิสูจน์โดยการอุปมานใน ZFC ในตรรกะลำดับที่หนึ่งที่ไม่มีความเท่าเทียมกัน "ความเท่าเทียมกันของเซต" ถูกกำหนดให้หมายความว่าเซตสองเซตมีสมาชิกเหมือนกัน เขียนในเชิงสัญลักษณ์ว่า "สำหรับทุก z, z อยู่ใน x ก็ต่อเมื่อ z อยู่ใน y" จากนั้น สัจพจน์ของความขยายจะยืนยันว่า ถ้าเซตสองเซตมีสมาชิกเหมือนกัน เซตทั้งสองนั้นจะอยู่ในเซตเดียวกัน

คำนิยาม- $(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\ใน 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)\ลูกศรขวา \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)\ลูกศรขวา \psi (Y){\bigr ]}$ ${\bigl [}\varphi (X)\Rightarrow \varphi (Y){\bigr ]}$ ${\bigl [}{\bigl (}\psi (X)\land \varphi (X){\bigr )}\ลูกศรขวา \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)\ลูกศรขวา \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})\ลูกศรขวา \psi (Y,z_{0})$

ดูเพิ่มเติม

หมายเหตุ

^ผู้เขียนบางท่านใช้ [ t ₁ / x ₁ , …, t _k / x _k ] เพื่อแสดงถึงการแทนที่ เช่น M. Wirsing (1990). Jan van Leeuwen (ed.). Algebraic Specification . Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 675– 788.ดูที่นี่: หน้า 682
^จากมุมมองของพีชคณิต เทอม เซต Tของเทอมคือพีชคณิตเทอมอิสระเหนือเซต Vของตัวแปร ดังนั้น สำหรับการแมปการแทนที่ σ: V → T แต่ละตัว จะมีโฮโมมอร์ฟิซึมσ : T → T ที่ไม่ซ้ำกัน ซึ่งสอดคล้องกับ σ บน V ⊆ T การประยุกต์ใช้ σที่กำหนดไว้ข้างต้นกับเทอม t จึงถูกมองว่าเป็นการ ประยุกต์ใช้ฟังก์ชัน σกับอาร์กิวเมนต์ t

การอ้างอิง

^ Hunter, Geoffrey (1996) [1971]. Metalogic: An Introduction to the Metatheory of Standard First-Order Logic . University of California Press (ตีพิมพ์ 1973). หน้า 118. ISBN 9780520023567. OCLC 36312727 .( สามารถเข้าถึงได้สำหรับผู้ใช้บริการที่มีความบกพร่องทางการอ่าน )
^ ^a ^b David A. Duffy (1991). หลักการพิสูจน์ทฤษฎีบทอัตโนมัติ . ไวลีย์.
^ ^a ^b Franz Baader , Wayne Snyder (2001). Alan RobinsonและAndrei Voronkov (บรรณาธิการ). ทฤษฎีการรวมเป็นหนึ่ง (PDF) . Elsevier. หน้า 439– 526. เก็บถาวรจากต้นฉบับ(PDF)เมื่อ 2015-06-08 . สืบค้นเมื่อ2014-09-24 .
^ N. Dershowitz; J.-P. Jouannaud (1990). "ระบบการเขียนใหม่" ในJan van Leeuwen (บรรณาธิการ). แบบจำลองเชิงรูปธรรมและความหมาย . คู่มือวิทยาการคอมพิวเตอร์เชิงทฤษฎี. เล่ม B. Elsevier. หน้า 243–320 .
^ Sobolev, SK (2001) [1994], "สัจพจน์ความเท่าเทียมกัน" , สารานุกรมคณิตศาสตร์ , EMS Press
^ Deutsch, Harry และ Pawel Garbacz, "เอกลักษณ์เชิงสัมพัทธ์", สารานุกรมปรัชญาแห่งสแตนฟอร์ด (ฉบับฤดูใบไม้ร่วง 2024), Edward N. Zalta และ Uri Nodelman (บรรณาธิการ), กำลังจะตีพิมพ์ URL: https://plato.stanford.edu/entries/identity-relative/#StanAccoIden
^ Sobolev, SK (2001) [1994], "ตัวแปรเฉพาะบุคคล" , สารานุกรมคณิตศาสตร์ , EMS Press
^ Sobolev, SK (2001) [1994], "ตัวแปรอิสระ" , สารานุกรมคณิตศาสตร์ , EMS Press
^ฟิตติ้ง, เอ็ม.ตรรกศาสตร์ลำดับที่หนึ่งและการพิสูจน์ทฤษฎีบทอัตโนมัติ (เบอร์ลิน/ไฮเดลเบิร์ก: สปริงเกอร์, 1990),หน้า 198–200
↑มาร์เกรต เอช. ฮอฟต์; ฮาร์ทมุท เอฟดับเบิลยู ฮอฟท์ (6 พฤศจิกายน 2545) การคำนวณด้วยคณิตศาสตร์ . เอลส์เวียร์. ไอเอสบีเอ็น 978-0-08-048855-4.
^ Andre Heck (6 ธันวาคม 2012). บทนำเกี่ยวกับ 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-08-06.

ลิงก์ภายนอก

การแทนที่ในห้องปฏิบัติการ n

[5] ผู้เขียนบางท่านใช้ [ t ₁ / x ₁ , …, t _k / x _k ] เพื่อแสดงถึงการแทนที่ เช่น M. Wirsing (1990). Jan van Leeuwen (ed.). Algebraic Specification . Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 675– 788.ดูที่นี่: หน้า 682

[6] จากมุมมองของพีชคณิต เทอม เซต Tของเทอมคือพีชคณิตเทอมอิสระเหนือเซต Vของตัวแปร ดังนั้น สำหรับการแมปการแทนที่ σ: V → T แต่ละตัว จะมีโฮโมมอร์ฟิซึมσ : T → T ที่ไม่ซ้ำกัน ซึ่งสอดคล้องกับ σ บน V ⊆ T การประยุกต์ใช้ σที่กำหนดไว้ข้างต้นกับเทอม t จึงถูกมองว่าเป็นการ ประยุกต์ใช้ฟังก์ชัน σกับอาร์กิวเมนต์ t

[1] Hunter, Geoffrey (1996) [1971]. Metalogic: An Introduction to the Metatheory of Standard First-Order Logic . University of California Press (ตีพิมพ์ 1973). หน้า 118. ISBN 9780520023567. OCLC 36312727 .( สามารถเข้าถึงได้สำหรับผู้ใช้บริการที่มีความบกพร่องทางการอ่าน )

[Duffy.1991-2] David A. Duffy (1991). หลักการพิสูจน์ทฤษฎีบทอัตโนมัติ . ไวลีย์.

[Baader.Snyder.2001-3] Franz Baader , Wayne Snyder (2001). Alan RobinsonและAndrei Voronkov (บรรณาธิการ). ทฤษฎีการรวมเป็นหนึ่ง (PDF) . Elsevier. หน้า 439– 526. เก็บถาวรจากต้นฉบับ(PDF)เมื่อ 2015-06-08 . สืบค้นเมื่อ2014-09-24 .

[Dershowitz.Jouannaud.1990-4] N. Dershowitz; J.-P. Jouannaud (1990). "ระบบการเขียนใหม่" ในJan van Leeuwen (บรรณาธิการ). แบบจำลองเชิงรูปธรรมและความหมาย . คู่มือวิทยาการคอมพิวเตอร์เชิงทฤษฎี. เล่ม B. Elsevier. หน้า 243–320 .

[7] Sobolev, SK (2001) [1994], "สัจพจน์ความเท่าเทียมกัน" , สารานุกรมคณิตศาสตร์ , EMS Press

[8] Deutsch, Harry และ Pawel Garbacz, "เอกลักษณ์เชิงสัมพัทธ์", สารานุกรมปรัชญาแห่งสแตนฟอร์ด (ฉบับฤดูใบไม้ร่วง 2024), Edward N. Zalta และ Uri Nodelman (บรรณาธิการ), กำลังจะตีพิมพ์ 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] ฟิตติ้ง, เอ็ม.ตรรกศาสตร์ลำดับที่หนึ่งและการพิสูจน์ทฤษฎีบทอัตโนมัติ (เบอร์ลิน/ไฮเดลเบิร์ก: สปริงเกอร์, 1990),หน้า 198–200

[HoftHoft2002-12] มาร์เกรต เอช. ฮอฟต์; ฮาร์ทมุท เอฟดับเบิลยู ฮอฟท์ (6 พฤศจิกายน 2545) การคำนวณด้วยคณิตศาสตร์ . เอลส์เวียร์. ไอเอสบีเอ็น 978-0-08-048855-4.

[HECK2012-13] Andre Heck (6 ธันวาคม 2012). บทนำเกี่ยวกับ 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-08-06.

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[หมายเหตุ 1 ]

[หมายเหตุ 2 ]

5 ] หรือ

[ 6 ]

[ 8 ]

[

[ 10 ]

[ 11 ]

[ 12 ]