Nested Quantifiers
Nested quantifiers are ones that occur within the scope of other quantifiers.

예.
∀x ∃y ( x+y=0 )   이것을 스코프를 더 명확히 나타내면 ∀x [ ∃y ( x+y=0 ) ]   로 쓸 수 있다.


한정자가 네스티드 되어있더라도, 전체 문장을 변화시키지 않는 범위내에서 한정자들을 이동시킬 수 있다.
즉, 프리한 변수에 대한 프레디컷이라던가, 한정자가 바인딩하고있는 변수외에 다른 변수의 프레디컷에 대해서는 한정자가 자유롭게 움직일 수 있다. 단, 프레디컷에 대해서 뛰어넘어 다닌다는 것이지, 한정자끼리 넘어다니지 않도록 주의한다.

즉, 한정자들의 순서를 임의대로 바꿀 수 없다.

예.            
∀x p(x) → ∃y q(x,y)     는      ∀x ∃y p(x)→q(x,y)        와 같지만,  ∃y ∀x  p(x)→q(x,y) 와는 다르다.

예.
p(x,y) = " x+y=0 "   이라고 하자.   ( on 실수집합)
∀x ∃y p(x,y)    :    모든 x에 대해, ∃y p(x,y) 는 참이다.             " x + y = 0 을 참이되게 하는  y 가 존재한다는 것" 은 모든 x에 대해 참이다.
∃y ∀x p(x,y)    :    ∀x p(x,y) 를 참이되게 하는 y가 존재한다.      " 모든 x 에 대해 x + y = 0 이 참이다" 를 만족하는 y 가 존재한다.

따라서, ∀x ∃y p(x,y) 는 참인 명제고, ∃y ∀x p(x,y) 는 거짓명제이다.


nested quantifiers 에 대해 다음이 성립한다.

1. ∀x  ∀y  p(x,y)    ≡   ∀x  ∀y  p(x,y)
2. ∃x  ∃y  p(x,y)    ≡   ∃y  ∃x  p(x,y)
3. ∃x  ∀y  p(x,y)    ⇒   ∀y ∃x  p(x,y)

특히 3번과 같이 다른종류의 한정자가 네스티드 되어있을때, 믹스트 퀀터파이어 라고 한다.

증명.
1 번.


2번은 ∧ 만 모두 ∨ 로 바꿔주면 1번과 마찬가지다.


3번.

3번이 동치가 안되는 반례를 앞에서 이미 들었으므로, 모든 증명이 완료되었지만, 3번에 대한 증명이 타당하다면, 위 증명을 ← 방향으로 적용했을때 증명이 안되어야 할 것이다.


보는바와 같이,  마지막행에서, ∃x p(x, c) 에서 c 가 arbitrary 하지 않으므로, ∀y∃x p(x,y ) 로 Univ. Intro. 를 쓰지 못하고, 증명이 막힌다.

한편, 마지막 줄에서, c가 arbitrary 하진 않지만, exist 하므로, ∃y∃x p(x,y) 로는 빠져나올수가 있다. 따라서, 다음이 성립한다.

 ∀x∀y p(x,y)   ⇒   ∃x∀y p(x,y)   ⇒   ∀y∃x p(x,y)  ⇒  ∃x∃y p(x,y)
 


nested quantifier 의 부정(negation)
이것은 최상위 한정자만 남기고 나머지부분을 프레디컷으로 처리한 후에, 단일 한정자에 대한 니게이션을 취하면 된다. 그리고 이 과정을 연쇄적으로 적용하면 된다.

특히, prenex normal form (PNF) 으로 표현되어있을때, 상당히 편리하게 니게이션 처리를 할 수 있다.

예. ¬∃x∀y∃z p(x,y,z)  ≡   ∀x¬ ∀y∃z p(x,y,z) ≡ ∀x∃y¬∃z p(x,y,z)≡ ∀x∃y∀z ¬p(x,y,z)