Extra Logic Practice

In today's brief lab, we'll continue practicing the skill of applying the rules of natural deduction to write rigorous, low-level proofs.

Note: this "lab" is not due, but will be good practice as you prep for the exam on Friday.

Problem: Logic Practice

For each claim:

  • In a sentence, describe what the claim is saying. Your description should be in the rough form "under assumptions ... we must show that ... ." You can reference the atomic propositions in the claims directly in your description, i.e., you don't need to instantiate the proof state into a real-world context.

  • Now instantiate the claim using real-world statements like "the sun is shining" or "it is cold outside" or "pigs can fly". Try to pick statements that make sense in the context of the claim itself, what is being assumed, and what you are trying to prove.

  • Finally, give a rigorous, natural deduction-style proof of the claim.

Claim 1

.

"Given that I know ( OR ) and I know ( OR ), I can deduce OR ( AND )."

"The sun is shining."
"It is nighttime."
"It is dark outside."
"I know that the sun is shining or it is nighttime, and I know that the sun is shining or it is dark outside. So I know that the sun is shining or it is nighttime and dark outside."

Strategy for proof:

  • We have 2 ORs on the left-hand-side that will need to be eliminated.
  • There is an OR and an AND that may need to be introduced.
  • Idea: eliminate the first of the LHS ORs ). We get on one side, which will let us OR-intro the full RHS expression. For the on the other side of that OR, we can use the other LHS OR to help!

Proof

Claim: .

(1) [given]
(2) [given]

(3) [assume for -elim 1]
(4) [-intro 3]

(5) [assume for -elim 1]

(6) [assume for -elim 2]
(7) [-intro 6]

(8) [assume for -elim 2]
(9) [-intro 5, 8]
(10) [-intro 9]

(11) [-elim 2, 6-7, 8-10]

(12) [-elim 1, 3-4, 5-11]


Claim 2

.

"Given that implies implies , we can prove that and together imply ."

"I am not paying attention."
"The ice is slippery."
"I will fall down."
"I know that if I am not paying attention, it means that if the ice is slippery then I will fall down. So I can deduce that if I am not paying attention when the ice is slippery, then I will fall down."
"I know that if I am not paying attention, then I will fall down if the ice is slippery. So I can deduce I will fall down if I am not paying attention when the ice is slippery."

Strategy for proof:

  • There are 2 arrows on the LHS, but they can't be eliminated yet.
  • But there is an arrow on the RHS out the outer level that can be introduced. So introduce that arrow by assuming .
  • Now using -elim will give us and , which will let us eliminate the LHS arrows to get .
  • We assumed and got , so we can finally introduce that RHS arrow!

Proof

Claim: .

(1) [given]

(2) [assume for intro]
(3) [-elim 2]
(4) [elim 1, 3]
(5) [-elim 2]
(6) [elim 4, 5]

(7) [intro 2-6]


Claim 3

.

"Given that implies or , I can deduce that either implies , or implies ."

"It is nighttime."
"The sun has set."
"Pigs can fly."
"I know that if it is nighttime, then either the sun has set or pigs can fly. Then I can deduce that either (i) if it is nighttime, then the sun has set; or (ii) if it is nighttime, then pigs can fly."

Strategy for proof:

  • We can't do any eliminations at the start because we can't use the arrow on the LHS yet.
  • The outermost operation on the RHS is an OR, so we will be using OR intro somewhere. How? We need to show the left or right side of that OR.
  • Those both have arrows, so let's target an arrow intro. Oh look: they both require assuming !
  • That will let us elim the LHS arrow, giving us . An OR elim will be next.
  • In one case, we'll get . In the other case, we'll get . Those aren't the same...
  • But wait! Our goal is to OR these together. So in each case, we can use an OR-intro to get to the goal at the end!

Proof

Claim: .

(1) [given]

(2) [assume for intro]
(3) [elim 1, 2]

(4) [assume for -elim 3]
(5) [intro 2-3, 4]
(6) [-intro 5]

(7) [assume for -elim 3]
(8) [intro 2-3, 7]
(9) [-intro 8]

(10) [-elim 3, 4-6, 7-9]