Changes

As noted above, it is usual to express the condition <math>(X, Y) \in \mathfrak{K}</math> by writing <math>X :> Y \, \text{in} \, \mathfrak{G}.</math>

As noted above, it is usual to express the condition <math>(X, Y) \in \mathfrak{K}</math> by writing <math>X :> Y \, \text{in} \, \mathfrak{G}.</math>

This relation is indicated by saying that <math>W\!</math> ''immediately derives'' <math>W',\!</math> by saying that <math>W'\!</math> is ''immediately derived'' from <math>W\!</math> in <math>\mathfrak{G},</math> and also by writing:

The immediate derivation relation is indicated by saying that <math>W\!</math> ''immediately derives'' <math>W',\!</math> by saying that <math>W'\!</math> is ''immediately derived'' from <math>W\!</math> in <math>\mathfrak{G},</math> and also by writing:

{| align="center" cellpadding="8" width="90%"

{| align="center" cellpadding="8" width="90%"

|}

|}

A ''derivation'' in <math>\mathfrak{G}</math> is a finite sequence <math>(W_1, \ldots, W_k)\!</math> of sentential forms over <math>\mathfrak{G}</math> such that each adjacent pair <math>(W_j, W_{j+1})\!</math> of sentential forms in the sequence is an immediate derivation in <math>\mathfrak{G},</math> in other words, such that:

A "derivation" in !G! is a finite sequence (W_1, ..., W_k)

of sentential forms over !G! such that each adjacent pair

(W_j, W_(j+1)) of sentential forms in the sequence is an

immediate derivation in !G!, in other words, such that:

W_j ::> W_(j+1), for all j = 1 to k-1.

| <math>W_j ::> W_{j+1},\ \text{for all}\ j = 1\ \text{to}\ k - 1.</math>

If there exists a derivation (W_1, ..., W_k) in !G!,

If there exists a derivation (W_1, ..., W_k) in !G!,

one says that W_1 "derives" W_k in !G!, conversely,

one says that W_1 "derives" W_k in !G!, conversely,