Propositional logic talks about Boolean combinations of propositions and inferences we can make about them.
- ¬（非）、∨（或）、∧（与）
- ⊢（推出，inference）
→（蕴含，implication）
p → q 表示命题 p 蕴含命题 q，其中 p 是蕴含式的假设（前提条件），q 是蕴含式的结论（逻辑结论）。
- If I won the lottery last week, then I purchased a lottery ticket
p | q | p → q |
T | T | T |
T | F | F |
F | T | T |
F | F | T |
蕴含可以理解为一个承诺或保证
- 如果 p 为真，且 q 也为真，那么这个保证被满足了，所以 p → q 是真。
- 如果 p 为真，但 q 为假，那么这个保证被违背了，所以 p → q 是假。
- 因为承诺了如果 p 发生，q 也会发生，但实际上并没有。
- 如果 p 为假，不论 q 是否为真，这个保证并没有被违背，所以 p → q 是真。
- 因为只承诺了“如果 p 发生”，而 p 并没有发生，所以不论 q 是什么状态，承诺都没有被触犯。
自然演绎
Natural deduction rules
- Use elimination rules to breakup the hypothesis
根据已有的假设来推导出新的结论
- Use introduction rules to form th e goal
引入一个假设用于后续的推导
Above the line are the premises of the rule. Below the line goes the conclusion.
The rule for conjunction
Our first rule is called the rule for conjunction (∧) and-introduction.
It allows us to conclude φ ∧ ψ, given that we have already concluded φ and ψ separately. We write this rule as:
For each of the connectives, there is one or more rules to introduce it and one or more rules to eliminate it.
The rules for and-elimination are these two:
Example: Prove that is valid.
The rule of double negation
Intuitively, there is no difference between a formula φ and its double negation ¬¬φ, which expresses no more and nothing less than φ itself.
The sentence ‘It is not true that it does not rain.’ is just a more contrived way of saying ‘It rains.’ Conversely, knowing ‘It rains,’ we are free to state this fact in this more complicated manner if we wish.
Thus, we obtain rules of elimination and introduction for double negation:
Example: Prove that is valid.
The rule for eliminating implication
This rule states that, given φ and knowing that φ implies ψ, we may rightfully conclude ψ.
The latter is one of the best known rules of propositional logic and is often referred to by its Latin name modus ponens.
In our calculus, we write this as:
Example: Prove that is valid.
The hybrid rule Modus Tollens
Let us see an example of this rule in the natural language setting:
‘If Abraham Lincoln was Ethiopian, then he was African. Abraham Lincoln was not African; therefore he was not Ethiopian.’
Example: Prove that is valid.
The rule implies introduction
It says: in order to prove , make a temporary assumption of φ and then prove ψ.
The rule for negation
⊥ itself represents a contradiction
Example: Prove that is valid.
The rule for disjunction
We may conclude ‘φ or ψ’ if we already have ψ.
Now let’s consider or-elimination.
- First, we assume φ is true and have to come up with a proof of χ.
- Next, we assume ψ is true and need to give a proof of χ as well.
- Given these two proofs, we can infer χ from the truth of φ ∨ ψ, since our case analysis above is exhaustive.
Example: Prove that is valid.
