| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 1.09 MB | Adobe PDF |
Authors
Abstract(s)
O objetivo da presente dissertação é definir uma interpretação funcional para a lógica clássica
em tipos finitos e, com isso, dar uma nova visão ao Teorema de Herbrand num âmbito mais geral.
Começamos por desenvolver um novo cálculo combinatório tipado chamado Cálculo de
Combinadores Estrela, que envolve tanto os bem-conhecidos tipos finitos (o tipo base e o tipo
função ou seta) como o mais recente tipo estrela. Enquanto o tipo seta representa funcionais,
o tipo estrela representa conjuntos finitos e não-vazios. Baseando-nos numa linguagem
de lógica clássica de primeira ordem com pelo menos uma constante, vamos desenvolver
uma extensão tipada desta mesma para o contexto de lógica clássica de ordem superior e
de tipos finitos. Neste sentido, cada objeto desta nova linguagem terá associado um tipo
finito. Esta nova linguagem vai herdar as constantes da linguagem da lógica de primeira
ordem, às quais acrescentamos novas constantes exclusivas da nova linguagem. Estas novas
constantes consistem nos chamados combinadores e nas chamadas constantes estrela. Por outro
lado, a nova linguagem terá igualmente símbolos primitivos adicionais como o quantificador
universal limitado, o símbolo da igualdade e o símbolo do pertence. Através da existência
de quantificadores limitados e ilimitados, definimos a classe de fórmulas base como sendo as
fórmulas sem quantificadores ilimitados. Esta classe de fórmulas surgirá em múltiplos resultados.
Uma vez a síntaxe da linguagem definida, apresentamos uma teoria adequada ao estudo do
Cálculo de Combinadores Estrela, correspondendo esta a uma extensão tipada da lógica clássica
de primeira ordem. Usamos um cálculo completo para a lógica clássica de primeira ordem
desenvolvido por Shoenfield, tal como axiomas que regem os combinadores, a igualdade, as
constantes estrela e os quantificadores limitados. É de referir que a maioria dos axiomas da
axiomática desta teoria são fechos universais de fórmulas base. Esta característica tornar-se-á
útil ao longo da dissertação. De seguida, apresentamos uma versão tipada do Axioma da Escolha
chamado Axioma da Escolha Limitado. Embora fora da axiomática original, este axioma terá
um papel fundamental no contexto da presente dissertação.
Com a sintaxe e a axiomática apresentadas, estudamos o Teorema da Completude Combinatorial
que nos permite representar certas funções através de termos da linguagem. Com estes termos,
é-nos possível introduzir a notação lambda como símbolo definido que, por sua vez, nos dá
acesso a lambda abstrações. Em poucas palavras, o Teorema da Completude Combinatorial
permite definir termos a partir dos combinadores da linguagem, termos estes que neste contexto
desempenham o papel do operador usual da substituição.
A partir deste estudo, continuamos a desenvolver o Cálculo de Combinadores Estrela analisando
as suas conversões de termos. Apresentamos as definições necessárias para podermos, entre
outros, discutir resultados relacionados com as propriedades de confluência e normalização
deste cálculo. Após concluirmos que cada termo do Cálculo de Combinadores Estrela pode ser
reduzido a uma forma normal e que esta forma normal é única, estudamos certas características
associadas à estrutura de termos normais. Para tal, definimos o conceito de termos set-like com
o objetivo de apresentarmos uma estrutura geral para termos normais e fechados.
Com os fundamentos do Cálculo de Combinadores Estrela definidos e estudados, passamos
a debruçar-nos sobre interpretações funcionais. Tendo por base a interpretação funcional de
Shoenfield, originalmente definida no âmbito da aritmética, passamos a estudar uma versão
herbrandizada da interpretação funcional de Shoenfield, desta vez no âmbito da lógica clássica
em tipos finitos o que permite traduzir a linguagem do Cálculo de Combinadores Estrela
em si mesma. A interpretação funcional é dita herbrandizada porque as testemunhas das
interpretações de fórmulas são acumuladas em conjuntos finitos. Após a apresentação do contexto necessário, focamo-nos em resultados associados a esta
interpretação, resultados estes que desvendam o papel desempenhado pelo Axioma da Escolha
Limitado no contexto da lógica clássica de ordem superior em todos os tipos finitos com o tipo
estrela. Começamos pelo Teorema da Correção. Este teorema central torna possível a extração
de informação sob forma de termos, dado o caráter construtivista da sua demonstração. É
de notar que a construção destes termos faz referência constante ao Teorema da Completude
Combinatorial no sentido em que usamos lambda abstrações para os definir.
A demonstração do Teorema da Correção requer um outro resultado: o Teorema da Monotonia.
Este último é um resultado que afirma que, tendo a interpretação de uma fórmula, a matriz da
interpretação é válida para a variável existencial da interpretação, mas também para qualquer
outra que a contenha. O Teorema da Monotonia está estritamente relacionado com o caráter
herbrandizado da interpretação funcional em questão.
Juntamente com o Teorema da Correção, torna-se pertinente estudarmos os chamados princípios
característicos da nossa interpretação funcional de Shoenfield. Estes são os princípios que,
embora figurem na hipótese do Teorema da Correção, desaparecem na conclusão. Neste sentido,
demonstramos que a versão herbrandizada da interpretação funcional de Shoenfield tem apenas
um princípio característico, nomeadamente o Axioma da Escolha Limitado. Depois de termos
demonstrado o Teorema da Correção e discutido o princípio característico da interpretação
funcional em causa, estudamos em que condições uma fórmula é equivalente à sua tradução.
O Teorema da Caracterização proporciona a resposta: uma fórmula e a sua interpretação são
sempre equivalentes na teoria associada ao Cálculo de Combinadores Estrela quando esta é
reforçada com o Axioma da Escolha Limitado.
Com base em tudo o que foi exposto anteriormente, foi possível então desenvolver um primeiro
contributo original da presente dissertação. O contributo em questão prende-se com uma
aplicação do Cálculo de Combinadores Estrela, nomeadamente uma nova generalização do bemconhecido Teorema de Herbrand. Após enunciarmos o teorema para lógica clássica de primeira
ordem, apresentamos uma série de resultados que permitem generalizar pela primeira vez o
teorema em questão no âmbito da nossa extensão da lógica clássica. O enunciado generalizado
envolve o Axioma da Escolha Limitado, axioma este que apenas fica visível quando o teorema
é enunciado em ordem superior. Após termos demonstrado a versão generalizada do Teorema
de Herbrand, apresentamos igualmente uma nova demonstração baseada num argumento
semântico, de modo a recuperar o resultado original a partir do resultado generalizado.
Com a parte matemática da dissertação concluída, fazemos incidir a nossa atenção
no segundo contributo original da presente dissertação, designadamente a formalização de
determinados resultados e noções associados ao Cálculo de Combinadores Estrela no assistente
de prova Lean. Começamos por descrever o que é um assistente de prova, juntamente com
vantagens e desvantagens do respetivo uso no âmbito da investigação matemática. De seguida,
fazemos uma breve introdução ao conceito de Proposições como Tipos (do inglês Propositions
as Types), a base de funcionamento das provas matemáticas em Lean, e apresentamos as táticas
(do inglês tactics) mais importantes para a leitura e a compreensão do código da formalização.
Após termos fornecido uma visão panorâmica do assistente de prova Lean, passamos a descrever
partes da nossa formalização original. Discutimos a formalização de conceitos básicos como os
tipos finitos, os termos e as fórmulas da linguagem, para depois apresentarmos a formalização
do enunciado e da demonstração do Teorema da Completude Combinatorial. De seguida,
prosseguimos com a apresentação da formalização da versão herbrandizada da interpretação funcional de Shoenfield. Concluímos a segunda parte da dissertação mencionando as principais
diferenças entre os enunciados matemáticos e os enunciados em Lean e explicamos como o
uso de Lean como assistente de prova permitiu detetar pequenas gralhas na escrita do texto
matemático. Como nota final, fazemos o ponto da situação no que diz respeito ao uso de
assistentes de prova pela comunidade matemática e mencionamos a importância destes no futuro
desenvolvimento desta área.
We begin by developing a new typed combinatory calculus called Star Combinary Calculus which involves both the well-known finite types and the more recent star type. With this calculus at hand we will construct a functional interpretation that translates a typed extension of classical first-order logic into itself. After having introduced the necessary context, we will prove the soundness of this interpretation together with other relevant results. We will then state and prove a new generalization of Herbrand’s Theorem that involves a bounded form of the Axiom of Choice, an axiom that only unveils itself in the theorem when it is stated in this newer context. Once the Star Combinatory Calculus is fully discussed, we lay our attention onto proof assistants, more in particular onto the proof assistant Lean. We will give a general overview of this proof assistant to then, as a final goal, provide an original formalization of some of the results associated with the Star Combinatorial Calculus in Lean.
We begin by developing a new typed combinatory calculus called Star Combinary Calculus which involves both the well-known finite types and the more recent star type. With this calculus at hand we will construct a functional interpretation that translates a typed extension of classical first-order logic into itself. After having introduced the necessary context, we will prove the soundness of this interpretation together with other relevant results. We will then state and prove a new generalization of Herbrand’s Theorem that involves a bounded form of the Axiom of Choice, an axiom that only unveils itself in the theorem when it is stated in this newer context. Once the Star Combinatory Calculus is fully discussed, we lay our attention onto proof assistants, more in particular onto the proof assistant Lean. We will give a general overview of this proof assistant to then, as a final goal, provide an original formalization of some of the results associated with the Star Combinatorial Calculus in Lean.
Description
Tese de Mestrado, Matemática, 2024, Universidade de Lisboa, Faculdade de Ciências
Keywords
Cálculo de Combinadores Estrela Interpretações funcionais Lógica de primeira ordem e lógica de ordem superior em todos os tipos finitos Teorema de Herbrand Assistente de prova Lean Teses de mestrado - 2024