# Lógica intermediária

Na lógica matemática, a lógica superintuicionista é a lógica proposicional estendendo a lógica intuicionista. Lógica clássica é a lógica superintuicionista consistente mais forte; assim, a lógica superintuicionista consistente é chamada de lógica intermediária (a lógica é intermediária entre lógica intuicionista e a lógica clássica).

## Definição

A lógica superintuicionista é um conjunto L de fórmulas proposicionais sobre um conjunto contável de variáveis p$_i$ satisfazendo as seguintes propriedades:
    1. todos axiomas da lógica intuicionista pertence a L;
    2. se F e G são fórmulas tal que F e F → G pertencem a L, logo G também pertence a L (fechado sob modus ponens);
    3. se F(11p11$_1$, p$_2$, ..., p$_n$) é a fórmula de L, e G$_1$, G$_2$, ..., G$_n$ são fórmulas quaisquer, então F(G$_1$, G$_2$, ..., G$_n$) pertence a L (fechado sob substituição).
Essa fórmula será intermediária se além disso
    4. L não for o conjunto de todas as fórmulas.

## Propriedades e exemplos

Existe um contínuo de diferentes lógicas intermediárias. Lógicas intermediárias específicas são muitas vezes construídas por adição de um ou mais axiomas à lógica intuicionista, ou por uma descrição semântica. Exemplos de lógica intermediária incluem:
* lógica intuicionista(IPC, Int, IL, H)
* lógica clássica (CPC, Cl, CL): IPC + p ∨ ¬p = IPC + ¬¬p → p = IPC + ((p → q) → p) → p
* a lógica da lei do terceiro excluído (KC, lógica de Jankov, lógica de De Morgan): IPC + ¬¬p ∨ ¬p
* lógica de Gödel–Dummett (LC, G): IPC + (p → q) ∨ (q → p)
* lógica de Kreisel–Putnam(KP): IPC + (¬p → (q ∨ r)) → ((¬p → q) ∨ (¬p → r))
* lógica de problemas finitos de Medvedev (LM, ML): definido semanticamente como a lógica de todas estruturas da forma $\langle {\mathcal {P}}(X)\setminus \{X\},\subseteq \rangle$ para conjuntos finitos X ("Booleano 'hypercubes' sem topo"), Desde 2010 não conhecida por ser recursivamente axiomatizada.
* lógica da realizabilidade
* lógica de Scott (SL): IPC + ((¬¬p → p) → (p ∨ ¬p)) → (¬¬p ∨ ¬p)
* lógica de Smetanich (SmL): IPC + (¬q → p) → (((p → q) → p) → p)
* lógica da cardinalidade limitada (BC$_n$): $\textstyle \mathbf {IPC} +\bigvee _{i=0}^{n}{\bigl\bigwedge _{j<i}p_{j}\to p_{i}{\bigr )}$
* lógica da largura limitada, também conhecida como a delimitada 'anti-cadeias' (BW$_n$, BA$_n$): $\textstyle \mathbf {IPC} +\bigvee _{i=0}^{n}{\bigl\bigwedge _{j\neq i}p_{j}\to p_{i}{\bigr )}$
* lógica de profundidade limitada (BD$_n$): IPC + p$_n$ ∨ (p$_n$ → (p$_{n−1}$ ∨ (p$_{n−1}$ → ... → (p$_2$ ∨ (p$_2$ → (p$_1$ ∨ ¬p$_1$)))...)))
* lógica de largura superior limitada BTW$_n$): $\textstyle \mathbf {IPC} +\bigvee _{i=0}^{n}{\bigl\bigwedge _{j<i}p_{j}\to \neg \neg p_{i}{\bigr )}$
* lógica de ramificação limitada (T$_n$, BB$_n$): $\textstyle \mathbf {IPC} +\bigwedge _{i=0}^{n}{\bigl{\biglp_{i}\to \bigvee _{j\neq i}p_{j}{\bigr )}\to \bigvee _{j\neq i}p_{j}{\bigr )}\to \bigvee _{i=0}^{n}p_{i}$
* lógica n-valorada de Gödel(G$_n$): LC + BC$_{n−1}$ = LC + BD$_{n−1}$
Lógica superintuicionista ou intermediária formam um reticulado completo com lógica intuicionista como a bottom e a lógica inconsistente (no caso de lógica super-intuicionista) ou lógica clássica (no caso de lógica intermediária) como o topo. Lógica clássica é co-átomo na grade da lógica superintuicionista; o reticulado das lógica intermediárias também tem um único co-átomo, denominado SmL.
As ferramentas para estudo da lógica intermediária são similares aos usados para a lógica intuicionista, tal como a semântica de Kripke. Por exemplo, lógica de Gödel–Dummett tem uma caracterização semântica simples em termos de ordem total.

## Semânticas

Dada a álgebra de Heyting H, o conjunto de fórmulas proposicionais que são válidas em H é uma lógica intermediária. Por outro lado, dada a lógica intermediária é possível a construção da álgebra de Lindenbaum que é uma álgebra de Heyting.
Uma estrutura Kripke intuicionista F é o conjunto parcialmente ordenado, e o modelo Kripke M é a estrutura de Kripke com valoração tal qual $\{x\mid M,x\Vdash p\}$ é um segmento inicial de F. O conjunto de fórmulas proposicional que são válidos em F são lógica intermediária. Dada a lógica intermediária L é possível construir um modelo Kripke M tal qual a lógica de M é L (essa construção é chamada modelo canônico). A estrutura de Kripke com essa propriedade pode não existir, mas uma estrutura geral sempre existe.

## Relação com lógicas modais

Seja A uma fórmula proposicional. A tradução de Gödel–Tarski de A é definida recursivamente como:
* $T(p_{n})=\Box p_{n}$
* $T(\neg A)=\Box \neg T(A)$
* $T(A\land B)=T(A)\land T(B)$
* $T(A\vee B)=T(A)\vee T(B)$
* $T(A\to B)=\Box (T(A)\to T(B))$
Se M é a Lógica_modal estendendo a S4 então ρM = {A | T(A) ∈ M} é uma lógica super-intuicionista, e M é chamada de acompanhamento modal' de ρM. Em particular:
* IPC = ρS4
* KC = ρS4.2
* LC = ρS4.3
* CPC = ρS5
Para cada lógica intermediária L existem várias lógicas modais M tal qual L = ρM.