치환 실례 문서 원본 보기

{{위키데이터 속성 추적}}
[[논리학]]에서 '''치환 실례'''(置換實例, {{llang|en|substitution instance}})는 명제를 구성하는 원자 명제를 다른 명제로 대신하여 얻는 명제이다.

== 명제 논리 ==
=== 정의 ===
[[명제 논리]]에서, 명제 형식 <math>P</math>의, 원자 명제 <math>p_1,\dots,p_n</math> 및 명제 형식 <math>Q_1,\dots,Q_n</math>에 대한 '''치환 실례''' <math>P[Q_1/p_1,\dots,Q_n/p_n]</math>는 <math>P</math> 속의 각 <math>p_i</math>에 <math>Q_i</math>를 넣어 얻는 명제이다. 즉, 다음과 같이 재귀적으로 정의된다.
* 원자 명제 <math>p</math>에 대하여,
** <math>p\ne p_i</math>라면, <math>p[Q_1/p_1,\dots,Q_n/p_n]=p</math>
** <math>p=p_i</math>라면, <math>p[Q_1/p_1,\dots,Q_n/p_n]=Q_i</math>
* 명제 형식 <math>P</math>에 대하여, <math>(\lnot P)[Q_1/p_1,\dots,Q_n/p_n]=\lnot (P[Q_1/p_1,\dots,Q_n/p_n])</math>
* 명제 형식 <math>P,Q</math>에 대하여, <math>(P\land Q)[Q_1/p_1,\dots,Q_n/p_n]=P[Q_1/p_1,\dots,Q_n/p_n]\land Q[Q_1/p_1,\dots,Q_n/p_n]</math>

=== 성질 ===
만약 <math>P</math>가 [[항진 명제 형식]]이라면, 모든 치환 실례 <math>P[Q_1/p_1,\dots,Q_n/p_n]</math> 역시 항진 명제 형식이다.<ref name="Hamilton">{{서적 인용
|성=Hamilton
|이름=Alan G.
|제목=Logic for Mathematicians
|url=https://archive.org/details/logicformathemat0000hami
|언어=en
|판=개정
|출판사=Cambridge University Press
|날짜=1988
|isbn=0-521-36865-0
}}</ref> 만약 <math>P</math>가 [[모순 명제 형식]]이라면, 모든 치환 실례 <math>P[Q_1/p_1,\dots,Q_n/p_n]</math> 역시 모순 명제 형식이다.<ref name="Hamilton" />

만약 모든 <math>i=1,\dots,n</math>에 대하여 <math>Q_i</math>와 <math>R_i</math>가 서로 [[동치]]라면, <math>P[Q_1/p_1,\dots,Q_n/p_n]</math>와 <math>P[R_1/p_1,\dots,R_n/p_n]</math>은 서로 동치이다.

=== 예 ===
명제
: <math>p\lor q\lor r</math>
의, 원자 명제 <math>p,q,r</math> 및 명제
: <math>p\land q</math>
: <math>\lnot p\land q</math>
: <math>p\land\lnot q</math>
에 대한 치환 실례는
: <math>(p\land q)\lor(\lnot p\land q)\lor(p\land\lnot q)</math>
이다.

