# Lógica

## Decidability in logic via reduction

Por Cristina Sernadas (Instituto Superior Técnico, CMAFcIO).

Abstract: Some reduction techniques are presented for proving decidability of mathematical theories and of logic problems, along with relevant illustrations.

## Type-2 computability with applications to differential equations

Por Daniel Graça (Universidade do Algarve).

## From ultrafilters to compactness

Por Pedro Filipe (Instituto Superior Técnico, Universidade de Lisboa).

Abstract: The compactness theorem is one of the key ingredients used in Lindstrom's Theorem that characterizes first-order logic and follows directly from Godel's completeness theorem, given the finite nature of proofs. In time, alternative proofs were found that don't require the usage of a formal proof system. In this seminar we will show one of these alternative proofs using ultrafilters and ultraproducts.

## Decidability of first-order theories

Por Cristina Sernadas (Instituto Superior Técnico, Universidade de Lisboa).

Abstract: Some results and reduction techniques for proving decidability of mathematical theories and completeness of logics are presented. The crucial role of the theory of real closed ordered fields is explained. Selected illustrations from Euclidean Geometry to Quantum Logic are discussed.

## One, and Only One

Por Elia Zardini (Universidade de Lisboa).

## Zigzag and Fregean arithmetic (part 2)

Por Fernando Ferreira (Universidade de Lisboa).

## Individual approach to witness hiding protocols

Por André Souto (Universidade de Lisboa).

## Zigzag and Fregean arithmetic

Por Fernando Ferreira (Universidade de Lisboa).

## On the undecidibility of type inhabitation for atomic polymorphism (part 2)

Por Clarence Protin (Independent Scholar).

Abstract: Pawel Urzyczyn has shown how to obtain a syntactic proof of the undecidability of type inhabitation for systems $F$ and $F_\omega$ by a reduction involving the codification of a certain undecidable $\forall,\rightarrow$- fragment of intutitionistic predicate calculus and the use of the Curry-Howard isomorphism. We show how this technique can be simplified and used to prove the undecidability of type inhabitation for atomic polymorphism.

## On the undecidibility of type inhabitation for atomic polymorphism

Por Clarence Protin (Independent Scholar).

Abstract: Pawel Urzyczyn has shown how to obtain a syntactic proof of the undecidability of type inhabitation for systems $F$ and $F_\omega$ by a reduction involving the codification of a certain undecidable $\forall,\rightarrow$- fragment of intutitionistic predicate calculus and the use of the Curry-Howard isomorphism. We show how this technique can be simplified and used to prove the undecidability of type inhabitation for atomic polymorphism.