[next] [prev] [prev-tail] [tail] [up]

12. Computational content of classical proofs

Classical

This section is based on [3]. We restrict to formulas in the language {⊥,→,∀} in this section, and - as in the paper - make use of a special nullary predicate variable X.

A formula is relevant if it ends with (logical) falsity. Definite and goal formulas are defined by a simultaneous recursion, as in [3].

(atr-relevant? formula)
(atr-definite? formula)
(atr-goal? formula)
To implement [3, Lemma 3.1], we need to construct proofs from formulas:
ND: ((D →⊥) → X) → DX for D relevant
MD: D → DX
KG: G → GX for G irrelevant
HG: GX → (G → X) → X
This is done by
(atr-rel-definite-proof formula)
(atr-arb-definite-proof formula)
(atr-irrel-goal-proof formula)
(atr-arb-goal-proof formula)
Next we need to implement [3, Lemma 3.2], which says that for goal formulas G⃗ = G1,…,Gn we can derive in minimal logic augmented with a special predicate variable X
X (⃗G → X) → ⃗G → X.

In our implementation this function is called

(atr-goals-to-x-proof goal1 ...)
Finally we implement [3, Theorem 3.3], which says the following. Assume that for definite formulas D⃗ and goal formulas ⃗G we can derive in minimal logic
D⃗ → (∀⃗y.⃗G → ⊥) → ⊥.

Then we can also derive in intuitionistic logic augmented with the special predicate variable X

D⃗ → (∀⃗y.⃗G → X) → X.

In particular, substitution of the formula

⃗ ∃⃗y.G := ∃ ⃗y.G1 ∧ ⋅⋅⋅∧ Gn

for X yields a derivation in intuitionistic logic of

⃗D → ∃⃗y.⃗G.

This is done by

(atr-min-excl-proof-to-x-proof min-excl-proof)
(atr-min-excl-proof-to-intuit-ex-proof min-excl-proof)

[next] [prev] [prev-tail] [front] [up]