Formal definition of "$\Rightarrow$" relation (derivation relation) for context-free grammars

Question

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 \land\phi=\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.

Answer 1

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$.