Model (logika): Porovnání verzí

Struktura pro [[jazyk (logika)|jazyk]] ''L'' (také model jazyka ''L''), který obsahuje z mimologických symbolů [[konstantní symbol (matematická logika)|konstantní symboly]] <math>c_\alpha; \alpha\in I_K</math>, [[funkční symbol]]y <math>\,f_\alpha</math> četností <math>n_\alpha; \alpha\in I_F</math> a [[predikátový symbol|predikátové symboly]] <math>\,p_\alpha</math> četností <math>n_\alpha; \alpha\in I_P</math>, je množina ''<math>A''</math> nazývaná ''nosič struktury'' spolu s [[konstanta]]mi <math>C_\alpha\in A; \alpha\in I_K</math>, [[funkce (matematika)|funkcemi]] <math>F_\alpha :A^{n_\alpha}\rightarrow A; \alpha \in I_F</math> a [[Relace (matematika)|relacemi]] <math>P_\alpha \subseteq A^{n_\alpha}; \alpha\in I_P</math>. Konstanta <math>\,C_\alpha</math>, resp. funkce <math>\,F_\alpha</math>, resp. relace <math>\,P_\alpha</math> se nazývá realizací konstantního symbolu <math>\,c_\alpha</math>, resp. funkčního symbolu <math>\,f_\alpha</math>, resp. predikátového symbolu <math>\,p_\alpha</math> v modelu <math>A</math> a značí se

<math>\,c_\alpha^A</math>, resp. <math>\,f_\alpha^A</math>, resp. <math>\,p_\alpha^A</math>. Struktura s nosičem <math>A</math> (a příslušnými realizacemi symbolů) se obvykle značí <math>\mathcal{A}</math>.

Méně formálně: Jazyk {{var|L}} obsahuje pouze symboly pro konstanty, funkce a predikáty a arity funkcí a predikátů. Model jazyka {{var|L}} přidává množinu <math>A</math> (nosič struktury, např. množinu přirozených čísel) a dodává symbolům jazyka {{var|L}} jejich realizace.

V tomto odstavci značí <math>\mathcal{A}</math> model jazyka ''L'' s mimologickými symboly popsanými výše. Ohodnocení [[proměnná#Logika|proměnných]] v modelu <math>\mathcal{A}</math> je každá [[funkce]] ''<math>e''</math> z množiny všech proměnných do nosiče <math>A</math>. Ohodnocení, které se shoduje s ohodnocením ''<math>e''</math> na všech proměnných kromě ''<math>x''</math> a na ''<math>x''</math> má hodnotu ''<math>a''</math>, značíme ''<math>e(x/a)''</math>.

Realizace [[term]]u ''<math>t''</math> jazyka ''L'' při ohodnocení proměnných ''<math>e''</math> v modelu ''A'', značíme <math>\,t^A<e></math>, (typograficky lépeznačíme <math>\,t^A\langle e\rangle</math>), se definuje [[indukce dle složitosti|indukcí dle složitosti]] takto:

* <math>\,t^A<\langle e>\rangle=e(x)</math>, je-li ''<math>t''</math> proměnná ''<math>x''</math>

* <math>\,t^A<\langle e>\rangle=c_\alpha^A</math>, je-li ''<math>t''</math> [[konstantní symbol (matematická logika)|konstantní symbol]] <math>\,c_\alpha</math>

* <math>t^A<\langle e>\rangle=F_f_\alpha^A(t_0^A<\langle e>\rangle,\ldots, t_{n_\alpha-1}^A<\langle e>\rangle)</math>, je-li <math>t=f_\alpha(t_0,\ldots,t_{n_\alpha-1})</math> a <math>t_0,\ldots,t_{n_\alpha-1}</math> jsou termy

Platnost [[formule (logika)|formule]] <math>\,\varphi</math> [[jazyk (logika)|jazyka]] ''L'' při ohodnocení proměnných ''<math>e''</math> v modelu <math>\mathcal{A}</math> definujeme [[indukce dle složitosti|indukcí dle složitosti]] takto (<math>\,\varphi</math> platí v <math>\mathcal{A}</math> při ohodnocení ''<math>e''</math> značíme <math>\mathcal{A}\models\varphi<\langle e>\rangle</math>, <math>\,\varphi</math> neplatí v <math>\mathcal{A}</math> při ohodnocení ''<math>e''</math> značíme <math>\mathcal{A}\not\models\varphi<\langle e>\rangle</math>):

* Je-li <math>\,\varphi</math> [[atomická formule]] tvaru <math>p_\alpha(t_0,\ldots,t_{n_\alpha-1})</math>, pak <math>\mathcal{A}\models\varphi<\langle e>\rangle</math>, pokud <math>(t_0^A<\langle e>\rangle,\ldots,t_{n_\alpha-1}^A<\langle e>\rangle)\in P_p_\alpha^A</math>.

* Je-li <math>\,\varphi</math> atomická formule tvaru <math>\,t_0=t_1</math>, pak <math>\mathcal{A}\models\varphi<\langle e>\rangle</math>, pokud <math>t_0^A<\langle e>\rangle=t_1^A<\langle e>\rangle</math>.

* Je-li <math>\,\varphi</math> [[formule (logika)|formule]] tvaru <math>\neg \psi</math>, pak <math>\mathcal{A}\models\varphi<\langle e>\rangle</math> pokud <math>\mathcal{A}\not\models\psi<\langle e>\rangle</math>

* Je-li <math>\,\varphi</math> [[formule (logika)|formule]] tvaru <math>\psi \Rightarrow \chi</math>, pak <math>\mathcal{A}\models\varphi<\langle e>\rangle</math> pokud buďto <math>\mathcal{A}\not\models\psi<\langle e>\rangle</math> nebo <math>\mathcal{A}\models\chi<\langle e>\rangle</math>.

* Je-li <math>\,\varphi</math> [[formule (logika)|formule]] tvaru <math>(\forall x)\psi</math>, pak <math>\mathcal{A}\models\varphi<\langle e>\rangle</math>, pokud <math>\mathcal{A}\models\psi<\langle e(x/a)>\rangle</math> pro všechna <math>a\in A</math>.

Říkáme, že <math>\,\varphi</math> platí v modelu <math>\mathcal{A}</math>, značíme <math>\mathcal{A}\models\varphi</math>, pokud <math>\mathcal{A}\models\varphi<\langle e>\rangle</math> pro každé ohodnocení proměnných ''<math>e''</math>.