Fellin, Giulio
[Verfasser:in];
Negri, Sara
[Verfasser:in];
Orlandelli, Eugenio
[Verfasser:in]
;
Giulio Fellin and Sara Negri and Eugenio Orlandelli
[Mitwirkende:r]
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
A constructivisation of the cut-elimination proof for sequent calculi for classical and intuitionistic infinitary logic with geometric rules - given in earlier work by the second author - is presented. This is achieved through a procedure in which the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. Additionally, a proof of Barr’s Theorem for geometric theories that uses only constructively acceptable proof-theoretical tools is obtained.