[질문] 한정사가 (t->Bool)->Bool 타입 가진다는데

[익명(175.201)]

t가 여기서 뭐지? 변수에 들어갈 수 있는 원소의 type라고 하면
t->Bool이 문장의 type 맞나?
그런데 그러면 Exists의 경우는 왜 그냥
(t -> Bool)->Bool이 되는거지

[ns(qwer2357)]

굳이 엄밀하게 따지고들면 T는 보통 1차논리식의 논의 범위? 라고 보면 될거고 등장가능한 원소의 type으로 이해하면 될거같고, 문장이 Formula의 의미면 Domain이 T일때 formula는 T->bool이니까. Quanfier를 쓴 formula자체는 남겨진 변수가 없으면 그냥 똑같이 문장으로 이해하지만

[ns(qwer2357)]

Quantifier는 (논의범위는 고정했을때) 문장을 받아서 참거짓을 돌려주는 함수로 이해할 수 있다는 얘기였음. 쉽게 보면 논의범위를 실수라고 하고(x는 실수) x^2 > 0은 x의 값에 따라 참이 될수도 거짓이 될수도 있는 식임.

[ns(qwer2357)]

이제 forall x, x^2 >0은 그냥 거짓인 well formed formula지만, "forall x"가 어떤 애냐고 하면 어떤 well formed formula를 집어넣었을때, 참 또는 거짓을 결정해주는 애라는거지. 즉 forall x ( x^2 > 0) = false가 되는 함수로 이해된다고. 뭐 굳이 가정을 많이 깔고 명시적으로 했을때 그렇

[ns(qwer2357)]

다는거지 뭐 집합론 등에서 그렇게 하고있진 않을거야. 일단 변수의 개수 부터 시작해서 뭐가 집합이고 뭐가 집합이 아니고까지 기초론에선 시비를 걸려고 치면 걸게 많아서..

[익명(175.201)]

ㅇㅇ 내가 생각한것도 한정사랑 식 안의 변수가 같나? 이거였거든 근데 막 엄밀하게 하는 건 아닌가보네

[익명(175.201)]

다른 건 다 이해가는데 그 점때문에 잘 안와닿았거든 ㄱㅅㄱㅅ

[ns(qwer2357)]

뭐 통상적인 경우를 상정하고 말했던거고 x는 실수 y는 복소수일때 forall x, exists y : x < |y|라 치면 Predicate(T,S)를 Predicate(T)로 바꾸는게 exists y니까 (TxS -> bool) -> (T ->bool)로도 볼수 있지. 물론 TxS -> bool이 S->(T->bool)이기도 하니까

[ns(qwer2357)]

그럼 한정사는 이상황에서 (S->Predicate(T)) -> Predicate(T)인가 물으면 맞는말일수밖에 없지.

[익명(175.201)]

한정사 두 개 묶음이 저런 타입을 갖는다는거?

[익명(175.201)]

아 아니네 허