Cálculos de múltipla conclusão para a lógica intuicionista sob uma perspectiva geométrica
| Autor: | CARVALHO, Ruan Vasconcelos Bezerra |
|---|---|
| Přispěvatelé: | OLIVEIRA, Anjolina Grisi de |
| Jazyk: | portugalština |
| Rok vydání: | 2017 |
| Předmět: | |
| Zdroj: | Repositório Institucional da UFPE Universidade Federal de Pernambuco (UFPE) instacron:UFPE |
| Popis: | Como verificar se uma prova clássica também é intuicionista? Em dedução natural basta não haver ocorrência da lei do terceiro excluído ou da eliminação da dupla negação, conforme proposto por Gentzen. No seu cálculo de sequentes o mesmo resultado é alcançado restringindo o número de fórmulas no lado direito a no máximo um. Assim não há múltiplaconclusão, embora esta seja importante para a simetria. Hoje já existem abordagens que levam isso em conta e propõem cálculos de sequentes para lógica intuicionista com várias fórmulas no consequente. Mas ainda que elas nos forneçam compreensões do que diferencia a lógica intuicionista da clássica, há o problema da burocracia inerente ao formalismo de Gentzen. Aqui separamos a lógica intuicionista da clássica em derivações não-sequenciais adotando uma abordagem geométrica. Propomos uma versão intuicionista para dois sistemas de múltipla conclusão inicialmente definidos apenas para a lógica clássica proposicional: os N-Grafos, apresentados por de Oliveira (2001) e baseado em dedução natural; e as proof-nets de Robinson (2003), inspiradas no cálculo de sequentes. How to verify if a classical proof is also intuitionistic? Gentzen’s natural deduction only requires no occurrence of the law of the excluded middle or the elimination of double negation rule in an intuitionistic derivation. His sequent calculus achieves the same result by restricting the number of formulas on the right-hand side to at most one, which removes its multiple-conclusion feature that is important for the calculus’ symmetry. There are approaches today that take this into account and present solutions for multipleconclusion sequent calculi for intuitionistic logic, but while giving us some useful insights on what constitutes an intuitionistic system, they inherit the bureaucracy from Gentzen’s formalism. Here we separate intuitionistic logic from classical in non-sequential derivations by adopting a geometric perspective in our approach. We propose an intuitionistic version for two multiple-conclusion systems initially defined for propositional classical logic: NGraphs, which was presented by de Oliveira (2001) as a symmetric natural deduction; and Robinson’s proof-nets (2003), that were inspired in sequent calculus. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|