Redes de evidências

As redes de provas, inventadas pelo lógico Jean-Yves Girard em 1986 no quadro da lógica linear , são uma ferramenta de demonstração formal para essa mesma lógica (ou seja, uma alternativa aos sequentes que também são usados na lógica clássica e intuicionista ). Grosso modo, é um equivalente da dedução natural da lógica intuicionista adaptada à lógica linear. Eles diferem, no entanto, pelo caráter geométrico desta abordagem: uma prova é formada por um hipergrafo e o critério de correção pode ser expresso como uma travessia do gráfico .

Definição

Definição indutiva de redes de prova para MLL

As redes de provas podem ser definidas para diferentes fragmentos da lógica linear, primeiro nos restringimos ao fragmento multiplicativo (MLL), ou seja, apenas com os símbolos e . $\ otimes$ ${\ displaystyle \ wp}$

Definimos as redes de prova por indução :

O link do axioma não tem premissa e tem duas conclusões e $NO$ $A ^ {\ bot}$
O link de corte tem duas premissas e e nenhuma conclusão $NO$ $A ^ {\ bot}$
Os tempos de ligação tem duas premissas e e uma conclusão $NO$ $B$ $A \ otimes B$
A ligação por tem duas premissas e e uma conclusão $NO$ $B$ ${\ displaystyle A \ wp B}$

Obtemos um hipergrafo, onde os links são orientados desde suas premissas até suas conclusões. Nós notamos :

cada declaração é uma premissa de no máximo um link
qualquer afirmação é a conclusão de no máximo um link

Em seguida, ligamos para:

hipótese de rede uma declaração que não é a conclusão de qualquer link
e conclusão da rede uma declaração que não é uma premissa de qualquer conexão

O critério de correção então afirma que o sequente é demonstrável na lógica multiplicativa linear se e somente se existe uma rede correta cujas hipóteses são e cujas conclusões são . ${\ displaystyle A_ {1}, \ ldots, A_ {n} \ vdash B_ {1}, \ ldots, B_ {m}}$ ${\ displaystyle A_ {1}, \ ldots, A_ {n}}$ ${\ displaystyle B_ {1}, \ ldots, B_ {m}}$

Redes de caixa

A lógica linear restrita ao fragmento multiplicativo é relativamente inexpressiva. Uma extensão das redes de prova para MELL, ou seja, para exponenciais ( claro ) e ( por que não ), é possível, mas requer a adição da noção de caixa. Uma caixa é a generalização de uma ligação de axioma: vista de fora, uma conclusão de caixa é equivalente a um conjunto de afirmações que seriam duas a duas conseqüências de uma ligação de axioma. Dentro da caixa, colocamos qualquer sequência que tenha sido comprovada externamente. Podemos, portanto, ver as caixas como um meio de integrar nas redes de provas elementos vindos de fora, ou seja, do cálculo das sequências. $!$ $?$ ${\ displaystyle A_ {1}, \ ldots, A_ {n}}$ ${\ displaystyle A_ {1}, \ ldots, A_ {n}}$

Para integrar as exponenciais ao nosso cálculo, colocamo-nos no quadro do cálculo misto, ou seja, nos damos a possibilidade de sublinhar qualquer conclusão de ligação, denotando assim uma gestão clássica e não mais linear do enunciado:

A introdução do curso é feita colocando uma matriz de conclusão em uma caixa de conclusão ${\ displaystyle A_ {1}, \ ldots, A_ {n}, B}$ ${\ displaystyle {\ underline {A_ {1}}}, \ ldots, {\ underline {A_ {n}}},! B}$
A introdução do porque não é feita colocando um link tendo por premissas ocorrências de e para conclusão $não$ $\ underline {A}$ ${\ displaystyle? A}$

Percebemos que:

Em ambos os casos, possivelmente é zero. $não$
No caso, é claro , podemos assumir que a rede tem apenas conclusões e nenhuma premissa, mesmo que isso signifique adicionar links de axioma (uma premissa se torna uma conclusão ) $NO$ ${\ displaystyle A ^ {\ bot}}$
O elo porque não corresponde ao enfraquecimento no caso 0-ário, ao abandono no caso unário e à contração no caso n-ário para $n \ geq 1$

Quantificadores

A adição de quantificadores à primeira ordem é bastante imediata, adicionamos dois links:

O link para tudo tem como premissa uma afirmação e para conclusão onde é uma variável nova ou autovariável $NO$ ${\ displaystyle \ forall xA}$ $x$
O link existe tem uma afirmação como premissa e como conclusão . A notação então denota a substituição da variável pelo termo no enunciado . ${\ displaystyle A [t / x]}$ ${\ displaystyle \ existe xA}$ $A [t / x]$ $x$ $t$ $NO$

Aditivos

Adicionar os aditivos às redes de evidências é uma tarefa difícil se alguém tentar fazer isso na ausência de caixas. Os diversos critérios de correção propostos para redes aditivas sem caixas não são unânimes entre os especialistas da área.

Critérios de correção

Um critério de correção é um critério que permite caracterizar as redes correspondentes às provas no cálculo dos sequentes. De facto, enquanto os sequentes têm uma correcção local (seguimento das regras de cálculo consideradas) e uma eliminação dos cortes totais, as redes de provas têm uma correcção global e uma eliminação dos cortes locais.

Critério original

O critério original devido a Jean-Yves Girard é expresso em termos de viagem em uma rede: nós simulamos o caminho de uma partícula ao longo das hiper-arestas da rede.

Critério de Danos-Regnier

Introduzimos a noção de switch: um switch em uma rede de prova é uma escolha de orientação de cada link por desta rede, ou seja, consideramos que cada link por está conectado a apenas um apenas uma de suas duas premissas. Se uma rede contém links por , então há switches. $eu$ $não$ $2 ^ {n}$

O critério é então declarado como segue: Uma rede de prova é correta se e somente se estiver conectada e acíclica para qualquer escolha de switch, ou seja, se e somente se para qualquer escolha de switch, o gráfico obtido é uma árvore.

Critério para redes com caixas

O critério anterior estende-se facilmente ao caso de caixas: Uma rede de caixas está correta se as redes contidas em cada caixa estão corretas e se a rede obtida pela substituição de cada caixa por uma hiperparagem também está correta (no sentido anterior).

O processamento de exponenciais é então feito da seguinte forma:

A introdução do curso é feita com o método acima.
O link porque não pode ser considerado como uma generalização de um link por : generalizamos a noção de switch pedindo para fazer uma escolha de uma premissa para cada link porque não .

Critério para redes quantificadoras