Propositional Logic Reasoning

Administration

Already familiar with the idea
- "If you know this and this, then you know that."
- High school geometry structures proofs this way, especially. You've used it in class discussion.
- We're simply formalizing such rules.
Two kinds of rules:
- "Basic" inference rules,
- Theorems/lemmas — i.e., combinations of the basic rules that we've previously proven valid
Theorems/lemmas are very important, as they let us structure proofs in larger units. But since that is familiar, we will focus on the "basic" inference rules.
Example inference rule
- If you have proved (or are given) a ⇒ b and a, what also should hold?
- Better: Use meta-variables instead.
- What's an example use of this in WaterWorld?
- One of the most obvious inference rules -- Called modus ponens or if-elimination
- Notice the two levels of "if" -- one proof-level and one formula-level -- Will introduce notation to avoid confusion
Some other simple inference rules
- Given φ and ψ, what also do you know?
- Given φ ∧ &psi, what also do you know?
- What corresponding rules hold for ∨?
- Hmmm, or-elimination isn't obvious… We'll come back to that. (Students might come up with case-elimination, however.)
- What do we need to know to claim ¬¬φ?
This is just a sampling. See online text for more.

Premises
- Almost any proof starts with some premises.
- Notation: (premises) ⊢ (conclusion)
- Read as the promises "proves" or "entails" the conclusion.
- The symbol ⊢ is called a turnstile.
φ ∧ ψ ⊢ ¬¬ ψ
- Steps needed to prove?
  - For each step, cite rule and previous results used. This is one way to write a proof, and what we'll use for now.
  - A proof is not just for convincing yourself, but also for convincing others. Make the proof easy to understand!
- Since we used meta-variables, really proves an infinite number of similar things simultaneously.
Slight variation: φ, ψ ⊢ ¬¬ ψ
- Here have two premises. In previous example, had one.
- Don't have to use all the premises.
φ ∧ ψ ⊢ ψ ∧ φ
- Have chosen not to include inference rules for commutativity, although including them would also make sense.
φ ∨ ψ ⊢ ψ ∨ φ
- We get stuck!

Clearly don't have all our inference rules yet.

Put more simply, we don't have "enough" inference rules.
The inference rules (so far) are incomplete — we can't prove everything that is true.
Clearly, we want a proof system that is complete.
Knowing whether a proof system is complete is difficult — such results can be proven, but that's beyond the scope of this course.

Can we have "too many" inference rules?

Some may be redundant. That's fine. They just provide us alternate ways to prove things.
Some may be invalid! Can "prove" false things! Proof system is unsound.
Clearly, we want a proof system that is sound.

Now, for a sampling of the remaining inference rules.

or-elimination
reduction ad absurdum (reduction to absurdity)
- If you know ¬φ ⊢ false then you can conclude φ.
- "Proof by contradiction"
if-introduction:
- If you know α, …, β ⊢ γ then you can conclude (α ∧ … ∧ β) → γ.
- Moves the "implication" from the level of proof premise/conclusion to within a single formula.
- A subtle, but important distinction.
Again, here's the full list.

First day ended roughly here.

¬(φ ∨ ψ) ⊢ ¬(ψ ∨ φ)
- Use previous results.
modus tollens: φ ⇒ ψ, ¬ψ ⊢ ¬φ
One direction of contrapositive: ¬ψ ⇒ ¬φ ⊢ φ ⇒ ψ
- Possible to also show φ ⇒ ψ ⊢ ¬ψ ⇒ ¬φ. Thus, the two formulas are equivalent. To show equivalences here, must show both directions!
H-has-2 ∧ J-safe ⊢_W G-unsafe
- That subscript "W" is just shorthand to say that really all the WaterWorld axioms are also premises. Usually omit, since clear from context.
- First, draw board and do informal reasoning.
Show B-safe,B-has-0,C-safe,C-has-1,H-safe,H-has-0 ⊢_W D-unsafe.

Define logics, like we've been doing.
Basis of one style of theorem provers
Define type systems
- E.g., given f:S→T and x:S, conclude f(x):T
- Just another "logic" for proving things
One way to define semantics of programming languages