v1

|- A→A

Důkaz

Vyjdu z

|- A→[(A→A)→A]→[(A→(A→A))→(A→A)]

To je instance A2 (A→(B→C))→[(A→B)→(A→C)], kde

  • A ~ A
  • B ~ A→A
  • C ~ A

Dále

|- A→[(A→A)→A]

je instance A1 (A→(B→A)), kde

  • A ~ A
  • B ~ (A→A)

Použiju pravidlo modus ponens

   A->((A->A)->A)    A->((A->A)->A)->[(A->(A->A))->(A->A)]
  ---------------------------------------------------------
                  (A->(A->A))->(A->A)

Tedy

|- (A→(A→A))→(A→A)

Nyní použiju pro modus ponens další instanci A1, tentokrát

|- (A→(A→A))

   (A->(A->A))    (A->(A->A))->(A->A)
  ------------------------------------
               (A->A)

A výsledkem je tvrzení v1

|- A→A

QED

 
a_-_a.txt · Last modified: 2006/04/26 21:08 by 85.160.5.202
 
Recent changes RSS feed Creative Commons License Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki