Matematické Fórum

Díky, brzy budeme mít první přednášku, snad se záhada rozluští tam :-)

↑ Lishaak:
Nepovažuji sice knihu H. J. Bartsche za kvalitní literaturu, ale tam je totéž, co říkám já, tedy že predikát je výroková formule. Přenechám ale diskuzi zkušenějším v této oblasti.

Rozfíl mezi výrokem a výrokovou formou je v tom, že do formy se musí něco dosadit. Výroková forma je třeba "x je větší než 5", výrok získám buď konkrétním dosazením "7 je větší než 5", "3 je větší než 5" nebo kvantifikací "exstuje číslo větší než 5", "každé číslo je větší než 5".

Jinak Bartsche jsem elektronicky nenašel, ale měl by být snadno k sehnání papírově (je to velmi oblíbená sbírka vzorců, v originále Taschenbuch mathematischer Formeln, česky Matematické vzorce).

Ja jsem to vzdycky vnimal tak, ze vyrokova logika obsahuje pouze promenne a logicke spojky.

Predikatova logika je nekolika radu, nejznamejsi je prvniho radu. Ta pouziva promenne, logicke spojky a ted prijde to podstatne:

funkcni symboly a predikatove symboly.

Funkcni symboly jsou zastupci funkci, tedy z nekolika argumentu se vytvori (jediny) novy prvek, ktery ovsem neni uzavrena formule. Predikatove symboly reprezentuji relace, tedy treba rovnost, usporadani, atd. Vysledek "operace" predikatoveho symbolu je tedy "TRUE" / "FALSE".

Pak jeste predikatova logika poskytuje kvantifikatory, no a pres co vsechno se da kvantifikovat, to urcuje rad logiky (jen pres promenne - 1. rad, i pres funkcni a predikatove symboly - vyssi rady).

Za promenne vyrokove logiky lze dosazovat uzavrene formule jinych teorii. Timto zpusobem tedy lze vyrokovou logiku pouzit i v predikatove logice.

Priklad: promenne x,y,z, konstanty 0,1 (ale to jsou vlastne jen nularni funkcni symboly z logickeho hlediska), ternarni funkcni symbol f, binarni predikat < zapisovan infixove, predikatova logika s rovnosti (to je terminus technicus, protoze rovnost je az prilis casty predikatovy symbol).

Pak jako predikaty lze oznacit treba

f(x, f(y, 1, 0), z) = 0
f(1,1,1) < 0
0 = 1

Ani jedno z toho neni formuli vyrokove logiky. Vyrok vyrobime tak, ze vezmeme nejakou vyrokovou formu (z promennych vyrokove logiky) a za tyto promenne vyrokove logiky dosadime treba vyse uvedene predikaty. Na zaver jeste musime kvatifikovat pres vsechny volne promenne (ne nutne pres celou formuli). Tak ziskame vyrok.

To je muj pohled na situaci. Nemam to ale podlozeno nicim vic nez tim, ze mi s touto interpretaci vyrok/predikat sedelo vsechno, co nam bylo v logice prezentovano.

Predikatem je podle me tedy "prima aplikace predikatoveho symbolu", tedy napr. f(1,1,1) by nebyl predikat. Asi vsichni se shodneme, ze vyrok f(1,1,1) => 0 je cosi divneho, zatimco (f(1,1,1) = 0) => (1 < 0) se zda byt pochopitelnejsi (za promenne vyrokove logiky do formule A => B lze dosadit jen veci, ktere jsou "TRUE" nebo "FALSE").

↑ Lishaak: Naprosto souhlasim, ze oznaceni "vyrok" je takove trochu stredoskolske, zalozene spise na intuitivnim vnimani cele situace.

Rekl bych tedy, ze vyrok je tvrzeni, o kterem lze (vramci nejake teorie) rozhodnout, zda je pravdivy ci ne. Kdybychom do toho trochu stourali, urcite by se nam po chvilce vynorily treba nerozhodnutelne formule, ale nechme je byt... :-)

Proto mam pocit, ze vyrokem by mela byt jen uzavrena formule. Tezko asi rozhodneme, jestli treba

x > 0 => x-1 > 0

je pravdiva ci ne v celociselne aritmetice. Lepsi uz je to treba pro

\forall x : (x > 0 => x-1 > 0)
(\forall x : x > 0) => (\exists x : x-1 > 0)

ci tak nejak podobne.

Nikde jsem nepsal, ze za vyrokove promenne lze dosazovat jen uzavrene formule. Ale psal jsem, ze abychom ve vysledku dostali vyrok, musime vsechny volne promenne nejak vazat, a na to mame pouze kvantifikatory (at uz je pouzijeme na celou formuli ci jen lokalne na nejakou jeji podformuli).