Wiki DAINF - Contribuições do usuário [pt-br]

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:37:58Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

== Motivação ==

O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

== O Método ==

Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

== Regras de Inferência ==

Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

=== Regras de Inferência Diretas ===

Exemplos:

[[Imagem:Regras.jpeg]]

=== Regras de Inferência Hipotéticas ===

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

==== Regra de Prova Condicional (RPC)====

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

==== Regra de Redução ao Absurdo (RAA)====

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

==== O uso adequado das Regras de Inferência Hipotéticas ====

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

=== Regras Derivadas ===

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

== Definições ==

'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

== Teoremas ==

Semanticamente, na conseqüência lógica, existe um tipo especial de fórmula, as fórmulas válidas, que são aquelas verdadeiras em toda e qualquer estrutura. Alternativamente, elas podem ser definidas como aquelas fórmulas que são conseqüência lógica de um conjunto vazio de premissas.

Caracterizando conseqüência lógica de uma maneira sintática, como feito em dedução natural, obtêm-se algo similar: os teoremas.

'''Definição 3:''' Uma fórmula <math>\alpha</math> é um teorema (do CQC) se há uma dedução de <math>\alpha</math> a partir do conjunto vazio de premissas.

Assim, <math>\alpha</math> é um teorema do CQC se e somente se <math>\oslash</math>├ <math>\alpha</math>, o que se abrevia escrevendo simplesmente ├ <math>\alpha</math>.

== Conseqüência sintática e conseqüência semântica ==

A definição semântica de conseqüência afirma que uma fórmula <math>\alpha</math> é conseqüência lógica (semântica) de um conjunto <math>\Gamma</math> de fórmulas se toda estrutura que for modelo de <math>\Gamma</math> é um modelo de <math>\alpha</math>, o que se indica por <math>\Gamma</math>╞ <math>\alpha</math>.

Já sintaticamente, um argumento é válido se sua conclusão puder ser produzida a partir das premissas por meio da aplicação de certas regras de inferência (dedução 2).

Tendo definidas as duas noções de conseqüência, pode-se mostrar que, no CQC, as duas noções coincidem. Isto é, <math>\alpha</math> é uma conseqüência sintática de <math>\Gamma</math> se e somente se <math>\alpha</math> é uma conseqüência semântica de <math>\Gamma</math>, o que vale dizer que o método de dedução natural é um sistema de prova correto e completo para o CQC. Correto porque se uma conclusão pode ser deduzida de um conjunto <math>\Gamma</math> de premissa, então ela de fato é conseqüência lógica de <math>\Gamma</math>. E completo porque, se uma fórmula é conseqüência lógica de um conjunto de premissas, há uma dedução demonstrando isso. Isso tudo é sintetizado no seguinte teorema (Teorema de Correção e Completude), onde <math>\Gamma</math> é um conjunto qualquer de fórmulas:

<math>\Gamma</math> ├ <math>\alpha</math> se e somente se <math>\Gamma</math>╞ <math>\alpha</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:36:48Z

Lihkluppel: /* Regras de Inferência Diretas */

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

== Motivação ==

O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

== O Método ==

Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

== Regras de Inferência ==

Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

=== Regras de Inferência Diretas ===

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

== Definições ==

'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

== Teoremas ==

Semanticamente, na conseqüência lógica, existe um tipo especial de fórmula, as fórmulas válidas, que são aquelas verdadeiras em toda e qualquer estrutura. Alternativamente, elas podem ser definidas como aquelas fórmulas que são conseqüência lógica de um conjunto vazio de premissas.

Caracterizando conseqüência lógica de uma maneira sintática, como feito em dedução natural, obtêm-se algo similar: os teoremas.

'''Definição 3:''' Uma fórmula <math>\alpha</math> é um teorema (do CQC) se há uma dedução de <math>\alpha</math> a partir do conjunto vazio de premissas.

Assim, <math>\alpha</math> é um teorema do CQC se e somente se <math>\oslash</math>├ <math>\alpha</math>, o que se abrevia escrevendo simplesmente ├ <math>\alpha</math>.

== Conseqüência sintática e conseqüência semântica ==

A definição semântica de conseqüência afirma que uma fórmula <math>\alpha</math> é conseqüência lógica (semântica) de um conjunto <math>\Gamma</math> de fórmulas se toda estrutura que for modelo de <math>\Gamma</math> é um modelo de <math>\alpha</math>, o que se indica por <math>\Gamma</math>╞ <math>\alpha</math>.

Já sintaticamente, um argumento é válido se sua conclusão puder ser produzida a partir das premissas por meio da aplicação de certas regras de inferência (dedução 2).

Tendo definidas as duas noções de conseqüência, pode-se mostrar que, no CQC, as duas noções coincidem. Isto é, <math>\alpha</math> é uma conseqüência sintática de <math>\Gamma</math> se e somente se <math>\alpha</math> é uma conseqüência semântica de <math>\Gamma</math>, o que vale dizer que o método de dedução natural é um sistema de prova correto e completo para o CQC. Correto porque se uma conclusão pode ser deduzida de um conjunto <math>\Gamma</math> de premissa, então ela de fato é conseqüência lógica de <math>\Gamma</math>. E completo porque, se uma fórmula é conseqüência lógica de um conjunto de premissas, há uma dedução demonstrando isso. Isso tudo é sintetizado no seguinte teorema (Teorema de Correção e Completude), onde <math>\Gamma</math> é um conjunto qualquer de fórmulas:

<math>\Gamma</math> ├ <math>\alpha</math> se e somente se <math>\Gamma</math>╞ <math>\alpha</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:36:27Z

Lihkluppel: /* Regras de Inferência Diretas */

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

== Motivação ==

O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

== O Método ==

Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

== Regras de Inferência ==

Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

==='''Regras de Inferência Diretas'''===

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

== Definições ==

'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

== Teoremas ==

Semanticamente, na conseqüência lógica, existe um tipo especial de fórmula, as fórmulas válidas, que são aquelas verdadeiras em toda e qualquer estrutura. Alternativamente, elas podem ser definidas como aquelas fórmulas que são conseqüência lógica de um conjunto vazio de premissas.

Caracterizando conseqüência lógica de uma maneira sintática, como feito em dedução natural, obtêm-se algo similar: os teoremas.

