Herbrandova struktura

v logika prvního řádu, a Herbrandova struktura S je struktura nad slovní zásobou σ, která je definována pouze syntaktickými vlastnostmi σ. Myšlenka je vzít symboly podmínky jako jejich hodnoty, např. označení konstantního symbolu C je jen "C" (symbol).

Herbrandovy struktury hrají důležitou roli v základech logické programování.^[1]

Herbrandův vesmír

Definice

The Herbrandův vesmír slouží jako vesmír v Herbrandova struktura.

(1) Herbrandův vesmír jazyka prvního řádu L^σ, je množina všech základní pojmy z L^σ. Pokud jazyk nemá žádné konstanty, je jazyk rozšířen přidáním libovolné nové konstanty.

Herbrandův vesmír je spočetně nekonečný, pokud je σ spočetný a existuje funkční symbol arity větší než 0.
V kontextu jazyků prvního řádu mluvíme také jednoduše o Herbrandův vesmír slovní zásoby σ.

(2) Herbrandův vesmír uzavřeného vzorce v Skolem normální forma F, je sada všech výrazů bez proměnných, které lze sestavit pomocí funkčních symbolů a konstant z F. Li F nemá tedy žádné konstanty F je rozšířen přidáním libovolné nové konstanty.

Tato druhá definice je důležitá v kontextu výpočetní rozlišení.

Příklad

Nechat L^σ být jazykem prvního řádu se slovní zásobou

konstantní symboly: C
funkční symboly: F(.), G(.)

pak Herbrandův vesmír L^σ (nebo σ) je {C, F(C), G(C), F(F(C)), F(G(C)), G(F(C)), G(G(C)), ...}.

Všimněte si, že relační symboly nejsou pro Herbrandův vesmír relevantní.

A Herbrandova struktura interpretuje termíny nad a Herbrandův vesmír.

Definice

Nechat S být struktura, se slovní zásobou σ a vesmírem U. Nechat T být množinou všech členů nad σ a T₀ být podmnožinou všech termínů bez proměnných. S se říká, že je Herbrandova struktura iff

U = T₀
F^S(t₁, ..., t_n) = F(t₁, ..., t_n) pro každého n- symbol funkční funkce F ∈ σ a t₁, ..., t_n ∈ T₀
C^S = C pro každou konstantu C v σ

Poznámky

U je Herbrandův vesmír σ.
Herbrandova struktura, která je modelem teorie T, se nazývá Herbrandův model z T.

Příklady

Pro konstantní symbol C a symbol unární funkce F(.) máme následující výklad:

U = {C, fc, ffc, fffc, ...}
fc → fc, ffc → ffc, ...
C → C

Herbrandova základna

Kromě vesmíru definovaného v Herbrandův vesmíra termín denotace definovaný v Herbrandova struktura, Herbrandova základna dokončí interpretaci označením relačních symbolů.

Definice

A Herbrandova základna je množina všech pozemních atomů, jejichž argumentačními termíny jsou Herbrandův vesmír.

Příklady

Pro symbol binární relace R, pojmeme výše uvedené podmínky:

{R(C, C), R(fc, C), R(C, fc), R(fc, fc), R(ffc, C), ...}

Viz také

Poznámky

^ http://logic.stanford.edu/herbrand/herbrand.html

Reference

Ebbinghaus, Heinz-Dieter; Flum, Jörg; Thomas, Wolfgang (1996). Matematická logika. Springer. ISBN 978-0387942582.

[1] ttp://logic.stanford.edu/herbrand/herbrand.html

[1]