Por Isabel Oitavem (Universidade Nova de Lisboa).

Related with investigations on simplicity of proofs, we focus on formulas of the form \phi implies \phi, adopting as framework the Pure Positive Implication Propositional Calculus based on Frege's axiomatization of implication. In this context, we search for a shortest proof of \phi implies \phi. There might be particular instances of this formula which admit proofs that are shorter than a shortest proof of \phi implies \phi in general. A first example is the case for \phi itself of the form \psi implies \psi. More examples are obtained by means of combinatory logic. This is joint work with Reinhard Kahle and Paulo Guilherme Santos.

Transmissão via Zoom.