== 1차 논리 ==
=== 정의 ===
[[1차 논리]]에서, [[항 (논리학)|항]] <math>t</math>의, 변수 <math>x_1,\dots,x_n</math> 및 항 <math>u_1,\dots,u_n</math>에 대한 '''치환 실례''' <math>t[u_1/x_1,\dots,u_n/x_n]</math>는 <math>t</math> 속의 각 <math>x_i</math>에 <math>u_i</math>를 넣어 얻는 항이다. 즉, 다음과 같이 재귀적으로 정의된다.<ref name="planetmath">{{플래닛매스|urlname=substitutability|title=Substitutability}}</ref>
* 연산 <math>\mathsf f</math> 및 항 <math>t_1,\dots,t_{m_\mathsf f}</math>에 대하여, (여기서 <math>m_\mathsf f</math>는 항수)
*: <math>\mathsf f(t_1,\dots,t_{m_\mathsf f})[u_1/x_1,\dots,u_n/x_n]=\mathsf f(t_1[u_1/x_1,\dots,u_n/x_n],\dots,t_{m_\mathsf f}[u_1/x_1,\dots,u_n/x_n])</math>
[[논리식]] <math>\phi</math>의, 변수 <math>x_1,\dots,x_n</math> 및 항 <math>t_1,\dots,t_n</math>에 대한 '''치환 실례''' <math>\phi[t_1/x_1,\dots,t_n/x_n]</math>는 <math>\phi</math> 속의 각 [[자유 변수]] <math>x_i</math>에 <math>u_i</math>를 넣어 얻는 논리식이다. 즉, 다음과 같이 재귀적으로 정의된다.<ref name="planetmath" />
* 항 <math>t,u</math>에 대하여, <math>(t=u)[t_1/x_1,\dots,t_n/x_n]=(t[t_1/x_1,\dots,t_n/x_n]=u[t_1/x_1,\dots,t_n/x_n])</math>
* 관계 <math>\mathsf R</math> 및 항 <math>u_1,\dots,u_{n_\mathsf R}</math>에 대하여, (여기서 <math>n_\mathsf R</math>는 항수)
*: <math>\mathsf R(u_1,\dots,u_{n_\mathsf R})[t_1/x_1,\dots,t_n/x_n]=\mathsf R(u_1[t_1/x_1,\dots,t_n/x_n],\dots,u_{n_\mathsf R}[t_1/x_1,\dots,t_n/x_n])</math>
* 논리식 <math>\phi</math>에 대하여, <math>(\lnot\phi)[t_1/x_1,\dots,t_n/x_n]=\lnot(\phi[t_1/x_1,\dots,t_n/x_n])</math>
* 논리식 <math>\phi,\psi</math>에 대하여, <math>(\phi\land\psi)[t_1/x_1,\dots,t_n/x_n]=\phi[t_1/x_1,\dots,t_n/x_n]\land\psi[t_1/x_1,\dots,t_n/x_n]</math>
* 논리식 <math>\phi</math> 및 변수 <math>x</math>에 대하여,
** <math>x\ne x_i</math>라면, <math>(\forall x\phi)[t_1/x_1,\dots,t_n/x_n]=\forall x(\phi[t_1/x_1,\dots,t_n/x_n])</math>
** <math>x=x_i</math>라면, <math>(\forall x\phi)[t_1/x_1,\dots,t_n/x_n]=\forall x(\phi[t_1/x_1,\dots,t_{i-1}/x_{i-1},t_{i+1}/x_{i+1},\dots,t_n/x_n])</math>
논리식 <math>\phi</math> 위의, 변수 <math>x</math>의 '''치환 가능 항'''({{llang|en|substitutable/free term for <math>x</math>}})은 다음 조건을 만족시키는 항 <math>t</math>이다.<ref name="planetmath" />
* 만약 <math>t</math>가 변수 <math>y</math>를 포함하며, <math>\phi</math>가 논리식 <math>\forall y\psi</math>를 포함한다면, <math>x</math>는 <math>\psi</math>의 자유 변수가 아니다.
즉, 다음과 같이 재귀적으로 정의된다.
* 항 <math>u,v</math>에 대하여, <math>t</math>는 <math>u=v</math> 위의 <math>x</math>의 치환 가능 항이다.
* 관계 <math>\mathsf R</math> 및 항 <math>t_1,\dots,t_{n_\mathsf R}</math>에 대하여, <math>t</math>는 <math>\mathsf R(t_1,\dots,t_{n_\mathsf R})</math> 위의 <math>x</math>의 치환 가능 항이다.
* <math>t</math>가 <math>\phi</math> 위의 <math>x</math>의 치환 가능 항이라면, <math>t</math>는 <math>\lnot\phi</math> 위의 <math>x</math>의 치환 가능 항이다.
* <math>t</math>가 <math>\phi,\psi</math> 위의 <math>x</math>의 치환 가능 항이라면, <math>t</math>는 <math>\phi\land\psi</math> 위의 <math>x</math>의 치환 가능 항이다.
* <math>t</math>가 변수 <math>y</math>를 포함하지 않거나, <math>x</math>가 <math>\phi</math>의 자유 변수가 아니라면, <math>t</math>는 <math>\forall y\phi</math> 위의 <math>x</math>의 치환 가능 항이다.

== 같이 보기 ==
* [[람다 대수#치환]]
* [[분지 유형 이론#치환]]

== 각주 ==
{{각주}}

== 외부 링크 ==
* {{플래닛매스|urlname=substitutionsinpropositionallogic|title=Substitutions in propositional logic}}
* {{플래닛매스|urlname=substitutability|title=Substitutability}}
* {{proofwiki|id=Definition:Substitution (Formal Systems)|제목=Definition:Substitution (formal systems)}}

[[분류:수리논리학]]
[[분류:명제 논리]]
[[분류:논리학 개념]]