| dbpprop:abstract
|
- In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well. Most variants of Hilbert systems take a characteristic tack in the way they balance a trade-off between logical axioms and rules of inference. Hilbert systems can be characterised by the choice of a large number of schemes of logical axioms and a small set of rules of inference. The most commonly studied Hilbert systems have either just one rule of inference —modus ponens, for propositional logics— or two — with generalisation, to handle predicate logics, as well— and several infinite axiom schemes. Hilbert systems for propositional modal logics, sometimes called Hilbert-Lewis systems, are generally axiomatised with two additional rules, the necessitation rule and the uniform substitution rule. A characteristic feature of the many variants of Hilbert systems is that the context is not changed in any of their rules of inference, while both natural deduction and sequent calculus contain some context-changing rules. Thus, if we are interested only in the derivability of tautologies, no hypothetical judgments, then we can formalize the Hilbert system in such a way that its rules of inference contain only judgments of a rather simple form. The same cannot be done with the other two deductions systems: as context is changed in some of their rules of inferences, they cannot be formalized so that hypothetical judgments could be avoided — not even if we want to use them just for proving derivability of tautologies. Systems of natural deduction take the opposite tack, including many deduction rules but very few or no axiom schemes.
- Hilbertkalküle sind axiomatische Kalküle für die klassische Aussagenlogik oder die Prädikatenlogik erster Stufe, das heißt Kalküle, in denen sich Theoreme und Argumente der Aussagenlogik oder der Prädikatenlogik erster Stufe herleiten lassen. Die beiden Hauptmerkmale von Hilbertkalkülen sind das Vorhandensein etlicher Axiome oder Axiomenschemata sowie die geringe Anzahl von Schlussregeln – im Fall der Angabe von Axiomenschemata oft nur einer einzigen Regel, des Modus ponendo ponens, und im Fall der Angabe von Axiomen zusätzlich einer Substitutionsregel. Die Bezeichnung „Hilbertkalkül“ geht auf den Mathematiker David Hilbert zurück, der die als Hilbertprogramm bekannt gewordene und später durch den Gödelschen Unvollständigkeitssatz als unlösbar erwiesene Forderung aufstellte, die gesamte Mathematik und Logik auf ein gemeinsames einheitliches und vollständiges Axiomensystem aufzubauen. In einem engeren Sinn werden gelegentlich nur von Hilbert selbst angegebene Kalküle als Hilbertkalküle bezeichnet, insbesondere der gemeinsam mit Paul Bernays 1934 im Werk „Grundlagen der Mathematik“ angegebene axiomatische aussagenlogische Kalkül.
- Hilbertovský kalkulus (také hilbertovský klasický kalkulus) je jeden z logických kalkulů, kterými se zabývá logika. Jde o kalkulus jednoznačně nejpoužívanější; je v něm formalizována celá matematika. Nazván byl po německém matematikovi Davidu Hilbertovi, který podobný kalkulus poprvé zavedl. Jiným typem logického kalkulu je například gentzenovský kalkulus.
- En logique, les systèmes à la Hilbert servent à définir les déductions formelles en suivant un modèle proposé par David Hilbert au début du XX siècle : un grand nombre d'axiomes logiques exprimant les principales propriétés de la logique que l'on combine au moyen de quelques règles, notamment la règle de modus ponens, pour dériver de nouveaux théorème. Les systèmes à la Hilbert héritent du système défini par Gottlob Frege et constituent les premiers systèmes déductifs, avant l'apparition de la déduction naturelle ou du calcul des séquents.
- System Hilberta – dowolny system automatycznego dowodzenia twierdzeń, w którym występuje pewien zbiór aksjomatów i reguł dowodzenia, a dowód składa się z ciągu formuł będących albo aksjomatami, albo formułami wyprowadzonymi z poprzednich formuł na podstawie reguł dowodzenia, z których ostatnia jest właśnie formułą którą chcemy dowieść. Jest to wnioskowanie w przód w przeciwieństwie do wnioskowania w tył znanego z innych systemów dowodzenia. Istnieje wiele Systemów Hilberta do różnych logik i dla jednej logiki. Podstawową regułą dowodzenia w większości z nich jest modus ponens: jeśli <math>x</math> i <math>x \supset y</math>, to <math>y</math> Ponadto zwykle dodaje się regułę substytucji: jeśli dana jest pewna formuła, to wolno dopisać formułę powstałą przez podstawienie dowolnej formuły za wszystkie wystąpienia pewnej zmiennej Zamiast skończonej liczby aksjomatów dopuszcza się skończoną liczbę schematów aksjomatu, czyli w istocie nieskończenie wiele aksjomatów.
- 在逻辑特别是数理逻辑中，希尔伯特风格演绎系统是归功于弗雷格和希尔伯特的一类形式演绎系统。这种演绎系统最经常为一阶逻辑而研究，但对其他逻辑也是有价值的。 所有演绎系统都在逻辑公理和推理规则之间作出取舍平衡。 希尔伯特风格的演绎系统可以刻画为选择了大量的逻辑公理模式和少量的推理规则。最常研究的希尔伯特风格演绎系统只有一个推理规则即肯定前件和几个无限公理模式。 自然演绎系统做了相反的取舍，包括了很多演绎规则但有非常少甚至没有公理模式。
|
| rdfs:comment
|
- In logic, especially mathematical logic, a Hilbert system, sometimes called Hilbert calculus or Hilbert–Ackermann system, is a type of system of formal deduction attributed to Gottlob Frege and David Hilbert. These deductive systems are most often studied for first-order logic, but are of interest for other logics as well. Most variants of Hilbert systems take a characteristic tack in the way they balance a trade-off between logical axioms and rules of inference.
- Hilbertkalküle sind axiomatische Kalküle für die klassische Aussagenlogik oder die Prädikatenlogik erster Stufe, das heißt Kalküle, in denen sich Theoreme und Argumente der Aussagenlogik oder der Prädikatenlogik erster Stufe herleiten lassen.
- Hilbertovský kalkulus (také hilbertovský klasický kalkulus) je jeden z logických kalkulů, kterými se zabývá logika. Jde o kalkulus jednoznačně nejpoužívanější; je v něm formalizována celá matematika. Nazván byl po německém matematikovi Davidu Hilbertovi, který podobný kalkulus poprvé zavedl. Jiným typem logického kalkulu je například gentzenovský kalkulus.
- En logique, les systèmes à la Hilbert servent à définir les déductions formelles en suivant un modèle proposé par David Hilbert au début du XX siècle : un grand nombre d'axiomes logiques exprimant les principales propriétés de la logique que l'on combine au moyen de quelques règles, notamment la règle de modus ponens, pour dériver de nouveaux théorème.
- System Hilberta – dowolny system automatycznego dowodzenia twierdzeń, w którym występuje pewien zbiór aksjomatów i reguł dowodzenia, a dowód składa się z ciągu formuł będących albo aksjomatami, albo formułami wyprowadzonymi z poprzednich formuł na podstawie reguł dowodzenia, z których ostatnia jest właśnie formułą którą chcemy dowieść. Jest to wnioskowanie w przód w przeciwieństwie do wnioskowania w tył znanego z innych systemów dowodzenia.
|
![[RDF Data]](/statics/sw-cube.png)
