Diferència entre revisions de la pàgina «Decidibilitat»
De Wikisofia
m (bot: -fómula +fórmula) |
|||
| (Hi ha una revisió intermèdia del mateix usuari que no es mostren) | |||
| Línia 1: | Línia 1: | ||
{{ConcepteWiki}} | {{ConcepteWiki}} | ||
| − | Propietat dels [[Sistema_formal|sistemes formals]] que disposen d'un [[Procediment_de_decisió|procediment de decisió]] efectiu, o un [[Algorisme|algorisme]], que permet determinar si tota expressió ben formada del sistema és o no és deduïble dins del sistema. Als [[Sistema_formal|sistemes formals]] que gaudeixen d'aquesta propietat per a totes les seves fórmules o expressions se'ls anomena decidibles. Una expressió ben formada és deduïble si és un [[Teorema|teorema]] del sistema. Al seu torn, una | + | Propietat dels [[Sistema_formal|sistemes formals]] que disposen d'un [[Procediment_de_decisió|procediment de decisió]] efectiu, o un [[Algorisme|algorisme]], que permet determinar si tota expressió ben formada del sistema és o no és deduïble dins del sistema. Als [[Sistema_formal|sistemes formals]] que gaudeixen d'aquesta propietat per a totes les seves fórmules o expressions se'ls anomena decidibles. Una expressió ben formada és deduïble si és un [[Teorema|teorema]] del sistema. Al seu torn, una fórmula és decidible dins d'un sistema si aquesta o la seva [[Negació|negació]] són teoremes del sistema. |
Segons el [[Teorema_de_Church|teorema de Church]], la [[Lògica|lògica de predicats]] de primer ordre no disposa de tal [[Procediment_de_decisió|procediment de decisió]]. Sí que el posseeix, en canvi, la [[Lògica|lògica d'enunciats]]: les [[Lògica#Taules_de_veritat|taules de veritat]] (i les expressions monádicas de la lògica de predicats, reductibles a expressions de lògica d'enunciats) | Segons el [[Teorema_de_Church|teorema de Church]], la [[Lògica|lògica de predicats]] de primer ordre no disposa de tal [[Procediment_de_decisió|procediment de decisió]]. Sí que el posseeix, en canvi, la [[Lògica|lògica d'enunciats]]: les [[Lògica#Taules_de_veritat|taules de veritat]] (i les expressions monádicas de la lògica de predicats, reductibles a expressions de lògica d'enunciats) | ||
Revisió de 19:50, 18 abr 2017
Propietat dels sistemes formals que disposen d'un procediment de decisió efectiu, o un algorisme, que permet determinar si tota expressió ben formada del sistema és o no és deduïble dins del sistema. Als sistemes formals que gaudeixen d'aquesta propietat per a totes les seves fórmules o expressions se'ls anomena decidibles. Una expressió ben formada és deduïble si és un teorema del sistema. Al seu torn, una fórmula és decidible dins d'un sistema si aquesta o la seva negació són teoremes del sistema.
Segons el teorema de Church, la lògica de predicats de primer ordre no disposa de tal procediment de decisió. Sí que el posseeix, en canvi, la lògica d'enunciats: les taules de veritat (i les expressions monádicas de la lògica de predicats, reductibles a expressions de lògica d'enunciats)