'''Definição 3:''' Uma fórmula <math>\alpha</math> é um teorema (do CQC) se há uma dedução de <math>\alpha</math> a partir do conjunto vazio de premissas.

Assim, <math>\alpha</math> é um teorema do CQC se e somente se <math>\oslash</math>├ <math>\alpha</math>, o que se abrevia escrevendo simplesmente ├ <math>\alpha</math>.

== Conseqüência sintática e conseqüência semântica ==

A definição semântica de conseqüência afirma que uma fórmula <math>\alpha</math> é conseqüência lógica (semântica) de um conjunto <math>\Gamma</math> de fórmulas se toda estrutura que for modelo de <math>\Gamma</math> é um modelo de <math>\alpha</math>, o que se indica por <math>\Gamma</math>╞ <math>\alpha</math>.

Já sintaticamente, um argumento é válido se sua conclusão puder ser produzida a partir das premissas por meio da aplicação de certas regras de inferência (dedução 2).

Tendo definidas as duas noções de conseqüência, pode-se mostrar que, no CQC, as duas noções coincidem. Isto é, <math>\alpha</math> é uma conseqüência sintática de <math>\Gamma</math> se e somente se <math>\alpha</math> é uma conseqüência semântica de <math>\Gamma</math>, o que vale dizer que o método de dedução natural é um sistema de prova correto e completo para o CQC. Correto porque se uma conclusão pode ser deduzida de um conjunto <math>\Gamma</math> de premissa, então ela de fato é conseqüência lógica de <math>\Gamma</math>. E completo porque, se uma fórmula é conseqüência lógica de um conjunto de premissas, há uma dedução demonstrando isso. Isso tudo é sintetizado no seguinte teorema (Teorema de Correção e Completude), onde <math>\Gamma</math> é um conjunto qualquer de fórmulas:

<math>\Gamma</math> ├ <math>\alpha</math> se e somente se <math>\Gamma</math>╞ <math>\alpha</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:36:05Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

== Motivação ==

O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

== O Método ==

Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

== Regras de Inferência ==

Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

='''Regras de Inferência Diretas'''=

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

== Definições ==

'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

== Teoremas ==

Semanticamente, na conseqüência lógica, existe um tipo especial de fórmula, as fórmulas válidas, que são aquelas verdadeiras em toda e qualquer estrutura. Alternativamente, elas podem ser definidas como aquelas fórmulas que são conseqüência lógica de um conjunto vazio de premissas.

Caracterizando conseqüência lógica de uma maneira sintática, como feito em dedução natural, obtêm-se algo similar: os teoremas.

'''Definição 3:''' Uma fórmula <math>\alpha</math> é um teorema (do CQC) se há uma dedução de <math>\alpha</math> a partir do conjunto vazio de premissas.

Assim, <math>\alpha</math> é um teorema do CQC se e somente se <math>\oslash</math>├ <math>\alpha</math>, o que se abrevia escrevendo simplesmente ├ <math>\alpha</math>.

== Conseqüência sintática e conseqüência semântica ==

A definição semântica de conseqüência afirma que uma fórmula <math>\alpha</math> é conseqüência lógica (semântica) de um conjunto <math>\Gamma</math> de fórmulas se toda estrutura que for modelo de <math>\Gamma</math> é um modelo de <math>\alpha</math>, o que se indica por <math>\Gamma</math>╞ <math>\alpha</math>.

Já sintaticamente, um argumento é válido se sua conclusão puder ser produzida a partir das premissas por meio da aplicação de certas regras de inferência (dedução 2).

Tendo definidas as duas noções de conseqüência, pode-se mostrar que, no CQC, as duas noções coincidem. Isto é, <math>\alpha</math> é uma conseqüência sintática de <math>\Gamma</math> se e somente se <math>\alpha</math> é uma conseqüência semântica de <math>\Gamma</math>, o que vale dizer que o método de dedução natural é um sistema de prova correto e completo para o CQC. Correto porque se uma conclusão pode ser deduzida de um conjunto <math>\Gamma</math> de premissa, então ela de fato é conseqüência lógica de <math>\Gamma</math>. E completo porque, se uma fórmula é conseqüência lógica de um conjunto de premissas, há uma dedução demonstrando isso. Isso tudo é sintetizado no seguinte teorema (Teorema de Correção e Completude), onde <math>\Gamma</math> é um conjunto qualquer de fórmulas:

<math>\Gamma</math> ├ <math>\alpha</math> se e somente se <math>\Gamma</math>╞ <math>\alpha</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:35:21Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

== Motivação ==

O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

== O Método ==

Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

== Regras de Inferência ==

Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

== Definições ==

'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

== Teoremas ==

Semanticamente, na conseqüência lógica, existe um tipo especial de fórmula, as fórmulas válidas, que são aquelas verdadeiras em toda e qualquer estrutura. Alternativamente, elas podem ser definidas como aquelas fórmulas que são conseqüência lógica de um conjunto vazio de premissas.

Caracterizando conseqüência lógica de uma maneira sintática, como feito em dedução natural, obtêm-se algo similar: os teoremas.

'''Definição 3:''' Uma fórmula <math>\alpha</math> é um teorema (do CQC) se há uma dedução de <math>\alpha</math> a partir do conjunto vazio de premissas.

Assim, <math>\alpha</math> é um teorema do CQC se e somente se <math>\oslash</math>├ <math>\alpha</math>, o que se abrevia escrevendo simplesmente ├ <math>\alpha</math>.

== Conseqüência sintática e conseqüência semântica ==

A definição semântica de conseqüência afirma que uma fórmula <math>\alpha</math> é conseqüência lógica (semântica) de um conjunto <math>\Gamma</math> de fórmulas se toda estrutura que for modelo de <math>\Gamma</math> é um modelo de <math>\alpha</math>, o que se indica por <math>\Gamma</math>╞ <math>\alpha</math>.

Já sintaticamente, um argumento é válido se sua conclusão puder ser produzida a partir das premissas por meio da aplicação de certas regras de inferência (dedução 2).

