計算機科學家邏輯/命題邏輯/語法

語法

為了定義語法，我們必須假設一組原子公式，作為歸納定義的起點。藉助三個連線詞和括號作為標點符號，我們歸納定義了更復雜的公式。

定義 1（命題邏輯的語法）

假設一個

• 可數的原子公式集 $P_{i}$，其中 $i=1,2,3,\cdots$，
• 連線詞 $\land ,\lor$ 和 $\lnot$，
• 標點符號 $($ 和 $)$。

命題公式集由以下歸納定義

• 原子公式是公式。
• 如果 $F$ 和 $G$ 是公式，則 $(F\land G)$ 和 $(F\lor G)$ 是公式。
• 如果 $F$ 是一個公式，則 $\lnot F$ 是一個公式

不同型別的公式被稱為合取、析取和否定。注意，這僅僅是對措辭的一種約定，到目前為止，我們沒有對這些連線詞給出任何語義，以證明這些名稱是合理的。

這個公式集的定義也以一種非常自然的方式引入了一個偏序，如果我們考慮子公式的概念。

定義 2（子公式）

公式的子公式是一個子串，它本身也是一個公式。

注意，關係“是子公式”確實是一個偏序。

公式集與子公式關係是一個良基關係。

為了簡化符號，我們引入以下縮寫

$A,B,C$ 代替 $P_{1},P_{2},P_{3}$

$(F_{1}\to F_{2})$ 代替 $(\lnot F_{1}\lor F_{2})$

$(F_{1}\leftrightarrow F_{2})$ 而不是 $((F_{1}\land F_{2})\lor (\lnot F_{1}\land \lnot F_{2}))$

$\bigvee _{i=1}^{n}~F_{i}$ 而不是 $(\cdots ((F_{1}\lor F_{2})\lor F_{3})\lor \cdots \lor F_{n})$

$\bigwedge _{i=1}^{n}~F_{i}$ 而不是 $(\cdots ((F_{1}\land F_{2})\land F_{3})\land \cdots \land F_{n})$

這些符號（除了第一個）只是簡單的縮寫；當這些箭頭符號或索引連線詞出現在公式中時，相應的子公式可以根據此定義進行替換。

回到我們之前的例子，您可以看到

$\lnot (ab(or1))\to high(or1,o)\leftrightarrow (high(or1,i1)\lor high(or1,i2))$

可以根據上述定義透過引入括號寫成公式

$(\lnot (ab(or1))\to (high(or1,o)\leftrightarrow (high(or1,i1)\lor high(or1,i2))))$

引入括號是為了避免任何歧義。為了提高可讀性，只要有可能，我們將省略它們。如果我們另外應用上述縮寫規則，我們將得到以下公式
$(\lnot \lnot (ab(or1))\lor$

$(high(or1,o)\land ((high(or1,i1)\lor high(or1,i2))\lor$

$(\lnot high(or1,o)\lor \lnot (high(or1,i1)\lor high(or1,i2))))))$