Decidability (logic) (original) (raw)
Rozhodnutelnost je matematický pojem z oblasti matematické logiky. Vyjadřuje, zda existuje konečný algoritmus, který pro každou formuli určí, zda je v dané teorii dokazatelná nebo není. Teorie, pro niž takový algoritmus existuje, se nazývá rozhodnutelná, v opačném případě pak nerozhodnutelná. Problematika rozhodnutelnosti úzce souvisí s Gödelovými větami o neúplnosti.
| Property | Value |
|---|---|
| dbo:abstract | Rozhodnutelnost je matematický pojem z oblasti matematické logiky. Vyjadřuje, zda existuje konečný algoritmus, který pro každou formuli určí, zda je v dané teorii dokazatelná nebo není. Teorie, pro niž takový algoritmus existuje, se nazývá rozhodnutelná, v opačném případě pak nerozhodnutelná. Problematika rozhodnutelnosti úzce souvisí s Gödelovými větami o neúplnosti. (cs) En , la decidibilitat és una propietat dels sistemes formals quan, per a qualsevulla fórmula en el llenguatge del sistema, existeix un mètode efectiu per determinar si aquesta fórmula pertany o no al conjunt de les veritats del sistema. Per exemple, la lògica proposicional és decidible, perquè existeix un algoritme (taula de veritat) que en un nombre finit de passos pot decidir si la fórmula és vàlida o no. Quan una fórmula no pot ser provada vertadera ni falsa, es diu que la fórmula és independent, i que per tant el sistema és no decidible. L'única manera d'incorporar una fórmula independent a les veritats del sistema és postulant-la com a axioma. Dos exemples molt importants de fórmules independents són l'axioma de l'elecció en la teoria de conjunts, i el cinquè postulat d'Euclides. (ca) In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer. Zeroth-order logic (propositional logic) is decidable, whereas first-order and higher-order logic are not. Logical systems are decidable if membership in their set of logically valid formulas (or theorems) can be effectively determined. A theory (set of sentences closed under logical consequence) in a fixed logical system is decidable if there is an effective method for determining whether arbitrary formulas are included in the theory. Many important problems are undecidable, that is, it has been proven that no effective method for determining membership (returning a correct answer after finite, though possibly very long, time in all cases) can exist for them. (en) En metalógica, la decidibilidad es una propiedad de los sistemas formales cuando, para cualquier fórmula en el lenguaje del sistema, existe un para determinar si esa fórmula pertenece o no al conjunto de las verdades del sistema. Por ejemplo, la lógica proposicional es decidible, porque existe un algoritmo (la tabla de verdad) que en un número finito de pasos puede decidir si la fórmula es válida o no. Cuando una fórmula no puede ser probada verdadera ni falsa, se dice que la fórmula es independiente, y que por lo tanto el sistema es no decidible. La única manera de incorporar una fórmula independiente a las verdades del sistema es postulándola como axioma. Dos ejemplos muy importantes de fórmulas independientes son el axioma de elección en la teoría de conjuntos, y el quinto postulado de la geometría euclidiana. (es) En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique. L’indécidabilité est la négation de la décidabilité. Dans les deux cas, il s'agit de formaliser l'idée qu'on ne peut pas toujours conclure lorsque l'on se pose une question, même si celle-ci est sous forme logique. (fr) Il concetto di decidibilità si trova in logica matematica e in teoria della computabilità con accezioni differenti. (it) 논리학에서 결정가능성(decidability)은 참/거짓을 묻는 결정 문제가 가질 수 있는 성질의 하나로, 해답을 내어놓는 기계적인 절차가 존재하는 성질을 가리킨다. 대표적으로 정지 문제의 결정불가능성이 알론조 처치와 앨런 튜링에 의해 증명된 바 있다. (ko) 決定可能（けっていかのう、英: decidable）は、数理論理学または現代論理学において、論理式の集合のメンバーシップの決定をする実効的（effectiveな）方法が存在することを指す。決定可能性（けっていかのうせい、英: decidability）は、そのような属性を指す。命題論理のような形式体系は、論理的に妥当な論理式（または定理）の集合のメンバーシップを実効的に決定できるなら、決定可能である。ある決まった論理体系における理論（論理的帰結で閉じている論理式の集合）は、任意の論理式がその理論に含まれるか否かを決定する実効的方法があれば、決定可能である。そうでなければ、決定不能である。 (ja) Rozstrzygalność (decydowalność) problemu matematycznego to następująca jego właściwość: istnieje algorytm, który oblicza odpowiedź na dowolne pytanie stawiane przez problem. Problem może być nierozstrzygalny, jeśli jego rozstrzygalność prowadziłaby do powstania sprzeczności. (pl) Em lógica, o termo decidível se refere a um problema de decisão, ou seja, a questão da existência de um método efetivo para determinar a pertinência em um conjunto de fórmulas. Sistemas lógicos, tais como a lógica proposicional, são decidíveis se a pertinência em seu conjunto de fórmulas logicamente válido pode ser efetivamente determinado. Uma teoria (conjunto de fórmulas fechada sob a consequência lógica) em um sistema lógico fixo é decidível se existe um algoritmo eficiente para determinar se fórmulas arbitrárias pertencem a ela. Muitos problemas importantes são indecidíveis. (pt) Алгоритмическая разрешимость — свойство формальной теории обладать алгоритмом, определяющим по данной формуле, выводима она из множества аксиом данной теории или нет. Теория называется разрешимой, если такой алгоритм существует, и неразрешимой, в противном случае. Вопрос о выводимости в формальной теории является частным, но вместе с тем важнейшим случаем более общей проблемы разрешимости. (ru) Алгоритмічна розв'язність — властивість формальної теорії володіти алгоритмом, який визначає за даною формулою, виводиться вона з множини аксіом даної теорії чи ні. Теорія називається розв'язною, якщо такий алгоритм існує, і нерозв'язною, в іншому випадку. Питання про виводимість у формальній теорії є частковим, але разом з тим найважливішим випадком більш загальної проблеми розв'язності. (uk) |
| dbo:wikiPageExternalLink | https://www.google.com.au/books/edition/Computability_and_Unsolvability/nbOqAAAAQBAJ%3Fhl=en&pg=PP1 https://www.google.com/books/edition/Set_Theory_for_Computing/KWvlBwAAQBAJ%3Fhl=en&gbpv=1&pg=PR2 |
| dbo:wikiPageID | 913118 (xsd:integer) |
| dbo:wikiPageLength | 16413 (xsd:nonNegativeInteger) |
| dbo:wikiPageRevisionID | 1121923628 (xsd:integer) |
| dbo:wikiPageWikiLink | dbr:Propositional_formula dbr:Quantifier_elimination dbr:Entscheidungsproblem dbr:Monadic_predicate_calculus dbr:Boris_Trakhtenbrot dbr:Algebraically_closed_field dbr:Peano_arithmetic dbr:Validity_(logic) dbr:Decidable_sublanguages_of_set_theory dbr:Decision_problem dbr:Deductive_closure dbr:Independence_(mathematical_logic) dbr:Infinite_chess dbr:Interpretability dbr:Presburger_arithmetic dbr:Computable_function dbc:Proof_theory dbr:Games dbr:Mojżesz_Presburger dbr:Andrzej_Mostowski dbr:Leopold_Löwenheim dbr:Linear_logic dbr:Logic dbr:Complete_theory dbr:Decidability_of_First-order_Theory_of_Real_Numbers dbr:Propositional_logic dbr:Syntax_(logic) dbr:Many-one_reduction dbr:Tree_(graph_theory) dbr:Truth_table dbr:Type_theory dbr:Gödel's_completeness_theorem dbr:Julia_Robinson dbr:Robinson_arithmetic dbr:Paraconsistent_logic dbr:Alfred_Tarski dbr:First-order_logic dbr:Formal_semantics_(logic) dbr:Formal_proof dbr:Formal_system dbr:Church's_thesis dbr:Logical_consequence dbr:Recursively_enumerable dbr:Group_(mathematics) dbr:Hyperbolic_geometry dbr:Abelian_group dbr:Academic_Press dbc:Concepts_in_logic dbr:Characteristic_(algebra) dbr:Chess dbr:Effective_method dbr:Higher-order_logic dbr:Ternary_logic dbr:Theory_(mathematical_logic) dbr:Zeroth-order_logic dbc:Metalogic dbr:Boolean_algebras_canonically_defined dbr:Real_closed_field dbr:Recursively_enumerable_set dbr:Second-order_logic dbr:Monadic_second-order_logic dbr:Sequent dbr:Signature_(logic) dbr:Skolem_arithmetic dbr:Undecidable_problem dbr:Tarski–Seidenberg_theorem dbr:Euclidean_geometry dbr:Tarski's_exponential_function_problem dbr:Existential_quantification dbr:S2S_(mathematics) dbr:Łoś-Vaught_test dbr:Springer-Verlag dbr:Logical_system dbr:Raphael_Robinson dbr:Decidable_set dbr:Model_completeness dbr:Logical_validity |
| dbp:wikiPageUsesTemplate | dbt:Authority_control dbt:Citation dbt:Portal dbt:Reflist dbt:Short_description dbt:Mathematical_logic dbt:Metalogic |
| dcterms:subject | dbc:Proof_theory dbc:Concepts_in_logic dbc:Metalogic |
| rdf:type | owl:Thing yago:WikicatConceptsInLogic yago:Abstraction100002137 yago:Cognition100023271 yago:Concept105835747 yago:Content105809192 yago:Idea105833840 yago:PsychologicalFeature100023100 |
| rdfs:comment | Rozhodnutelnost je matematický pojem z oblasti matematické logiky. Vyjadřuje, zda existuje konečný algoritmus, který pro každou formuli určí, zda je v dané teorii dokazatelná nebo není. Teorie, pro niž takový algoritmus existuje, se nazývá rozhodnutelná, v opačném případě pak nerozhodnutelná. Problematika rozhodnutelnosti úzce souvisí s Gödelovými větami o neúplnosti. (cs) In logic, a true/false decision problem is decidable if there exists an effective method for deriving the correct answer. Zeroth-order logic (propositional logic) is decidable, whereas first-order and higher-order logic are not. Logical systems are decidable if membership in their set of logically valid formulas (or theorems) can be effectively determined. A theory (set of sentences closed under logical consequence) in a fixed logical system is decidable if there is an effective method for determining whether arbitrary formulas are included in the theory. Many important problems are undecidable, that is, it has been proven that no effective method for determining membership (returning a correct answer after finite, though possibly very long, time in all cases) can exist for them. (en) En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique. L’indécidabilité est la négation de la décidabilité. Dans les deux cas, il s'agit de formaliser l'idée qu'on ne peut pas toujours conclure lorsque l'on se pose une question, même si celle-ci est sous forme logique. (fr) Il concetto di decidibilità si trova in logica matematica e in teoria della computabilità con accezioni differenti. (it) 논리학에서 결정가능성(decidability)은 참/거짓을 묻는 결정 문제가 가질 수 있는 성질의 하나로, 해답을 내어놓는 기계적인 절차가 존재하는 성질을 가리킨다. 대표적으로 정지 문제의 결정불가능성이 알론조 처치와 앨런 튜링에 의해 증명된 바 있다. (ko) 決定可能（けっていかのう、英: decidable）は、数理論理学または現代論理学において、論理式の集合のメンバーシップの決定をする実効的（effectiveな）方法が存在することを指す。決定可能性（けっていかのうせい、英: decidability）は、そのような属性を指す。命題論理のような形式体系は、論理的に妥当な論理式（または定理）の集合のメンバーシップを実効的に決定できるなら、決定可能である。ある決まった論理体系における理論（論理的帰結で閉じている論理式の集合）は、任意の論理式がその理論に含まれるか否かを決定する実効的方法があれば、決定可能である。そうでなければ、決定不能である。 (ja) Rozstrzygalność (decydowalność) problemu matematycznego to następująca jego właściwość: istnieje algorytm, który oblicza odpowiedź na dowolne pytanie stawiane przez problem. Problem może być nierozstrzygalny, jeśli jego rozstrzygalność prowadziłaby do powstania sprzeczności. (pl) Em lógica, o termo decidível se refere a um problema de decisão, ou seja, a questão da existência de um método efetivo para determinar a pertinência em um conjunto de fórmulas. Sistemas lógicos, tais como a lógica proposicional, são decidíveis se a pertinência em seu conjunto de fórmulas logicamente válido pode ser efetivamente determinado. Uma teoria (conjunto de fórmulas fechada sob a consequência lógica) em um sistema lógico fixo é decidível se existe um algoritmo eficiente para determinar se fórmulas arbitrárias pertencem a ela. Muitos problemas importantes são indecidíveis. (pt) Алгоритмическая разрешимость — свойство формальной теории обладать алгоритмом, определяющим по данной формуле, выводима она из множества аксиом данной теории или нет. Теория называется разрешимой, если такой алгоритм существует, и неразрешимой, в противном случае. Вопрос о выводимости в формальной теории является частным, но вместе с тем важнейшим случаем более общей проблемы разрешимости. (ru) Алгоритмічна розв'язність — властивість формальної теорії володіти алгоритмом, який визначає за даною формулою, виводиться вона з множини аксіом даної теорії чи ні. Теорія називається розв'язною, якщо такий алгоритм існує, і нерозв'язною, в іншому випадку. Питання про виводимість у формальній теорії є частковим, але разом з тим найважливішим випадком більш загальної проблеми розв'язності. (uk) En , la decidibilitat és una propietat dels sistemes formals quan, per a qualsevulla fórmula en el llenguatge del sistema, existeix un mètode efectiu per determinar si aquesta fórmula pertany o no al conjunt de les veritats del sistema. Per exemple, la lògica proposicional és decidible, perquè existeix un algoritme (taula de veritat) que en un nombre finit de passos pot decidir si la fórmula és vàlida o no. (ca) En metalógica, la decidibilidad es una propiedad de los sistemas formales cuando, para cualquier fórmula en el lenguaje del sistema, existe un para determinar si esa fórmula pertenece o no al conjunto de las verdades del sistema. Por ejemplo, la lógica proposicional es decidible, porque existe un algoritmo (la tabla de verdad) que en un número finito de pasos puede decidir si la fórmula es válida o no. (es) |
| rdfs:label | Decidibilitat (ca) Rozhodnutelnost (cs) Decidibilidad (es) Decidability (logic) (en) Décidabilité (fr) Decidibilità (it) 결정가능성 (ko) 決定可能性 (ja) Rozstrzygalność (pl) Decidibilidade (pt) Алгоритмическая разрешимость (ru) Алгоритмічна розв'язність (uk) |
| owl:sameAs | freebase:Decidability (logic) yago-res:Decidability (logic) wikidata:Decidability (logic) dbpedia-ca:Decidability (logic) dbpedia-cs:Decidability (logic) dbpedia-es:Decidability (logic) dbpedia-fa:Decidability (logic) dbpedia-fr:Decidability (logic) dbpedia-he:Decidability (logic) dbpedia-it:Decidability (logic) dbpedia-ja:Decidability (logic) dbpedia-ko:Decidability (logic) dbpedia-pl:Decidability (logic) dbpedia-pt:Decidability (logic) dbpedia-ru:Decidability (logic) dbpedia-sl:Decidability (logic) dbpedia-sr:Decidability (logic) dbpedia-uk:Decidability (logic) https://global.dbpedia.org/id/3zBrf |
| prov:wasDerivedFrom | wikipedia-en:Decidability_(logic)?oldid=1121923628&ns=0 |
| foaf:isPrimaryTopicOf | wikipedia-en:Decidability_(logic) |
| is dbo:knownFor of | dbr:Julia_Robinson |
| is dbo:notableIdea of | dbr:Rudolf_Carnap |
| is dbo:wikiPageDisambiguates of | dbr:Decidability |
| is dbo:wikiPageRedirects of | dbr:Decidability_(Logic) dbr:Semidecidability dbr:Semidecidable dbr:Decidability_(computer_science) dbr:Decidable_(logic) dbr:Essentially_undecidable dbr:Semi-decidability |
| is dbo:wikiPageWikiLink of | dbr:Quantifier_elimination dbr:Quantum_logic dbr:Rudolf_Carnap dbr:Entscheidungsproblem dbr:List_of_first-order_theories dbr:Monadic_predicate_calculus dbr:László_Kalmár dbr:Metalogic dbr:Parity_game dbr:Dependent_ML dbr:Description_logic dbr:Algorithm dbr:Alloy_(specification_language) dbr:Hyperbolic_group dbr:Peano_axioms dbr:Vadalog dbr:Decidability_of_first-order_theories_of_the_real_numbers dbr:Decidable_sublanguages_of_set_theory dbr:Decision_problem dbr:Dehornoy_order dbr:Index_of_logic_articles dbr:Index_of_philosophy_articles_(D–H) dbr:List_of_incomplete_proofs dbr:List_of_mathematical_logic_topics dbr:Tarski's_axioms dbr:Presburger_Award dbr:Presburger_arithmetic dbr:Schanuel's_conjecture dbr:Spatial–temporal_reasoning dbr:Context-free_grammar dbr:Coq dbr:Anatoly_Maltsev dbr:General_set_theory dbr:Prenex_normal_form dbr:Church–Turing_thesis dbr:Frank_Ramsey_(mathematician) dbr:Bounded_quantifier dbr:Mojżesz_Presburger dbr:Constant_problem dbr:Constructive_set_theory dbr:Thoralf_Skolem dbr:Take-grant_protection_model dbr:Andrzej_Grzegorczyk dbr:Bernays–Schönfinkel_class dbr:Logic dbr:Simply_typed_lambda_calculus dbr:Computability_logic dbr:Computable_analysis dbr:Decidability dbr:Decidability_(Logic) dbr:Kripke_semantics dbr:Spread_(intuitionism) dbr:Theory_of_computation dbr:Many-one_reduction dbr:Automated_theorem_proving dbr:Burton_Dreben dbr:Admissible_rule dbr:Total_order dbr:Type_system dbr:Wanda_Szmielew dbr:Web_Ontology_Language dbr:Wilhelm_Ackermann dbr:William_Pugh_(computer_scientist) dbr:Gödel_Prize dbr:Julia_Robinson dbr:Robinson_arithmetic dbr:20th_century_in_science dbr:Alfred_Tarski dbr:Algorithmically_random_sequence dbr:Fallibilism dbr:Finite-state_transducer dbr:First-order_logic dbr:Formal_verification dbr:Bar_induction dbr:Formal_system dbr:Foundations_of_mathematics dbr:Glossary_of_game_theory dbr:History_of_logic dbr:History_of_mathematics dbr:List_of_Russian_mathematicians dbr:List_of_Russian_scientists dbr:Natural_deduction dbr:Logical_framework dbr:Warren_Goldfarb dbr:RE_(complexity) dbr:Real_closed_ring dbr:Géraud_Sénizergues dbr:Harry_R._Lewis dbr:Heyting_algebra dbr:Subcountability dbr:Abelian_group dbr:Affine_logic dbr:Alasdair_Urquhart dbr:Effective_method dbr:Termination_analysis dbr:Theory_(mathematical_logic) dbr:Zeno_machine dbr:Modal_companion dbr:Automatic_sequence dbr:Boolean_algebras_canonically_defined dbr:Boolean_ring dbr:Büchi's_problem dbr:Büchi_arithmetic dbr:Free_group dbr:Group_isomorphism_problem dbr:Typing_rule dbr:Independence-friendly_logic dbr:Raphael_M._Robinson dbr:Real_closed_field dbr:Second-order_logic dbr:Semidecidability dbr:Semidecidable dbr:Mathematical_universe_hypothesis dbr:Monadic_second-order_logic dbr:Turing_machine dbr:Satisfiability dbr:Satisfiability_modulo_theories dbr:Skolem_arithmetic dbr:Undecidable_problem dbr:Well-structured_transition_system dbr:Type_inference dbr:Tarski–Seidenberg_theorem dbr:Euclidean_geometry dbr:Exponential_field dbr:Extensionality dbr:List_of_terms_relating_to_algorithms_and_data_structures dbr:List_of_unsolved_problems_in_mathematics dbr:Programming_language dbr:Two-element_Boolean_algebra dbr:Tarski's_exponential_function_problem dbr:Transseries dbr:Evert_Willem_Beth dbr:Finite-valued_logic dbr:Finite_model_property dbr:Outline_of_logic dbr:Theory_of_pure_equality dbr:Decidability_(computer_science) dbr:Decidable_(logic) dbr:Essentially_undecidable dbr:Semi-decidability |
| is dbp:subDiscipline of | dbr:Harry_R._Lewis |
| is foaf:primaryTopic of | wikipedia-en:Decidability_(logic) |