AKA predicate calculus
AKA functional calculus
일차논리,first-order_logic(FOL)와 동일. (nLab)

하지만 대개의 경우에 그렇고 술어논리가 이차논리인 경우도 있는듯... or 경우에 따라서 이차논리도 포함하는 것?... QQQ

//수백 술어논리
"술어논리는 보통 일차논리,first-order_logic를 뜻하는데 한정기호,quantifier가 변수,variable만을 한정하는 경우이며, 한정기호가 변수 뿐 아니라 술어,predicate 관계도 한정하는 기호논리,symbolic_logic를 이차논리,second-order_logic라고 한다."

간단히 단어만 놓고보면:
술어,predicate 논리,logic.

Compare: 명제논리,propositional_logic(=0차논리)
저기에

• quantifier - maybe 양화사,quantifier
  
• ...tbw
  

이 추가
그래서 새로 생긴 개념?이

• arity - maybe 항수,arity
  
• free variable vs non-free variable(bound variable) ... // curr. 변수,variable#s-2
  
• ...tbw
  
  

//foldoc
명제논리,propositional_logic의 확장,extension with separate 기호,symbols for 술어,predicates, subject{링크가 http://foldoc.org/subject 으로 걸려있는데 동형이의어에 잘못 걸린 링크.}s, and 양화사quantifiers.

chk, from e2
{
명제,proposition와 달리, 술어,predicate는 일반적이다(generic): it applies to a whole range of things. By filling in concrete examples of these things, a predicate becomes a proposition.
그래서 술어를 명제 with 자유변수,free_variable로 생각할 수 있다.
술어(pred.)의 t/f가 정해지면 명제(prop.)가 된다.
술어는 결정되지 않음. 명제는 결정됨.
}

일차술어논리 = 일차논리,first-order_logic와 같은 것인지 아님 포함관계가 있는지 chk
{
chk; from 연세대_특강자료 p52
1929년 괴델은 1차 술어논리학의 완전성,completeness을 증명.
1930년 괴델은 이어서 산술체계의 불완전성,incompleteness을 증명하면서 괴델 기수법을 소개한다. (see 괴델_수,Goedel_number)
• 괴델 기수법은 1차 술어 논리식을 자연수와 일대일로 맵핑을 시켜주는 기법
}
이차술어논리 = 이차논리,second-order_logic (이것 이상은 고차논리,higher-order_logic)

간단한 예 - 삼단논법,syllogism

chk
{
형식체계,formal_system에 predicate_calculus 와 같은 단어로 되어 있는데 같은 말인지 chk
}

프롤로그,Prolog의 표현이 이것을 기반으로 함.