Tendo definidas as duas noções de conseqüência, pode-se mostrar que, no CQC, as duas noções coincidem. Isto é, <math>\alpha</math> é uma conseqüência sintática de <math>\Gamma</math> se e somente se <math>\alpha</math> é uma conseqüência semântica de <math>\Gamma</math>, o que vale dizer que o método de dedução natural é um sistema de prova correto e completo para o CQC. Correto porque se uma conclusão pode ser deduzida de um conjunto <math>\Gamma</math> de premissa, então ela de fato é conseqüência lógica de <math>\Gamma</math>. E completo porque, se uma fórmula é conseqüência lógica de um conjunto de premissas, há uma dedução demonstrando isso. Isso tudo é sintetizado no seguinte teorema (Teorema de Correção e Completude), onde <math>\Gamma</math> é um conjunto qualquer de fórmulas:

<math>\Gamma</math> ├ <math>\alpha</math> se e somente se <math>\Gamma</math>╞ <math>\alpha</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:34:25Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

== Motivação ==

O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

== O Método ==

Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

== Regras de Inferência ==

Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

== Definições ==

'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

== Teoremas ==

Semanticamente, na conseqüência lógica, existe um tipo especial de fórmula, as fórmulas válidas, que são aquelas verdadeiras em toda e qualquer estrutura. Alternativamente, elas podem ser definidas como aquelas fórmulas que são conseqüência lógica de um conjunto vazio de premissas.

Caracterizando conseqüência lógica de uma maneira sintática, como feito em dedução natural, obtêm-se algo similar: os teoremas.

'''Definição 3:''' Uma fórmula <math>\alpha</math> é um teorema (do CQC) se há uma dedução de <math>\alpha</math> a partir do conjunto vazio de premissas.

Assim, <math>\alpha</math> é um teorema do CQC se e somente se <math>\oslash</math>├ <math>\alpha</math>, o que se abrevia escrevendo simplesmente ├ <math>\alpha</math>.

== Conseqüência sintática e conseqüência semântica ==

A definição semântica de conseqüência afirma que uma fórmula <math>\alpha</math> é conseqüência lógica (semântica) de um conjunto <math>\Gamma</math> de fórmulas se toda estrutura que for modelo de <math>\Gamma</math> é um modelo de <math>\alpha</math>, o que se indica por <math>\Gamma</math>╞ <math>\alpha</math>.

Já sintaticamente, um argumento é válido se sua conclusão puder ser produzida a partir das premissas por meio da aplicação de certas regras de inferência (dedução 2).

Tendo definidas as duas noções de conseqüência, pode-se mostrar que, no CQC, as duas noções coincidem. Isto é, <math>\alpha</math> é uma conseqüência sintática de <math>\Gamma</math> se e somente se <math>\alpha</math> é uma conseqüência semântica de <math>\Gamma</math>, o que vale dizer que o método de dedução natural é um sistema de prova correto e completo para o CQC. Correto porque se uma conclusão pode ser deduzida de um conjunto <math>\Gamma</math> de premissa, então ela de fato é conseqüência lógica de <math>\Gamma</math>. E completo porque, se uma fórmula é conseqüência lógica de um conjunto de premissas, há uma dedução demonstrando isso. Isso tudo é sintetizado no seguinte teorema (Teorema de Correção e Completude), onde <math>\Gamma</math> é um conjunto qualquer de fórmulas:

<math>\Gamma</math> ├ <math>\alpha</math> se e somente se <math>\Gamma</math>╞ <math>\alpha</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:32:28Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

== '''Motivação''' ==
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

'''Teoremas'''
----
Semanticamente, na conseqüência lógica, existe um tipo especial de fórmula, as fórmulas válidas, que são aquelas verdadeiras em toda e qualquer estrutura. Alternativamente, elas podem ser definidas como aquelas fórmulas que são conseqüência lógica de um conjunto vazio de premissas.

Caracterizando conseqüência lógica de uma maneira sintática, como feito em dedução natural, obtêm-se algo similar: os teoremas.

'''Definição 3:''' Uma fórmula <math>\alpha</math> é um teorema (do CQC) se há uma dedução de <math>\alpha</math> a partir do conjunto vazio de premissas.

Assim, <math>\alpha</math> é um teorema do CQC se e somente se <math>\oslash</math>├ <math>\alpha</math>, o que se abrevia escrevendo simplesmente ├ <math>\alpha</math>.

'''Conseqüência sintática e conseqüência semântica'''
----
A definição semântica de conseqüência afirma que uma fórmula <math>\alpha</math> é conseqüência lógica (semântica) de um conjunto <math>\Gamma</math> de fórmulas se toda estrutura que for modelo de <math>\Gamma</math> é um modelo de <math>\alpha</math>, o que se indica por <math>\Gamma</math>╞ <math>\alpha</math>.

Já sintaticamente, um argumento é válido se sua conclusão puder ser produzida a partir das premissas por meio da aplicação de certas regras de inferência (dedução 2).

Tendo definidas as duas noções de conseqüência, pode-se mostrar que, no CQC, as duas noções coincidem. Isto é, <math>\alpha</math> é uma conseqüência sintática de <math>\Gamma</math> se e somente se <math>\alpha</math> é uma conseqüência semântica de <math>\Gamma</math>, o que vale dizer que o método de dedução natural é um sistema de prova correto e completo para o CQC. Correto porque se uma conclusão pode ser deduzida de um conjunto <math>\Gamma</math> de premissa, então ela de fato é conseqüência lógica de <math>\Gamma</math>. E completo porque, se uma fórmula é conseqüência lógica de um conjunto de premissas, há uma dedução demonstrando isso. Isso tudo é sintetizado no seguinte teorema (Teorema de Correção e Completude), onde <math>\Gamma</math> é um conjunto qualquer de fórmulas:

<math>\Gamma</math> ├ <math>\alpha</math> se e somente se <math>\Gamma</math>╞ <math>\alpha</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:31:44Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

'''Teoremas'''
----
Semanticamente, na conseqüência lógica, existe um tipo especial de fórmula, as fórmulas válidas, que são aquelas verdadeiras em toda e qualquer estrutura. Alternativamente, elas podem ser definidas como aquelas fórmulas que são conseqüência lógica de um conjunto vazio de premissas.

Caracterizando conseqüência lógica de uma maneira sintática, como feito em dedução natural, obtêm-se algo similar: os teoremas.

