First - Order  Predicate  Logic

.......... 문장의 주어가 개별 개체 (individual object) 일 때 일차 술어논리(first order predicate logic) 을 사용한다고 한다. 예를들면 "Socrates is  mortal (소크라테스는 죽는다)" 과 같은 경우이다. 반면에  주어가 또다른 술어로 구성되어 있을 때 우리는 second order logic 또는 higher order logic을 사용한다고 말한다. 예들들면 "Being mortal is tragic (죽는다는 것은 비극이다)" 에서 Being mortal 과 같은 경우이다 ................

술어논리 (Predicate Logic) 에서 정량자 (Quantifier) 가 변수에만 적용되고, 술어나 함수에 대해서는 허용하지 않는 경우 이를 일차 술어계산(First Order Predicate Calculus)이라고 한다. 예를 들어 (∀x) P(x) 같은 경우이다. 반면에 (∀P) P(x) 문장은 술어부호 P 에 정량자가 적용되므로 일차 술어계산에서는 허용되지 않는 문장이다. 대부분의 모든 논리적인 표현은 일차 술어계산으로 모두 나타낼 수 있으므로, PROLOG와 같은 인공지능 언어들은 일차 술어계산에 근거하고 있다.

... 일차술어논리는 "거기에 .... 한 물체가 있다" 라든가 "모든 물체에 대해 그것은 ... 한 경우이다" 와 같은 정량화된 문장을 형식화하는 기호논리학에서의 한 이론이다. 반면에 higher-order logic 라고 하는 것은 "거기에 .... 한 물체의 집합이 있다" 라든가 "모든 성질에 대해 그것은 .... 한 경우이다" 를 허용하는 것으로써 일차술어논리에서는 그것이 허용되지 않는다.

그럼에도 불구하고, 일차술어논리는 집합이론 전부와 거의 모든 수학을 형식화하기에 충분할 정도로 강력하다. 그것은 수학의 기초가 되는 전통적인 논리 이론이다. 그것은 명제론 (sentential logic) 보다는 더 강한 이론이지만, 산술 (arithmetic), 집합이론, second-order logic 보다는 약한 이론이다.

다른 논리 이론과 같이 일차술어논리는 다음과 같은 것으로 구성된다.

• 문법적으로 정확한 문장을 어떻게 구축하느냐는 설명 (well-formed formula, wff)
• 공리 (axiom) 의 집합, 그 자체가 wff 인 각각의 공리
• 공리나 이전에 증명된 정리로부터 나온 정리를 증명하도록 해주는 추론 규칙의 집합

두가지 유형의 공리가 있다 : 정량화된 문장을 포함하는 적절한 추론에 관한 일반 진리치를 포함하는 논리적 공리 (logical axioms which embody the general truths about proper reasoning involving quantified statements) 와, 집합이론에서 집합을 묘사하는 instance axiom 이나 산술에서 수를 묘사하는 공리와 같이, 즉시 대상물을 묘사하는 공리가 그것이다.

First-order calculus 에서 추론 규칙의 집합이 유한한 반면에, 공리의 집합은 무한 일 수 있다. 그러나 주어진 well-formed formula 에 대해 그것이 공리인지 아닌지를 결정할 수 있는 일반 알고리즘이 있을 필요가 있다. 더구나, 주어진 추론 규칙의 응용이 정확한지 아닌지를 결정할 수 있는 알고리즘이 또한 있어야 한다. .... Wikipedia : First-order logic

term :

Prolog   논리 (Logic)   연결사 (Connective)   술어논리 (Predicate Logic)   기호 논리학 (Symbolic Logic)   추론 (Reasoning)   추론 규칙 (Inference Rule)   정량자 (Quantifier)   일차논리 (First-order Predicate Calculus)   전문가시스템 (Expert System)   논리식(wff)   공리 (Axiom)

site :

Wikipedia : First-order logic