O teorema da compactação para FOL foi formalizado em Coq / Isabelle / etc?
12
Estive procurando uma formalização do teorema da compactação para o FOL, mas não encontrei nenhum. Alguém conhece esse desenvolvimento ou trabalho relacionado?
Você já tentou perguntar nas listas de correspondência Coq ou Isabelle?
31512 Dave McLaren
2
Não tenho certeza se isso é adequado para a história, mas veja isso . Completude existe, e compacidade não está longe disso.
Kaveh
Veja também a entrada AFP para uma versão em Isabelle / HOL (de 2004).
Makarius 4/03/13
Respostas:
16
O teorema da compactação para a lógica clássica de primeira ordem é uma conseqüência direta do teorema da completude e, na verdade, pode-se provar diretamente a compactação pelo argumento do estilo Henkin usado para a completude, sem nunca mencionar a derivação.
O teorema da completude para as FOL clássicas em relação aos modelos padrão de Tarski foi formalizado em Mizar. Veja a série de artigos em http://fm.mizar.org/2005-13/fm13-1.html
Digo "quase" porque há um ponto técnico, comprovando a correção de um algoritmo de classificação, que ainda não tive tempo de concluir, mas o principal ingrediente (teorema construtivo de ultra-filtro para linguagens contáveis) é formalizado.
Pode-se considerar também Completude e, portanto, Compacidade, para uma noção não padrão de validade, e obter uma prova construtiva completa e formalizada.
Respostas:
O teorema da compactação para a lógica clássica de primeira ordem é uma conseqüência direta do teorema da completude e, na verdade, pode-se provar diretamente a compactação pelo argumento do estilo Henkin usado para a completude, sem nunca mencionar a derivação.
O teorema da completude para as FOL clássicas em relação aos modelos padrão de Tarski foi formalizado em Mizar. Veja a série de artigos em http://fm.mizar.org/2005-13/fm13-1.html
O mesmo teorema da completude, mas com uma prova construtiva, foi quase formalizado por mim no assistente de prova Coq, consulte o arquivo zip em https://sites.google.com/site/dankoilik/publications/phd-thesis
Digo "quase" porque há um ponto técnico, comprovando a correção de um algoritmo de classificação, que ainda não tive tempo de concluir, mas o principal ingrediente (teorema construtivo de ultra-filtro para linguagens contáveis) é formalizado.
Pode-se considerar também Completude e, portanto, Compacidade, para uma noção não padrão de validade, e obter uma prova construtiva completa e formalizada.
fonte
A compactação para o FOL foi feita no HOL por John Harrison e relatada no TPHOLs 1998. Consulte Formalizando a teoria básica do modelo de primeira ordem .
fonte