Loading...
Publication
Proof Mining: análise quantitativa de demonstrações matemáticas
| Name: | Description: | Size: | Format: | |
|---|---|---|---|---|
| 728.87 KB | Adobe PDF |
Authors
Advisor(s)
Abstract(s)
Esta dissertação foca-se em dois resultados obtidos através da utilização de ferramentas de proof mining. O programa tem como objectivo obter informação adicional de teoremas matemáticos já deduzidos utilizando ferramentas ou técnicas da lógica matemática. O intuito será obter versões quantitativas dos teoremas de convergência para a iteração implícita de Browder e explícita de Halpern para famílias de funções não expansivas (Sn) e ponto de ancora u ∈ C, onde C indica um subconjunto fechado, limitado e convexo de um espaço de Banach (Teoremas 7 e 8) obtidos por T. Suzuki em [28], onde a ferramenta crucial é a utilização de interpretações funcionais. De forma resumida, estas interpretações São aplicações que traduzem fórmulas A para fórmulas do tipo ∀x∃yAf (x, y), onde Af (x, y) é uma fórmula livre de quantificadores. Começamos por apresentar e caracterizar a linguagem formal L ω da aritmética de tipos finitos PAω e respetivos modelos standard e dos funcionais fortemente majorizáveis. Em seguida, é expresso a interpretação funcional a ser utilizada no decorrer desta tese, designada por interpretação funcional limitada e a representação formal de números reais, mais concretamente, ao nível de espaços normados, onde a teoria da aritmética de Peano em todos os tipos finitos é extendida a espaços normados (PAω,X ⊴ ). Uma prova modificada do teorema de Browder é então introduzida para mostrar como evitar argumentos de compacidade fraca sequencial através de provas modificadas. Essa subsecção ´e finalizada, introduzindo um Princípio generalizado, e a respetiva versão quantitativa, de forma a eliminar a compacidade fraca sequencial pela utilização de ferramentas de proof mining. A ultima secção é dedicada às versões quantitativas dos teoremas de convergência de Browder e Halpern, desenvolvidas por U.Kohlenbach e P.Pinto em [17].
The main focus in this master thesis is the application of proof mining tools, which is, in few words, the extraction of additional information from mathematical theorems using techniques from logic. The goal is to obtain quantitative convergence theorems from Browder’s implicit iteration and Halpern’s explicit iteration for families of nonexapnsive functions (Sn) with anchor point u ∈ C, where C states for a bounded closed convex subset of a Banach space (Theorems 7 and 8) obtained by T. Suzuki in [28], where the main tool is the employment of functional interpretations. We begin by presenting and characterizing the formal language L ω of Peano arithmetic in all finite types PAω and respective standard and strongly majorizable functionals models. Next, we introduce the functional interpretation used throughout this thesis, which is called the bounded functional interpretation. The formal representation of real numbers at the level of normed spaces, where the arithmetic for all finite types is extended to normed spaces (PAω,X ⊴ ) is displayed in the next section. The modified Browder proof is introduced to show how to avoid weak sequential compacity arguments through the usage of modified proofs. This subsection ends with a representation of a general principle, and quantitative version respectively, as a way to eliminate weak sequential compacity using proof mining tools. The final chapter is dedicated to quantitative versions of convergence theorems of Browder and Halpern, as developed by U.Kohlenbach and P.Pinto in [17].
The main focus in this master thesis is the application of proof mining tools, which is, in few words, the extraction of additional information from mathematical theorems using techniques from logic. The goal is to obtain quantitative convergence theorems from Browder’s implicit iteration and Halpern’s explicit iteration for families of nonexapnsive functions (Sn) with anchor point u ∈ C, where C states for a bounded closed convex subset of a Banach space (Theorems 7 and 8) obtained by T. Suzuki in [28], where the main tool is the employment of functional interpretations. We begin by presenting and characterizing the formal language L ω of Peano arithmetic in all finite types PAω and respective standard and strongly majorizable functionals models. Next, we introduce the functional interpretation used throughout this thesis, which is called the bounded functional interpretation. The formal representation of real numbers at the level of normed spaces, where the arithmetic for all finite types is extended to normed spaces (PAω,X ⊴ ) is displayed in the next section. The modified Browder proof is introduced to show how to avoid weak sequential compacity arguments through the usage of modified proofs. This subsection ends with a representation of a general principle, and quantitative version respectively, as a way to eliminate weak sequential compacity using proof mining tools. The final chapter is dedicated to quantitative versions of convergence theorems of Browder and Halpern, as developed by U.Kohlenbach and P.Pinto in [17].
Description
Keywords
Teoremas Análise quantitativa Proof mining Matemática Theorem Mathematics
Citation
Fino, António Miguel Dias - Proof Mining [Em linha]: análise quantitativa de demonstrações matemáticas. [S.l.]: [s.n.], 2023. 63 p.