Vtyjkyuk

This is probably more of a logic question.
I'm looking for formal definition of derivation relation for context-free grammars (CFGs). The books on subject tend to define derivation relation for CFGs in two ways (here I'm using "$rightarrow$" for material implication, "$mapsto$" for production relation and "$Rightarrow$" for derivation relation):

1. Let G(V, T, P, S) be a CFG, then:
   $$forall alpha (forall beta (forall gamma (forall A (alpha in (V cup T)^* land beta in (V cup T)^* land gamma in (V cup T)^* land A in V rightarrow quad ([A mapsto gamma] in P rightarrow [alpha A beta Rightarrow alpha gamma beta]) quad )))) $$


2. Let G(V, T, P, S) be a CFG, then:
   $$forall eta (forall phi(eta in (V cup T)^* land phi in (V cup T)^* land [eta Rightarrow phi] rightarrow quad (exists alpha (exists beta (exists gamma (exists A (alpha in (V cup T)^* land beta in (V cup T)^* land gamma in (V cup T)^* land A in V quad land [A mapsto gamma] in P land eta=alpha A beta landphi=alpha gamma beta))))) quad ))$$

The second definition is from Wikipedia (written in more cumbersome notation).Then there is a definition of reflexive transitive closure of =>:

Let G(V, T, P, S) be a CFG, then

• $forall alpha(alpha in (V cup T)^* rightarrow [alpha Rightarrow ^* alpha] )$


• $forall alpha(forall beta( forall gamma ( alpha in (V cup T)^* land beta in (V cup T)^* land gamma in (V cup T)^* rightarrow quad ([alpha Rightarrow ^* beta] land [beta Rightarrow gamma] rightarrow [alpha Rightarrow ^* gamma]) quad )))$

Now, in proofs regarding CFGs (for example, proof that if there is a derivation tree in G for $w$, then $S Rightarrow ^* w$) we use the following theorem:

Let G(V, T, P, S) be a CFG, then
$$forall eta (forall phi ( eta in (V cup T)^* land phi in (V cup T)^* land [eta Rightarrow phi] rightarrow quad (forall alpha (forall beta (alpha in (V cup T)^* land beta in (V cup T)^* rightarrow [alpha eta beta Rightarrow alpha phi beta])) ) quad ))$$

This theorem, as I understand it, describes the essence of "context-freeness": if we can derive one string from another, then we can perform such derivation in any surrounding context.

Now, to prove this last theorem, both definitions of => relation are used. I've tried to derive one definition from another, but failed.

The question is: are these two definitions equivalent, or the correct definition is actually a conjunction of these two?

Remark:
I've tried using mace4 to find counterexample and succeeded. Here are the definitions I used:

formulas(assumptions).
 % string axioms
 exists x (symbol(x)).

 string(e).
 all x (symbol(x) -> string(x)).
 all x (all y (string(x) & string(y) -> string(x + y))).

 all x (string(x) -> x = x).
 all x (string(x) -> x = x + e).
 all x (string(x) -> x = e + x).
 all x (
 all y (
 string(x) & string(y) -> (
 x = y -> (
 exists s (
 exists w (
 symbol(s) & string(w) & x = s + w & y = s + w
 )
 )
 )
 )
 )
 ).
end_of_list.

formulas(assumptions).
 exists s ( exists w (symbol(s) & string(w) & production(s, w))).

 all x (
 all y (
 string(x) & string(y) & derivation(x, y) -> (
 exists s (
 exists w (
 exists a (
 exists b (
 symbol(s) & string(w) & string(a) & string(b) & production(s, w) & x = (a + s) + b & y = (a + w) + b
 )
 )
 )
 )
 )
 )
 ).
end_of_list.

formulas(goals).
 all s (
 all w (
 all a (
 all b (
 symbol(s) & string(w) & string(a) & string(b) & production(s, w) -> (
 derivation((a + s) + b, (a + w) + b)
 )
 )
 )
 )
 ).
end_of_list.

Thank you for your time.

It is like the relation between an inference rule and the derivation concept in math logic.

An inference rule, like e.g. modus ponens is a single elementary inferential step.

The derivability relation holds between a formula $varphi$ and a set of formulas $Gamma$ (in symbols : $Gamma vdash varphi$) iiff we have a "chain" of elementary inferential steps (i.e. applications of the rules of inference) starting from the formulas in $Gamma$ (the assumptions or axioms) and ending with $varphi$.

In the field of Context-free grammar we have production rules :

a single elementary "transformational" step that licenses the transformation (replacement) of string $alpha$ with string $beta$.

In this case, we say that $alpha$ directly yields $beta$; in symbols :

$alpha Rightarrow beta$ (or, according to you : $alpha ↦ beta$).

And we have the repetitive application of production rules : $alpha Rightarrow^* beta$, meaning that there is a chain of applications of production rules starting with $alpha$ and ending with $beta$.

Having said that, a formal definition must be inductive :

$alpha Rightarrow^* beta$ iff :

either (i) there is a production rule $R$ such that $(alpha, beta) in R$, i.e. $alpha Rightarrow beta$,

or (ii) there is a string $gamma$ and a production rule $R$ such that :

$alpha Rightarrow^* gamma$ and $gamma Rightarrow beta$.