语法分析树的图论类型界定及形式化定义以支撑合式公式证明的技术问询
我最近在梳理合式公式（WFF）的形式化定义，卡在了语法分析树的图论建模环节——想把这个直觉上的树结构转化为严谨的数学定义，好支撑后续“WFF等价于拥有合法解析树的字符串”这个命题的证明。先给大家举个具体的例子来展开：
考虑字符串 $((A\lor B)\lor A)$，我们能画出一棵非正式的解析树，每个节点对应一个子公式：
- 根节点是完整公式
$(A \lor B) \lor A$，它有两个子节点：$(A\lor B)$和$A$ - 左子节点
$(A\lor B)$又有两个子节点：$A$和$B$
按层级划分的话：根节点在第0层，$(A\lor B)$ 和 $A$ 在第1层，$A$ 和 $B$ 在第2层。
核心建模困惑
现在我想把这个结构用数学图来精确表示，遇到两个关键问题：
- 子节点的有序性：第1层的两个节点必须有明确的顺序——
$(A\lor B)$要在$A$前面，但我觉得不需要整个图是全序的，只需要每个节点的子节点集合是有序的就行。 - 重复公式的节点处理：字符串里的
$A$出现了两次，如果把节点看作普通集合的元素，那么从根节点指向$A$的边，和从$(A\lor B)$指向$A$的边，会指向同一个$A$节点。这时候用普通集合定义节点就不合适了，可能需要多重集合或者带标记的集合？
合式公式的定义背景
先明确一下我目前用的WFF定义：
- 字母表包含原子符号
$A, B, C, \ldots$和连接符$\lor, \land, \implies, \lnot$ - 所有符号的任意拼接构成字符串集合
$\textbf{STR}$ - 有一系列生成连接式的函数，比如析取函数：
$$
\begin{align}
f_{\lor}: \textbf{STR} \times \textbf{STR} &\to \textbf{STR}\
(A, B) &\mapsto (A\lor B)
\end{align}
$$
这类函数（$f_{\lor}, f_{\land}, f_{\implies}, f_{\lnot}$）被收集在集合$\mathcal{F}$中，原子符号集合$\mathcal{A}\subset \textbf{STR}$。
WFF被定义为 $\mathcal{A}$ 在 $\textbf{STR}$ 中关于 $\mathcal{F}$ 的归纳闭包。
我的核心目标
我想证明：WFF中的元素，恰好是那些拥有合法解析树的字符串，其中解析树需要满足两个核心条件：
- 根节点对应的字符串等于该WFF元素
- 每个节点要么是原子符号（无子女），要么是某个函数
$f\in \mathcal{F}$作用于其有序子节点元组的结果
但现在的问题是，我没法精准定义这个“语法解析树”的结构，所以想请教大家。
我初步探索的三种思路
我自己琢磨了几个方向，但都觉得不够完善，想请大家帮忙打磨成严谨的定义：
思路一：带节点顺序标记的根有序有向树
给每个节点分配一个整数标记，让标记的顺序和子公式在字符串中的左右顺序对应。比如根节点标记0，第1层的$(A\lor B)$标记1，$A$标记2，第2层的$A$标记3，$B$标记4。
缺点：标记顺序不一定唯一，需要额外约定来固定规范顺序，有点“过度设计”的感觉，而且没直接解决重复公式的节点问题。
思路二：双标记的根有向树
给每个节点加两个标记：
- 第一个标记用来区分同一公式的不同出现（比如把例子里的两个
$A$标记为$A_1$和$A_2$，$B$标记为$B_1$） - 第二个标记用来指定同一父节点下子节点的左右顺序，由此在节点集合上诱导出一个偏序，足以对应字符串里的子公式顺序。
特点：更贴合直觉，能明确区分重复出现的子公式，但额外增加了不少结构，显得有点繁琐。
思路三：带边标记的根有向多重图
放弃严格的树结构，改用有向图：
- 有唯一的根节点（无父节点），子节点可以有多个父节点（对应同一子公式被多次引用）
- 给边加标记，比如
$(A\lor B)$指向$A$的边标记1，指向$B$的边标记2；对于$(A\lor A)$，父节点会有两条边指向$A$，分别标记1和2 - 还可以给节点额外标记：根节点标记为
$((A\lor B), f_{\lor})$，叶子节点标记为$(A, \mathcal{A})$或$(B, \mathcal{A})$，明确节点对应的公式和生成方式。
特点：边标记能直接对应生成函数的输入元组顺序，辅助后续的证明，但需要定义“根有向部分边有序多重图”这类结构，术语上有点绕，不确定是不是标准做法。
求助需求
我刚接触这个领域，可能漏掉了一些标准术语或者现成的定义。想请大家帮忙：
- 把上面的思路精准化，给出严谨的形式化定义
- 告诉我有没有标准的术语来描述这类语法解析树
- 如果有相关的参考资料（比如逻辑教材、形式语言文献里的定义）也请推荐一下
备注：内容来源于stack exchange，提问作者Jagerber48
