12. Computational content of classical proofs

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

1

,…,G

n

we can derive in minimal logic augmented with a special predicate variable 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

and goal formulas

we can derive in minimal logic

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

In particular, substitution of the formula

for X yields a derivation in intuitionistic logic of

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)