Seminário de Lógica Matemática

Modified realizability and functional interpretations: some logical and mathematical observations

Sala 6.2.33, FCUL, Lisboa

Fernando Ferreira
CMAF-CIO / Faculdade de Ciências da Universidade de Lisboa

Abstract: We review some basic and well-known facts about the possibility of extracting computational information from proofs in classical, intuitionistic and semi-intuitionistic systems. Intuitionistic reasoning is tailored to have a clear constructive content and Kleene’s (numerical) realizability was a way of establishing precisely what this means for intuitionistic proofs in arithmetic. We review the variant of modified realizability due to Kreisel and see it as a form of a functional interpretation. An emphasis throughout is on the fact that there are some semi-intuitionistic principles which are amenable to computational extraction. Even Kreisel’s modified realizability displays not only the constructive content of intuitionistic logic but goes a bit further since it also realizes a certain (non-intuitionistic) principle of independence of premises. This principle is a characteristic principle of modified realizability. We explain what are these characteristic principles and compare them with so-called side principles, which are also amenable to computational extraction.

Markov’s principle is a characteristic principle of Gödel’s functional dialectica interpretation. We review the dialectica interpretation and also analyze Markov’s principle via the so-called Friedman’s trick. We make a short comparison between both treatments of Markov’s principle. We introduce a new interpretation (the H-interpretation: H for herbrandized) and see that LLPO (the lesser limited principle of omniscience) is one of its characteristic principles. The extraction of computational information now takes the form of bounds, not of precise witnesses. We discuss this issue and a monotonicity condition now so central in several recently defined functional interpretations. Finally, we extend the H-interpretation to the second-order arithmetical setting in such a way that WKL (weak König’s lemma) turns out to be a characteristic principle.

Some open questions and some projects will be discussed during the talk.

This seminar is supported by National Funding from FCT - Fundação para a Ciência e a Tecnologia, under the project: UID/MAT/04561/2013.

15h00
CMAF-CIO - Centro de Matemática, Aplicações Fundamentais e Investigação Operacional
Microplásticos no ocerano

O curso procura dar formação sobre a problemática da contaminação por detritos de plástico dos nossos ecossistemas, bem como alertar para os potenciais efeitos deletérios nos organismos, utilizando uma abordagem de ensino científico, com um discurso adequado a formandos sem formação científica - candidaturas até 03 de agosto.

Logótipo do evento, sobre fotografia dos Açores

Um simpósio internacional que reúne investigadores especializados em várias disciplinas (taxonomia, ecologia da vegetação, biogeografia, filogeografia, paleoecologia ou conservação da biodiversidade), focados na flora e vegetação terrestre e marinha da região da Macaronésia (Açores, Madeira, Selvagens, Canárias e Cabo Verde).

Composição de imagens relativas à área das ciências forenses

O curso visa dotar os formandos com os conhecimento necessários à integração de equipas profissionais multidisciplinares nas áreas Médico-Legais e Forenses, em Laboratórios ou Serviços Médico-Legais e Forenses - candidaturas até 27 de julho.

Cientista a trabalhar com tubos de ensaio

Os participantes neste curso irão adquirir os conhecimentos essenciais à integração de equipas profissionais multidisciplinares na área das Análises Clínicas/Patologia Clínica, em laboratórios privados, públicos, hospitalares ou do Estado - candidaturas até 27 de julho.

Logótipo do evento

Physics Day é um evento promovido pelo Departamento de Física da Faculdade de Ciências da ULisboa, com um duplo objetivo: valorizar a diversidade e excelência da formação dos doutorados e promover um espaço de diálogo direto entre empresas e estudantes.

Saída de campo (Geologia)

O curso, com candidaturas até 20 de julho, convida os professores do Ensino Básico e Secundário a explorar a Geologia a partir das rochas que afloram nas imediações da sua escola.

Gotas de água

O curso visa capacitar os formandos para a aplicação dos índices de qualidade ecológica utilizados na avaliação da qualidade ambiental em sistemas de transição, no âmbito da Diretiva Quadro da Água (DQA) - candidaturas até 31 de agosto.

Composição de três imagens relativas à área da deteção remota

2.ª edição do curso, com candidaturas até 18 de outubro.

A conferência visa reunir os principais especialistas no domínio da Imagiologia Médica por Micro-ondas (MMWI) e incluirá palestras, apresentações e pósteres de resumos revistos por pares e artigos de conferências, bem como workshops em áreas satélite de investigação com interesse para a investigação em MMWI.

Páginas