Constructive proof (original) (raw)
Een bewijs door constructie is een manier om een wiskundig bewijs te leveren. Door een voorbeeld te construeren, een methode te geven hoe het geconstrueerd kan worden, laat men zien dat er een wiskundig object is dat aan bepaalde eisen voldoet.
| Property | Value |
|---|---|
| dbo:abstract | In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object. This is in contrast to a non-constructive proof (also known as an existence proof or pure existence theorem), which proves the existence of a particular kind of object without providing an example. For avoiding confusion with the stronger concept that follows, such a constructive proof is sometimes called an effective proof. A constructive proof may also refer to the stronger concept of a proof that is valid in constructive mathematics.Constructivism is a mathematical philosophy that rejects all proof methods that involve the existence of objects that are not explicitly built. This excludes, in particular, the use of the law of the excluded middle, the axiom of infinity, and the axiom of choice, and induces a different meaning for some terminology (for example, the term "or" has a stronger meaning in constructive mathematics than in classical). Some non-constructive proofs show that if a certain proposition is false, a contradiction ensues; consequently the proposition must be true (proof by contradiction). However, the principle of explosion (ex falso quodlibet) has been accepted in some varieties of constructive mathematics, including intuitionism. Constructive proofs can be seen as defining certified mathematical algorithms: this idea is explored in the Brouwer–Heyting–Kolmogorov interpretation of constructive logic, the Curry–Howard correspondence between proofs and programs, and such logical systems as Per Martin-Löf's intuitionistic type theory, and Thierry Coquand and Gérard Huet's calculus of constructions. (en) En matemáticas, una prueba constructiva es un método de demostración para constatar la existencia de un objeto matemático creando o proporcionando un método para crear el objeto. Esto contrasta con una prueba no constructiva (también conocida como prueba de existencia o teorema de existencia pura), que prueba la existencia de un tipo particular de objeto sin proporcionar un ejemplo. Para evitar confusiones con el concepto más fuerte que se trata a continuación, tal prueba constructiva a veces se denomina prueba efectiva. Una prueba constructiva también puede referirse al concepto más fuerte de una prueba que es válida según los criterios de la matemática constructiva. El constructivismo es una filosofía matemática que rechaza todos los métodos de prueba que implican la existencia de objetos que no se construyen explícitamente. Esto excluye, en particular, el uso del principio del tercero excluido, el axioma del infinito y el axioma de elección, e induce un significado diferente para alguna terminología (por ejemplo, el término "o" tiene un significado más fuerte en las matemáticas constructivas que en las clásicas). Algunas demostraciones no constructivas muestran que si cierta proposición es falsa, se produce una contradicción; en consecuencia, la proposición debe ser verdadera (prueba por contradicción). Sin embargo, el principio de explosión (ex falso quodlibet) ha sido aceptado en algunas variedades de matemáticas constructivas, incluido el intuicionismo. Las pruebas constructivas pueden verse como una definición de los algoritmos matemáticos certificados: esta idea se explora en la de la lógica intuicionista, la correspondencia de Curry-Howard entre pruebas y programas, y los sistemas lógicos como la de y el cálculo de construcciones de y Gérard Huet. (es) Une première vision d'une démonstration constructive est celle d'une démonstration mathématique qui respecte les contraintes des mathématiques intuitionnistes, c'est-à-dire qui ne fait pas appel à l'infini, ni au principe du tiers exclu. Ainsi, démontrer l'impossibilité de l'inexistence d'un objet ne constitue pas une démonstration constructive de son existence : il faut pour cela en exhiber un et expliquer comment le construire. Si une démonstration est constructive, on doit pouvoir lui associer un algorithme. Cet algorithme est le contenu calculatoire de la démonstration. La correspondance de Curry-Howard énonce cette association, usuellement appelée correspondance preuve-programme, pour les démonstrations constructives. Une deuxième vision d'une démonstration constructive découle de la remarque précédente, c'est une démonstration à laquelle on peut donner un contenu calculatoire. En 1990, Timothy G. Griffin étend la correspondance de Curry-Howard à la loi de Peirce, ((α → β) → α) → α, et montre ainsi que l'on peut associer, via des continuations, un contenu calculatoire à la logique classique, faisant d'elle une logique constructive. (fr) Een bewijs door constructie is een manier om een wiskundig bewijs te leveren. Door een voorbeeld te construeren, een methode te geven hoe het geconstrueerd kan worden, laat men zien dat er een wiskundig object is dat aan bepaalde eisen voldoet. (nl) Em matemática, ou ainda na filosofia, uma demonstração ou prova construtiva é uma demonstração da existência de certo objeto matemático através da sua construção. Uma demonstração construtiva fornece um algoritmo para obter o objeto em questão. Em constraste, temos as provas não-construtivas, que provam a existência sem necessariamente mostrar como encontrar um exemplo (como por exemplo a redução ao absurdo ou o princípio do terceiro excluído). Uma demonstração construtiva de existência não pode ser baseada em mostrar a impossibilidade da inexistência. Algumas vezes, usa-se a expressão construção via axioma da escolha, não obstante o axioma da escolha não conduza a demonstração construtivas, pois é um axioma do infinito. (pt) 构造性证明（英語：Constructive proof）是数学证明方法的一种，通过直接或间接构造出具有命题所要求的性质的实例来完成证明。与构造性证明相对的概念是非构造性证明。后者只证明满足命题要求的物体存在，而不提供具体的实例或构造这样的实例的方法。 构造性证明也可以指数学构成主义中被认可的一种更强的证明。数学构成主义是数学哲学的一支，它认为要证明一个对象的存在，必须将其构造出来。因此，他们拒绝使用如排中律，无穷公理和选择公理这样的公理。同时也有一些用语和以往不同，例如或的语意会比基础数学中的更强。 数学构成主义拒绝使用反证法，然而爆炸原理在一些数学构成主义的变体中是被接受的，包括直觉主义。 (zh) Конструктивное доказательство — доказательство, в котором существование математического объекта доказывается путем прямого построения —в отличие от неконструктивного доказательства (также известного как чистая теорема существования), которое доказывает существование объекта с определёнными свойствами без предоставления конкретного примера. Конструктивная математика отвергает всё, кроме конструктивного доказательства. Это приводит к ограничению на допустимые методы доказательства (в частности, закон исключенного третьего не используется), а также другому пониманию терминов. Например, термин «или» имеет более сильное значение в конструктивной математике, чем в классической. Иногда используется эквивалентный термин «эффективное доказательство». (ru) В математиці конструктивне доведення — це метод доведення, що підтверджує існування математичного об'єкта шляхом надання або створення способу відтворення даного об'єкта. Він протиставляється неконструктивному доведенню (також відомому як теорема доведення існування, або чиста теорема існування), яке доводить існування певного об'єкта без надання прикладів. Деякі неконструктивні доведення показують, що якщо якась передумова помилкова, то випливає протиріччя; отже, передумова повинна бути істинною (доведення від протилежного). Проте в деяких розділах конструктивної математики, в тому числі в інтуїціонізмі, був прийнятий принцип вибуху (лат. ex Falso QuodLibet, «за брехнею нічого не слідує»). Конструктивізм — це математична філософія, яка відкидає всі, за виключенням конструктивних, докази в математиці. Це призводить до обмеження дозволених методів доведень (спочатку закон виключеного третього не було прийнято застосовувати) і іншого змісту термінології (наприклад, термін «або» має більш обмежений зміст в конструктивній математиці, ніж в класичній). Конструктивні доведення можна розглядати як визначення перевірених математичних алгоритмів: ця ідея досліджується в інтерпретації конструктивної логіки , у відповідності Каррі-Говарда, а також в таких логічних системах, як інтуїціоністська теорія типів та числення конструкцій й . (uk) |
| dbo:wikiPageExternalLink | http://plato.stanford.edu/entries/brouwer/weakcounterex.html http://www.maths.unsw.edu.au/~jim/proofs.html |
| dbo:wikiPageID | 360113 (xsd:integer) |
| dbo:wikiPageLength | 14334 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1090644431 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Probabilistic_method dbr:Minor_(graph_theory) dbr:Algorithm dbc:Constructivism_(mathematics) dbr:Paul_Gordan dbr:Per_Martin-Löf dbr:E._M._Wright dbr:Infinite_set dbr:Intuitionism dbr:Intuitionistic_type_theory dbr:Limited_principle_of_omniscience dbr:Complex_number dbr:Constructivism_(philosophy_of_mathematics) dbr:Mathematics dbr:Gelfond–Schneider_theorem dbr:Mathematical_object dbr:Non-constructive_algorithm_existence_proofs dbr:Georg_Cantor dbr:Graph_(discrete_mathematics) dbr:Constructive_set_theory dbr:Anne_Sjerp_Troelstra dbr:Logarithms dbr:Calculus_of_constructions dbr:G.H._Hardy dbr:Torus dbr:Irrational_number dbr:James_Franklin_(philosopher) dbr:Law_of_excluded_middle dbr:Curry–Howard_correspondence dbr:Errett_Bishop dbr:Euclid dbr:Euclid's_theorem dbr:Brouwer–Heyting–Kolmogorov_interpretation dbr:Cauchy_sequence dbr:Diaconescu's_theorem dbr:Dirk_van_Dalen dbr:Goldbach's_conjecture dbr:Hilbert's_basis_theorem dbr:Proof_by_contradiction dbr:Mathematical_proof dbr:Grete_Hermann dbr:Gérard_Huet dbr:Hilbert's_Nullstellensatz dbc:Mathematical_proofs dbr:Counterexample dbr:Prime_number dbr:Thierry_Coquand dbr:Zero_of_a_function dbr:Axiom_of_choice dbr:Axiom_of_infinity dbr:Polynomial dbr:Square_root_of_2 dbr:Constructive_reverse_mathematics dbr:Constructivism_(mathematics) dbr:Graph_minor_theorem dbr:Rational_number dbr:Real_number dbr:Existence_theorem dbr:Principle_of_explosion dbr:System_of_linear_equations dbr:Forbidden_minors dbr:Constructive_logic dbr:Law_of_the_excluded_middle dbr:Constructive_mathematics |
| dbp:wikiPageUsesTemplate | dbt:ISBN dbt:Mvar dbt:Refbegin dbt:Refend dbt:Reflist dbt:Short_description dbt:Slink |
| dcterms:subject | dbc:Constructivism_(mathematics) dbc:Mathematical_proofs |
| gold:hypernym | dbr:Method |
| rdf:type | dbo:Software yago:WikicatMathematicalProofs yago:WikicatMathematicalTheorems yago:Abstraction100002137 yago:Argument106648724 yago:Communication100033020 yago:Evidence106643408 yago:Indication106797169 yago:MathematicalProof106647864 yago:Message106598915 yago:Proof106647614 yago:Proposition106750804 yago:Statement106722453 yago:Theorem106752293 |
| rdfs:comment | Een bewijs door constructie is een manier om een wiskundig bewijs te leveren. Door een voorbeeld te construeren, een methode te geven hoe het geconstrueerd kan worden, laat men zien dat er een wiskundig object is dat aan bepaalde eisen voldoet. (nl) 构造性证明（英語：Constructive proof）是数学证明方法的一种，通过直接或间接构造出具有命题所要求的性质的实例来完成证明。与构造性证明相对的概念是非构造性证明。后者只证明满足命题要求的物体存在，而不提供具体的实例或构造这样的实例的方法。 构造性证明也可以指数学构成主义中被认可的一种更强的证明。数学构成主义是数学哲学的一支，它认为要证明一个对象的存在，必须将其构造出来。因此，他们拒绝使用如排中律，无穷公理和选择公理这样的公理。同时也有一些用语和以往不同，例如或的语意会比基础数学中的更强。 数学构成主义拒绝使用反证法，然而爆炸原理在一些数学构成主义的变体中是被接受的，包括直觉主义。 (zh) In mathematics, a constructive proof is a method of proof that demonstrates the existence of a mathematical object by creating or providing a method for creating the object. This is in contrast to a non-constructive proof (also known as an existence proof or pure existence theorem), which proves the existence of a particular kind of object without providing an example. For avoiding confusion with the stronger concept that follows, such a constructive proof is sometimes called an effective proof. (en) En matemáticas, una prueba constructiva es un método de demostración para constatar la existencia de un objeto matemático creando o proporcionando un método para crear el objeto. Esto contrasta con una prueba no constructiva (también conocida como prueba de existencia o teorema de existencia pura), que prueba la existencia de un tipo particular de objeto sin proporcionar un ejemplo. Para evitar confusiones con el concepto más fuerte que se trata a continuación, tal prueba constructiva a veces se denomina prueba efectiva. (es) Une première vision d'une démonstration constructive est celle d'une démonstration mathématique qui respecte les contraintes des mathématiques intuitionnistes, c'est-à-dire qui ne fait pas appel à l'infini, ni au principe du tiers exclu. Ainsi, démontrer l'impossibilité de l'inexistence d'un objet ne constitue pas une démonstration constructive de son existence : il faut pour cela en exhiber un et expliquer comment le construire. Une deuxième vision d'une démonstration constructive découle de la remarque précédente, c'est une démonstration à laquelle on peut donner un contenu calculatoire. (fr) Em matemática, ou ainda na filosofia, uma demonstração ou prova construtiva é uma demonstração da existência de certo objeto matemático através da sua construção. Uma demonstração construtiva fornece um algoritmo para obter o objeto em questão. Em constraste, temos as provas não-construtivas, que provam a existência sem necessariamente mostrar como encontrar um exemplo (como por exemplo a redução ao absurdo ou o princípio do terceiro excluído). (pt) Конструктивное доказательство — доказательство, в котором существование математического объекта доказывается путем прямого построения —в отличие от неконструктивного доказательства (также известного как чистая теорема существования), которое доказывает существование объекта с определёнными свойствами без предоставления конкретного примера. Иногда используется эквивалентный термин «эффективное доказательство». (ru) В математиці конструктивне доведення — це метод доведення, що підтверджує існування математичного об'єкта шляхом надання або створення способу відтворення даного об'єкта. Він протиставляється неконструктивному доведенню (також відомому як теорема доведення існування, або чиста теорема існування), яке доводить існування певного об'єкта без надання прикладів. (uk) |
| rdfs:label | Konstruktiver Beweis (de) Constructive proof (en) Prueba constructiva (es) Démonstration constructive (fr) 구성적 증명 (ko) Bewijs door constructie (nl) Demonstração construtiva (pt) Конструктивное доказательство (ru) Конструктивне доведення (uk) 构造性证明 (zh) |
| owl:sameAs | freebase:Constructive proof yago-res:Constructive proof wikidata:Constructive proof dbpedia-cy:Constructive proof dbpedia-de:Constructive proof dbpedia-es:Constructive proof dbpedia-fr:Constructive proof dbpedia-ko:Constructive proof dbpedia-nl:Constructive proof dbpedia-pt:Constructive proof dbpedia-ru:Constructive proof dbpedia-simple:Constructive proof dbpedia-uk:Constructive proof dbpedia-zh:Constructive proof https://global.dbpedia.org/id/2pRCf |
| prov:wasDerivedFrom | wikipedia-en:Constructive_proof?oldid=1090644431&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Constructive_proof |
| is dbo:wikiPageRedirects of | dbr:Non-constructive_proof dbr:Nonconstructive dbr:Nonconstructive_proof dbr:Effective_proof dbr:Non-constructive dbr:Proof_by_construction dbr:Proof_of_Existence dbr:Proof_of_existence dbr:Existence_proof dbr:Existential_proof dbr:Weak_counterexample |
| is dbo:wikiPageWikiLink of | dbr:Cantor's_first_set_theory_article dbr:Primitive_root_modulo_n dbr:Proof_of_impossibility dbr:Non-constructive_proof dbr:Nonconstructive dbr:Nonconstructive_proof dbr:David_Hilbert dbr:Dependent_type dbr:Intuitionistic_logic dbr:Lie's_third_theorem dbr:List_of_mathematical_logic_topics dbr:Coq dbr:Craig_interpolation dbr:Mathematical_Treatise_in_Nine_Sections dbr:Non-constructive_algorithm_existence_proofs dbr:Fundamental_theorem_of_algebra dbr:Gelfond–Schneider_constant dbr:Georg_Cantor dbr:Gleason's_theorem dbr:Constant-recursive_sequence dbr:Constructive_quantum_field_theory dbr:Conway's_Game_of_Life dbr:Optimal_solutions_for_Rubik's_Cube dbr:Orthonormality dbr:Functional_programming dbr:Gödel_numbering_for_sequences dbr:Irrational_number dbr:Law_of_thought dbr:Linear_extension dbr:List_of_Chinese_discoveries dbr:Brouwer_fixed-point_theorem dbr:Normal_number dbr:P-adic_number dbr:Cellular_automaton dbr:Hilbert's_Nullstellensatz dbr:Hyperreal_number dbr:Hensel's_lemma dbr:Effective_proof dbr:Realizability dbr:Skolem–Mahler–Lech_theorem dbr:Fiber_bundle_construction_theorem dbr:Free_abelian_group dbr:Cantor's_diagonal_argument dbr:Solved_game dbr:Value_at_risk dbr:Tarski–Seidenberg_theorem dbr:Non-constructive dbr:Euclidean_geometry dbr:Euclid–Mullin_sequence dbr:Existence_theorem dbr:Existential_quantification dbr:Proof_by_construction dbr:Proof_of_Existence dbr:Proof_of_existence dbr:Existence_proof dbr:Existential_proof dbr:Weak_counterexample |
| is foaf:primaryTopic of | wikipedia-en:Constructive_proof |