치환 실례

논리학에서 치환 실례(置換實例, 영어: substitution instance)는 명제를 구성하는 원자 명제를 다른 명제로 대신하여 얻는 명제이다.

명제 논리

정의

명제 논리에서, 명제 형식 $P$의, 원자 명제 $p_{1},\dots ,p_{n}$ 및 명제 형식 $Q_{1},\dots ,Q_{n}$에 대한 치환 실례 $P[Q_{1}/p_{1},\dots ,Q_{n}/p_{n}]$는 $P$ 속의 각 $p_{i}$에 $Q_{i}$를 넣어 얻는 명제이다. 즉, 다음과 같이 재귀적으로 정의된다.

• 원자 명제 $p$에 대하여,
  • $p\neq p_{i}$라면, $p[Q_{1}/p_{1},\dots ,Q_{n}/p_{n}]=p$
  • $p=p_{i}$라면, $p[Q_{1}/p_{1},\dots ,Q_{n}/p_{n}]=Q_{i}$
• 명제 형식 $P$에 대하여, $(\lnot P)[Q_{1}/p_{1},\dots ,Q_{n}/p_{n}]=\lnot (P[Q_{1}/p_{1},\dots ,Q_{n}/p_{n}])$
• 명제 형식 $P,Q$에 대하여, $(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}]$

성질

만약 $P$가 항진 명제 형식이라면, 모든 치환 실례 $P[Q_{1}/p_{1},\dots ,Q_{n}/p_{n}]$ 역시 항진 명제 형식이다. 만약 $P$가 모순 명제 형식이라면, 모든 치환 실례 $P[Q_{1}/p_{1},\dots ,Q_{n}/p_{n}]$ 역시 모순 명제 형식이다.

만약 모든 $i=1,\dots ,n$에 대하여 $Q_{i}$와 $R_{i}$가 서로 동치라면, $P[Q_{1}/p_{1},\dots ,Q_{n}/p_{n}]$와 $P[R_{1}/p_{1},\dots ,R_{n}/p_{n}]$은 서로 동치이다.

예

명제

$p\lor q\lor r$

의, 원자 명제 $p,q,r$ 및 명제

$p\land q$

$\lnot p\land q$

$p\land \lnot q$

에 대한 치환 실례는

$(p\land q)\lor (\lnot p\land q)\lor (p\land \lnot q)$

이다.

1차 논리

정의

1차 논리에서, 항 $t$의, 변수 $x_{1},\dots ,x_{n}$ 및 항 $u_{1},\dots ,u_{n}$에 대한 치환 실례 $t[u_{1}/x_{1},\dots ,u_{n}/x_{n}]$는 $t$ 속의 각 $x_{i}$에 $u_{i}$를 넣어 얻는 항이다. 즉, 다음과 같이 재귀적으로 정의된다.

• 연산 ${\mathsf {f}}$ 및 항 $t_{1},\dots ,t_{m_{\mathsf {f}}}$에 대하여, (여기서 $m_{\mathsf {f}}$는 항수)

  ${\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}])$

논리식 $\phi$의, 변수 $x_{1},\dots ,x_{n}$ 및 항 $t_{1},\dots ,t_{n}$에 대한 치환 실례 $\phi [t_{1}/x_{1},\dots ,t_{n}/x_{n}]$는 $\phi$ 속의 각 자유 변수 $x_{i}$에 $u_{i}$를 넣어 얻는 논리식이다. 즉, 다음과 같이 재귀적으로 정의된다.

• 항 $t,u$에 대하여, $(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}])$
• 관계 ${\mathsf {R}}$ 및 항 $u_{1},\dots ,u_{n_{\mathsf {R}}}$에 대하여, (여기서 $n_{\mathsf {R}}$는 항수)

  ${\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}])$

• 논리식 $\phi$에 대하여, $(\lnot \phi )[t_{1}/x_{1},\dots ,t_{n}/x_{n}]=\lnot (\phi [t_{1}/x_{1},\dots ,t_{n}/x_{n}])$
• 논리식 $\phi ,\psi$에 대하여, $(\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}]$
• 논리식 $\phi$ 및 변수 $x$에 대하여,
  • $x\neq x_{i}$라면, $(\forall x\phi )[t_{1}/x_{1},\dots ,t_{n}/x_{n}]=\forall x(\phi [t_{1}/x_{1},\dots ,t_{n}/x_{n}])$
  • $x=x_{i}$라면, $(\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}])$

논리식 $\phi$ 위의, 변수 $x$의 치환 가능 항(영어: substitutable/free term for $x$)은 다음 조건을 만족시키는 항 $t$이다.

• 만약 $t$가 변수 $y$를 포함하며, $\phi$가 논리식 $\forall y\psi$를 포함한다면, $x$는 $\psi$의 자유 변수가 아니다.

즉, 다음과 같이 재귀적으로 정의된다.

• 항 $u,v$에 대하여, $t$는 $u=v$ 위의 $x$의 치환 가능 항이다.
• 관계 ${\mathsf {R}}$ 및 항 $t_{1},\dots ,t_{n_{\mathsf {R}}}$에 대하여, $t$는 ${\mathsf {R}}(t_{1},\dots ,t_{n_{\mathsf {R}}})$ 위의 $x$의 치환 가능 항이다.
• $t$가 $\phi$ 위의 $x$의 치환 가능 항이라면, $t$는 $\lnot \phi$ 위의 $x$의 치환 가능 항이다.
• $t$가 $\phi ,\psi$ 위의 $x$의 치환 가능 항이라면, $t$는 $\phi \land \psi$ 위의 $x$의 치환 가능 항이다.
• $t$가 변수 $y$를 포함하지 않거나, $x$가 $\phi$의 자유 변수가 아니라면, $t$는 $\forall y\phi$ 위의 $x$의 치환 가능 항이다.

같이 보기

• 람다 대수#치환
• 분지 유형 이론#치환

외부 링크

• “Substitutions in propositional logic”. 《PlanetMath》 (영어). 
• “Substitutability”. 《PlanetMath》 (영어). 
• “Definition:Substitution (formal systems)”. 《ProofWiki》 (영어).