FERREIRA, Francicleber Martins. Modelos minimais e hierarquia de expressividade. 2007. 122 f. Dissertação (Mestrado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2007. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-11T15:45:38Z No. of bitstreams: 1 2007_dis_fmferreira.pdf: 752533 bytes, checksum: 98c57917ae2bd6af5de38f25d9ce7c39 (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-15T15:38:19Z (GMT) No. of bitstreams: 1 2007_dis_fmferreira.pdf: 752533 bytes, checksum: 98c57917ae2bd6af5de38f25d9ce7c39 (MD5) / Made available in DSpace on 2016-07-15T15:38:19Z (GMT). No. of bitstreams: 1 2007_dis_fmferreira.pdf: 752533 bytes, checksum: 98c57917ae2bd6af5de38f25d9ce7c39 (MD5) Previous issue date: 2007 / Neste trabalho, o conceito de Modelo Minimal e seu uso na semântica de certas lógicas são estudados. Nós analisamos o poder expressivo de diversas lógicas que usam o conceito de Modelo Minimal para definir sua relação de satisfação. Os principais teoremas estudados foram o Teorema de Löwenheim-Skolem e o Teorema de Definibilidade de Beth. No Capítulo 1, nós damos algumas motivações e revisamos alguns conceitos básicos de Lógica. No Capítulo 2, nos estudamos a Lógica de Menor Ponto Fixo|LFP. Nós exibimos uma prova de que o Teorema de Beth não vale para LFP. Nós usamos teorias infinitas para provar isso. Utilizando um resultado de Hodkinson para L!!1!, nós mostramos que o Teorema de Beth continua não valendo mesmo para teorias finitas de LFP. Nós continuamos estudando problemas de definibilidade para LFP e demonstramos que, para tipos especiais de definições implícitas formadas por Sistemas Recursivos, que funcionam como definições recursivas em determinados contextos, existe uma definição explícita. Nós promavos ainda que o Teorema de LÄowenheim-Skolem Descendente vale para qualquer conjunto de fórmulas de LFP, independentemente de sua cardinalidade. No Capítulo 3, a Circunscrição de McCarthy e as Teorias Circunscritivas Aninhadas de Lifschitz, uma generalização da primeira. Nós abordamos o poder expressivo de Circunscrição e a falha do Teorema de LÄowenheim-Skolem Descendente. Nós também investigamos questões de definibilidade no contexto de Circunscrição. Nós encerramos esse capítulo mostrando que as Teorias Circunscritivas Aninhadas possuem poder expressivo comparável com o da Lógica de Segunda-Ordem. No Capítulo 4, nós estendemos uma lógica criada por van Benthem dando origem a duas outras lógicas, a saber, U-MIN e I-MIN. Nós provamos que ambas são equivalentes entre si em poder expressivo e daí em diante chamamos U-MIN de MIN. Nós introduzimos a Lógica Si-MIN de minimalização simultânea e provamos que Si-MIN é equivalente a U-MIN e I-MIN e também à Lógica de Segunda-Ordem. Nós então propomos o fragmento MIN¢ de MIN, cujo poder expressivo situa-se entre o da Lógica de Segunda-Ordem e o de LFP. No Capítulo 5, nós reunimos nossas conclusões e apontamos trabalhos futuros.

Esta dissertação estabelece a incompletude de um sistema formal cujas únicas constantes não-lógicas são 0 e s (respectivamente, o número natural 0 e a função sucessor segundo a interpretação standard), fundamentando-se, para tanto, em um teorema cuja prova necessita essencialmente da maquinária lógica de segunda-ordem e que foi designado de Teorema das Definições Recursivas. / We establish here the incompleteness of the formal system S2 for arithmetic_a formal system whose signature is {0, s}_by means of the Theorem of the Definition by Recursion (TDR). However, unlike the standard proofs of incompleteness, the proof of TDR, by virtue of restricted signature, uses essentially the power of second-order logic.

Esta dissertação estabelece a incompletude de um sistema formal cujas únicas constantes não-lógicas são 0 e s (respectivamente, o número natural 0 e a função sucessor segundo a interpretação standard), fundamentando-se, para tanto, em um teorema cuja prova necessita essencialmente da maquinária lógica de segunda-ordem e que foi designado de Teorema das Definições Recursivas. / We establish here the incompleteness of the formal system S2 for arithmetic_a formal system whose signature is {0, s}_by means of the Theorem of the Definition by Recursion (TDR). However, unlike the standard proofs of incompleteness, the proof of TDR, by virtue of restricted signature, uses essentially the power of second-order logic.

FERREIRA, Francicleber Martins. Modelos minimais e hierarquia de expressividade. 2007. 109 f. : Dissertação (mestrado) - Universidade Federal do Ceará, Centro de Ciências, Departamento de Computação, Fortaleza-CE, 2007. / Submitted by guaracy araujo (guaraa3355@gmail.com) on 2016-06-29T18:55:46Z No. of bitstreams: 1 2007_dis_fmferreira.pdf: 752533 bytes, checksum: 98c57917ae2bd6af5de38f25d9ce7c39 (MD5) / Approved for entry into archive by guaracy araujo (guaraa3355@gmail.com) on 2016-06-29T18:56:33Z (GMT) No. of bitstreams: 1 2007_dis_fmferreira.pdf: 752533 bytes, checksum: 98c57917ae2bd6af5de38f25d9ce7c39 (MD5) / Made available in DSpace on 2016-06-29T18:56:33Z (GMT). No. of bitstreams: 1 2007_dis_fmferreira.pdf: 752533 bytes, checksum: 98c57917ae2bd6af5de38f25d9ce7c39 (MD5) Previous issue date: 2007 / Neste trabalho, o conceito de Modelo Minimal e seu uso na semântica de certas lógicas são estudados. Nós analisamos o poder expressivo de diversas lógicas que usam o conceito de Modelo Minimal para definir sua relação de satisfação. Os principais teoremas estudados foram o Teorema de Löwenheim-Skolem e o Teorema de Definibilidade de Beth. No Capítulo 1, nós damos algumas motivações e revisamos alguns conceitos básicos de Lógica. No Capítulo 2, nos estudamos a Lógica de Menor Ponto Fixo|LFP. Nós exibimos uma prova de que o Teorema de Beth não vale para LFP. Nós usamos teorias infinitas para provar isso. Utilizando um resultado de Hodkinson para L!!1!, nós mostramos que o Teorema de Beth continua não valendo mesmo para teorias finitas de LFP. Nós continuamos estudando problemas de definibilidade para LFP e demonstramos que, para tipos especiais de definições implícitas formadas por Sistemas Recursivos, que funcionam como definições recursivas em determinados contextos, existe uma definição explícita. Nós promavos ainda que o Teorema de LÄowenheim-Skolem Descendente vale para qualquer conjunto de fórmulas de LFP, independentemente de sua cardinalidade. No Capítulo 3, a Circunscrição de McCarthy e as Teorias Circunscritivas Aninhadas de Lifschitz, uma generalização da primeira. Nós abordamos o poder expressivo de Circunscrição e a falha do Teorema de LÄowenheim-Skolem Descendente. Nós também investigamos questões de definibilidade no contexto de Circunscrição. Nós encerramos esse capítulo mostrando que as Teorias Circunscritivas Aninhadas possuem poder expressivo comparável com o da Lógica de Segunda-Ordem. No Capítulo 4, nós estendemos uma lógica criada por van Benthem dando origem a duas outras lógicas, a saber, U-MIN e I-MIN. Nós provamos que ambas são equivalentes entre si em poder expressivo e daí em diante chamamos U-MIN de MIN. Nós introduzimos a Lógica Si-MIN de minimalização simultânea e provamos que Si-MIN é equivalente a U-MIN e I-MIN e também à Lógica de Segunda-Ordem. Nós então propomos o fragmento MIN¢ de MIN, cujo poder expressivo situa-se entre o da Lógica de Segunda-Ordem e o de LFP. No Capítulo 5, nós reunimos nossas conclusões e apontamos trabalhos futuros.