L9

Question 1

Outline CHC for STLC and PLC

Answer 1

232

Question 2

IPL rules

Answer 2

233-235

(1) Truth
(2) Falsehood + disjunction

Remember both elimination and introduction rules.

No separate true/false relations

Remember the case-typing like rule for disjunction elimination

Question 3

Calculus of truth and falsehoods - propositions, true contexts, false contexts, proofs, refutations, contradictions (and their SEMANTIC MEANINGS), treatment of negation.

Answer 3

236

no implication

negation is primitive

Question 4

Proofs in CTF (rules for deriving F; D |- A true)

Answer 4

237

Question 5

Refutations in CTF

Answer 5

238

Question 6

CHC given CTF (table of connective, what to do to prove, and how to refute). Explain why this is still intuitionistic.

Answer 6

239

Question 7

Proof of A => not not A in CTF

Answer 7

240

Question 8

Why can’t we prove not not A implies A in CTF

Answer 8

241

Question 9

Why can’t we prove A and B entails A

Answer 9

242,

it’s Intuitionistically valid though

Question 10

Proof by contradiction principle

Answer 10

243

Question 11

Contradiction rule

Answer 11

244

A contradiction arises when a proposition has both a proof and a refutation

Question 12

Proof of DNE in CTF+contra=ClassicalLogic

Answer 12

245

Question 13

Proof of A.B => A in CLogic

Answer 13

246

Question 14

Proof of A+B false => A false in CL

Answer 14

247

Question 15

Proof of law of EM in CL

Answer 15

248

• uses the lemma A.B false => A false.

Question 16

Syntax of proof and refutation terms in CL

Answer 16

249

(propositions, true contexts, false contexts, values, continuations, contradictions)

Note the correspondence between each of these terms and their corresponding rules in CTF+contra

with the mu-terms corresponding to the two ways of using proof by contradiction

Question 17

Proof terms rules in CL (typing)

Answer 17

250

Question 18

Continuation terms rules in CL (typing)

Answer 18

251

Question 19

Contradictions terms rules in CL (typing)

Answer 19

252

Question 20

Op sem of ClassLogic

Answer 20

253

Question 21

Classical STLC - how is it nondeterministic?

Answer 21

254

Question 22

Substitution lemmas in STLC+CL

Answer 22

255

Question 23

Purpose of proof theory for STLC

Answer 23

256

Question 24

1. Show that ¬A ∨ B,A;· ⊢ B true is derivable

Answer 24

257

Question 25

2. Show that ¬(¬A ∧ ¬B); · ⊢ A ∨ B true is derivable

Answer 25

257

Question 26

3. Prove substitution for values (you may assume exchange and weakening hold).

Answer 26

257