First, there is no such thing as the 'correct' or 'classical' or 'normal' first-order logic. There are probably as many variations of first-order logic as there are logicians, and among the dozens, perhaps hundreds, of logic textbooks that have been published almost no two use exactly the same logical system. The syntax can be written in a large variety of ways (infix, prefix, postfix; graphically like Peirce or like Frege; etc.); there are many widely different notions of first-order proofs (natural deduction systems, Gentzen tablaux, resolution-style proof systems, etc.) and there are even several semantic options. Some versions allow function symbols, others not; some use few connectives, some use only one, others allow many; and so on. I emphasize this rather elementary point only to provide some pre-emptive answer to the frequently heard complaint that any new idea violates the norms of 'normal' first-order logic. Of course all these varieties are profoundly alike in a certain sense (modulo a few well-known distinctions, such as the presence or absence of equality) but the issue we need to face is, how best to characterize this common quality? What makes a logic first-order?

One kind of answer, the one most often found in elementary textbooks, is purely syntactic. It characterizes first-order languages by their conformity to a kind of syntactic layering: there are individual symbols and relation symbols, and a language is first-order if it respects this layering by keeping these categories distinct and only allowing quantification over the individuals. In contrast, higher-order languages (which are well known to be less tractable in many ways) have a syntax which blurs or even eliminates this distinction by allowing relations to hold betwen other relations and allowing quantification over relations. On this view, then, the essentially first-order nature of FOL is essentially a syntactic restriction. This has the merit of being very easy to state and trivial to check. However, it misses the essential point.

Another kind of answer would be semantic: a language is first-order if it has a conventional Tarskian model theory in which individual names denote things in the universe and relation names denote relations over the universe. This is better, but it ignores the fact that one can give such a semantics to a notation which most people would consider non-first-order, such as type theory.

I wish to suggest a different answer, based on the relationship between the semantic and proof-theoretic qualities of the language. The reason why FOL plays such a central role in the foundations of mathematics and in knowledge representation is not because of a simple syntactic restriction. FOL has a fundamental logical character which make it in a sense into the canonical computational representational logic: it is the strongest possible relational logic which is both complete and compact. Relational means that the logic mentions entities and relations between them. Completeness means that proof theory and the semantics are in correspondence. Without this, of course, one could erect all kinds of semantic fantasies but they would have no bearing on the actual proofs that could be obtained. Compactness means that proofs can only use finite resources. Any conclusion from an infinite set of assumptions must be finitely derivable from some finite subset of them. This means that proofs are things that can actually be implemented and constructed by mortal people and physical machines.

所以我认为，first-order logic 应该是指量词的作用范围仅仅在个体变元上。而不是更高的层

欢迎指教

按Pat Hayes的说法,一价逻辑 有多种说法：
1）从语法层次：
“there are individual symbols and relation symbols, and a language is first-order if it respects this layering by keeping these categories distinct and only allowing quantification over the individuals.”
即 如lyf5 所说，量词的作用范围仅仅在个体变元上。
2）从语义层次：
“ language is first-order if it has a conventional Tarskian model theory in which individual names denote things in the universe and relation names denote relations over the universe.“
即必须遵循Tarskian模型论语义，所以，RDF不是一价逻辑
3）语义和证明论的关系：
“based on the relationship between the semantic and proof-theoretic qualities of the language”
太高深了，我也不懂。

以下是引用lyf5在2004-7-8 14:46:49的发言： 我认为，first-order Predicate logic 并不是指含有一个变元的的谓词逻辑。 比如说P(x,y)这个谓词，它含有两个变元，但如果存在量词或全称量词只作用于个体变元的话，比如说对于所有的x,都至少存在一个y使得p成立，这个命题依然是一阶的。 而高阶逻辑因该是指量词的作用范围超过了个体变元，作用到了谓词本身，就好像复合函数的味道，比如f(g(x))。 所以我认为，first-order logic 应该是指量词的作用范围仅仅在个体变元上。而不是更高的层 欢迎指教