Planeamento
Aulas Teóricas
AT01 Apresentação e preliminares 14/02
Apresentação dos docentes. Apresentação da disciplina: objectivos, programa, bibliografia, método de avaliação e horário das sessões de dúvidas.
Programa de Hilbert com vista à formalização da Matemática. Consequências positivas do programa na ciência e na sociedade, não obstante o seu insucesso. Interpretação da noção de formalização proposta por Hilbert à luz da teoria moderna da computação.
Noção de linguagem formal como subconjunto de monóide livre gerado por alfabeto contável. Representação unária dos números naturais.
Referência a diversos modelos de computação (Turing, Church, Kleene,..). Postulado de Church-Turing. Justificação do modelo adoptado (Mathematica).
AT02 Computabilidade de funções e decidibilidade de conjuntos 16/02
Conjuntos decidíveis. Primeiros resultados.
Demonstração da existência de enumeração injectiva computável de universo linguístico.
Conjuntos computavelmente enumeráveis e sua caracterização através da computabilidade da função característica parcial.
AT03 Teoremas fundamentais 23/02
Teorema da projecção e variantes.
Caracterização alternativa de conjunto computavelmente enumerável como domínio de função computável e como contradomínio de função computável.
Estudo da computabilidade e da enumerabilidade computável face às operações sobre conjuntos. Teorema de Post.
Enumerabilidade computável de imagem e imagem inversa por aplicação computável de conjunto computavelmente enumerável. Decidibilidade de imagem inversa por aplicação computável de conjunto decidível. Contra-exemplo relativo à imagem.
AT04 Gödelizações e funções recursivas 28/02
Gödelizações: noção e teorema fundamental. Computabilidade no universo dos naturais.
Noção de função recursiva segundo Kleene. Exemplo com demonstração da correcção.
AT05 Indecidibilidade do problema da terminação 1/03
Função universal computável. Indexação das funções computáveis. Utilização de índices para definir computabilidade de sequência de conjuntos enumeráveis.
AT06 Linguagens de primeira ordem 6/03
AT07 Cálculo de Hilbert 8/03
AT08 Equivalência das noções de derivação 13/03
Teorema do menor ponto fixo. Definições indutivas versus pontos fixos.
Equivalência das noções de derivação.
AT09 Metateoremas e regras admissíveis 15/03
Noção de dependência de hipótese e de generalização essencial sobre dependente de hipótese.
Metateorema da hipótese inútil.
Metateorema da dedução (MTD).
AT10 Metateoremas e regras admissíveis (conc) 20/03
Variantes, aplicações e corolários do metateorema da dedução (MTC e MTCP).
Metateorema da substitutição por equivalente (MTSE).
Regra da substituição (RS).
AT11 Semidecidibilidade da lógica de 1a ordem 22/03
Enumerabilidade computável do fecho por derivação de conjunto computavelmente enumerável.
AT12 Apresentações e teorias 27/03
Noção de teoria, teoria coerente e teoria exaustiva. Primeiros exemplos. Apresentações de teorias. Teorias axiomatizáveis, teorias decidíveis e teorias semi-decidíveis. Resultados fundamentais: decidibilidade de teoria exaustiva e semi-decidível; enumerabilidade computável de teoria axiomatizável; teorema de Craig (toda a teoria semi-decidível é axiomatizável).
AT13 Satisfação, consequência semântica e validade 29/03
Estrutura de interpretação. Atribuição. Denotação de termo. Satisfação local e global. Validade. Consequência semântica. Exemplos.
AT14 TESTE 3/04
Teste.
AT15 Lemas semânticos 12/04
Lemas das variáveis omissas. Lemas das fórmulas fechadas. Lemas da substituição.
AT16 Correcção do cálculo de Hilbert 17/04
Validade dos axiomas. Correcção das regras de inferência. Correcção forte e fraca do cálculo de Hilbert. Demonstração da coerência do cálculo de Hilbert por via semântica e sua crítica face ao programa de Hilbert. Teoria de estrutura de interpretação.
AT17 Lema de Lindenbaum 19/04
Panorâmica da técnica de Henkin para a demonstração da completude do cálculo de Hilbert. Lema de Lindenbaum.
Preservação da coerência de conjunto de fómulas por enriquecimento da assinatura com constantes.
AT18 Construção de Henkin 24/04
Coerência da extensão existencial de conjunto coerente. Lema fundamental da construção de Henkin.
AT19 Completude 26/04
Lema da existência de modelo de conjunto coerente. Teorema de completude de Gödel. Corolários: teoremas da cardinalidade e da compacidade.
AT20 Igualdade 3/05
Assinaturas com igualdade. Teorias com igualdade. Teoria da igualdade. Resultados básicos sobre teorias com igualdade. Existência de modelos normais. Lógica de primeira ordem com igualdade.
AT21 Aritmética 8/05
Teorias da aritmética. Estrutura padrão. Teorias Th(N), N e P. Aritmética como lógica (FOLA) e sua incompletude forte usando o argumento de não compacidade.
Aplicação representável em teoria da aritmética. Exemplo.
AT22 - Representabilidade 10/05
Aplicação representável em teoria da aritmética (exemplo). Conjunto representável em teoria da aritmética. Lema da equivalência entre representabilidade de conjunto e da respectiva aplicação característica. Referência ao teorema de normalização de Kleene. Lema da remoção da recursão primitiva por codificação das sequências de números naturais. Aplicações e conjuntos computáveis à Gödel.
AT23 Representabilidade (conc) 15/05
Aplicação beta de Gödel. Representabilidade das aplicações computáveis em Th(N). Referência à representabilidade das aplicações computáveis na teoria finitamente axiomatizada N.
Lema de Cantor (argumento da diagonal). Gödelização da linguagem da aritmética. Substituição em fórmula de variável por termo como operação nos naturais.
AT24 Primeiro teorema da incompletude 17/05
Noção de extensão de fórmula em teoria da aritmética. Propriedades básicas. Teorema de Church. Primeiro teorema da incompletude (Gödel-Rosser) e corolários sobre Th(N). Teorema de Tarski. Indecidibilidade da lógica de primeira ordem.
AT25 Pseudo-representação da derivabilidade 22/05
Pseudo-representação da derivabilidade em teoria apropriada da aritmética, recorrendo apenas à Gödelização das fórmulas e ao teorema da projecção. Propriedades básicas da pseudo-representação da derivabilidade. Propriedades adicionais no caso de teoria coerente-omega. Condições HBL.
AT26 Segundo teorema da incompletude de Gödel 24/05
Teorema do ponto fixo. Teorema de Löb. Segundo teorema da incompletude de Gödel. Obtenção do primeiro teorema da incompletude de Gödel como corolário. Referência a fragmentos interessantes da matemática decidíveis.