Portal de Periódicos da CAPES

The FAN principle and weak König's lemma in herbrandized second-order arithmetic

2020; Elsevier BV; Volume: 171; Issue: 9 Linguagem: Inglês

10.1016/j.apal.2020.102843

1873-2461

Fernando Ferreira,

Logic, programming, and type systems

We introduce a herbrandized functional interpretation of a first-order semi-intuitionistic extension of Heyting Arithmetic and study its main properties. We then extend the interpretation to a certain system of second-order arithmetic which includes a (classically false) formulation of the FAN principle and weak König's lemma. It is shown that any first-order formula provable in this system is classically true. It is perhaps worthy of note that, in our interpretation, second-order variables are interpreted by finite sets of natural numbers.