LEI.tex

\calculusName{Logic of Epistemic Inconsistency}
\calculusAcronym{LEI}
\calculusLogic{Paraconsistent Logics}
\calculusLogicOrder{First-Order}
\calculusType{Natural Deduction}
\calculusYear{1993}

\calculusAuthor{Ana Teresa Martins}
\calculusAuthor{Lilia Ramalho Martins}
\calculusAuthor{Felipe Ferreira de Morais}


\entryTitle{Logic of Epistemic Inconsistency}
\entryAuthor{Ana Teresa Martins}     
\entryAuthor{Francicleber Ferreira}


\maketitle

\begin{entry}{LEI}  

\begin{calculus}

\[
\begin{array}{ccccccccccccccc}

  
  \infer[!I]{\alpha !}{\deduce{\alpha}{\Pi}}
  
  &
  \quad
  &
  
  \infer[!E]{\alpha}{\alpha !}
  
  &
  \quad
  &
  
  \infer[?I]{\alpha ?}{\alpha}
  
  &
  \quad
  &
  
  \infer[?E]{\beta}{\alpha ? & \deduce{\beta}{\deduce{\Pi}{[\alpha]}}}
  
  &
  \quad
  &
  
  \infer[\neg I]{\neg \alpha}{\infer*{\bot}{[\alpha]}}
  
  
  

\\
\\
  

  
  \infer[\neg E]{\bot}{A & \neg A}
  
  &
  \quad
  &
  
  \infer[\neg ? I]{\neg(\alpha ?)}{(\neg\alpha) ?}
  
  &
  \quad
  &
  
  \infer[\neg ? E]{(\neg\alpha) ?}{\neg (\alpha ?)}
  
%  \infer[\sim I]{\sim \alpha}{\infer*{\bot}{[\alpha]}}
%  
%  &
%  \quad
%  &
%  
%  \infer[\sim E]{\bot}{\alpha & \sim \alpha}
%  
  &
  \quad
  &
  
  \infer[\bot\sim]{\alpha}{\infer*{\bot}{[\sim\alpha]}}
  
  &
  \quad
  &
  
  \infer[\bot\neg]{\alpha}{\infer*{\bot}{[\neg\alpha]}}
  
 
  
  \\
  \\
  
  
  \infer[\neg\land I]{\neg(\alpha\land\beta)}{\neg\alpha \lor \neg\beta}

  &
  \quad
  &
  
  \infer[\neg\land E]{\neg\alpha \land \neg\beta}{\neg(\alpha \lor \beta)}

  
  &
  \quad
  &
  
  \infer[\neg\lor I]{\neg(\alpha \lor \beta)}{\neg\alpha \land \neg\beta}
  
  &
  \quad
  &
  
  \infer[\neg\lor E]{\neg\alpha \lor \neg\beta}{\neg(\alpha\land\beta)}
  

  &
  \quad
  &
  
  \infer[\neg\neg I]{\neg\neg \alpha}{\alpha}
  
  
  
  \\
  \\
  
  
  \infer[\neg\neg E]{\alpha}{\neg\neg \alpha}
  
  &
  \quad
  &
  
  \infer[\neg\forall I]{\neg\forall x \alpha}{\exists x \neg\alpha}
  
  &
  \quad
  &
  
  \infer[\neg\forall E]{\exists x \neg\alpha}{\neg\forall x \alpha}
  
  &
  \quad
  &
  
  
  \infer[\neg\exists I]{\neg\exists x \alpha}{\forall x \neg\alpha}
  
  &
  \quad
  &
  
  \infer[\neg\exists E]{\neg\forall x \alpha}{\exists x \neg\alpha}
  
  \\
  \\
  
  
  %\infer[\neg\neg E]{\alpha}{\neg\neg \alpha}
  
  &
  \quad
  &
  
  \infer[\neg\to I]{\neg(\alpha \to \beta)}{\alpha \land \neg\beta}
  
  &
  \quad
  &
  
  %\infer[\neg\forall E]{\exists x \neg\alpha}{\neg\forall x \alpha}
  
  &
  \quad
  &
  
  
  \infer[\neg\to E]{\alpha \land \neg\beta}{\neg(\alpha \to \beta)}
  
  &
  \quad
  &
  
  %\infer[\neg\exists E]{\neg\forall x \alpha}{\exists x \neg\alpha}
 % 
%  \\
%  \\
%  
%  \infer[\neg ? I]{\neg(\alpha ?)}{(\neg\alpha) ?}
%  
%  &
%  \quad
%  &
%  
%  \infer[\neg ? E]{(\neg\alpha) ?}{\neg (\alpha ?)}
  
  \end{array}
\]
\vspace{-1em}

