Formal Proof in Logic
Models in Propositional Logic
在命题逻辑中，模型非常直接。一个模型就是对公式中每个命题变量的一个赋值，即指定每个变量是真是假。
例如， (A ∧ B) → C
一个可能的模型是：A = true，B = true，C = true，在这个模型中，公式为真。
A formula in logic is
- satisfiable if it is true in some model
- valid if it is true in every model
- unsatisfiable if it is false in every model
Models in Predicate Logic
在谓词逻辑（中，模型的概念更加复杂，因为它不仅涉及变量的真值赋值，还涉及对域中元素的解释以及函数和关系的解释。一个谓词逻辑的模型必须提供：
- A set corresponding to each set name
- 域，讨论的对象的集合。
- An element of a set corresponding to each constant symbol
- 每个个体常量的解释，将其指派给域中的一个元素。
- A function corresponding to each function symbol
- 每个n元谓词的解释，将其指派为在域中元素上的一个n元关系。
- A relation corresponding to each predicate name
- 每个n元函数符号的解释，将其指派为在域中元素上的一个n元函数。
例如，∀x(p(x)→Q(x))。P(x) : “x是偶数”，Q(x): “x大于0”。
一个可能的模型可能具有域 {1, 2, 3}，在这个模型中，公式为真。
If any model makes all of H1 , H2 , …, Hn true then it will also make G true.
- The symbol is pronounced “models”, and the relationship is sometimes called semantic entailment.
- A set of formulae { H1 , H2 , …, Hn } are said to be consistent if they have at least one model, and inconsistent or contradictory if they have no models .
- 如果一组公式是不一致的，即没有任何模型能够使得所有公式同时为真。
Equisatisfiable
如果公式 X 可满足，那么必须存在至少一个解使得公式 Y 也可满足。
同样的，如果公式 Y 可满足，那么必须存在至少一个解使得公式 X 也可满足。
但是，这并不意味着这两个公式是等价的，只是它们是否可以被满足这个条件是相同的。
- Equisatisfiability is weaker than equivalence.
E.g., If X and Y are equisatisfiable, are they equivalent?
- X and Y are both satisfiable with the Model M .
- Therefore,X and Y are equisatisfiable but they are not equal.
Proof systems
（用来描述和评估逻辑系统或证明系统质量和能力）
- A proof system is sound if it only allows us to prove things which are actually true.
- A proof system is complete if it allows us to prove all things which are actually true.
- A proof system is consistent if it never allows us to prove both φ and ¬φ for any formula φ
- A proof system is decidable if we can implement an algorithm* which, when given a formula φ as input will answer “yes” if φ is provable and “no” otherwise.
- Finding such an algorithm was called the Entscheidungs problem.