| dbpprop:abstract
|
- In mathematics and logic, a higher-order logic is distinguished from first-order logic in a number of ways. One of these is the type of variables appearing in quantifications; in first-order logic, roughly speaking, it is forbidden to quantify over predicates. See second-order logic for systems in which this is permitted. Another way in which higher-order logic differs from first-order logic is in the constructions allowed in the underlying type theory. A higher-order predicate is a predicate that takes one or more other predicates as arguments. In general, a higher-order predicate of order n takes one or more predicates of order n − 1 as arguments, where n > 1. A similar remark holds for higher-order functions. Higher-order logic, abbreviated as HOL, is also commonly used to mean higher order simple predicate logic, that is the underlying type theory is simple, not polymorphic or dependent. Higher-order logics are more expressive, but their properties, in particular with respect to model theory, make them less well-behaved for many applications. By a result of Gödel, classical higher-order logic does not admit a sound and complete proof calculus; however, such a proof calculus does exist which is sound and complete with respect to Henkin models. Examples of higher order logics include Church's Simple Theory of Types, Thierry Coquand's calculus of constructions, which allows for both dependent and polymorphic types, and of course HOL.
- Unter Logik höherer Stufe versteht man eine Erweiterung der Prädikatenlogik erster Stufe. Sie basiert auf dem typisierten Lambda-Kalkül und geht auf Alonzo Churchs Theory of Simple Types zurück. Entwickelt um 1940 als ein Versuch der Formalisierung der Logik in der Principia Mathematica von Whitehead und Russell, ist sie von Leon Henkin und Peter Andrews eingehend untersucht worden. Anfang der 1970er Jahre wurden nicht-klassische Versionen der Logik höherer Stufe entwickelt, die die Grundlage der modernen Typtheorie und Beweistheorie (Girard, Huet, Harper, Honsell) bilden. Da die Logik höherer Stufe sowohl mächtig als auch relativ einfach auf einem Computer zu implementieren ist, wurden in letzter Zeit einige Theorembeweiser hierfür entwickelt, die gleichermaßen für die Mathematik als auch für die Informatik von Interesse sind.
- V matematice se logika vyššího řádu odlišuje od predikátové logiky prvního řádu několika způsoby. Jeden z nich je typ proměnných, přes které se kvantifikuje; v logice prvního řádu se kvantifikuje pouze pro proměnné pro individua a nelze kvantifikovat (volně řečeno) přes proměnné pro predikátové symboly. To lze v logice druhého řádu a dalších systémech. Další vlastnost, kterou se logika vyššího řádu liší od logiky prvního řádu, jsou dovolené konstrukce v typové teorii, na které je (případně) založena. Predikát vyššího řádu je takový predikát, který má jeden nebo víc jiných predikátů jako argumenty. Obecně, predikát vyššího řádu, který má řád n, má jeden nebo víc predikátů řádu (n − 1) jako svoje argumenty (pro n > 1). Podobnou vlastnost mají funkce vyšších řádů, běžně využívané ve funkcionálním programování Logiky vyšších řádů mají větší vyjadřovací sílu, ale kvůli svým vlastnostem, zvláště vzhledem k teorii modelů, mají méně vhodné chování pro mnoho aplikací. Gödel dokázal, že klasická logika vyššího řádu nedovoluje korektní a úplný důkazový systém. Ale existuje takový důkazový systém, který je korektní a úplný vzhledem k Henkinovským modelům. Příklady logik vyšších řádů jsou Churchova jednoduchá teorie typů (angl. 'Simple Theory of Types') a kalkulus konstrukcí (angl. 'calculus of constructions').
- Les logiques d'ordre supérieur sont des logiques formelles qui étendent le calcul des prédicats du premier ordre en permettant d'utiliser les variables dans les termes en tant que fonctions, et dans les expressions en tant que prédicats. D'un point de vue sémantique, cela revient à dire que l'on considère les fonctions et prédicats comme des objets à part entière, au même titre que, par exemple, un nombre entier. On s'autorisera ainsi, d'une part, à quantifier les prédicats et fonctions et, d'autre part, à donner des fonctions ou des prédicats en arguments d'autres fonctions et prédicats. Néanmoins, on pourra se doter d'un système de typage qui restreindra le genre d'objet qui pourra être donné en tant que tel ou tel argument de tel ou tel prédicat ou telle ou telle fonction. Un prédicat d'ordre supérieur est un prédicat qui prend comme argument un ou plusieurs autres prédicats. De manière générale, un prédicat d'ordre n prend comme argument un ou plusieurs prédicats d'ordre n-1, avec n > 1. Les mêmes définitions s'appliquent aux fonctions d'ordre supérieur. Les lambda-calculs typés, comme le calcul des constructions, s'inspirent de telles logiques dans ce qu'on appelle le paradigme fonctionnel. Un lien fort est tissé entre les mathématiques et l'informatique grâce à l'isomorphisme de Curry-Howard qui associe un lambda-calcul à une logique. C'est de ce domaine que sont issus les langages de programmation fonctionnelle.
- 高階述語論理（こうかいじゅつごろんり、英: Higher-order logic）は、一階述語論理と様々な意味で対比される用語である。 例えば、その違いは量化される変項の種類にも現われている。一階述語論理では、大まかに言えば述語に対する量化ができない。述語を量化できる論理体系については二階述語論理に詳しい。 その他の違いとして、基盤となる型理論で許されている型構築の違いがある。高階述語（higher-order predicate）とは、引数として1つ以上の別の述語をとることができる述語である。一般に n 階の高階述語の引数は1つ以上の (n − 1) 階の述語である（ここで n > 1）。同じことは高階関数（higher-order function）にも言える。 高階述語論理は表現能力が高いが、その特性、特にモデル理論に関わる部分では、多くの応用について性格が良いとは言えない。クルト・ゲーデルの業績により、古典的高階述語論理は（帰納的に公理化された）健全で完全な証明計算が認められないとされた。しかし、Henkin model によれば、健全で完全な証明計算は存在する。 高階述語論理の例として、アロンゾ・チャーチの Simple Theory of Types や Calculus of Constructions (CoC) がある。
- 在数学中，高阶逻辑在很多方面有别于一阶逻辑。 其一是变量类型出现在量化中；粗略的说，一阶逻辑中禁止量化谓词。允许这么做的系统请参见二阶逻辑。 高阶逻辑区别于一阶逻辑的其他方式是在构造中允许下层的类型论。高阶谓词是接受其他谓词作为参数的谓词。一般的，阶为 n 的高阶谓词接受一个或多个(n − 1)阶的谓词作为参数，这里的 n > 1。对高阶函数类似的评述也成立。 高阶逻辑更加富有表达力，但是它们的性质，特别是有关模型论的，使它们对很多应用不能表现良好。作为哥德尔的结论，经典高阶逻辑不容许可靠的和完备的证明演算；这个缺陷可以通过使用 Henkin 模型来修补。 高阶逻辑的一个实例是构造演算。
|
| rdfs:comment
|
- In mathematics and logic, a higher-order logic is distinguished from first-order logic in a number of ways. One of these is the type of variables appearing in quantifications; in first-order logic, roughly speaking, it is forbidden to quantify over predicates. See second-order logic for systems in which this is permitted. Another way in which higher-order logic differs from first-order logic is in the constructions allowed in the underlying type theory.
- Unter Logik höherer Stufe versteht man eine Erweiterung der Prädikatenlogik erster Stufe. Sie basiert auf dem typisierten Lambda-Kalkül und geht auf Alonzo Churchs Theory of Simple Types zurück. Entwickelt um 1940 als ein Versuch der Formalisierung der Logik in der Principia Mathematica von Whitehead und Russell, ist sie von Leon Henkin und Peter Andrews eingehend untersucht worden.
- V matematice se logika vyššího řádu odlišuje od predikátové logiky prvního řádu několika způsoby. Jeden z nich je typ proměnných, přes které se kvantifikuje; v logice prvního řádu se kvantifikuje pouze pro proměnné pro individua a nelze kvantifikovat (volně řečeno) přes proměnné pro predikátové symboly. To lze v logice druhého řádu a dalších systémech.
- Les logiques d'ordre supérieur sont des logiques formelles qui étendent le calcul des prédicats du premier ordre en permettant d'utiliser les variables dans les termes en tant que fonctions, et dans les expressions en tant que prédicats. D'un point de vue sémantique, cela revient à dire que l'on considère les fonctions et prédicats comme des objets à part entière, au même titre que, par exemple, un nombre entier.
|
![[RDF Data]](/statics/sw-cube.png)