\end{calculus}


\begin{clarifications}
  The syntax of LEI is given by the following BNF rule
  \begin{center} 
    \begin{math}
      %\begin{array}{lll}
        \phi ::= p \in Atomic \mid \bot \mid \phi \land \phi 
                 \mid \phi \lor \phi \mid \phi \rightarrow \phi 
                 \mid \neg \phi \mid \sim \phi \mid \exists x\phi 
                 \mid \forall x\phi.
      %\end{array}
    \end{math}
  \end{center}
  
  LEI is intended to deal with the concept of plausibility. The $?$ and $!$
  post-fixed operators symbolize credulous and skeptical plausibility. The
  skeptical plausibility can be defined as the dual of $?$, that is $\alpha ! :=
  \sim ((\sim \alpha)?)$ LEI is a paraconsistent logic. It has two negation
  symbols $\sim$ (the classical negation) and $\neg$ (the paraconsistent
  negation). The $\sim$ can be defined as $\sim \alpha := \alpha \to \bot$. The
  intuitionistic absurd rule $\neg E$ is restricted to $?$-free formulas, which
  are represented by Roman capital letters. Introduction and elimination rules for
  $\land$, $\lor$, $\to$, $\forall$ and $\exists$ are the usual ones. The $?E$ and
  $!I$ rule has a quite involved restriction for its application. We need the
  following definitions.
  
  %\begin{definition} [Connection]
  By a \emph{connection} in a deduction $\Pi$ between two formula occurrences
  $\alpha$ and $\beta$, we understand a sequence $\alpha_{1},\ldots,\alpha_{n}$ of
  formula occurrences in $\Pi$ such that $\alpha_{1}=\alpha, \alpha_{n}=\beta$,
  and one of the following conditions holds for each $i \leq n$:

  \begin{enumerate}
  
  \item
   $\alpha_{i}$ is not the major premise of an application of $\vee E$, 
  $\exists E$ and
  $?E$, and $\alpha_{i+1}$ stands immediately below $\alpha_{i}$; or vice 
  versa;
  
  \item 
  $\alpha_{i}$ is a premise of an application of $\rightarrow E$, $\neg E$ or
  $\sim E$, and $\alpha_{i+1}$ is side connected with  $\alpha_{i}$;
  
  \item 
  $\alpha_{i}$ is  the major premise of an application of $\vee E$, $\exists E$ and
  $?E$, and $\alpha_{i+1}$ is a hypothesis discharged by this application;  or 
  vice versa;
  
  \item 
  $\alpha_{i}$ is a consequence of an application of $\rightarrow I$, 
  $\neg I$, $\sim I$,
  $\bot\neg$, $\bot\!\!\sim$, and $\alpha_{i+1}$ is a hypothesis discharged by 
  this application;
   or vice versa;
  \end{enumerate}
%\end{definition}

  Two formula occurrences $\alpha$ and $\beta$  are said to be \emph{modally
  independent} in a deduction $\Pi$ iff every connection in $\Pi$ between $\alpha$
  and $\beta$ contains an occurrence of a ?-closed formula.
  
  The $?E$ can only be applied when each occurrence of $\alpha$ is modally
  independent in $\Pi$ from $\beta$ and any (open) assumption of $\Pi$. The $!I$
  requires that $\alpha$ is modally independent from any (open) assumption of
  $\Pi$.
\end{clarifications}

\begin{history}
  The Logic of Epistemic Inconsistency was proposed by Pequeno and
  Buchsbaum~\cite{pequeno1991}. The natural deduction system for LEI was created
  by Martins and Pequeno~\cite{martins1993}.
\end{history}

\begin{technicalities}
  Completeness and correctness for LEI has been proved in~\cite{martins1997}.
  Normalization for the system above has been proved in~\cite{martins2007}.
\end{technicalities}

\end{entry}