'''Definição 3:''' Uma fórmula <math>\alpha</math> é um teorema (do CQC) se há uma dedução de <math>\alpha</math> a partir do conjunto vazio de premissas.

Assim, <math>\alpha</math> é um teorema do CQC se e somente se <math>\oslash</math>├ <math>\alpha</math>, o que se abrevia escrevendo simplesmente ├ <math>\alpha</math>.

'''Conseqüência sintática e conseqüência semântica'''
----
A definição semântica de conseqüência afirma que uma fórmula <math>\alpha</math> é conseqüência lógica (semântica) de um conjunto <math>\Gamma</math> de fórmulas se toda estrutura que for modelo de <math>\Gamma</math> é um modelo de <math>\alpha</math>, o que se indica por <math>\Gamma</math>╞ <math>\alpha</math>.

Já sintaticamente, um argumento é válido se sua conclusão puder ser produzida a partir das premissas por meio da aplicação de certas regras de inferência (dedução 2).

Tendo definidas as duas noções de conseqüência, pode-se mostrar que, no CQC, as duas noções coincidem. Isto é, <math>\alpha</math> é uma conseqüência sintática de <math>\Gamma</math> se e somente se <math>\alpha</math> é uma conseqüência semântica de <math>\Gamma</math>, o que vale dizer que o método de dedução natural é um sistema de prova correto e completo para o CQC. Correto porque se uma conclusão pode ser deduzida de um conjunto <math>\Gamma</math> de premissa, então ela de fato é conseqüência lógica de <math>\Gamma</math>. E completo porque, se uma fórmula é conseqüência lógica de um conjunto de premissas, há uma dedução demonstrando isso. Isso tudo é sintetizado no seguinte teorema (Teorema de Correção e Completude), onde <math>\Gamma</math> é um conjunto qualquer de fórmulas:

<math>\Gamma</math> ├ <math>\alpha</math> se e somente se <math>\Gamma</math>╞ <math>\alpha</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:31:07Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

'''Teoremas'''
----
Semanticamente, na conseqüência lógica, existe um tipo especial de fórmula, as fórmulas válidas, que são aquelas verdadeiras em toda e qualquer estrutura. Alternativamente, elas podem ser definidas como aquelas fórmulas que são conseqüência lógica de um conjunto vazio de premissas.

Caracterizando conseqüência lógica de uma maneira sintática, como feito em dedução natural, obtêm-se algo similar: os teoremas.

'''Definição 3:''' Uma fórmula <math>\alpha</math> é um teorema (do CQC) se há uma dedução de <math>\alpha</math> a partir do conjunto vazio de premissas.

Assim, <math>\alpha</math> é um teorema do CQC se e somente se <math>\oslash</math>├ <math>\alpha</math>, o que se abrevia escrevendo simplesmente ├ <math>\alpha</math>.

'''Conseqüência sintática e conseqüência semântica'''
----
A definição semântica de conseqüência afirma que uma fórmula <math>\alpah</math> é conseqüência lógica (semântica) de um conjunto <math>\Gamma</math> de fórmulas se toda estrutura que for modelo de <math>\Gamma</math> é um modelo de <math>\alpha</math>, o que se indica por <math>\Gamma</math>╞ <math>\alpha</math>.

Já sintaticamente, um argumento é válido se sua conclusão puder ser produzida a partir das premissas por meio da aplicação de certas regras de inferência (dedução 2).

Tendo definidas as duas noções de conseqüência, pode-se mostrar que, no CQC, as duas noções coincidem. Isto é, <math>\alpha</math> é uma conseqüência sintática de <math>\Gamma</math> se e somente se <math>\alpha</math> é uma conseqüência semântica de <math>\Gmma</math>, o que vale dizer que o método de dedução natural é um sistema de prova correto e completo para o CQC. Correto porque se uma conclusão pode ser deduzida de um conjunto <math>\Gamma</math> de premissa, então ela de fato é conseqüência lógica de <math>\Gamma</math>. E completo porque, se uma fórmula é conseqüência lógica de um conjunto de premissas, há uma dedução demonstrando isso. Isso tudo é sintetizado no seguinte teorema (Teorema de Correção e Completude), onde <math>\Gamma</math> é um conjunto qualquer de fórmulas:

<math>\Gamma</math> ├ <math>\alpha</math> se e somente se <math>\Gamma</math>╞ <math>\alpha</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:27:49Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

'''Teoremas'''
----
Semanticamente, na conseqüência lógica, existe um tipo especial de fórmula, as fórmulas válidas, que são aquelas verdadeiras em toda e qualquer estrutura. Alternativamente, elas podem ser definidas como aquelas fórmulas que são conseqüência lógica de um conjunto vazio de premissas.

Caracterizando conseqüência lógica de uma maneira sintática, como feito em dedução natural, obtêm-se algo similar: os teoremas.

'''Definição 3:''' Uma fórmula <math>\alpha</math> é um teorema (do CQC) se há uma dedução de <math>\alpha</math> a partir do conjunto vazio de premissas.

