In logic, finite model theory, and computability theory, Trakhtenbrot's theorem (due to Boris Trakhtenbrot) states that the problem of validity in first-order logic on the class of all finite models is undecidable. In fact, the class of valid sentences over finite models is not recursively enumerable (though it is co-recursively enumerable). Trakhtenbrot's theorem implies that Gödel's completeness theorem (that is fundamental to first-order logic) does not hold in the finite case. Also it seems counter-intuitive that being valid over all structures is 'easier' than over just the finite ones.
| Attributes | Values |
|---|
| rdfs:label
| - Satz von Trachtenbrot (de)
- Teoremo de Trahtenbrot (eo)
- Théorème de Trakhtenbrot (fr)
- Теорема Трахтенброта (ru)
- Trakhtenbrot's theorem (en)
|
| rdfs:comment
| - En logiko kaj , la teoremo de Trahtenbrot (de ) statas ke la problemo de en la klaso de ĉiuj finiaj modeloj estas nedecidebla. Fakte, la klaso de validaj frazoj super finiaj modeloj estas ne , kvankam ĝi estas kun-rikure numerigebla. (eo)
- Der Satz von Trachtenbrot, benannt nach Boris Trachtenbrot, ist ein Satz aus der mathematischen Logik. Er wurde 1950 bewiesen und besagt, dass die in allen endlichen Modellen allgemeingültigen Sätze der Prädikatenlogik erster Stufe nicht rekursiv aufzählbar sind. Daraus ergeben sich Konsequenzen für die Prädikatenlogik zweiter Stufe. (de)
- Теорема Трахтенброта — теорема о неразрешимости истинности формул логики первого порядка для конечных моделей. Была сформулирована Б. А. Трахтенбротом в 1950 г. Её следствием является существование неограниченного числа формул, выражающих условие (а, следовательно, и определение) конечности множества и среди них имеется неограниченное множество независимых. Также её следствием является отсутствие самой слабой аксиомы бесконечности (для любой аксиомы бесконечности найдется более слабая аксиома бесконечности). (ru)
- En logique mathématique, le théorème de Trakhtenbrot dit que le problème de validité d'une formule de la logique du premier ordre sur la classe des modèles finis est indécidable. Autrement dit, il n'existe pas d'algorithme qui prend en entrée une formule avec des quantificateurs du premier ordre comme « pour tout x, il existe y tel que y est le père de x » et qui répond oui si la formule est vraie dans toute situation avec un nombre fini d'éléments et non sinon. (fr)
- In logic, finite model theory, and computability theory, Trakhtenbrot's theorem (due to Boris Trakhtenbrot) states that the problem of validity in first-order logic on the class of all finite models is undecidable. In fact, the class of valid sentences over finite models is not recursively enumerable (though it is co-recursively enumerable). Trakhtenbrot's theorem implies that Gödel's completeness theorem (that is fundamental to first-order logic) does not hold in the finite case. Also it seems counter-intuitive that being valid over all structures is 'easier' than over just the finite ones. (en)
|
| dcterms:subject
| |
| Wikipage page ID
| |
| Wikipage revision ID
| |
| Link from a Wikipage to another Wikipage
| |
| Link from a Wikipage to an external page
| |
| sameAs
| |
| has abstract
| - En logiko kaj , la teoremo de Trahtenbrot (de ) statas ke la problemo de en la klaso de ĉiuj finiaj modeloj estas nedecidebla. Fakte, la klaso de validaj frazoj super finiaj modeloj estas ne , kvankam ĝi estas kun-rikure numerigebla. (eo)
- Der Satz von Trachtenbrot, benannt nach Boris Trachtenbrot, ist ein Satz aus der mathematischen Logik. Er wurde 1950 bewiesen und besagt, dass die in allen endlichen Modellen allgemeingültigen Sätze der Prädikatenlogik erster Stufe nicht rekursiv aufzählbar sind. Daraus ergeben sich Konsequenzen für die Prädikatenlogik zweiter Stufe. (de)
- En logique mathématique, le théorème de Trakhtenbrot dit que le problème de validité d'une formule de la logique du premier ordre sur la classe des modèles finis est indécidable. Autrement dit, il n'existe pas d'algorithme qui prend en entrée une formule avec des quantificateurs du premier ordre comme « pour tout x, il existe y tel que y est le père de x » et qui répond oui si la formule est vraie dans toute situation avec un nombre fini d'éléments et non sinon. Ce théorème a été démontré par Boris Trakhtenbrot en 1950. Le théorème a un impact important : il démontre qu'il n'existe pas de système de déduction complet pour les validités en logique du premier ordre sur les modèles finis. (fr)
- In logic, finite model theory, and computability theory, Trakhtenbrot's theorem (due to Boris Trakhtenbrot) states that the problem of validity in first-order logic on the class of all finite models is undecidable. In fact, the class of valid sentences over finite models is not recursively enumerable (though it is co-recursively enumerable). Trakhtenbrot's theorem implies that Gödel's completeness theorem (that is fundamental to first-order logic) does not hold in the finite case. Also it seems counter-intuitive that being valid over all structures is 'easier' than over just the finite ones. The theorem was first published in 1950: "The Impossibility of an Algorithm for the Decidability Problem on Finite Classes". (en)
- Теорема Трахтенброта — теорема о неразрешимости истинности формул логики первого порядка для конечных моделей. Была сформулирована Б. А. Трахтенбротом в 1950 г. Её следствием является существование неограниченного числа формул, выражающих условие (а, следовательно, и определение) конечности множества и среди них имеется неограниченное множество независимых. Также её следствием является отсутствие самой слабой аксиомы бесконечности (для любой аксиомы бесконечности найдется более слабая аксиома бесконечности). (ru)
|
| prov:wasDerivedFrom
| |
| page length (characters) of wiki page
| |
| foaf:isPrimaryTopicOf
| |
| is Link from a Wikipage to another Wikipage
of | |
| is Wikipage redirect
of | |
| is foaf:primaryTopic
of | |
![[RDF Data]](/fct/images/sw-rdf-blue.png)
![[cxml]](/fct/images/cxml_doc.png)
![[csv]](/fct/images/csv_doc.png)
![[text]](/fct/images/ntriples_doc.png)
![[turtle]](/fct/images/n3turtle_doc.png)
![[ld+json]](/fct/images/jsonld_doc.png)
![[rdf+json]](/fct/images/json_doc.png)
![[rdf+xml]](/fct/images/xml_doc.png)
![[atom+xml]](/fct/images/atom_doc.png)
![[html]](/fct/images/html_doc.png)