Əvəzetmə (məntiq)

**Əvəzetmə** — formal dillərdə ifadələr üzərində aparılan sintaktik çevrilmə. Bir ifadəyə əvəzetməni *tətbiq etmək* onun dəyişənlərini və ya yer tutucu simvollarını ardıcıl şəkildə digər ifadələrlə əvəz etmək deməkdir. 

Nəticədə alınan ifadə ilkin ifadənin *əvəzetmə nümunəsi* (və ya qısaca *nümunəsi*) adlanır.

## Təklif məntiqi
### Tərif
Burada *ψ* və *φ* təklif məntiqinin formullarını ifadə edir. *ψ*, *φ*-nin *əvəzetmə nümunəsi*dir o halda və yalnız o halda ki, *ψ* ifadəsi *φ*-dəki təklif dəyişənlərinin yerinə formulalar qoymaqla, eyni dəyişənin hər bir təkrarlanmasını eyni formul ilə əvəz etməklə əldə olunsun. Məsələn:

::*ψ:* (R → S) & (T → S)
aşağıdakı ifadənin əvəzetmə nümunəsidir:
::*φ:* P & Q

Yəni *ψ* ifadəsi *φ*-dəki P və Q dəyişənlərini müvafiq olaraq (R → S) və (T → S) ilə əvəz etməklə alınır. Oxşar olaraq:

::*ψ:* (A ↔ A) ↔ (A ↔ A)
aşağıdakı ifadənin əvəzetmə nümunəsidir:
::*φ:* (A ↔ A)

çünki *ψ* ifadəsi *φ*-dəki hər bir A-nı (A ↔ A) ilə əvəz etməklə əldə olunur.

Təklif məntiqi üçün bəzi deduksiya sistemlərində yeni bir ifadə (bir təklif) çıxarışın (isbatın) bir sətrinə yalnız o halda əlavə edilə bilər ki, o, əvvəlki sətirdəki ifadənin əvəzetmə nümunəsi olsun. Bu, bəzi aksiomatik sistemlərdə yeni sətirlərin daxil edilmə üsuludur. çevrilmə qaydalarından istifadə edən sistemlərdə isə qayda, çıxarışa müəyyən dəyişənləri daxil etmək məqsədilə *əvəzetmə nümunəsi*ndən istifadəni əhatə edə bilər.

### Tautologiyalar
Bir təklif formulu hər bir qiymətləndirmə (və ya interpretasiya) altında doğru olarsa, o, tautologiya adlanır. Əgər Φ tautologiyadırsa və Θ onun əvəzetmə nümunəsidirsə, onda Θ da tautologiya olacaq. Bu fakt əvvəlki bölmədə təsvir edilən deduksiya qaydasının səsli (sound) olmasını təmin edir.

## Birinci dərəcəli məntiq

Birinci dərəcəli məntiqdə *əvəzetmə* dəyişənlər çoxluğundan terminlər çoxluğuna olan tam təsvir kimi müəyyən olunur: . Bir çox, lakin hamısı deyil müəlliflər əlavə olaraq tələb edirlər ki, *σ*(*x*) = *x* yalnız sonlu sayda dəyişən istisna olmaqla bütün dəyişənlər üçün doğru olsun.

Yazılış 
*i*=1,…,*k* üçün hər bir *x**i* dəyişənini uyğun *t**i* termini ilə əvəz edən, digər bütün dəyişənləri isə olduğu kimi saxlayan əvəzetməni göstərir; *x**i*-lər cüt-cüt fərqli olmalıdır. Əksər müəlliflər əlavə olaraq tələb edirlər ki, hər bir *t**i* termini sintaktik baxımdan *x**i*-dən fərqli olsun; bu, eyni əvəzetmə üçün sonsuz sayda fərqli yazılışın qarşısını almaq üçündür.

Bu əvəzetmənin *tətbiqi* postfiks notasiyada *t*  kimi yazılır və *t* terminində hər bir *x**i*-nin bütün occurrences-larının eyni anda *t**i* ilə əvəz edilməsi deməkdir.

Əvəzetmə *σ*-nın *t* termininə tətbiqinin nəticəsi *tσ* həmin *t* terminəsinin *nümunəsi* adlanır. Məsələn,  əvəzetməsini. əvəzlənməsi idempotentdir, məs. ((*x*+*y*) )  = ((*y*+*y*)+*y*)  = (*y*+*y*)+*y*),  = (*y*+*y*)+*y*,  əvəzlənməsi isə idempotent deyil, məs. ((*x*+*y*) )  = ((*x*+*y*)+*y*)  = ((*x*+*y*)+*y*) +*y*. İşə-gəlişlə əlaqəli olmayan əvəzetmələrə nümunə   = , lakin   = .

Əvəzetmənin *sahəsi* (*dom*(*σ*)) faktiki olaraq əvəz edilən dəyişənlər çoxluğu kimi müəyyən olunur, yəni
*dom*(*σ*) = .

Əgər əvəzetmə sahəsindəki bütün dəyişənləri yer (ground) terminlərlə — yəni dəyişənsiz terminlərlə — əvəz edirsə, o, *yer əvəzetməsi* adlanır. Əgər *t* terminindəki bütün dəyişənlər əvəzetmənin sahəsinə daxildirsə, yer əvəzetmənin nümunəsi *tσ* yer termini olur.

Əvəzetmə *σ* *xətti* adlanır, əgər *tσ* termini (və deməli, sahəsindəki dəyişənləri dəqiq əhatə edən istənilən xətti termin üçün) xəttidirsə.
Əvəzetmə *σ* *düz* (*flat*) adlanır, əgər hər bir *x* üçün *xσ* yenə dəyişən olarsa.
Əvəzetmə *σ* *yenidadlandırma* adlanır, əgər o, bütün dəyişənlər çoxluğu üzərində permutasiyadır. Yenidadlandırma əvəzetmələrinin hər zaman tərs əvəzetməsi *σ*−1 mövcuddur və hər bir *t* üçün *tσσ*−1 = *t* = *tσ*−1*σ* bərabərliyi ödənir. Lakin ixtiyari əvəzetmə üçün tərs müəyyən etmək mümkün deyil.

Məsələn,  yer əvəzetməsidir;  yer olmayan və düz olmayan, lakin xətti əvəzetmədir və s.

İki əvəzetmə o zaman *bərabər* hesab olunur ki, hər bir dəyişəni sintaktik baxımdan eyni terminə göndərsinlər, yəni formal olaraq *σ* = *τ* əgər hər bir *x* ∈ *V* üçün *xσ* = *xτ* olarsa.

İki əvəzetmənin *kompozisiyası* assosiativ əməliyyatdır, lakin kommutativ deyil; yəni ümumiyyətlə *στ* ≠ *τσ*. Əvəzetmə kompozisiyasının neytral elementi bütün dəyişənləri özünə göndərən *eyniyyət əvəzetməsi*dir. Əgər *σσ* = *σ* olarsa, *σ* *idempotent* adlanır.

Məsələn,  ilə  bərabərdir, lakin  ilə eyni deyil.

## İstinadlar