술어 추상화

Predicate abstraction

논리학에서 술어 추상화문장으로부터 술어를 만들어 낸 결과물이다.Q가 어떤 공식이라면, 그 문장에서 형성된 술어적 추상성은 (λy)이다.Q) 여기서 λ은 추상화 연산자이며, in에 의해 (λy)의 모든 y 발생이 구속되는 경우.Q. 결과 술어( (x.Q(x))는 ( (x.Q(x))(t)에서와 같이 t라는 용어를 인수로 받아들일 수 있는 단음 술어로, 't'로 표시된 물체는 Q와 같은 성질을 가지고 있다고 한다.

추상화의 법칙은 ( λx.Q(x) )(t) ≡ Q(t/x) 여기서 Q(t/x)는 Q에서 x의 모든 자유 발생을 t로 대체한 결과물이다.이 법칙은 적어도 두 가지 경우에 일반적으로 실패하는 것으로 나타난다: (i) t가 불손할 때 그리고 (ii) Q가 모달 연산자를 포함할 때.

모달 논리학에서 "de re/de detco difference"는 다음과 같이 명시된다.

1. (DE DITDO): ( )

2. (DE RE):( x . A( )( t) 상자

(1)에서 모달 연산자는 공식 A(t)에 적용되며, t 용어는 모달 연산자의 범위에 포함된다.(2) t는 모달 연산자의 범위에 포함되지 않는다.

참조

술어 추상화의 의미론 및 추가적인 철학적 발전은 Fitting and Mendelson, First-order Modal Logic, Springer, 1999를 참조한다.