Formule (logika)

Z Wikipedie, otevřené encyklopedie
(Přesměrováno z Term)
Skočit na: Navigace, Hledání

Formule (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.

Obsah

Definice [editovat]

Nechť L je jazyk. V následující definici uvažujeme pouze dvě logické spojky \neg a \Rightarrow a jeden kvantifikátor \forall. Zbylé spojky a kvantifikátor lze zavést definicemi.

Term [editovat]

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.
  • 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

Atomická formule [editovat]

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 [editovat]

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 [editovat]

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). 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<y) není ani otevřená ani uzavřená
  • formule 0+0=0 je otevřená i uzavřená

Volná a vázaná proměná, substituovatelnost [editovat]

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.

Související články [editovat]