Seminários 2006

• 12/12/2006
  "O que a Lógica Matemática tem a dizer a Zenão? A formalização de paradoxos da filosofia - Parte II",
  por Renan Claudino (monitor de Lógica Matemática).
  Resumo:
  O filósofo grego Zenão tornou-se famoso por seus paradoxos ligados à natureza do movimento. Nesse seminário apresentamos uma formulação dos argumentos atribuídos a Zenão em uma linguagem lógica de primeira-ordem. Para torná-los deduções legítimas, será necessário acrescentar algumas premissas (falsas, é claro, dada as conclusões não verdadeiras). Isso definirá um espaço limitado de proposições que podem ser tacitamente (ou inconscientemente) assumidas pelos leitores, quando esses se encantam com a verossimilhança dos paradoxos. Nosso propósito será discernir quais suposições mais provavelmente dão a aparência de validade aos raciocínios contra-sensuais. Para descobrí-las com objetividade, a estratétia será a comparação com argumentações semelhantes, porém válidas, uma vez que a validade de uma argumentação pode tornar mais claras suas premissas.
  
  
• 28/11/2006
  "Sistemas de Tipos com Dicionários - Parte IV: Uma Aplicação",
  por Eduardo Ochs.
  Resumo:
  Um artigo de Anders Kock de 1977, chamado "A Simple Axiomatics for Differentiation", descreve como fazer cálculo diferencial num ambiente em que um certo objeto, A (um anel), faz papel de "R com infinitesimais nilpotentes". Se definimos D := {x in A | x² = 0} e consideramos um certo mapa α : A×A → A^D, basta impor um axioma - "α é inversível" - para que possamos definir, para cada f : A → A, a sua derivada, f' : A → A; e esta noção de derivada se comporta como esperado: (f+g)' = f'+g', (fg)' = f'g + fg', e a regra da cadeia vale.
  No artigo original todos as definições e diagramas são feitos usando a notação categórica tradicional, que é precisa mas bastante opaca. Vamos ver como usar a notação de sistemas de tipos com dicionários para produzir versões auxiliares para cada diagrama em que os nomes das funções indicam como elas levam cada "ponto" do domínio num "ponto" do contradomínio - por exemplo, a função α acima passa a ser chamada de (y, y_x) → (dx → y + y_x dx), e a inversa dela passa a ser chamada de (dx → f(x + dx)) → (f(x), f'(x)).
  (Ver resumo da Parte III - 14/11/2006)
  
  
• 21/11/2006
  "O Teorema Fundamental da Aritmética: História e Aplicações",
  por Bruno Kappel.
  Resumo:
  O Teorema Fundamental da Aritmética (TFA) afirma que todo número natural maior do que 1 pode ser decomposto de maneira única como um produto de números primos. Sua importância no desenvolvimento da aritmética formal é salientada por vários autores e o estudo do TFA faz parte da formação básica de todo estudante de matemástica. Apesar disso, muitos alunos não compreendem completamente a natureza deste resultado e nem a sua prova.
  Em nosso trabalho, classificamos as provas do TFA, existentes na literatura, em quatro grupos, de acordo com o uso, ou não, da noção de Máximo Divisor Comum e do uso, ou não, do Princípio de Indução Matemática como um método de prova. Apresentamos uma prova de cada tipo, bem como um esboço da história do TFA. Finalmente, discutimos algumas aplicações do TFA.
  
  
• 14/11/2006
  "Sistemas de Tipos com Dicionários - Parte III",
  por Eduardo Ochs.
  Resumo:
  Nesta terceira parte vamos reexaminar - desta vez com bem mais detalhes - a tradução entre árvores de derivação nos sistemas de tipos com dicionários ("TSDs") e derivações em "pure type systems" ("PTSs"); esta tradução é bem parecida com a tradução entre Dedução Natural e Cálculo de Seqüentes. Uma derivação num TSD é como uma derivação em um PTS em que: (0) o nome de cada variável indica o seu "nível" (os PTSs e TSDs que nos interessam são estratificados); (1) as variáveis do contexto - omitidas em TSDs, explícitas em PTSs - são obtidas por inspeção da árvore acima de cada nó; (2) os contextos são "mínimos", num certo sentido preciso; (3) aplicações das regra "weakening" e "exchange" são sempre implícitas; (4) as declarações de tipo, omitidas em derivações em TSDs, aparecem quando aplicamos o algoritmo que constrói o dicionário.
  Vamos ver também como representar lógica de 1ª ordem em TSDs e PTSs, e vamos definir formalmente os sistemas de tipos em que estamos mais interessados - eles correspondem aos sistemas $\lambda \rightarrow$, $\lambda 2$ e $\lambda P$ do $\lambda$-cubo [Geuvers93], mas os nossos sistemas incluem somas dependentes ("$\Sigma$"s).
  (Ver resumo da Parte II - 24/10/2006)
  
  
• 31/10/2006
  "On games and the polynomial-space completeness of intuitionistic propositional logic - Part III",
  por Marcelo Correa, IM-UFF.
  Resumo:
  Besides recalling and closing points and questions that were under discussion in the last talk, now comments will be actually made on how to adapt the considered approach to prove the PSPACE completeness of the purely implicational fragment of intuitionistic Logic. The challenges that must be faced to do the same for the classical case will be pointed out.
  (Ver resumo da Parte II - 10/10/2006)
  
  
• 24/10/2006
  "Sistemas de Tipos com Dicionários - Parte II",
  por Eduardo Ochs.
  Resumo:
  Uma derivação em um sistema de tipos se parece com uma árvore em cálculo de seqüentes, mas num seqüente as hipóteses e conclusões são proposições, e num "judgment" em teoria de tipos ao invés de proposições temos declarações da forma a:A, onde A é um tipo e a é uma variável ou um termo daquele tipo.
  Derivações em sistemas de tipos ficam grandes demais - elas contêm muitas informações redundantes que são necessárias para a formalização mas que obscurecem a visão intuitiva do que está acontecendo. No entanto, se permitimos certos "nomes longos" para variáveis e termos - e se desistimos de manter a distinção sintática entre variáveis e termos - então as declarações de tipo se tornam redundantes e podem ser apagadas - o tipo associado a um nome longo é, a grosso modo, o nome longo "reescrito em maiúsculas" - e em certos casos os contextos (as hipóteses à esquerda dos "|-"s) também podem ser apagados. A árvore com nomes longos (e talvez com os contextos suprimidos também) é muito menor que a original mas é equivalente a ela - um algoritmo simples, que percorre a árvore com nomes longos a partir das folhas e monta um dicionário no processo, reconstrói a árvore original a partir da árvore menor.
  Na primeira parte (3/out/2006) vimos a semântica intuitiva para judgments e derivações, tanto na linguagem padrão quanto na linguagem com nomes longos, e vimos como a tradução entre as duas linguagens funciona. Nesta segunda parte vamos formalizar "Pure Type Systems" (como em Geuvers, "Logics and Type Systems" (1993)), usando o sistema com nomes longos para entender as regras de PTSs, e vamos começar a ver como usar o sistema com nomes longos para destrinchar artigos que usam uma linguagem algébrica demais ou categórica demais - o nosso primeiro exemplo será o artigo "A simple axiomatics for differentiation" (Anders Kock, 1977).
  
  
• 17/10/2006
  "Definibilidade nos cálculos relacionais com domínio estruturado",
  por Petrucio Viana, IM-UFF.
  Resumo:
  Apresentamos vários operadores com os quais o Cálculo Relacional de DeMorgan-Peirce-Schröeder-Tarski pode ser estendido, para tratar as noções de concorrência e paralelismo. E mostramos alguns resultados sobre a interdefinibilidade destes operadores.
  
  
• 10/10/2006
  "On games and the polynomial-space completeness of intuitionistic propositional logic - Part II",
  por Marcelo Correa, IM-UFF.
  Resumo:
  In the first talk, it was presented an alternative proof of Ladner and Statman's result that intuitionistic propositional logic is PSPACE-complete, combining proof and game-theoretical approaches and, so, gaining the main benefits obtained in each of them: the very informative aspect of a proof-theoretical framework and the stimulating and intuitive appeal of certain graph and semantical games. Now some adjustments on this proof are pointed out. Comments will also be made on how to adapt such approach for dealing with the purely implicational fragment of intuitionistic Logic and on the challenges that must be faced to do the same for the classical case.
  
  
• 03/10/2006
  "Sistemas de Tipos com Dicionários",
  por Eduardo Ochs.
  
  
• 26/09/2006
  "Algebrização da Lógica Proposicional - Parte IX",
  por Petrucio Viana, IM-UFF.
  Resumo:
  Nesse seminário, vamos revisar os conceitos e resultados sobre a Álgebra Booleana que são relevantes para a lógica algébrica. Em particular, enfocaremos a Álgebra de Lindembaum e o Teorema da Representação, de Stone.
  (Ver resumo da Parte I - 08/06/2006)
  
  
• 12/09/2006
  "Semânticas para Lógica Modal"
  por Renata de Freitas, IM-UFF.
  Resumo:
  Durante muito tempo, desde o trabalho de I. Lewis, em 1918, a Lógica Modal foi estudada apenas através de um aparato dedutivo. Somente em 1963, S. Kripke propôs uma semântica para a Lógica Modal, atualmente conhecida como semântica de Kripke, ou semântica de mundos possíveis. Em 1970, D. Scott e R. Montague propuseram, independentemente, uma outra abordagem semântica para a Lógica Modal, a chamada semântica de vizinhanças. Nesse seminário, vamos apresentar a linguagem da Lógica Modal (básica) e estas duas formulações semânticas: de mundos possíveis e de vizinhanças. Vamos, também, identificar a relação entre elas, mostrando que a semântica de vizinhanças pode ser vista como uma generalização da semântica de mundos possíveis.
  
  
• 24/08/2006
  "O que a Lógica Matemática tem a dizer para Zenão? A formalização de paradoxos da filosofia."
  por Renan Claudino (monitor de Lógica Matemática).
  Resumo:
  O filósofo grego Zenão tornou-se famoso por seus paradoxos ligados à natureza do movimento. Nesse seminário, reescrevemos os argumentos atribuídos a Zenão em uma linguagem lógica de primeira-ordem. Para torná-los deduções legítimas, será necessário acrescentar algumas premissas (falsas, é claro, dada as conclusões não verdadeiras). Isso definirá um espaço limitado de proposições que podem ser tacitamente (ou inconscientemente) assumidas pelos leitores, quando esses se encantam com a verossimilhaça dos paradoxos. Nosso propósito será discernir quais suposições mais provavelmente dão a aparêcia de validade aos raciocínios contra-sensuais.
  
  
• 17/08/2006
  "Algebrização da Lógica Proposicional - Parte VIII",
  por Petrúcio Viana, IM-UFF.
  Resumo:
  Nesse seminário, vamos investigar procedimentos de decisão parcial para o problema da conseqüência restrito a sublinguagens de LP.
  (Ver resumo da Parte I - 08/06/2006)
  
  
• 03/08/2006
  "Algebrização da Lógica Proposicional - Parte VII",
  por Petrúcio Viana, IM-UFF.
  Resumo:
  Nesse seminário, vamos estabelecer uma relação funtorial entre a lógica proposicional (LP) com semântica booleana e LP com semântica de Kripke, obtendo como corolário um sistema dedutivo para LP através de Diagramas (Gerais) de Venn.
  (Ver resumo da Parte I - 08/06/2006)
  
  
• 27/07/2006
  "Algebrização da Lógica Proposicional - Parte VI",
  por Petrúcio Viana, IM-UFF.
  Resumo:
  Nesse seminário, continuamos uma análise da Lógica Proposicional (LP) de modo a salientar as propriedades básicas de LP que são essenciais para o processo de algebrização. Em particular, vamos mostrar que o fato da relação de conseqüência tautológica ser compacta nos permite definir teorias proposicionais indecidíveis.
  (Ver resumo da Parte I - 08/06/2006)
  
  
• 20/07/2006
  "On games and the polynomial-space completeness of intuitionistic propositional logic",
  por Marcelo Correa, IM-UFF.
  Resumo:
  Ladner (1977) presented purely semantical proofs (based on Kripke-Frames) of the polynomial-space completeness of the modal logics S4 and T. As Gödel's translation establishes a strong relationship between S4 and Intuitionistic Propositional Logic (IPL), it implies the polynomial-space completeness of IntTaut, the validity decision problem for IPL. Statman(1979) also proved the latter result by adopting a proof-theoretical approach. On the other hand, problems of existing a winning strategy concerning a large class of two-person games of perfect information are representatives of PSPACE-complete problems for theoretical computer scientists.
  We shall present an alternative and simpler proof of this Ladner and Statman's result by means of a reduction from the problem of existing a winning strategy in the game GEOGRAPHY to IntTaut, mixing the game and the proof-theoretical approaches. We also point out how it could be adapted to deal with the implicational fragment of IPL following rewritting techniques developed by Svejdar (2003).
  
  
• 13/07/2006
  "Algebrização da Lógica Proposicional - Parte V",
  por Petrúcio Viana, IM-UFF.
  
  
• 06/07/2006
  "Algebrização da Lógica Proposicional - Parte III",
  por Petrúcio Viana, IM-UFF.
  
  
• 29/06/2006
  "Algebrização da Lógica Proposicional - Parte III",
  por Petrúcio Viana, IM-UFF.
  
  
• 14/06/2006
  "Algebrização da Lógica Proposicional - Parte II",
  por Petrúcio Viana, IM-UFF.
  
  
• 08/06/2006
  "Algebrização da Lógica Proposicional - Parte I",
  por Petrúcio Viana, IM-UFF.
  Resumo:
  Algebrizar uma lógica L consiste em associar a L uma classe de álgebras AlgL de modo que se estabeleça uma correspondência entre as propriedades de L e as propriedades de AlgL. Deste modo, um canal se estabelece para a transferência de resultados de AlgL a L. Podemos verificar se L possui ou não certas propriedades examinando o que acontece em AlgL.
  Nesta série de seminários, exemplificamos o aspecto positivo do procedimento acima, através de seu exemplo mais representativo: a algebrização da lógica proposicional.