Propriedade do modelo finito: diferenças entre revisões

← Ver a alteração anterior Ver a alteração posterior →

Conteúdo apagado Conteúdo adicionado

Em linha

Revisão das 13h49min de 3 de março de 2015

Em lógica, dizemos que a estrutura L tem a propriedade do modelo finito (ou, PMF) se existe uma classe de modelos M de L (isto é, cada modelo em M é um modelo de L) de tal forma que qualquer não-teorema de L seja falso segundo algum modelo finito de M. Uma outra forma de interpretação, é dizer que a estrutura L tem a PMF se, para cada fórmula A de L, A é um L-teorema se, e somente se, A é um teorema da teoria de modelos finitos de L.

Se L é axiomatizável (e tem um conjunto de regras recursivas) e tem a PMF, então L é decidível. No entanto, a afirmação de que se L é recursivamente axiomatizável, tem a PMF e é decidível, é falsa. Mesmo se houver um número finito de modelos finitos para escolher (a menos de isomorfismos) ainda há o problema de verificar se a estrutura de tais modelos valida a lógica, e isso não pode ser decidível quando a lógica não é finitamente axiomatizável, mesmo quando é recursivamente axiomatizável. (Note que a lógica é recursivamente enumerável se, e somente se, for recursivamente axiomatizável, resultado conhecido como o teorema de Craig.)

Exemplo

Uma fórmula de primeira ordem com um quantificador universal tem a PMF. Uma fórmula de primeira ordem sem símbolos funcionais, em que todos os quantificadores existenciais aparecem primeiro na fórmula, também tem a PMF.^[1]

Veja Mais

Semânticas de Kripke

Referências

Blackburn P., de Rijke M., Venema Y. Modal Logic. Cambridge University Press, 2001.
A Urquhart. Decidability and the Finite Model Property. Journal of Philosophical Logic, 10 (1981), 367-370.

↑ Leonid Libkin, Elements of finite model theory, chapter 14

[1] Leonid Libkin, Elements of finite model theory, chapter 14

[1]

Revisão das 12h40min de 25 de fevereiro de 2015 editar Vitor Mazuco (discussão \| contribs) Autorrevisores 274 847 edições m Foram revertidas as edições de 189.70.212.214 (usando Huggle) ← Ver a alteração anterior		Revisão das 13h49min de 3 de março de 2015 editar desfazer 143.107.99.43 (discussão) É necessário que o modelo seja finito (somo sugere o próprio nome da propriedade) Etiqueta: Editor Visual Ver a alteração posterior →
Linha 1:		Linha 1:
	Em [[lógica]], dizemos que a estrutura '''L''' tem a '''propriedade do modelo finito''' (ou, PMF) se existe uma classe de modelos M de '''L''' (isto é, cada modelo em M é um modelo de '''L''') de tal forma que qualquer não-teorema de '''L''' seja falso segundo algum modelo de M. Uma outra forma de interpretação, é dizer que a estrutura '''L''' tem a PMF se, para cada fórmula A de '''L''', A é um L-teorema se, e somente se, A é um teorema da teoria de modelos finitos de '''L'''.		Em [[lógica]], dizemos que a estrutura '''L''' tem a '''propriedade do modelo finito''' (ou, PMF) se existe uma classe de modelos M de '''L''' (isto é, cada modelo em M é um modelo de '''L''') de tal forma que qualquer não-teorema de '''L''' seja falso segundo algum modelo finito de M. Uma outra forma de interpretação, é dizer que a estrutura '''L''' tem a PMF se, para cada fórmula A de '''L''', A é um L-teorema se, e somente se, A é um teorema da teoria de modelos finitos de '''L'''.

	Se '''L''' é axiomatizável (e tem um conjunto de regras recursivas) e tem a PMF, então '''L''' é decidível. No entanto, a afirmação de que se '''L''' é recursivamente axiomatizável, tem a PMF e é decidível, é falsa. Mesmo se houver um número finito de modelos finitos para escolher (a menos de isomorfismos) ainda há o problema de verificar se a estrutura de tais modelos valida a lógica, e isso não pode ser decidível quando a lógica não é finitamente axiomatizável, mesmo quando é recursivamente axiomatizável. (Note que a lógica é recursivamente enumerável se, e somente se, for recursivamente axiomatizável, resultado conhecido como o [[teorema de Craig]].)		Se '''L''' é axiomatizável (e tem um conjunto de regras recursivas) e tem a PMF, então '''L''' é decidível. No entanto, a afirmação de que se '''L''' é recursivamente axiomatizável, tem a PMF e é decidível, é falsa. Mesmo se houver um número finito de modelos finitos para escolher (a menos de isomorfismos) ainda há o problema de verificar se a estrutura de tais modelos valida a lógica, e isso não pode ser decidível quando a lógica não é finitamente axiomatizável, mesmo quando é recursivamente axiomatizável. (Note que a lógica é recursivamente enumerável se, e somente se, for recursivamente axiomatizável, resultado conhecido como o [[teorema de Craig]].)