등호가 있는 1차 술어 논리에서,
무한 집합을 공리화하는 체계가 있는데,
(예시 : 임의의 2 이상의 정수 n에 대해, Pn=∃x_1,∃x_2, ∃x_3, ... , ∃x_n (~x_1=x_2)&(~x_1=x_3)&...(~x_1=x_n)& (~x_2=x_3)&....& (~x_(n-1)=x_n) 이라는 명제라고 하자. 즉, Pn은 x1, x2, x3, ..., xn이 있어서 이들이 모두 서로 다르다는 것을 의미한다.
그러면, A={Pn | n은 2 이상의 정수}를 만족하는 수학적 대상은 언제나 무한집합이고, 무한집합인 모델은 언제나 A의 모든 명제를 만족한다.
따라서 A는 무한집합의 공리 체계이다.)
그러면, 유한 집합에 대한 공리 체계는 어떤 게 있나요?
즉, 어떤 1차술어 명제들의 집합 B에 대해, B를 만족하는 모델은 언제나 유한집합이고, 모든 유한집합인 모델은 B를 만족하는 그런 B의 예시로 어떤 게 있나요?
P_1 :== forall x_0, forall x_1, x_0 = x_1 P_2 :== forall x_0, forall x_1, forall x_2, ~ (x_1 = x_2) implies (x_0 = x_1 or x_0 = x_2) ...
Q_1 = ∀x_0 ∀ x_1, x_0=x_1 Q_2 = ∀x_0 ∀x_1 ∀x_2 (~(x_1 =x_2) -> (x_0=x_1 or x_0= x_2)) ... 이면, 이미 원소가 2개인 집합은 Q_1을 만족하지 못하지 않나요? (Q_2는 만족하는데, Q_1은 만족하지 않는 것 같아요.)
Q_1 :== P_1, Q_2 :== P_1 or P_2, ...
그러니까, A={Q_1, Q_2, Q_3, ...} 라는 집합이 있을 때, 원소가 2개인 모델은 Q_1을 만족하지 않기 때문에, A는 유한 집합을 공리화하는 집합이 아니지 않나요?
집합 A의 모든 명제를 만족하는 모델은 원소가 1개인 모델이기 때문에, 사실상 집합 A는 유한 집합에 대한 공리 체계가 아니라 원소가 1개인 집합에 대한 공리 체계라고 생각해요.
그러네요
혹시 수리논리학에서 주요 개념 및 주요 메타 정리들 어떤 것들까지 보셨는지 여쭈어봐도 될까요? 예를 들면, 혹시 Lowenheim-Skolem theorem 증명 보신 적 있으신가요?
아니요
그러면, 혹시 completeness theorem이나 compactness theorem은 아시나요?
네, 명제 논리에 대해서는 Coq으로 형식증명해봤어요
https://github.com/KiJeong-Lim/portfolio/blob/main/src/A_report_on_the_propositional_logic.v#L5142
그런데 왜 물어보세요?
유한한 모델만 있는 이론이 있냐는 뜻이지? =가 standard하게 해석된다고 가정하면 가능. 예를 들어 ∀x. x = 0. 다만 극단적인 예시로 =에 비표준 해석이 부여되면 무한한 크기의 비표준 모델이 생길 수 있지