정주희 교수님의 "수리논리와 집합론 입문" 154쪽에는 다음과 같은 문단이 있습니다:
＞ 원소나열법과 조건제시법은 부분집합 기호 ⊆에 이어 두 번째로 L_SET에 추
＞ 가되는 기호들이다. 그러나 이렇게 새로운 기호를 도입하여 사용하는 표기법들을
＞ (1)에서 보듯이 명확하게 `형식을 갖추어' 정의하는 것은 썩 쉬운 일이 아니다. 이
＞ 러한 정의는 충분히 가능하며 또한 현대 수리논리학의 핵심적인 개념이지만 아
＞ 쉽게도 이 책의 범위를 넘는다.
식 (1)은 151쪽에 있습니다:
＞ t ⊆ s ≡def ∀x (x ∈ t → x ∈ s) (1)
그런데 제가 궁금한 건 원소나열법과 조건제시법을 형식을 갖추어 정의하는 방법입니다.
혹시 이 방법을 아신다면, 제게 설명해주실 수 있나요?
해당 댓글은 삭제되었습니다.
다루긴 하는데요, 조건제시법을 형식을 갖추어 정의한다는 게 어떤 건지 잘 모르겠어요 ㅇㅅㅇ
보편양화사를 A 존재양화사를 E 논리식을 f parameter를 p로 두면 separation인 AxApEyAu(uㅌy iff uㅌx and f(u,p))에서 x f p가 주어졌을때 separation을 만족하는 y를 편의상 {uㅌx : f(u,p)}로 두고 싶다는 거(extensionality에 의해 가능).
x f p가 주어지면 [uㅌy iff uㅌx and f(u,p)] iff y={uㅌx:f(u,p)}.
Zf에서는 클래스가 논리식임에도 xㅌC를 정의하는 이유와 비슷
댓글 감사합니다. 이걸 컴퓨터 프로그램으로 바꾸려면 어떻게 해야될까요?
AxApEyAu[(uㅌy iff uㅌx and f(u,p)) iff y={uㅌx:f(u,p)}]를 원하는 거임? { : }는 그냥 informal 표기법.
오! 저랑 같은 생각이네요. 감사합니다.