Assim, <math>\alpha</math> é um teorema do CQC se e somente se <math>\oslash</math>├ <math>\alpha</math>, o que se abrevia escrevendo simplesmente ├ <math>\alpha</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:24:45Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math> se deriva uma fórmula <math>\beta</math>, então se pode descartar <math>\alpha</math> e introduzir <math>\alpha</math><math>\rightarrow</math><math>\beta</math> na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese <math>\alpha</math>, uma contradição <math>\beta</math><math>\wedge</math>¬<math>\beta</math> é derivada, então se pode descartar <math>\alpha</math> e introduzir ¬<math>\alpha</math> na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:21:13Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese ''a'' se deriva uma fórmula ''b'', então se pode descartar ''a'' e introduzir ''a -> b'' na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese ''a'', uma contradição ''b^¬b'' é derivada, então se pode descartar ''a'' e introduzir ''¬a'' na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Diz-se que <math>\alpha</math> é conseqüência lógica (sintática) de <math>\Gamma</math>, o que se denota por ‘<math>\Gamma</math>├ <math>\alpha</math>’, se há uma dedução de <math>\alpha</math>a partir de <math>\Gamma</math>.

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:19:50Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese ''a'' se deriva uma fórmula ''b'', então se pode descartar ''a'' e introduzir ''a -> b'' na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese ''a'', uma contradição ''b^¬b'' é derivada, então se pode descartar ''a'' e introduzir ''¬a'' na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam <math>'''\Gamma'''</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math> a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que <math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam  um conjunto qualquer de fórmulas e uma fórmula. Diz-se que  é conseqüência lógica (sintática) de , o que se denota por ‘├ ’’, se há uma dedução de a partir de .

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:18:59Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese ''a'' se deriva uma fórmula ''b'', então se pode descartar ''a'' e introduzir ''a -> b'' na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese ''a'', uma contradição ''b^¬b'' é derivada, então se pode descartar ''a'' e introduzir ''¬a'' na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam <math>\Gamma</math> um conjunto qualquer de fórmulas e <math>\alpha</math> uma fórmula. Uma dedução de <math>\alpha</math>a partir de <math>\Gamma</math> é uma seqüência finita <math>\delta</math>1,...,<math>\delta</math>n de fórmulas, tal que<math>\delta</math>n = <math>\alpha</math> e cada <math>\delta</math>i, 1 \Gamma</math> ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam  um conjunto qualquer de fórmulas e uma fórmula. Diz-se que  é conseqüência lógica (sintática) de , o que se denota por ‘├ ’’, se há uma dedução de a partir de .

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:17:12Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese ''a'' se deriva uma fórmula ''b'', então se pode descartar ''a'' e introduzir ''a -> b'' na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese ''a'', uma contradição ''b^¬b'' é derivada, então se pode descartar ''a'' e introduzir ''¬a'' na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam <math>\Gamma</math>\Gamma um conjunto qualquer de fórmulas e \alpha uma fórmula. Uma dedução de \alphaa partir de \Gamma é uma seqüência finita \delta1,...,\deltan de fórmulas, tal que\deltan = \alpha e cada $$\delta$$i, 1 < i < n, é uma fórmula que pertence a \Gamma ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam  um conjunto qualquer de fórmulas e uma fórmula. Diz-se que  é conseqüência lógica (sintática) de , o que se denota por ‘├ ’’, se há uma dedução de a partir de .

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:13:43Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese ''a'' se deriva uma fórmula ''b'', então se pode descartar ''a'' e introduzir ''a -> b'' na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese ''a'', uma contradição ''b^¬b'' é derivada, então se pode descartar ''a'' e introduzir ''¬a'' na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam \Gamma um conjunto qualquer de fórmulas e \alpha uma fórmula. Uma dedução de \alphaa partir de \Gamma é uma seqüência finita \delta1,...,\deltan de fórmulas, tal que\deltan = \alpha e cada $$\delta$$i, 1 < i < n, é uma fórmula que pertence a \Gamma ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam  um conjunto qualquer de fórmulas e uma fórmula. Diz-se que  é conseqüência lógica (sintática) de , o que se denota por ‘├ ’’, se há uma dedução de a partir de .

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:11:16Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese ''a'' se deriva uma fórmula ''b'', então se pode descartar ''a'' e introduzir ''a -> b'' na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese ''a'', uma contradição ''b^¬b'' é derivada, então se pode descartar ''a'' e introduzir ''¬a'' na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' Sejam $$\Gamma$$ um conjunto qualquer de fórmulas e \alpha uma fórmula. Uma dedução de \alphaa partir de \Gamma é uma seqüência finita \delta1,...,\deltan de fórmulas, tal que\deltan = \alpha e cada \deltai, 1 < i < n, é uma fórmula que pertence a \Gamma ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.

'''Definição 2:''' Sejam  um conjunto qualquer de fórmulas e uma fórmula. Diz-se que  é conseqüência lógica (sintática) de , o que se denota por ‘├ ’’, se há uma dedução de a partir de .

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:09:03Z

Lihkluppel:

