Zemin ifadesi - Ground expression

Gelen matematiksel mantık , bir zemin terim a biçimsel sisteminin bir olan terim hiçbirini içermiyor değişkenleri . Benzer şekilde, temel formül herhangi bir değişken içermeyen bir formüldür .

Gelen kimliği ile birinci derece mantık , cümle S ( a ) ∨ P ( B ) ile, bir zemin formülü bir ve b sabit sembolleri olmak. Bir zemin ifadesi bir zemin terim veya toprak formülüdür.

Örnekler

0 sayısı için sabit bir 0 sembolü , ardıl fonksiyon için bir tekli fonksiyon sembolü s ve toplama için bir ikili fonksiyon sembolü + içeren bir imza üzerinde birinci dereceden mantıktaki aşağıdaki ifadeleri düşünün .

  • s (0), s ( s (0)), s ( s ( s (0))), ... temel terimlerdir,
  • 0 + 1, 0 + 1 + 1, ... temel terimlerdir,
  • x  +  s (1) ve s ( x ) terimlerdir, ancak temel terimler değildir,
  • s (0) = 1 ve 0 + 0 = 0 zemin formülleridir,

Resmi tanımlama

Aşağıda, birinci dereceden diller için resmi bir tanım bulunmaktadır . C sabit semboller seti, V (bireysel) değişkenler seti , F fonksiyonel operatörler seti ve P yüklem sembolleri seti ile birinci dereceden bir dil verilsin .

Zemin şartları

Temel terimler, değişken içermeyen terimlerdir . Mantıksal özyineleme (formül özyineleme) ile tanımlanabilirler:

  1. C'nin unsurları temel terimlerdir;
  2. Eğer f ∈ F bir N -ary fonksiyon sembolü ve α 1 , α 2 , ..., α n zemin koşulları, daha sonra f (α 1 α, 2 , ..., α n ) öğütülmüş bir terimdir.
  3. Her temel terim, yukarıdaki iki kuralın sonlu bir uygulamasıyla verilebilir (başka temel terim yoktur; özellikle, yüklemler temel terimler olamaz).

Kabaca konuşursak, Herbrand evreni tüm temel terimlerin kümesidir.

Yer atomu

Bir zemin yüklemi , temel atom veya yer değişmezi , argüman terimlerinin tümü temel terimler olan atomik bir formüldür .

Eğer p ∈ P bir N -ary yüklem sembolü ve α 1 , α 2 , ..., α n zemin koşulları, daha sonra p (α 1 , α 2 , ..., α n ) olan bir zemin yüklemi ya da zemin atom.

Kabaca konuşursak, Herbrand tabanı tüm temel atomların kümesidir, bir Herbrand yorumu ise tabandaki her yer atoma bir doğruluk değeri atar .

Zemin formülü

Temel formül veya temel cümle, değişken içermeyen bir formüldür.

Serbest değişkenli formüller, aşağıdaki gibi sözdizimsel özyineleme ile tanımlanabilir:

  1. Topraklanmamış bir atomun serbest değişkenleri, içinde meydana gelen tüm değişkenlerdir.
  2. ¬ serbest değişkenler p kişilerce aynıdır p . Serbest değişkenler s ∨ q , p ∧ q , p → q kişilerce serbest değişkenlerdir p ya da serbest değişken q .
  3. ∀ x   p ve ∃ x   p'nin serbest değişkenleri, x hariç p'nin serbest değişkenleridir .

Referanslar

  • Dalal, M. (2000), "Mantık tabanlı bilgisayar programlama paradigmaları", Rosen, KH; Michaels, JG (ed.), Handbook of discrete and cominatorial mathematics , s. 68
  • Hodges, Wilfrid (1997), Daha kısa bir model teorisi , Cambridge University Press , ISBN   978-0-521-58713-6
  • Birinci Derece Mantık: Sözdizimi ve Anlambilim