A lógica limitada positiva, ou lógica contínua noutros contextos, é uma extensão da lógica de primeira ordem para acomodar estruturas métricas e normadas (completas). Ela partilha várias propriedades modelares interessantes, principalmente a existência de ultraprodutos juntamente com o teorema de Łos correspondente e resultados de saturação.
Argumentos modelares baseados em ultraprodutos normalmente procedem por contradição e bloqueiam informações quantitativas da prova. A mineração de provas de ultraprodutos na lógica limitada positiva foi tratada por Günzel e Kohlenbach, que introduziram um sistema que interpreta estruturas métricas e normadas abstratas com base na interpretação funcional monotónica. Dentro dessa estrutura, foi proposto um princípio de limitação uniforme que substitui os argumentos de ultraprodutos em várias aplicações teóricas de modelos. Além disso, um metateorema geral garante a eliminação desse princípio de limitação uniforme para produzir resultados quantitativos.
Nesta palestra, farei uma breve introdução à lógica limitada positiva em vários formatos e uma visão geral da abordagem de mineração de provas. Se o tempo permitir, também discutirei outra abordagem de Towsner para eliminar ultraprodutos na lógica de primeira ordem padrão e compararei as duas abordagens.
Apresentação por Jin Wei (TU Darmstadt).