Download Sistema de Deduccion Natural de Gentzen PDF

TitleSistema de Deduccion Natural de Gentzen
TagsMathematics Physics & Mathematics Deductive Reasoning Validity Metaphilosophy
File Size601.0 KB
Total Pages93
Document Text Contents
Page 1

Grado en
Ingenierı́a

Informática

Sistema de deducción natural de Gentzen

Grado en Ingenierı́a Informática

Octubre de 2011

Page 2

Grado en
Ingenierı́a

Informática Definición

Definición
El sistema de deducción natural de Gentzen es un sistema de
demostración que denotaremos

G = (A,L,X,R),

donde cada uno de los elementos se describe a continuación:

Page 46

Grado en
Ingenierı́a

Informática Regla de eliminación de la
disyunción

(E∨) : {ϕ ∨ ψ,ϕ→ χ, ψ → χ} ` χ.

• La regla de eliminación de la disyunción NO es
ϕ ∨ ψ ` ϕ
ϕ ∨ ψ ` ψ,

ya que de la validez de una disyunción de dos fórmulas no se puede
deducir la validez de las dos fórmulas.

Page 47

Grado en
Ingenierı́a

Informática Regla de eliminación de la
disyunción

(E∨) : {ϕ ∨ ψ,ϕ→ χ, ψ → χ} ` χ.

• La regla de eliminación de la disyunción NO es
ϕ ∨ ψ ` ϕ
ϕ ∨ ψ ` ψ,

ya que de la validez de una disyunción de dos fórmulas no se puede
deducir la validez de las dos fórmulas.

Page 92

Grado en
Ingenierı́a

Informática Modus Tollens

{ϕ→ ψ,¬ψ} ` ¬ϕ

1) ϕ→ ψ (Premisa)
2) ¬ψ (Premisa)

3) ϕ (Premisa auxiliar)
4) ψ (E→(1,3))
5) ψ ∧ ¬ψ (I∧(2,4))

4) ¬ϕ (I¬(3-5))

Page 93

Grado en
Ingenierı́a

Informática Modus Tollens

{ϕ→ ψ,¬ψ} ` ¬ϕ

1) ϕ→ ψ (Premisa)
2) ¬ψ (Premisa)

3) ϕ (Premisa auxiliar)
4) ψ (E→(1,3))
5) ψ ∧ ¬ψ (I∧(2,4))

4) ¬ϕ (I¬(3-5))

Similer Documents