语法树

• 符号

  • 非逻辑符号 $\mathcal{L}$
    • 个体常量
    • 谓词符号
    • 函数符号
  • 逻辑符号
    • 个体变量 $V$
    • 逻辑运算符
    • 量词符号
    • 辅助符号: 逗号，括号

• 项

  • 归纳基: 个体常量 $\left{c\right}$ $\cup$ 个体变量$V$
  • 归纳步: $t_{1}, t_{2}, \dots,t_{n}$ 是项 $\Rightarrow$ 函数 (不含谓词) $f(t_{1}, t_{2}, \dots,t_{n})$ 是项

• 一阶逻辑公式

  • 归纳基: 原子公式 $:=$ $t_{1}, t_{2}, \dots,t_{n}$ 是项 $\Rightarrow$ 谓词 $F(t_{1}, t_{2}, \dots,t_{n})$ 是原子公式
  • 归纳步: apply 逻辑运算符 $\cup$ 量词运算符 on 公式 $\Rightarrow$ 公式

• 子公式 $:=$ 自身 $\cup$ 逻辑运算符/量词运算符の操作数の子公式

个体变量语义

• 量词辖域 $:=$ $\forall x(辖域)$ or $\exists x(辖域)$
• 变量语义
  • 局部 (辖域内)
    • 自由变元
    • 约束变元
  • 全局
    • 自由变量 $:=$ 存在出现是自由出现
    • 约束变量 $:=$ 任意出现是约束出现
    • 句子/闭公式 $:=$ 任意变量是约束变量