邏輯學
邏輯學（Logic）研究形式推理（Formal Reasoning）的結構。數理邏輯（Mathematical Logic）提供描述命題、推理規則與真值結構的形式系統，是離散數學（Discrete Mathematics）與理論電腦科學（Theoretical Computer Science）的重要基礎。
邏輯系統通常從四個層面理解：語法（Syntax）、語意（Semantics）、證明理論（Proof Theory）與模型理論（Model Theory）。語法描述公式的形式結構，語意定義公式在模型中的真值，證明理論研究形式推理，而模型理論分析邏輯系統的整體性質。
語法（Syntax）
語法（Syntax）描述合法公式（Well-formed Formula, WFF）的生成規則。此層面僅關注符號如何組合，不涉及公式的真值。
命題邏輯（Propositional Logic）
命題邏輯研究由命題變數與邏輯連接詞構成的公式系統。
命題變數
邏輯連接詞（Logical Connectives）
其中各連接詞語義如下。
否定（Negation）
表示命題 不成立。
合取（Conjunction）
表示命題 與 同時成立。
析取（Disjunction）
表示命題 或 至少一個成立。
蘊涵（Implication）
表示若 成立則 成立。
雙條件（Biconditional）
表示 與 具有相同真值。
若 為公式，則以下亦為合法公式：
謂詞邏輯（First-Order Logic）
謂詞邏輯（First-Order Logic）在命題邏輯的基礎上引入物件與關係，使邏輯能描述結構化命題。
變數（Variables）
量詞（Quantifiers）
全稱量詞（Universal Quantifier）
表示對所有 ，命題 成立。
存在量詞（Existential Quantifier）
表示至少存在一個 使 成立。
若 為公式，則
亦為合法公式。
語意（Semantics）
語意（Semantics）定義公式在某個詮釋或模型中的真值。
命題邏輯語意（Propositional Semantics）
命題邏輯透過真值指派（Truth Assignment）定義語意。
其中
-
表示真（True）
-
表示假（False）
語意蘊涵（Semantic Entailment）描述在所有滿足前提的情況下結論必然成立。
表示在所有使 為真的真值指派下，公式 亦為真。
謂詞邏輯語意（First-Order Semantics）
在謂詞邏輯中，真值依賴於模型（Model）的結構。
模型定義為
其中
-
為論域（Domain）
-
為詮釋函數（Interpretation）
詮釋函數將符號映射到論域中的物件或關係。
滿足關係（Satisfaction Relation）
表示公式 在模型 中成立。
證明理論（Proof Theory）
證明理論（Proof Theory）研究形式推導與可證性。此領域關注如何透過推理規則從前提集合導出結論，而不直接依賴語意解釋。
形式可證性（Provability）
表示公式 可以由前提集合 透過推理規則導出。
一個基本推理規則為假言推理（Modus Ponens）。
若 與 為真，則可推出 。
模型理論（Model Theory）
模型理論研究邏輯語言與其數學結構之間的關係。其核心問題在於公式在不同模型中的成立條件。
滿足關係
描述公式 在模型 中是否成立。
在此框架下，可以研究邏輯語言在不同結構中的可滿足性與可表達能力。
元性質（Meta-properties）
元性質（Meta-properties）描述整個邏輯系統在語法與語意之間的關係。
正確性（Soundness）
若某公式在系統中可被證明，則其在所有模型中皆為真。
完備性（Completeness）
若某公式在所有模型中皆為真，則其可以被形式系統證明。
可滿足性（Satisfiability）
若存在某個真值指派使公式成立，則該公式為可滿足。
命題邏輯中的可滿足性問題（Boolean Satisfiability Problem, SAT）是計算理論與自動推理的重要研究問題。
計算邏輯（Computational Logic）
計算邏輯（Computational Logic）研究如何將邏輯推理轉化為可計算問題，是人工智慧（Artificial Intelligence）與自動推理系統的重要基礎。
命題邏輯可滿足性問題定義為
此問題詢問是否存在真值指派使公式 為真。
SAT 問題是計算複雜度理論中的核心問題之一，並在形式驗證（Formal Verification）、知識表示（Knowledge Representation）與自動定理證明（Automated Theorem Proving）等領域具有重要應用。
