치환 실례

논리학에서 치환 실례(置換實例, 영어: 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$ 에 대하여,
- $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}]$ 역시 항진 명제 형식이다.^[1] 만약 $P$ 가 모순 명제 형식이라면, 모든 치환 실례 $P[Q_{1}/p_{1},\dots ,Q_{n}/p_{n}]$ 역시 모순 명제 형식이다.^[1]

만약 모든 $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}$ 를 넣어 얻는 항이다. 즉, 다음과 같이 재귀적으로 정의된다.^[2]

연산 ${\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}$ 를 넣어 얻는 논리식이다. 즉, 다음과 같이 재귀적으로 정의된다.^[2]

항 $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$ $\phi$ 및 변수 $x$ $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$ 이다.^[2]

만약 $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$ 의 치환 가능 항이다.