|-(∀x)(∀y)A ↔ (∀y)(∀x)A

Důkaz

budu dokazovat dve implikace:

dle schematu specifikace (za Ax[t] vezmu Ax[x]):

(∀x)(∀y)A -> (∀y)A
(∀y)A -> A

tedy (slozeni implikaci):

(∀x)(∀y)A -> A

pravidlo generalizace:

(∀x)[(∀x)(∀y)A -> A]

v (∀x)(∀y)A urcite neni x volne, tedy muzu pouzit schema preskoku:

(∀x)(∀y)A -> (∀x)A

pravidlo generalizace:

(∀y)[(∀x)(∀y)A -> (∀x)A]

schema preskoku:

(∀x)(∀y)A -> (∀y)(∀x)A

analogicky... :)

(pozn.: je to psane jen tak narychlo, kdyztak to nekdo vylepsete... :) )

 
axaya_ayaxa.txt · Last modified: 2006/05/14 17:52 by 195.113.65.3
 
Recent changes RSS feed Creative Commons License Donate Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki