A matemática tem muitos símbolos. Alguns podem dizer muitos símbolos. Então, vamos fazer algumas contas com fotos.
Vamos ter um papel, no qual iremos desenhar. Para começar, o papel está vazio, diremos que é equivalente a ou .
Se escrevermos outras coisas no papel, elas também serão verdadeiras.
Por exemplo
Indica que as reivindicações e são verdadeiras.Q
Agora, digamos que, se desenharmos um círculo em torno de alguma afirmação, essa afirmação é falsa. Isso representa não lógico.
Por exemplo:
Indica que é falso e é verdadeiro.Q
Podemos até colocar o círculo em torno de várias sub-declarações:
Como a parte dentro do círculo costuma ser lida como , colocando um círculo ao redor, significa . Podemos até aninhar círculosnão ( P e Q )
É exibido como .
Se desenharmos um círculo sem nada, isso representa ou . falso
Como o espaço vazio era verdadeiro, a negação do verdadeiro é falsa.
Agora, usando esse método visual simples, podemos realmente representar qualquer afirmação na lógica proposicional.
Provas
O próximo passo depois de poder representar declarações é poder prová-las. Para provas, temos 4 regras diferentes que podem ser usadas para transformar um gráfico. Começamos sempre com uma folha vazia que, como sabemos, é uma verdade vazia e, em seguida, usamos essas regras diferentes para transformar nossa folha de papel vazia em um teorema.
Nossa primeira regra de inferência é Inserção .
Inserção
Vamos chamar o número de negações entre um subgráfico e o nível superior de "profundidade". A inserção nos permite introduzir qualquer declaração que desejamos em uma profundidade ímpar.
Aqui está um exemplo de como realizamos a inserção:
Erasure
A próxima regra de inferência é Erasure . O apagamento nos diz que, se tivermos uma declaração em uma profundidade uniforme, podemos removê-la completamente.
Aqui está um exemplo de apagamento sendo aplicado:
Double Cut
Double Cut é uma equivalência. O que significa que, diferentemente das inferências anteriores, ele também pode ser revertido. O Double Cut nos diz que podemos desenhar dois círculos em torno de qualquer subgrafo e, se houver dois círculos em torno de um subgrafo, podemos remover os dois.
Aqui está um exemplo do Double Cut sendo usado
Iteração
A iteração também é uma equivalência. 1 O contrário é chamado Deiteração. Se temos uma declaração e um corte no mesmo nível, podemos copiá-la dentro de um corte.
Por exemplo:
A deiteração nos permite reverter uma iteração . Uma instrução pode ser removida por meio da Deiteração se existir uma cópia dela no próximo nível.
Esse formato de representação e prova não é de minha própria invenção. Eles são uma pequena modificação de uma lógica diagramática, denominados Gráficos Existenciais Alfa . Se você quiser ler mais sobre isso, não há muita literatura, mas o artigo vinculado é um bom começo.
Tarefa
Sua tarefa será provar o seguinte teorema:
Isso, quando traduzido para a simbolização lógica tradicional, é
.
Também conhecido como Axioma Łukasiewicz-Tarski .
Pode parecer envolvido, mas os gráficos existenciais são muito eficientes no que diz respeito ao tamanho da prova. Selecionei esse teorema porque acho que é um comprimento apropriado para um quebra-cabeça divertido e desafiador. Se você está tendo problemas com este, eu recomendaria tentar alguns teoremas mais básicos primeiro para entender o sistema. Uma lista desses pode ser encontrada na parte inferior da postagem.
Isso é prova de golfe, portanto sua pontuação será o número total de etapas da prova do início ao fim. O objetivo é minimizar sua pontuação.
Formato
O formato deste desafio é flexível. Você pode enviar respostas em qualquer formato claramente legível, incluindo formatos desenhados à mão ou renderizados. No entanto, para maior clareza, sugiro o seguinte formato simples:
Representamos um corte entre parênteses, o que quer que estejamos cortando é colocado dentro dos parênteses. O corte vazio seria apenas
()
por exemplo.Representamos átomos apenas com suas letras.
Como exemplo, aqui está a declaração de objetivo neste formato:
(((A((B(A))))(((((C)((D((E)))))(((C((D(F))))(((E(D))((E(F))))))))(G))))((H(G))))
Esse formato é bom porque é legível por humanos e por máquinas, portanto, incluí-lo em sua postagem seria bom.
Quanto ao seu trabalho real, recomendo lápis e papel ao trabalhar. Acho que o texto não é tão intuitivo quanto o papel quando se trata de gráficos existenciais.
Prova de exemplo
Nesta prova de exemplo, provaremos o seguinte teorema:
Prova:
Teoremas da Prática
Aqui estão alguns teoremas simples que você pode usar para praticar o sistema:
Segundo Axioma de Łukasiewicz
Axioma de Meredith
1: A maioria das fontes usa uma versão mais sofisticada e poderosa da iteração , mas, para manter esse desafio simples, estou usando esta versão. Eles são funcionalmente equivalentes.
fonte
Respostas:
19 passos
(())
[corte duplo](AB()(((G))))
[inserção](AB(A)(((G))))
[iteração](((AB(A)))(((G))))
[corte duplo](((AB(A))(((G))))(((G))))
[iteração](((AB(A))(((G))))((H(G))))
[inserção](((AB(A))(((G)(()))))((H(G))))
[corte duplo](((AB(A))(((DE()(C)(F))(G))))((H(G))))
[inserção](((AB(A))(((DE(C)(DE(C))(F))(G))))((H(G))))
[iteração](((AB(A))(((DE(CD(F))(DE(C))(F))(G))))((H(G))))
[iteração](((AB(A))(((E(CD(F))(DE(C))(F)((D)))(G))))((H(G))))
[corte duplo](((AB(A))(((E(CD(F))(DE(C))(E(D))(F))(G))))((H(G))))
[iteração](((AB(A))(((G)((CD(F))(DE(C))(E(D))((E(F)))))))((H(G))))
[corte duplo](((AB(A))(((G)((CD(F))(DE(C))(((E(D))((E(F)))))))))((H(G))))
[corte duplo](((AB(A))(((G)((C((D(F))))(DE(C))(((E(D))((E(F)))))))))((H(G))))
[corte duplo](((AB(A))(((G)((DE(C))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[corte duplo](((AB(A))(((G)((D(C)((E)))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[corte duplo](((AB(A))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[corte duplo](((A((B(A))))(((G)(((C)((D((E)))))(((C((D(F))))(((E(D))((E(F)))))))))))((H(G))))
[corte duplo]Teoremas da prática
Segundo axioma de Łukasiewicz: 7 passos
(())
[corte duplo](A()(B)(C))
[inserção](A(A(B))(B)(C))
[iteração](A(AB(C))(A(B))(C))
[iteração]((AB(C))(A(B))((A(C))))
[corte duplo]((AB(C))(((A(B))((A(C))))))
[corte duplo]((A((B(C))))(((A(B))((A(C))))))
[corte duplo]Axioma de Meredith: 11 passos
(())
[corte duplo](()(D(A)(E)))
[inserção]((D(A)(E))((D(A)(E))))
[iteração]((D(A)(E))((D(A)(E(A)))))
[iteração]((D(A)(E))(((E(A))((D(A))))))
[corte duplo](((E)((D(A))))(((E(A))((D(A))))))
[corte duplo](((E)((C)(D(A))))(((E(A))((D(A))))))
[inserção](((E)((C)(D(A)(C))))(((E(A))((D(A))))))
[iteração](((E)((C)((A)(C)((D)))))(((E(A))((D(A))))))
[corte duplo](((E)((C)((A)(((C)((D)))))))(((E(A))((D(A))))))
[corte duplo](((E)((C)((A(B))(((C)((D)))))))(((E(A))((D(A))))))
[inserção]Pesquisador à prova de Haskell
(O que você achou que eu faria isso manualmente? :-P)
Isso apenas tenta inserção, introdução de corte duplo e iteração. Portanto, ainda é possível que essas soluções possam ser vencidas usando apagamento, eliminação de corte duplo ou deiteração.
fonte
22 Passos
(((())(())))
(((AB())(CDE(F)()))H(G))
(((AB(A))(CDE(F)(CD(F)))(G))H(G))
(((A((B(A))))(((((C))DE(F)(C((D(F)))))(G))))((H(G))))
(((A((B(A))))(((((C)DE)DE(F)(C((D(F)))))(G))))((H(G))))
(((A((B(A))))(((((C)((D((E)))))((((((D))E(F)))(C((D(F)))))))(G))))((H(G))))
(((A((B(A))))(((((C)((D((E)))))((((((D)E)E(F)))(C((D(F)))))))(G))))((H(G))))
(((A((B(A))))(((((C)((D((E)))))((((((D)E)((E(F)))))(C((D(F)))))(G))))))((H(G))))
Algumas coisas que aprendi ao concluir este quebra-cabeça:
Reduza a representação fornecida. Isso envolve a reversão de cortes e iterações duplos. Por exemplo, esse axioma reduz para
(((AB(A))(((C)DE)(CD(F))(E(D))(E(F)))(G))H(G))
depois de reverter cortes duplos e(((AB(A))(()CDE(F)))H(G)))
depois de reverter iterações.Procure átomos dispersos. Por exemplo, H é usado como uma variável dummy e, portanto, pode ser inserido em qualquer ponto.
Soluções para Teoremas da Prática:
Solução para o segundo axioma de Łukasiewicz: [8 etapas]
(())
(()AB(C))
((AB(C))AB(C))
((A((B(C))))A((B))(C))
((A((B(C))))A(A(B))(C))
((A((B(C))))(((A(B))((A(C))))))
Solução para o axioma de Meredith: [12 etapas]
(())
(()(A)D(E))
(((A)D(E))(A)D(E(A)))
(((((A)D))(E))(A)D(E(A)))
(((((A(B))D)(C))(E))(A)D(E(A)))
(((((A(B))(C)D)(C))(E))(A)D(E(A)))
(((((A(B))(((C)((D)))))(C))(E))(((((A)D))(E(A)))))
fonte
\$
como início / fim, o que acho que tornaria sua solução muito mais fácil de ler. Espero que você tenha um bom tempo aqui :)