https://x.com/gamak01/status/1903736998638289002
위의 트윗을 읽은 뒤, 다음 논증을 진술해 봤습니다.
이 논증의 결론에서, C ^ B
는 집합 B
에서 집합 C
로의 함수 전체의 집합을 나타냅니다.
집합론에서 이 논증의 결론을 구체적으로 어떻게 증명할 수 있을까요? 이에 대해 깊이 생각해 본 적이 저는 이제껏 한 번도 없었네요.
https://x.com/gamak01/status/1903736998638289002
위의 트윗을 읽은 뒤, 다음 논증을 진술해 봤습니다.
이 논증의 결론에서, C ^ B
는 집합 B
에서 집합 C
로의 함수 전체의 집합을 나타냅니다.
집합론에서 이 논증의 결론을 구체적으로 어떻게 증명할 수 있을까요? 이에 대해 깊이 생각해 본 적이 저는 이제껏 한 번도 없었네요.
[f(a)](b)=c라고 하자. f(a)는 B로부터 C로의 함수이므로, c∈C이며 그러한 c는 단일하다. 한편, f의 정의에 따라, 어떠한 a, b에 대해서도 그러한 c가 존재한다. 이제 다음의 관계 R을 정의하자: R:=𝜆(x,y).𝜆z.[f(x)](y)=z. 상술한 바로부터, 어떠한 a, b에 대해서도 R(a,b)c인 c가 존재하며, 이는 또한 단일하게 존재한다. 따라서 A×B로부터 C로의 함수가 존재한다. 증명 끝.
답변해 주셔서 감사합니다.
그런 함수 g
는 다음과 같이 정의할 수 있죠?
집합론에서는 함수도 집합으로 정의되니, 함수 g
가 존재함을 보이는 일은 곧 집합 g
가 존재함을 보이는 일이죠. 그런데 이를 어떻게 증명하는지는 제가 잘 몰라서 오늘 새벽에 다른 분에게 그 증명 방법을 질문했습니다. 그분이 제게 치환 공리(대체 공리, replacement axiom)나 분리 공리[separation axiom]를 이용하면 된다고 답하시더군요.
제가 곧 집합론을 공부하기 시작할 예정인데, 그 공리들을 바탕으로 위의 집합이 존재함을 저도 직접 증명할 수 있으면 좋겠습니다.
함수를 집합으로 보지 않더라도 상관은 크게 없습니다. 어떤 R에 대해, 그 R이 X×Y에서 정의되면서 모든 x∈X에 대해 xRy인 y가 단일하기만 하면, 함수 f: X→Y가 존재한다는 것이 함수의 정의로부터 따라나와요. 원소성(membership)은 일종의 관계이므로, 임의의 x와 y로부터 (x, y)가 (단일하게?) 존재한다는 (자명한) 사실만 주어지면 위의 증명이 가능합니다.
집합론에서는 함수도 집합으로 정의됩니다. 그래서 @car_nap 님이 말씀하신 '함수의 정의'가 정확히 무엇인지 판단하기 어려워요. 그 정의를 구체적으로 알려 주실 수 있나요?
그리고 집합론적 기초론은 보통 일차 논리의 연역 체계와, 그 안에서 정식화된 집합론의 공리계로 이뤄져 있지 않나요? 함수를 집합으로 보지 않는 경우, 함수에 대한 존재 양화(정량, quantification)에 관한 구문은 어떻게 제시하실지도 궁금합니다.
https://plato.stanford.edu/entries/logic-higher-order/#SyntSecoOrdeLogi
저는 이차 논리를 자세히 배운 적이 없어요. 하지만 이차 논리에 관한 스탠퍼드 철학 백과사전 항목의 2절을 보니, 이차 논리에서는 함수 변수에 대한 양화가 가능한가 보군요. 그렇다고 해서 이차 논리에 함수의 정의가 기본적으로 제시되어 있다고 판단하기는 어려운 듯해요. 이차 논리에는 함수 변수라는 원시 개념과 더불어 이를 포함한 구문론이 제시되어 있다고 이해해야겠죠.
대상 언어 차원에서 함수가 집합으로 정의될 필요는 없습니다. 이는 소속성 술어를 포함하지 않는 언어에서도 관계가 술어로써 정의될 수 있는 것과 같은 연유입니다. 때문에, 집합론의 공리 체계를 고려하지 않더라도 요구되는 증명은 수행될 수 있다는 것이 요지입니다.
말씀하신 것처럼, 함수에 대한 양화가 가능하려면 고차 논리 또는 유형론이 필요합니다! (수학자들은 별다른 진지한 고려 없이 그냥 양화 구문을 쓰는 것 같긴 합니다.) 이에 관한 디테일을 논하는 것은 불필요해 보여서, 함수에 대한 비형식적 정의를 다음과 같이 제시하겠습니다:
f가 X로부터 Y로의 함수이다 := f(x)=y가 X×Y 위의 관계이고, 모든 x∈X에 대해 (i) f(x)=y인 y∈Y가 존재하며 (ii) f(x)=y이고 f(x)=z라면 y=z이다.
위의 정의은 꽤나 지저분한데, 사실 “f는 함수이다” 대신 “어떤 관계 R이 함수이다”의 꼴로 쓰는 편이 형식적으로 더 엄밀한 탓입니다. 즉,
R이 X로부터 Y로의 함수이다 := R이 X×Y 위의 관계이고 (즉, 모든 Rxy인 x, y에 대해 x∈X이고 y∈Y이며) 모든 x∈X에 대해 (i) ∃yRxy이며, (ii) Rxy이고 Rxz라면 y=z이다.
이제 직관적으로, 고차 언어를 사용해 다음의 귀결을 얻을 수 있습니다. (고차 논리의 두 가지 변환(conversion) 규칙이 사용됨.)
X로부터 Y로의 함수 f가 존재한다 iff 어떤 X×Y 위의 관계 R이 존재해서, (i) 모든 x∈X에 대해 ∃y(y∈Y∧Rxy)이며, (ii) Rxy이고 Rxz라면 y=z이다.
한편 여기에서 (i)를 ‘존재성’(existence) 조건, (ii)를 단일성(uniqueness) 조건이라고 부릅니다! 두 조건은 어떤 관계가 함수인지, 또는 어떤 함수가 존재하는지를 판별하기 위해 고려되어야 할 유일한 두 조건입니다.
[* 참고로, “R이 X로부터 Y로의 함수이다”로부터 위의 귀결을 얻는 과정을 상세히 쓰면 다음과 같습니다.
이렇게 얻어진 5는 위의 ‘귀결’과 의미가 동일합니다.]
이건 동의할 수 없습니다. 보통 수학자들은 제가 다음과 같이 설명한 집합론적 기초론으로 자신들의 수학 이론을 형식적으로 서술할 수 있음을 알 것입니다.
수학자들이 별다른 진지한 고려 없이 무단으로 함수 변수에 대한 존재 양화를 한다고 @car_nap 님이 추측하시는 근거가 무엇인지 저로서는 파악하지 못하겠어요.
@car_nap 님은 고차 논리를 이용해 함수임 관계의 정의를 제시하셨어요. 이 정의는 제가 미처 생각지 못한 것이고, 그 자체로 매우 흥미롭습니다.
그렇지만 저는 맨 처음에 "집합론에서"라는 말을 명시적으로 제 질문에 넣었습니다. @car_nap 님의 첫 답변은 몇몇 내용이 생략돼 있고, 그 뒤의 답변은 집합론과 상관이 별로 없어요.
첫 답변에 나온 증명은 집합으로서의 함수 g
의 존재성을 집합론의 공리들에서부터 밝히는 과정이 생략돼 있고, 그 뒤의 답변은 집합론이 아닌 고차 논리에서 함수를 정의하는 방법을 알려 줍니다.
논리학에 흥미가 없는 많은 수학자는 고차 논리를 잘 모를 것이라는 점도 덧붙입니다. 하지만 일차 논리와 집합론을 알 가능성은 커요.
죄송하지만 뭐에 화를 내시는지도 잘 이해하기가 어렵고, 어떤 종류의 증명을 원하시는지도 사실 잘 이해하기가 어렵습니다. 저는 불휘님이 진술한 논증에 상당하는 증명을 만든 것 뿐이에요. 그럼 이만 줄입니다.
화...? 저는 화난 상태가 아니었어요. 하지만 아마 다음과 같은 제 표현 때문에 @car_nap 님이 그렇게 느끼셨나 봅니다.
이건 동의할 수 없습니다. 보통 수학자들은 제가 다음과 같이 설명한 집합론적 기초론으로 자신들의 수학 이론을 형식적으로 서술할 수 있음을 알 것입니다.
수학자들이 별다른 진지한 고려 없이 무단으로 함수 변수에 대한 존재 양화를 한다고 @car_nap 님이 추측하시는 근거가 무엇인지 저로서는 파악하지 못하겠어요.
@car_nap 님의 의견에 제가 강하게 반대한다는 뜻을 밝히려고 저런 표현을 쓴 것이지, 저런 말을 했을 때 제가 화난 상태는 아니었어요. 수학자들이 함수에 대한 존재 양화를 하는 것은 집합론에서 함수가 집합으로 정의됨을 알기 때문이죠. 그래서 그들은 그런 존재 양화를 '그냥' 하는 게 아닙니다.
이미 제가 알려 드리지 않았나요? 이전에 제가 다른 분의 답변을 인용했었죠.
@car_nap 님은 집합론에서의 증명 방법 대신에 고차 논리에서의 증명 방법을 알려 주셨죠. 제가 원한 답변은 그게 아니었지만, 그 증명 방법도 흥미로우니 나중에 시도하겠습니다.