Əvəzetmə (məntiq)

Burada ψ və φ təklif məntiqinin formullarını ifadə edir. ψ, φ-nin əvəzetmə nümunəsidir 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:^[3]

ψ: (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.^[4] 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əsindən istifadəni əhatə edə bilər.

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əntiqdə əvəzetmə dəyişənlər çoxluğundan terminlər çoxluğuna olan tam təsvir kimi müəyyən olunur: σ: V → T. Bir çox,^{[5]:73[6]:445} lakin hamısı deyil^[7]:250 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ış Şablon:Mset^{[note 1]} 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 Şablon:Mset 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.^{[note 2]}

Ə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, Şablon:Mset əvəzetməsiniŞablon:Mset.Şablon:Mset əvəzlənməsi idempotentdir, məs. ((x+y) Şablon:Mset) Şablon:Mset = ((y+y)+y) Şablon:Mset = (y+y)+y), Şablon:Mset = (y+y)+y, Şablon:Mset əvəzlənməsi isə idempotent deyil, məs. ((x+y) Şablon:Mset) Şablon:Mset = ((x+y)+y) Şablon:Mset = ((x+y)+y) +y. İşə-gəlişlə əlaqəli olmayan əvəzetmələrə nümunə Şablon:Mset Şablon:Mset = Şablon:Mset, lakin Şablon:Mset Şablon:Mset = Şablon:Mset.

Ə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(σ) = Şablon:Mset.

Ə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 σ⁻¹ mövcuddur və hər bir t üçün tσσ⁻¹ = t = tσ⁻¹σ 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, Şablon:Mset yer əvəzetməsidir; Şablon:Mset 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əsidir. Əgər σσ = σ olarsa, σ idempotent adlanır.^{[5]:73–74[6]:445–446}

Məsələn, Şablon:Mset ilə Şablon:Mset bərabərdir, lakin Şablon:Mset ilə eyni deyil.

Sitat səhvi: " note " adlı qrup üçün <ref> teqləri mövcuddur, lakin müvafiq <references group="note"/> teq tapılmadı