Revisiting the proof theory of Classical S4

Bruno Lopes; Cecília Englander; Fernanda Lobo; Marcela Cruz

Capa da revista O que nos faz pensar nº 39

PDF

Published: Dec 30, 2016

Keywords:

Modal Logic, Proof Theory, Normalisation

Bruno Lopes

Instituto de Computação da Universidade Federal Fluminense

Cecília Englander

Departamento de Informática da Pontifícia Universidade Católica do Rio de Janeiro

Fernanda Lobo

Marcela Cruz

Universidade Católica San Pablo

Abstract

In 1965 Dag Prawitz presented an extension of Gentzen-type systems of Natural Deduction to modal concepts of S4. Maria da Paz Medeiros showed in 2006 that the proof of normalisation for classical S4 does not hold and proposed a new proof of normalisation for a logically equivalent system, the system NS4. However two problems in the proof of the critical lemma used by Medeiros in her proof were pointed out by Yuuki Andou in 2009. This paper presents a proof of the critical lemma, resulting in a proof of normalisation for NS4.

Issue

Vol. 25 No. 39 (2016): Philosophy, Logic and Computation

Section

Articles

Copyright Notice

The author of the article or book reviews submitted and approved for publication authorizes the editors to reproduce it and publish it in the journal O que nos faz pensar, with the terms “reproduction” and “publication” being understood in accordance with the definitions of the Creative Commons Attribution-NonCommercial 4.0 International license. The article or book reviews may be accessed both via the World Wide Web – Internet (WWW – Internet), and in printed form, its being permitted, free of charge, to consult and reproduce the text for the personal use of whoever consults it. This authorization of publication has no time limit, with the editors of the journal O que nos faz pensar being responsible for maintaining the identification of the author of the article.

Author Biographies

Bruno Lopes, Instituto de Computação da Universidade Federal Fluminense

Professor na Universidade Federal Fluminense (IC/UFF) e pesquisador no FR∀M∃ Lab. Já fui pesquisador visitante no Deduc˫eam/INRIA, com o qual desenvolvo parceria em conjunto com a Université Lyon 3 e com o TecMF/PUC-Rio. Minha principal linha de trabalho é na área de lógica para sistemas concorrentes mas também tenho trabalhado no desenvolvimento de provadores de teoremas extensíveis, normalização para sistemas de dedução natural, ontologias, formalização de sistemas multi-agentes e teoria da prova para lógicas.

Cecília Englander, Departamento de Informática da Pontifícia Universidade Católica do Rio de Janeiro

Possui graduação em Matemática pela Universidade Federal Fluminense (licenciatura e bacharelado, 2006) e mestrado e doutorado em Teoria da Computação pela Pontifícia Universidade Católica do Rio de Janeiro.

Fernanda Lobo

Possui graduação em Filosofia pela Universidade Federal do Rio de Janeiro (2006), mestrado em Lógica e Metafísica pela Universidade Federal do Rio de Janeiro (2009) e doutorado em Filosofia pela Pontifícia Universidade Católica do Rio de Janeiro (2015). Suas pesquisas enfatizam questões relacionadas às áreas de Filosofia da Lógica, Filosofia da Linguagem e Filosofia Antiga, principalmente nos seguintes temas: futuros contingentes, determinismo, bivalência, modalidades, tempo e lógicas aristotélica e estoica. Possui interesse na área de Ensino de Filosofia no nível médio.

Marcela Cruz, Universidade Católica San Pablo

Doutoranda em Informática pela Pontifícia Universidade Católica do Rio de Janeiro, mestrado em de Ciência da Computação pela Universidade Federal de Pernambuco. Possui graduação em Engenharia de Sistemas pela Universidad Nacional de San Agustín de Arequipa. Tem experiência na área de Ciência da Computação, com ênfase em Teoria da Prova, Lógica e Sistemas de Prova.