Na teoria dos modelos, um modelo canônico é uma estrutura associada, de modo sistemático, a um conjunto de sentenças atômicas de uma linguagem de primeira ordem. A construção parte dos termos fechados da linguagem, identifica termos que devem ter o mesmo valor e define relações e funções de forma compatível com as sentenças atômicas dadas.
Essa construção pode ser vista como um processo inverso ao do diagrama: enquanto o diagrama registra, por meio de sentenças, a informação atômica satisfeita por uma estrutura, o modelo canônico reconstrói uma estrutura gerada por termos a partir de um conjunto de sentenças atômicas. Em contextos próximos, especialmente na programação lógica, construções análogas também são descritas como modelos de termos fechados ou modelos de Herbrand.
Fechamento atômico
Para que a construção seja bem definida, é necessário considerar não apenas as sentenças atômicas inicialmente dadas, mas também as igualdades e substituições que elas implicam. Seja uma assinatura de primeira ordem e seja um conjunto de sentenças atômicas de . Diz-se que é fechado, no sentido relevante para a construção, quando satisfaz as seguintes condições:
para todo termo fechado de , a sentença pertence a ; se pertence a , então a substituição de por preserva as sentenças atômicas pertencentes a .
Quando o conjunto inicial de sentenças atômicas não é fechado, considera-se seu menor fechamento por igualdade e substituição. Esse fechamento garante que termos identificados por igualdade tenham o mesmo comportamento nas relações e funções da estrutura construída.
Construção
Suponha que tenha ao menos um termo fechado. Se a linguagem não possuir termos fechados, é comum expandi-la temporariamente com uma constante nova para realizar a construção. Seja o conjunto dos termos fechados de . Define-se uma relação de equivalência entre termos fechados por:
se, e somente se, pertence ao fechamento atômico de .
O domínio do modelo canônico é o conjunto das classes de equivalência dos termos fechados:
.
A interpretação dos símbolos de é definida da seguinte forma:
cada constante é interpretada por sua classe de equivalência, isto é, ; cada símbolo funcional de aridade é interpretado por ; cada símbolo relacional de aridade vale em quando a sentença atômica pertence ao fechamento atômico de .
A definição é independente da escolha dos representantes das classes de equivalência, pois o fechamento por igualdade assegura que termos equivalentes possam ser substituídos sem alterar as sentenças atômicas verdadeiras.
Propriedade universal
O modelo canônico satisfaz as sentenças atômicas de partida e é gerado por seus termos fechados. Mais precisamente, para um conjunto de sentenças atômicas de , o modelo canônico satisfaz , e todo elemento de é da forma para algum termo fechado de .
Além disso, se é qualquer outra -estrutura que satisfaz , então existe um único homomorfismo de em que envia cada classe de termo para o valor de em :
.
Essa propriedade caracteriza o modelo canônico, a menos de isomorfismo. Em termos algébricos, ele funciona como uma estrutura inicial entre os modelos de gerados pelos dados atômicos especificados.
Relação com diagramas positivos
O diagrama de uma estrutura é obtido ao expandir a linguagem com constantes que nomeiam elementos da estrutura e registrar sentenças verdadeiras nessa expansão. O diagrama ordinário inclui sentenças atômicas e negações de sentenças atômicas; sua parte positiva registra apenas as sentenças atômicas verdadeiras.
Nesse contexto, o modelo canônico realiza o movimento inverso: parte de informação atômica positiva e constrói uma estrutura que a satisfaz. Quando o conjunto de sentenças atômicas é o diagrama positivo de uma estrutura suficientemente nomeada por termos fechados, o modelo canônico recupera uma estrutura isomorfa à parte gerada pelos elementos nomeados.
Ver também
Teoria dos modelos Lógica de primeira ordem Homomorfismo Universo de Herbrand
Categoria:Teoria dos modelos Categoria:Lógica matemática