치환 실례

틀:위키데이터 속성 추적 논리학에서 치환 실례(置換實例, 틀:Llang)는 명제를 구성하는 원자 명제를 다른 명제로 대신하여 얻는 명제이다.

명제 논리

정의

명제 논리에서, 명제 형식 $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\ne 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$에 대하여, $(\mathrm{\neg }P)[Q_1/p_1,\dots ,Q_n/p_n]=\mathrm{\neg }(P[Q_1/p_1,\dots ,Q_n/p_n])$
• 명제 형식 $P,Q$에 대하여, $(P\wedge Q)[Q_1/p_1,\dots ,Q_n/p_n]=P[Q_1/p_1,\dots ,Q_n/p_n]\wedge 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\vee q\vee r$

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

$p\wedge q$

$\mathrm{\neg }p\wedge q$

$p\wedge \mathrm{\neg }q$

에 대한 치환 실례는

$(p\wedge q)\vee (\mathrm{\neg }p\wedge q)\vee (p\wedge \mathrm{\neg }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$를 넣어 얻는 항이다. 즉, 다음과 같이 재귀적으로 정의된다.

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

  $𝖿(t_1,\dots ,t_{m_{𝖿}})[u_1/x_1,\dots ,u_n/x_n]=𝖿(t_1[u_1/x_1,\dots ,u_n/x_n],\dots ,t_{m_{𝖿}}[u_1/x_1,\dots ,u_n/x_n])$

논리식 $\varphi$의, 변수 $x_1,\dots ,x_n$ 및 항 $t_1,\dots ,t_n$에 대한 치환 실례 $\varphi [t_1/x_1,\dots ,t_n/x_n]$는 $\varphi$ 속의 각 자유 변수 $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])$
• 관계 $𝖱$ 및 항 $u_1,\dots ,u_{n_{𝖱}}$에 대하여, (여기서 $n_{𝖱}$는 항수)

  $𝖱(u_1,\dots ,u_{n_{𝖱}})[t_1/x_1,\dots ,t_n/x_n]=𝖱(u_1[t_1/x_1,\dots ,t_n/x_n],\dots ,u_{n_{𝖱}}[t_1/x_1,\dots ,t_n/x_n])$

• 논리식 $\varphi$에 대하여, $(\mathrm{\neg }\varphi )[t_1/x_1,\dots ,t_n/x_n]=\mathrm{\neg }(\varphi [t_1/x_1,\dots ,t_n/x_n])$
• 논리식 $\varphi ,\psi$에 대하여, $(\varphi \wedge \psi )[t_1/x_1,\dots ,t_n/x_n]=\varphi [t_1/x_1,\dots ,t_n/x_n]\wedge \psi [t_1/x_1,\dots ,t_n/x_n]$
• 논리식 $\varphi$ 및 변수 $x$에 대하여,
  • $x\ne x_i$라면, $(\mathrm{\forall }x\varphi )[t_1/x_1,\dots ,t_n/x_n]=\mathrm{\forall }x(\varphi [t_1/x_1,\dots ,t_n/x_n])$
  • $x=x_i$라면, $(\mathrm{\forall }x\varphi )[t_1/x_1,\dots ,t_n/x_n]=\mathrm{\forall }x(\varphi [t_1/x_1,\dots ,t_{i-1}/x_{i-1},t_{i+1}/x_{i+1},\dots ,t_n/x_n])$

논리식 $\varphi$ 위의, 변수 $x$의 치환 가능 항(틀:Llang)은 다음 조건을 만족시키는 항 $t$이다.

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

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

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

같이 보기

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

외부 링크

• 틀:플래닛매스
• 틀:플래닛매스
• 틀:Proofwiki