| dbpprop:abstract
|
- Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature. Together with model theory, axiomatic set theory, and recursion theory, proof theory is one of the so-called four pillars of the foundations of mathematics. Proof theory is important in philosophical logic, where the primary interest is in the idea of a proof-theoretic semantics, an idea which depends upon technical ideas in structural proof theory to be feasible.
- Die Beweistheorie ist ein Teilgebiet der mathematischen Logik, das Beweise als formale mathematische Objekte behandelt. Dies ermöglicht ihre Analyse mit mathematischen Techniken. Beweise werden üblicherweise als induktiv definierte Datenstrukturen dargestellt, wie Listen oder Bäume. Diese werden gemäß den Axiomen und Schlussregeln des betrachteten logischen Systems konstruiert. Die Beweistheorie ist von syntaktischer Natur im Gegensatz zur Modelltheorie, die von semantischer Natur ist. Manchmal wird die Beweistheorie auch als Teil der philosophischen Logik aufgefasst, dabei ist vor allem die Idee der beweistheoretischen Semantik von Interesse.
- La teoría de la demostración o teoría de la prueba es una rama de la lógica matemática que trata a las demostraciones como objetos matemáticos, facilitando su análisis mediante técnicas matemáticas. Las demostraciones suelen presentarse como estructuras de datos inductivamente definidas que se construyen de acuerdo con los axiomas y reglas de inferencia de los sistemas lógicos. En este sentido, la teoría de la demostración se ocupa de la sintaxis, en contraste con la teoría de modelos, que trata con la semántica. Junto con la teoría de modelos, la teoría de conjuntos axiomática y la teoría de la recursión, la teoría de la demostración es uno de los "cuatro pilares" de los fundamentos de las matemáticas.
- La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l'anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du XX siècle. Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au 2 Congrès international de mathématiques en 1900 avec pour objectif de résoudre le problème de la cohérence des mathématiques. Cet objectif a été invalidé par le non moins célèbre théorème d'incomplétude de Gödel en 1931, ce qui n'a toutefois pas empêché la théorie de la démonstration de se développer, notamment grâce aux travaux de Jacques Herbrand et de Gerhard Gentzen. Ce dernier a démontré l'un des résultats principaux de la théorie de la démonstration, connu sous le nom de Hauptsatz (théorème principal) ou théorème d'élimination des coupures. Gentzen a ensuite utilisé ce théorème pour donner la première preuve purement syntaxique de la cohérence de l'arithmétique. Après une période de calme, qui a tout de même permis d'établir un certain nombre d'autres résultats de cohérence relative et d'esquisser une classification des théories axiomatiques, la théorie de la démonstration a connu une renaissance spectaculaire au cours des années 1960 avec la découverte de la correspondance de Curry-Howard qui a exhibé un lien structurel nouveau et profond entre logique et informatique : essentiellement la procédure d'élimination des coupures définie par Gentzen peut être vue comme un processus de calcul, si bien que les démonstrations formelles deviennent alors des programmes dont le type est la proposition à démontrer. Depuis, la théorie de la démonstration s'est développée en étroite symbiose avec d'autres domaines de la logique et de l'informatique théorique, notamment le lambda-calcul, et a donné naissance à de nouveaux modèles du calcul, le plus récent étant la logique linéaire de Jean-Yves Girard en 1986. Aujourd'hui, une partie de la théorie de la démonstration se confond avec la sémantique des langages de programmation et interagit avec de nombreuses autres disciplines de la logique ou de l'informatique théorique : calcul des prédicats calcul des propositions calcul des séquents déduction naturelle système à la Hilbert lambda-calcul logique combinatoire logique linéaire Automate cellulaire programmation fonctionnelle réalisabilité Théorie des catégories sémantique dénotationnelle Théorie des jeux théorème de Herbrand théorie des domaines théorie des types linguistique
- 証明論（英: Proof theory）は、数理論理学の一分野であり、証明を数学的オブジェクトとして形式的に表し、それに数学的解析を施す。証明は帰納的に定義されたデータ構造で表されることが多く、単純なリスト、入れ子リスト、木構造などがある。これらは論理体系の公理や推論規則によって構築される。そのため、証明論には統辞論的性質があるが、対照的にモデル理論には意味論的性質がある。モデル理論、公理的集合論、再帰理論などと共に数学基礎論の四本柱とされている。証明論は哲学的論理学の一分野と見ることもでき、その場合の主要な興味は証明論的意味論であり、その技法的基礎として構造証明論（structural proof theory）の考え方がある。
- Bewijstheorie is een tak van de wiskundige logica die bewijzen als formele wiskundig objecten opvat. Hierdoor kunnen bewijzen door middel van wiskundige technieken worden geanalyseerd. Bewijzen worden meestal gepresenteerd als inductief gedefinieerde datastructuren, zoals gewone lijsten, boxed lijsten, of boomstructuren, die volgens de axioma's en afleidingsregels van het logisch systeem worden geconstrueerd. Als zodanig is de bewijstheorie syntactisch van aard, dit in tegenstelling tot de modeltheorie, die van nature semantisch is. Samen met de modeltheorie, de axiomatische verzamelingenleer en de recursietheorie wordt de bewijstheorie gezien als één van de vier zogenaamde pilaren van de grondslagen van de wiskunde. Bewijs theorie kan ook beschouwd worden als een tak van de filosofische logica, waar het primaire interessegebied in het idee van een bewijs-theoretische semantiek ligt, een opvatting die afhangt van het feit of bepaalde technische ideeën in de structurele bewijstheorie al of niet haalbaar zijn.
- Teoria dowodu to dział logiki matematycznej zajmujący się analizą pojęcia dowodu oraz możliwych sposobów używania go w rozważaniach matematycznych. Za ojca tej dziedziny uważa się Davida Hilberta, jednego z najwybitniejszych matematyków przełomu dziewiętnastego i dwudziestego wieku. Do głównych zadań teorii dowodu należy kształtowanie takich systemów logicznych wraz z odpowiednimi zestawami aksjomatów, które nadawałyby się do formalizowania dowodów matematycznych, następnie zaś badanie siły tych systemów (im silniejszy system, tym więcej twierdzeń można udowodnić na jego gruncie wychodząc z danego zbioru aksjomatów). Bada się też szczegółowo strukturę dowodów formalnych, co czyni teorię dowodu odpowiednikiem syntaktyki logicznej (czasem obu tych terminów używa się zamiennie).
- Теория доказательств — раздел математической логики, в котором феномен математического доказательства сам становится объектом, например алгебры или арифметики. Доказательство обычно представляют как индуктивно возникающие структуры данных, начиная с простейших, таких как плоские списки, деревья, вплоть до гипотетических предельно сложных структур/машин которые строятся в соответствии с аксиомами и правилами вывода логических систем, имеющих соответствующие сложности/холистичности семантик. Если синтаксис и семантику логики представить как две полярные точки, то теория доказательств лежит в области синтаксиса, а модельная теория в области семантики. Другими полюсами логики могут быть вероятность, возможность и т. д. Компьютеры являются срезом синтаксиса/семантики логики. В логике компьютеры воспринимаются платонически, как некий абсолют, в котором машина Тьюринга — одна из точек основания пирамиды, наряду с живой клеткой, а вершина — как некий Абсолютный Дух в стиле Гегеля. То есть принципиально различных типов машин и организмов бесконечно много. Одной из моделей, целью которых был математических универсум были работы Готлоба Фреге или параллельная концепция так называемых «оснований математики» Гильберта. В неё наряду с теорией доказательств входили также теория моделей, аксиоматическая теория множеств, теорией рекурсии. Теория доказательства может рассматриваться как ветвь философской логики, в которой основной интерес проективный потенциал или семантика теории доказательств (proof-theoretic semantics), и обратная задача нахождения/конструирования машин и пути в логическом универсуме межу исходными данными и доказательством.
- 证明论是数理逻辑的一个分支，它将数学证明表达为形式化的数学客体，从而通过数学技术来简化对他们的分析。证明通常用归纳式地定义的数据结构来表达，例如链表，盒链表，或者树，它们根据逻辑系统的公理和推理规则构造。因此，证明论本质上是语法逻辑，和本质上是语义学的模型论形相反。和模型论，公理化集合论，以及递归论一起，证明论被称为数学基础的四大支柱之一。 证明论也可视为哲学逻辑的分支，其主要兴趣在于证明论语义学的思想，该思想依赖于结构证明论的技术型想法才可行。
|
| rdfs:comment
|
- Proof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed according to the axioms and rules of inference of the logical system. As such, proof theory is syntactic in nature, in contrast to model theory, which is semantic in nature.
- Die Beweistheorie ist ein Teilgebiet der mathematischen Logik, das Beweise als formale mathematische Objekte behandelt. Dies ermöglicht ihre Analyse mit mathematischen Techniken. Beweise werden üblicherweise als induktiv definierte Datenstrukturen dargestellt, wie Listen oder Bäume. Diese werden gemäß den Axiomen und Schlussregeln des betrachteten logischen Systems konstruiert. Die Beweistheorie ist von syntaktischer Natur im Gegensatz zur Modelltheorie, die von semantischer Natur ist.
- La teoría de la demostración o teoría de la prueba es una rama de la lógica matemática que trata a las demostraciones como objetos matemáticos, facilitando su análisis mediante técnicas matemáticas. Las demostraciones suelen presentarse como estructuras de datos inductivamente definidas que se construyen de acuerdo con los axiomas y reglas de inferencia de los sistemas lógicos.
- La théorie de la démonstration, aussi connue sous le nom de théorie de la preuve (de l'anglais proof theory), est une branche de la logique mathématique. Elle a été fondée par David Hilbert au début du XX siècle. Hilbert a proposé cette nouvelle discipline mathématique lors de son célèbre exposé au 2 Congrès international de mathématiques en 1900 avec pour objectif de résoudre le problème de la cohérence des mathématiques.
- Bewijstheorie is een tak van de wiskundige logica die bewijzen als formele wiskundig objecten opvat. Hierdoor kunnen bewijzen door middel van wiskundige technieken worden geanalyseerd. Bewijzen worden meestal gepresenteerd als inductief gedefinieerde datastructuren, zoals gewone lijsten, boxed lijsten, of boomstructuren, die volgens de axioma's en afleidingsregels van het logisch systeem worden geconstrueerd.
- Teoria dowodu to dział logiki matematycznej zajmujący się analizą pojęcia dowodu oraz możliwych sposobów używania go w rozważaniach matematycznych. Za ojca tej dziedziny uważa się Davida Hilberta, jednego z najwybitniejszych matematyków przełomu dziewiętnastego i dwudziestego wieku.
- Теория доказательств — раздел математической логики, в котором феномен математического доказательства сам становится объектом, например алгебры или арифметики.
|
![[RDF Data]](/statics/sw-cube.png)
