Dubbio sulla scrittura di una affermazione in logica predicati

[astrifiammante]

Un saluto a tutto il forum. Ho una domanda stupida (visto che non sono uno specialista di logica). L'assioma:

Se due punti stanno sulla stessa retta e giacciono entrambi sullo stesso piano allora tutti i punti della retta giacciono su quel piano

si può tradurre con la seguente dicitura?

$$\forall A,B(A\neq B \land \mathcal{G}(A,r) \land \mathcal{G}(B,r)\land \mathcal{G'}(A,\alpha) \land \mathcal{G'}(B,\alpha)\to (\forall P (\mathcal{G}(P,r)\to\mathcal{G'}(P,\alpha))) $$


ove $ \mathcal{G}(A,r)$, $ \mathcal{G'}(A,\alpha)$ sono rispettivamente le relazioni $A$ giace su $r$ e $A$ giace su $\alpha$. Non ho usato quantificatori su $r$ ed $\alpha$ perchè le ho considerate costanti. In oltre la loro esistenza non va denunciata visto che avevo già fatto in precedenza uso degli assiomi come

per due punti passa una ed una sola retta

. Oppure, se devo usare i quantificatori anche su queste due variabili:

$$\forall A,B( A\neq B\land \exists r(\mathcal{G}(A,r) \land \mathcal{G}(B,r)) \land \exists \alpha(\mathcal{G'}(A,\alpha) \land \mathcal{G'}(B,\alpha))\to(\forall P (\mathcal{G}(P,r)\to\mathcal{G'}(P,\alpha)) )$$

Però così non mi tornano i campi dei quantificatori esistenziali..............perchè dopo l'implicazione che porta a per ogni $P$ , $r$ ed $\alpha$ sono fuori dai loro campi di azione.

[astrifiammante]

Forse ho risolto:

$$ \forall r, \alpha ( \exists A,B (A\neq B \land \mathcal{G}(A,r)\land\mathcal{G}(B,r)

\land\mathcal{G'}(A,\alpha)\land\mathcal{G'}(B,\alpha))\to\forall P(\mathcal{G}(P,r)\to\mathcal{G'}(P,\alpha)) )$$

In tal modo tutti gli scope tornano. Esatto?