Lógica da justificação

As lógicas da justificação são lógicas epistêmicas para raciocinar sobre justificação. Em algumas delas, especificamente nas desenvolvidas por Newton da Costa, dois operadores unários são adicionados à linguagem proposicional, J e J', para, respectivamente, representar as noções de justificação forte e justificação fraca. Em outras, apresentadas por Sergei Artemov , os operadores tradicionais (e.g. "□" para "necessidade" e "B" para "crença") dão lugar a uma coleção de termos, estruturas construídas para representar justificações, que se prefixam a fórmulas e dão origem a frases com a forma τ : φ (e leitura ‘τ é uma justificação para φ’).

Motivações

Os formalismos de da Costa resultam de trabalhos levados com o objetivo de modelar o conhecimento científico . Na lógica e na matemática, subscreve, obtém-se conhecimento forte, enquanto nas demais ciências obtém-se conhecimento fraco . A diferença entre conhecimento forte e fraco é que, para este, tem-se apenas uma justificação fraca, enquanto, para aquele, tem-se justificação forte. Por sua vez, uma justificação é forte quando garante à proposição que justifica o status de verdade necessária, enquanto uma justificação fraca garante à proposição apenas o status de verdade contingente .

O primeiro sistema relatado por Artemov, a Lógica das Provas LP, resulta de um programa de pesquisa interessado em fornecer uma semântica de demonstrabilidade para a lógica intuicionista. Esse sistema é adequado para raciocinar apenas sobre justificações fortes. Desde aquele momento, entretanto, muitos outros sistemas de lógica da justificação foram relatados, muitos deles motivados pelo interesse de construir quadros adequados para o raciocínio sobre justificações fracas e a análise logicamente orientada de questões de epistemologia .