전시 $\langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle \implies \langle \exists y: P.y : Q.y \rangle $ 정리입니다.

Aug 21 2020

Fitch와 같은 Natural Deduction 시스템을 사용하는 가능한 증거는 어렵지 않습니다. 하지만 Equational Logic을 사용하여 증명하고 싶습니다. 이 시스템은 DeMorgan 등과 같은 명제 논리의 일반적인 규칙과 다음과 같은 책에서 사용되는 Predicate 논리 규칙을 사용합니다.

이산 수학에 대한 논리적 접근 방식 (David Gries).
- 전체 책은 여기에서 찾을 수 있습니다. https://link.springer.com/book/10.1007/978-1-4757-3837-7
- 503 페이지의 규칙 목록.
1990 년대 프로그래밍 (Edward Cohen).

내 증명은 다음과 같이 시작됩니다.

나는 선행이 유지된다고 가정한다 $$\langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle$$ 도달하려고 $$\langle \exists x:: P.x \land Q.x \rangle$$

시도 된 증거 :

$$ \begin{align*} & \langle \forall x:: P.x \rangle \land \langle \exists x:: Q.x \rangle\\ \implies & \{\text{Instantiation } (\forall)\}\\ & P.a \land \langle \exists x:: Q.x \rangle \\ \equiv & \{\text{Distributivity of} \land \text{over} \exists \} \\ & \langle \exists x:: P.a \land Q.x \rangle \end{align*} $$

물론 그 증거는 완전하지 않습니다. 누군가 가이 맥락 에서이 증명이 가능한지 알고 있습니까?

답변

1 shibai Aug 21 2020 at 14:15

논리적 의미에 대한 공식적인 증명을 만들 때 먼저 직관적으로 추론하는 것이 도움이됩니다. 또한 작업중인 부분적인 증거가 막 다른 골목으로 이어지는 지 여부를 밝혀내는 데 도움이 될 수 있습니다. 예를 들어 부분 증명은 다음과 같이 직관적으로 읽습니다.

모두 $x$ 재산이있다 $P.x$ 그리고 약간 있습니다 $x$ 재산 $Q.x$, 다음이 있어야합니다. $x$ 재산 $P.x\land Q.x$: 실제로,하자 $a$ 임의의 객체이면 속성이 있음을 알 수 있습니다. $P.a$. 약간 있기 때문에$x$ 재산 $Q.x$, 우리는 몇 가지 $x$ 와 $P.a\land Q.x$...하지만 이제는?

이것은 보편적 인 수량자를 먼저 인스턴스화하는 것이 최선의 아이디어가 아니라 실존 적 수량자를 나타내는 것임을 보여줍니다.

모두 $x$ 재산이있다 $P.x$ 그리고 약간 있습니다 $x$ 재산 $Q.x$, 다음이 있어야합니다. $x$ 재산과 $P.x\land Q.x$: 실제로, 속성을 가진 객체를 말하십시오 $Q$ 불린다 $a$ (그래서 $Q.a$), 그 이후로 $x$ 재산이있다 $P.x$, 특히 $a$ 재산이 있어야한다 $P.a$. 이것을 사실과 결합하면$a$ 재산이있다 $Q.a$, 우리는 결론을 내릴 수 있습니다 $a$ 재산이있다 $P.a\land Q.a$. 특히,이 몇 가지 $x$ 와 $P.x\land Q.x$.

자연 추론을 사용하여 공식적으로 작성하면 다음과 같습니다.

$\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle$ (함축 소개에 대한 가정)
$\langle \exists x :: Q.x\rangle$(결합 제거, 1)
2.1$Q.a$(존재 적 엘림에 대한 가정)
2.2$\langle \forall x :: P.x\rangle$(결합 제거, 1)
2.3$P.a$(유니버설 엘림, 2.2)
2.4$P.a\land Q.a$(결합 소개, 2.1, 2.3)
2.5$\langle \exists x :: P.x\land Q.x\rangle$ (기존 소개, 2.4)
$\langle \exists x :: P.x\land Q.x\rangle$ (존재 엘림, 2, 2.1-2.5)

우리가 결론 $\langle \forall x :: P.x\rangle\land\langle \exists x :: Q.x\rangle \implies \langle \exists x :: P.x\land Q.x\rangle$ 1-3에 대한 암시 소개로.

이 주장은 공리적 주장을 생성하는 방법을 안내합니다. 이 경우의 주요 트릭은 실존 적 인트로가 실존 적 한정자에서 전체 인수를 래핑하는쪽으로 추론함으로써 회피된다는 것입니다. 그런 다음 실존 적 한정자의 범위 내에서 마치 존재하지 않은 것처럼 추론 할 수 있습니다.

(전례) $\langle \forall x :: P.x\rangle\land\langle\exists x :: Q.x\rangle$

$\equiv$ $\langle \forall y :: P.y\rangle\land\langle\exists x :: Q.x\rangle$ (변수 변경)

$\equiv$ $\langle \exists x :: \langle \forall y :: P.y\rangle \land Q.x\rangle$ (분포 $\land$ 위에 $\exists$; 이것은 전체 진술을$\exists$)