|-(∀x)(∀y)A ↔ (∀y)(∀x)A
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... :) )