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

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

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

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

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

명제

${\displaystyle p\lor q\lor r}$

의, 원자 명제 ${\displaystyle p,q,r}$ 및 명제

${\displaystyle p\land q}$

${\displaystyle \lnot p\land q}$

${\displaystyle p\land \lnot q}$

에 대한 치환 실례는

${\displaystyle (p\land q)\lor (\lnot p\land q)\lor (p\land \lnot q)}$

이다.

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

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

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

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

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

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

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

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

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

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

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

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

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