What counts as first order?
----pat hayes
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.
[返回] 中文XML论坛 - 专业的XML技术讨论区 →
W3CHINA.ORG讨论区 - Web新技术讨论 → 『 Semantic Web(语义Web)/描述逻辑/本体 』 → 何谓“一阶谓词逻辑”？
(订阅本版)
2004/1/5 9:26:00
新浪微博
何谓“一阶谓词逻辑”？
