Kanonický tvar formule

Formule v predikátové logice je v kanonickém tvaru, pokud

1. žádná proměnná, která se ve formuli vyskytuje jako volná, se v ní nevyskytuje jako vázaná,
2. za každým kvantifikátorem je jiná proměnná.

Ke každé formuli existuje ekvivalentní formule v kanonickém tvaru. Každou formuli $F$ lze převést do kanonického tvaru vhodným přejmenováním vázaných proměnných.

Příklad

$F:=\mathrm{\forall }x\mathrm{\exists }y(P(x,y)\wedge Q(x,z))$

$G:=\mathrm{\exists }u(\mathrm{\forall }vP(u,v)\vee Q(v,v))$

Ve formuli $F$ jsou proměnné $x$ a $y$ vázané a proměnná $z$ volná. $F$ je tedy kanonická. Ve formuli $G$ jsou všechny výskyty proměnné $u$ vázané, ale výskyty proměnné $v$ jsou jak vázané tak volné. $G$ proto není v kanonickém tvaru. Výsledkem převodu $G$ do kanonického tvaru je formule (vzniklá přejmenováním vázaných proměnných):

$G^{\prime }:=\mathrm{\exists }u(\mathrm{\forall }wP(u,w)\vee Q(v,v))$

Odkazy

Související články

• Kanonický tvar