Propositional Logic: Syntax, Semantics, Natural Deduction

Alphabet for Propositional Logic

• List of logic symbols - Wikipedia

Symbol
$\wedge$	and	conjunction
$\vee$	or	disjunction
$⟹$	if...then...	implication
$\mathrm{\neg }$	not	negation
$⟺$	iff(if and only if)	equivalence, bi-implication
$\mathrm{\perp }$	falsity	falsum, absurdum. 永远为F
$\mathrm{\top }$		always true
$\mathrm{\forall }$		for all
$\mathrm{\exists }$		exists
$⊢$		$A⊢B$ says “$B$ is a theorem of $A$”. In other words, $A$ proves $B$ via a deductive system.
$\models$		$A\models B$ “in every model, it is not the case that $A$ is true and $B$ is false”
$⊬$		$A⊬B$ says “$B$ is not a theorem of $A$”. In other words, $B$ is not derivable from $A$ via a deductive system.
$⊭$		says “$A$ does not guarantee the truth of $B$ ”. In other words, $A$ does not make $B$ true.

• Given a formula $G$ and an interpretation $I$, if $G$ is true under $I$, we say that $I$ is a model for $G$. 可以记作 $I\models G$
• Valid : also called Tautology，在所有interpretation下都为真。F is valid 记作 $\models F$
• inconsistency: 在所有interpretation下都为F
• invalid: 至少一种interpretation为F
• conjunctive normal form（CNF），交集符号相连的literal，CNF中的这些literal叫做clause
• disjunctive normal form （DNF），并集符号相连的literal
• 
• $\mathrm{\Gamma }⊢\phi$意为从$\mathrm{\Gamma }$推导出$\phi$. If there exists a derivation with hyposthesis (premises) $\mathrm{\Gamma }$ and conclusion $\phi$ . When $\mathrm{\Gamma }=\varphi$ we say that $\phi$ is a theorem.
• $\mathrm{\Gamma }$ is consistent if $\mathrm{\Gamma }⊬\mathrm{\perp }$
• $\mathrm{\Gamma }$ is inconsistent if $\mathrm{\Gamma }⊢\mathrm{\perp }$

Logic and Calculus: Resolution for propositional logic

• soundness：$\varphi ⊢\rho ⟹\varphi \models \rho$ ,可靠性（正确性），如果某个公式能在推理系统中被证明，那么它在所有模型中都是真的
• completeness：$\varphi \models \rho ⟹\varphi ⊢\rho$ ,完备性，如果某个公式能在推理系统中被证明，那么它在所有模型中都是真的
• The idea is to work by contradiction（反证）, i.e. to use refutation: Theory united with negated consequence must be unsatisfiable.
  • example：为了证明$\mathrm{\Gamma }\models \phi$ 可以转而证明 $\mathrm{\Gamma }\models \phi \text{iff}\mathrm{\Gamma }\cup \{\mathrm{\neg }\phi \}\text{ is unsatisfiable}$ 或者写成 $\mathrm{\Gamma }\models \phi \text{iff}⊭\mathrm{\Gamma }\wedge \{\mathrm{\neg }\phi \}$
  • 反驳方法是：
    1. 把 $\mathrm{\Gamma }$ 的所有公式 + $\mathrm{\neg }\phi$ 写成一个集合
    2. 转成 CNF
    3. 看它是否 unsatisfiable
    4. 如果能推导出空子句（contradiction），说明集合不可满足
    5. 因此 $\phi$ 必然成立
• 
• 

First Order Logic