'''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica nos anos 30, por Gentzen e Jaśkowski. O método de dedução natural permite mostrar a validade de um argumento de uma maneira muito mais prática e compacta em relação ao método da tabela-verdade.

Basicamente, o procedimento consiste em aplicar um conjunto de regras de inferência ao conjunto de premissas, gerando conclusões intermediárias às quais aplicam-se novamente as regras, até atingir-se a conclusão final desejada. A esse processo dá-se o nome deduzir, derivar ou provar a conclusão a partir do conjunto das premissas, e a seu resultado, obviamente, uma dedução ou derivação ou prova.

'''Motivação'''
----
O sistema de dedução natural surgiu a partir da insatisfação reinante com relação aos sistemas de demonstração formal existentes anteriormente, que foram criados por Hilbert, Frege, e Russell. Jaśkowski começou, em 1929, a desenvolver um sistema dedutivo mais natural, utilizando-se de uma notação diagramática e, posteriormente atualizando sua proposta em meados dos anos 30. Porém, a forma moderna da dedução natural foi proposta por G. Gentzen, um matemático alemão, em uma dissertação entregue à faculdade de ciências matemáticas da universidade de Göttingen, no ano de 1935. Gentzen foi motivado pelo desejo de estabilizar a consistência da teoria dos números. Ele encontrou, rapidamente, uso para seu cálculo de dedução natural, mas ficou descontente com a complexidade de suas demonstrações, e em 1938 deu uma nova consistência as suas demonstrações.

Prawitz desenvolveu uma monografia em 1965 apresentando o sistema de dedução natural na forma mais conhecida nos dias de hoje, incluindo também aplicações para lógica modal e de segunda ordem.Ele se baseou bastante no trabalho de Gentzen.

'''O Método'''
----
Uma dedução é construída da seguinte maneira: primeiro, faz-se uma lista das premissas que estão a dispor, colocando-se uma em cada linha, e escrevendo “P” ao lado, para indicar que se trata de uma premissa. Cada linha em uma derivação é numerada e deve-se ter uma “justificativa” para a fórmula que nela se encontra. Feito isto, aplica-se alguma regra de inferência que permita acrescentar uma nova linha a essa derivação, contendo uma fórmula que é o resultado da aplicação da regra a fórmulas anteriores.

As regras básicas de inferência são postuladas (aceitas sem demonstração). Tais regras devem preservar a verdade: se as fórmulas às quais a regra se aplica são verdadeiras, a fórmula resultante também o será.

'''Regras de Inferência'''
----
Em princípio, não há um limite quanto ao número de regras que se pode ter em um sistema. Há, naturalmente, um mínimo necessário – o conjunto de regras deve ser completo, isto é, idealmente elas devem ser capazes de mostrar a validade de todas as formas de argumento –, tendo, para cada operador, duas regras: uma que introduza o operador (ou seja, cujo resultado seja uma fórmula cujo símbolo principal é aquele operador), e uma que elimine o operador (ou seja, que, tomando como entrada uma fórmula cujo símbolo principal seja o operador, dê como resultado uma fórmula mais simples, de onde o operador tenha sido eliminado). De modo similar, para os quantificadores.

Existe quatro tipos de regras de inferência: as diretas, as hipotéticas, as derivadas e as para quantificadores.

'''Regras de Inferência Diretas'''

Exemplos:

[[Imagem:Regras.jpeg]]

'''Regras de Inferência Hipotéticas'''

O conjunto anterior de regras de inferência permite demonstrar a validade de um grande número de argumentos. Contudo, esse conjunto de regras não é completo, pois existem formas de argumento que são válidas no CQC (cálculo quantificacional clássico, o cálculo de predicados de primeira ordem), mas cuja validade não pode ser demonstrada apenas com essas regras. Em primeiro lugar, ainda faltam regras para os quantificadores. Em segundo lugar, foram mostradas apenas oito regras – quando se deveria ter ao menos dez (duas para cada operador). Este tópico tratará das regras para operadores que ainda faltam. Elas se diferenciam das regras diretas do tópico anterior por exigirem o uso de hipóteses.

'''Regra de Prova Condicional (RPC)'''

[[Imagem:regra2.jpeg]]

Isto é, se, a partir de uma hipótese ''a'' se deriva uma fórmula ''b'', então se pode descartar ''a'' e introduzir ''a -> b'' na derivação.

'''Regra de Redução ao Absurdo (RAA)'''

[[Imagem:regra3.jpeg]]

Isto é, se, a partir de uma hipótese ''a'', uma contradição ''b^¬b'' é derivada, então se pode descartar ''a'' e introduzir ''¬a'' na derivação.

'''O uso adequado das Regras de Inferência Hipotéticas'''

'''I.''' Uma linha vertical deve ser introduzida na derivação toda vez que uma hipótese adicional for introduzida.

'''II.''' Não deve ser usada uma fórmula que ocorre à direita de uma linha vertical depois de terminada esta linha.

'''III.''' As hipóteses devem ser descartadas na ordem inversa em que foram introduzidas.

'''IV.''' A dedução não termina enquanto não forem descartadas todas as hipóteses adicionadas.

'''Regras Derivadas'''

Regras derivadas, como o próprio nome diz, são regras que foram obtidas a partir das outras regras que já foram mostradas anteriormente. Regras derivadas servem para abreviar parte de uma dedução; tudo o que se pode fazer com elas pode também ser feito sem elas, usando-se apenas as regras iniciais. Assim, regras derivadas são regras de abreviação.

Exemplos:

[[Imagem:regras2.jpeg]]

Obs.: Os dois traços que separam a premissa da regra de sua conclusão em DN, CT e DM significa que são regras de inferência reversíveis: funcionam nas duas direções.

Existem, claro, outras regras derivadas. Na verdade, pode-se introduzir tantas regras derivadas quanto desejar, pois cada forma de argumento provada válida corresponde a uma regra. As regras derivadas usuais vão corresponder àquelas formas de argumento mais comumente empregadas, apenas isso. O que determina se uma regra é primitiva ou derivada é, basicamente, uma questão de convenção.

'''Definições'''
----
'''Definição 1:''' $$Sejam \Gamma um conjunto qualquer de fórmulas e \alpha uma fórmula. Uma dedução de \alphaa partir de \Gamma é uma seqüência finita \delta1,...,\deltan de fórmulas, tal que\deltan = \alpha e cada \deltai, 1 < i < n, é uma fórmula que pertence a \Gamma ou foi obtida a partir de fórmulas que aparecem antes na seqüência, por meio da aplicação de alguma regra de inferência.$$

'''Definição 2:''' Sejam  um conjunto qualquer de fórmulas e uma fórmula. Diz-se que  é conseqüência lógica (sintática) de , o que se denota por ‘├ ’’, se há uma dedução de a partir de .

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:05:02Z

Lihkluppel:

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T21:01:48Z

Lihkluppel:

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T20:59:34Z

Lihkluppel:

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T17:33:28Z

Lihkluppel:

Arquivo:Regras2.jpeg

2009-03-30T17:10:42Z

Lihkluppel:

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T17:10:33Z

Lihkluppel:

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T17:08:25Z

Lihkluppel:

Arquivo:Regra3.jpeg

2009-03-30T17:05:49Z

Lihkluppel:

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T17:05:34Z

Lihkluppel:

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T17:02:22Z

Lihkluppel:

Arquivo:Regra2.jpeg

2009-03-30T17:01:56Z

Lihkluppel: foi enviada uma nova versão de "Imagem:Regra2.jpeg": Revertido para a versão de 30 de Março de 2009 - 17h01min

Arquivo:Regra2.jpeg

2009-03-30T17:01:46Z

Lihkluppel: foi enviada uma nova versão de "Imagem:Regra2.jpeg"

Arquivo:Regra2.jpeg

2009-03-30T17:01:06Z

Lihkluppel:

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T17:00:37Z

Lihkluppel:

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T16:55:47Z

Lihkluppel:

Arquivo:Regras.jpeg

2009-03-30T16:53:57Z

Lihkluppel:

Dedução Natural: Alexandre, Liège e Danilo

2009-03-30T16:48:20Z

Lihkluppel: Nova página: '''Dedução natural''' é um dos sistemas dedutivos utilizados para construir demonstrações formais na Lógica. Tal sistema foi introduzido pela primeira vez na Lógica Clássica no...

Lógica para Computação - Turmas S71 e S73 - 2009.1

2009-03-26T21:25:39Z

Lihkluppel: /* Assuntos e Equipes */

== Assuntos e Equipes ==

=== Engenharia de Computação (S71) ===

# [[Axiomatização: Vinícius, Daniel e André]]
#* 24/03/2009
#* Equipe debatedora: 12
# [[Dedução Natural: Alexandre, Liège e Danilo]]
#* 24/03/2009
#* Equipe debatedora: 11
# Tablôs Analíticos: Rebeca, Líria e Cristiane
#* 25/03/2009
#* Equipe debatedora: 10
# Tablôs KE: Lucas, Demétrius e João
#* 25/03/2009
#* Equipe debatedora: 9
# Formas Normais: Kelvin, Dalton e Jorge
#* 31/03/2009
#* Equipe debatedora: 8
# Resolução Proposicional: Henrique P., Cibele e Amanda
#* 01/04/2009
#* Equipe debatedora: 7
# Substituição e Unificação: Felipe Lisboa e equipe
#* 15/04/2009
#* Equipe debatedora: 1
# Lógicas Não Clássicas: Eduardo Bonet, Tiago e Jean
#* 22/04/2009
#* Equipe debatedora: '''14'''
# Ontologias: Márcio, Cláudio, Henrique Rein.
#* 05/05/2009
#* Equipe debatedora: '''13'''
# Programação em Lógica: Augusto, Guilherme, Marlos
#* 06/05/2009
#* Equipe debatedora: 5
# Z, uma linguagem de Especificação: Suleiman, Rafael, Julio, Luiz
#* 12/05/2009
#* Equipe debatedora: 4
# Ontologias e Web Semântica (com lógicas de descrição): Marcos, André, Maurício
#* 13/05/2009
#* Equipe debatedora: 3
# VDM, uma linguagem de especificação: Fabio César, Eduardo Rachid e Cleverson
#* 19/05/2009
#* Equipe debatedora: '''6'''
# Provador de teorema - Otter: André Luiz, Gionatta e Pedro.
#* 20/05/2009
#* Equipe debatedora: '''2'''

=== Bacharelado em Sistemas de Informação (S73) ===

# [[Axiomatização: Lucas Campos Silva, Marcelo Butzke Leopoldino, Isaac Toyoshi Takiguchi Jr.]]
#* 25/03/2009
#* Equipe debatedora: 14
# Dedução Natural: Rubens Carlos Meggetto Junior, Estevan Frederico Pasquetta Jantsk, Thomaz Teodorovicz
#* 25/03/2009
#* Equipe debatedora: 13
# Tablôs Analíticos: Daniel Felipe Warkentin, Raul Vitor Tessaro Esteves
#* 01/04/2009
#* Equipe debatedora: 12
# Tablôs KE: Cristiano De Oliveira Viana Correia, Jonatas Da Luz, Luan Nestor Vageti Aruquipa
#* 03/04/2009
#* Equipe debatedora: 11
# Formas Normais: Emerson Shigueo Sugimoto, Rodrigo Cirino De Andrade, Vagner Vengue
#* 22/04/2009
#* Equipe debatedora: 10
# Resolução Proposicional: Ana Paula Ferreira, Fernando Bozza, Vanessa Maria Da Silva
#* 24/04/2009
#* Equipe debatedora: 9
# Substituição e Unificação: Bruno Milczewski, Mario Sergio Esperanca Silva, Thiago Vinicius Pereira
#* 29/04/2009
#* Equipe debatedora: 1
# Lógicas Não Clássicas: Andressa Caroline Portes Da Cunha, Melina Deraldo Dos Santos, Thays Boiko
#* 06/05/2009
#* Equipe debatedora: 2
# Ontologias: Fernando Hiroshi Suemitsu, Bruno Guilherme Andretta De Miranda, Matheus Alves De Souza
#* 08/05/2009
#* Equipe debatedora: 3
# Provadores de Teoremas: Andrei Magaievski, Andre Luiz De Lacerda, Ricardo Trizzolini Piekarski
#* 13/05/2009
#* Equipe debatedora: 4
# Programação em Lógica: Andre Hoeldtke Castro, Rafael Oliveira Tavares Pinto, Vinicius Andreatta
#* 15/05/2009
#* Equipe debatedora: 8
# A linguagem de especificação Z: Bruna Pereira Segan, Leticia Ueda, Kelly Cristina Schultz
#* 20/05/2009
#* Equipe debatedora: 7
# Um provador de teoremas: Eduardo Carvalho Zanello, Gregorio Ivanchechen De Mattos, Pablo Kravicz, Ana Cristina Da Silva
#* 22/05/2009
#* Equipe debatedora: 6 e '''5'''


== Material para os Trabalhos ==

# Axiomatização
#* pp.33-41 de Lógica para Computação
# Dedução Natural
#* pp.41-48 de Lógica para Computação
#* [http://pt.wikibooks.org/wiki/L%C3%B3gica:_C%C3%A1lculo_Proposicional_Cl%C3%A1ssico:_Dedu%C3%A7%C3%A3o_Natural_-_Parte_I Dedução Natural no Wikibooks]
# Tablôs Analíticos
#* pp. 48-56 de Lógica para Computação
#* [http://pt.wikibooks.org/wiki/L%C3%B3gica:_C%C3%A1lculo_Proposicional_Cl%C3%A1ssico:_Tabl%C3%B4s_sem%C3%A2nticos Tablôs Semânticos no Wikibooks]
# Tablôs KE
#* [http://www.teses.usp.br/teses/disponiveis/45/45134/tde-04052007-175943/ Tese de Doutorado do professor Adolfo Neto]
# Formas Normais
#* pp. 77-88 de Lógica para Computação
# Resolução Proposicional
#* pp. 88-92 de Lógica para Computação
#* [http://pt.wikipedia.org/wiki/Princ%C3%ADpio_da_resolu%C3%A7%C3%A3o Princípio da Resolução]
# Substituição e Unificação
#* [http://pt.wikipedia.org/wiki/Unifica%C3%A7%C3%A3o Unificação]
# Lógicas Não Clássicas
#* [http://pt.wikibooks.org/wiki/L%C3%B3gica:_L%C3%B3gicas_N%C3%A3o-cl%C3%A1ssicas:_Introdu%C3%A7%C3%A3o Introdução]
#* A lógica paraconsistente <math>C_1</math>, de Newton da Costa
#** [http://wwwexe.inf.ufsc.br/~arthur/publicacoes/dissertacoes/diss_Arthur.zip Dissertação de Mestrado de Arthur Buchsbaum]
#** [ftp://logica.cle.unicamp.br/pub/e-prints/vol.5,n.1,2005-revised.pdf Logics of Formal Inconsistency]
# Ontologias
#* Procurar Ademir Freddo e pedir material em português
# Provadores de Teoremas
#* [http://pt.wikipedia.org/wiki/Prova_autom%C3%A1tica_de_teoremas Prova automática de teoremas]
#* [http://en.wikipedia.org/wiki/Automated_theorem_proving Automated theorem proving]
# Programação em Lógica
#* Procurar no livro "Lógica para Ciência da Computação"
#* Procurar "prolog" no Google
#* [http://pt.wikipedia.org/wiki/Prolog Prolog]
# Uma linguagem de Especificação
#* Escolher entre Z, VDM e Alloy (ou propor outra)
#** Z
#*** [http://www.teses.usp.br/teses/disponiveis/45/45134/tde-02112008-224245/ Geração parcial de código Java a partir de especificações formais Z, Alvaro Heiji Miyazawa]
#** VDM
#*** [http://www.ic.unicamp.br/~eliane/Cursos/MO409/artigos/artigo-vdm.ps Modelagem e Especificação de Sistemas usando VDM: um Survey, Adilson Luiz Bonifácio e Rodrigo Bonacin]
#*** [http://en.wikipedia.org/wiki/Vienna_Development_Method VDM na Wikipedia]
#*** [http://www.ic.unicamp.br/~eliane/Cursos/MO409/Curso2003/Apresentacoes/VDM.ppt Slides sobre VDM, Cibele Brunetto - Unicamp (contém Bibliografia!)]
#*** [http://atterer.net/uni/sep/ Automatic Test Data Generation From VDM-SL Specifications]
#*** [http://glasnost.itcarlow.ie/~meudecc/research/thesis/thesis.zip Tese de Doutorado sobre VDM]
#*** [http://wiki.di.uminho.pt/twiki/bin/view/Education/Archive/EDFS Especificação e Desenvolvimento Formal de Software]
# Um provador de teoremas
#* Escolher entre Otter, Isabelle, Lotrec, zChaff ou KEMS (ou propor outro)
# Ontologias e Web Semântica (com lógicas de descrição)
#* [http://www.eci.ufmg.br/mba/onto_frames/index.htm Tutorial básico do Protege]

== Regras ==

=== Forma de entrega ===

Os arquivos referentes aos itens abaixo deverão ser entregues/enviados pelo [http://ead.dainf.ct.utfpr.edu.br/course/view.php?id=21 sistema de EAD do DAINF].

=== Apresentação ===

Cada apresentação consistirá de:
# uma equipe (a equipe apresentadora) apresentando o assunto (usando ''slides'', quadro e outros recursos que achar conveniente)
#* esta apresentação deverá durar de 20 a 30 minutos
#* todos os integrantes da equipe devem participar desta apresentação
#* todos os integrantes da equipe devem conhecer TODO o assunto
# Depois disso, uma equipe (a equipe debatedora) deverá fazer perguntas para testar os conhecimentos da equipe apresentadora. Durante este debate (com duração de até 15 minutos), ambas as equipes serão avaliadas.

=== Parte Escrita ===

* Tamanho: entre 5 e 10 páginas
* Usar o [http://www.sbc.org.br/index.php?language=1&subject=60&content=downloads&id=286 modelo para publicação de artigos da SBC] mas, para as referências, seguir o padrão ABNT que pode ser encontrado nas [http://www.utfpr.edu.br/documentos/normas_trabalhos_utfpr.pdf NORMAS PARA ELABORAÇÃO DE TRABALHOS ACADÊMICOS da UTFPR]
* A parte escrita é preparada exclusivamente pela equipe apresentadora e deverá ser entregue uma semana antes da apresentação para o professor e para a equipe debatedora.

=== Resolução dos Exercícios ===

* Para aquelas equipes cujo assunto está no livro "Lógica para Computação", será exigida também a entrega (em formato digital) da resolução completa dos exercícios do livro referentes ao assunto.

=== Entrada na Wiki do DAINF ===

A partir da parte escrita, a equipe deverá preparar uma entrada (mini-artigo) que será publicada na Wiki do DAINF.

=== ''Slides'' da Apresentação ===

Os ''slides'' da apresentação deverão ser entregues com uma semana de antecedência.

Observações importantes:
* procure começar sua apresentação com um exemplo, que deverá ser retomado após a apresentação das bases formais;
* os slides devem ser numerados.

== Critérios de Avaliação ==

# Apresentação '''(peso 2)'''
#* Domínio do conteúdo
#* Capacidade de expressão
# Parte escrita '''(peso 3)'''
#* Conteúdo
#* Qualidade do texto
#* Originalidade
#* Concordância com as normas ABNT
# Resolução dos exercícios '''(peso 1)'''
#* Correção das respostas
# Entrada no wiki do DAINF '''(peso 1)'''
#* Conteúdo
#* Qualidade do texto
#* Originalidade
#* Concordância com as normas Wiki
# Slides da apresentação '''(peso 1)'''
#* Legibilidade
#* Citação de referências
#** Todo slide que contiver material (figura, texto, etc) que não tenha sido desenvolvido pela equipe, deverá conter, na parte inferior da página, em fonte pequena, a referência: "Fonte: (REFERÊNCIA ESTILO ABNT)." Por exemplo, se alguém usar a foto de Hal Abelson obtida da Wikipedia, deverá citar da seguinte forma: "Fonte: WIKIPEDIA. '''Hal Abelson.''' Disponível em:<http://en.wikipedia.org/wiki/Hal_Abelson>. Acesso em: 23 mar. 2009."
# Participação no debate '''(peso 2)''': cada participante de equipe (debatedora ou apresentadora) será avaliado durante o debate de acordo com os seguintes critérios:
#* participação ativa no debate
#* qualidade e pertinência das perguntas feitas
#* correção das respostas dadas