Cesko.wiki Formule (logika)
Author
Albert FloresFormule (také predikátová formule, srov. výroková formule) je v matematice a logice syntaktický pojem reprezentující nějaké (matematické) tvrzení v jisté formální teorii predikátové logiky prvního řádu.
Definice
Nechť L je jazyk. V následující definici uvažujeme pouze dvě logické spojky \neg a \Rightarrow a jeden kvantifikátor \forall. +more Zbylé spojky a kvantifikátor lze zavést definicemi.
Term
Termy jazyka L jsou definovány indukcí podle složitosti takto: Množina termů je nejmenší množina splňující: * Každá proměnná je term. * Každý konstantní symbol c jazyka L je term. +more * Kdykoli F je n-ární funkční symbol jazyka L a t_1, \ldots, t_n jsou termy, pak F(t_1, \ldots, t_n) je term. * Nic, co nevzniklo pomocí předchozích pravidel, není term, neboli každý term vznikne konečným použitím tří výše uvedených pravidel Zde je vhodné poznamenat, jaký význam má ve formuli term. Term je obecně nějaký prvek domény. Proto jsou proměnné termy a rovněž funkční symboly jsou termy (funkční symbol reprezentuje relaci zobrazení z domény do domény). Term je ve formuli „vstupem“ predikátového symbolu (v syntaktickém stromu formule se term nacházi pod predikátovým symbolem).
Atomická formule
Atomická formule jazyka L je výraz tvaru P(t_1, \ldots, t_n), kde P je n-ární predikátový symbol jazyka L a t_1, \ldots, t_n jsou termy nebo (jde-li o logiku s rovností) tvaru \,t_1=t_2, kde \,t_1,t_2 jsou termy.
Formule
Formule jazyka L jsou definovány indukcí podle složitosti takto: Množina formulí je nejmenší množina splňující: * Každá atomická formule je formule * Když \varphi je formule, x proměnná, pak \neg \varphi a (\forall x)(\varphi) jsou formule. * Když \varphi, \psi jsou formule, pak \varphi \Rightarrow \psi je formule.
Uzavřená a otevřená formule
Formule se nazývá otevřená, neobsahuje-li žádný kvantifikátor, a uzavřená, je-li každá proměnná v ní obsažená kvantifikována (tj. je na ni aplikován některý kvantifikátor). +more Uzavřená formule se nazývá též sentence.
Například: * formule x+y=z je otevřená ale ne uzavřená * formule (\forall x) (\exists y) (x+y=xy) je uzavřená ale ne otevřená * formule (\forall x) (x není ani otevřená ani uzavřená * formule 0+0=0 je otevřená i uzavřená
Volná a vázaná proměnná, substituovatelnost
Podformulí formule \varphi je každá formule, která je částí formule \varphi.
Říkáme, že proměnná x je vázaná ve formuli \varphi, jestliže existuje podformule formule \varphi ve tvaru (\forall x) \psi(x). Říkáme, že proměnná x je volná ve formuli \varphi, jestliže x má výskyt v nějaké podformuli \,\psi formule \varphi takové, že \,\psi není podformulí žádné formule tvaru (\forall x)( \chi(x)).
Říkáme, že term t je substituovatelný za proměnnou x do formule \varphi, jestliže x není volná v žádné podformuli tvaru (\forall y) \psi, kde proměnná y má výskyt v termu t. Tedy, pokud náš term t obsahuje proměnnou y, která je v místě substituce vázaná, musí tam být i x vázaná.
Je-li x proměnná, t term a \varphi formule, \varphi(x/t) značí formuli, která vznikne nahrazením (substitucí) termu t za každý volný výskyt proměnné x v \varphi.
Otevřené formule nemají vázané proměnné, uzavřené formule nemají volné proměnné.