数理解析研究所講究録
1021 巻 1997 年 28-47

28Classical$\mathrm{B}\mathrm{r}\mathrm{o}\mathrm{u}\mathrm{w}\mathrm{e}\Gamma^{-\mathrm{H}\mathrm{e}\mathrm{y}}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}-\mathrm{K}\mathrm{o}\mathrm{l}\mathrm{m}\mathrm{o}\mathrm{g}_{0\Gamma}\mathrm{o}\mathrm{v}$interpretation
Masahiko Sato

(佐藤雅彦)

Department of lnformation Science
Kyoto University. kyot. jp$\mathrm{m}\mathrm{a}\mathrm{s}\mathrm{a}\mathrm{h}\mathrm{i}\mathrm{k}\mathrm{o}\emptyset \mathrm{k}\mathrm{u}\mathrm{i}_{\mathrm{S}}$$0-\mathrm{u}.\mathrm{a}\mathrm{C}$

Abstract. The Brouwer-Heyting-Kolmogorov interpretation explains themeaning of logical operations as operators that construct proofs fromprook of the operands. The BHK interpretation is usually understoodas giving intuitionistic interpretation for the logical operators, but, as
pointed out by Troelstra and van Dalen [12], it is possible to understandthe BHK interpretation classically. We elaborate this idea and develop
a classical theory of prook as abstract mathematical entities where thetruth of a proposition becomes equivalent to the existence of proofs of
the proposition.
, and give
We develop a first order theory of arithmetic, equivalent toa classical BHK interpretation for the theory. We show the soundness ofof a formula is
the interpretation by showing that if a derivationinterpretation
proof
interpretation
a
of .
of is
given, then theof theWe also show that the interpreted value of derivations is preserved under
reductions of derivations.
calculus and develop a classicalWe also present a system of
BHK interpretation for it. Since tlle calculus in non-deterministic, weinterpret a derivation by a set of proofs. We show the soundness of theinterpretation, and show that if a derivation reduces toderivation,
associated set of prook for the latter derivation is smaller
than that for the former derivation.
$\mathrm{P}\mathrm{A}$

$P$

$A$

$P$

$A$

$\mathrm{c}\mathrm{a}\mathrm{t}_{\mathrm{C}}1_{1}/\mathrm{t}1\iota \mathrm{r}\mathrm{o}\mathrm{w}$$\mathrm{a}\mathrm{n}\mathrm{o}\mathrm{t}1_{1}\mathrm{e}\mathrm{r}$$\mathrm{t}\mathrm{l}\iota \mathrm{e}\mathrm{n}\mathrm{t}\mathrm{l}\iota \mathrm{e}$1Introduction

The Tarskian interpretation of formulas interprets a mathematical formula either
as true or false. The(BHK) interpretation, on thehand,interprets a mathematical formula by as signing the set of proofs ofother
the given formula. In the BHK interpretation, a formula is true if and only if it
has a proof. Here, the notion of a proof is not understood as a formal derivation
but as an informal mathematical object just like a natural number or a real
number.
is true if and only if either
the Tarskian interpretation, for example,$A\supset
B$ is true if and only if it
is false or is true. the BHK interpretation,
has a proof , i.e., if there is a function such that for any proof of $A,$ $f(p)$ is
a proof of . A disjunction $A\vee B$ is true in the Tarskian interpreration if either$\mathrm{B}\mathrm{r}\mathrm{o}\mathrm{u}\mathrm{w}\mathrm{e}\mathrm{r}- \mathrm{H}\mathrm{e}\mathrm{y}\mathrm{t}\mathrm{i}\mathrm{n}\mathrm{g}-\mathrm{K}_{0}1\mathrm{m}\mathrm{o}\mathrm{g}\mathrm{o}\mathrm{r}\mathrm{o}\mathrm{v}$$A\supset B$

$\ln$

$B$

$A$

$f$

$B$

$\ln$

$f$

$p$

29
or is true, and it is true in the BHK interpretation if or has a proof, and in the first case $(0,p)$ is a proof of $A\vee B$ and in the second case $(1, p)$ is
a proof of $AB$ . So the BHK interpretation gives finer interpretation than the
Tarskian interpretation. In addition to this, these two interpretations have thefollowing essential differences.
A proposition is classically true if it is true under the Tarskian interpretation,and it is intuitionistically true if it is true under the BHK interpretation. Since
the law of the excluded middle is always true classically but not always true
intuitionistically, we know that these two interpretations are not equivalent.
However, as pointed out in Troelstra and van Dalen [12], by modifying the
BHK interpretation appropriately it is possible to interpret propositions in terms
of proofs in such a way that any proposition is classically true if and only if it has
a proof. In this paper, we elaborate this idea, and show that this classical BHK
interpretation is consistent with the intuitionistic BHK interpretation in thesense that any proof of a proposition under the intuitionistic BHK interpretationis also a proof of the proposition in the classical BHK interpreration.
We also present a formal system of arithmetic in a mo dified natural deduction
style and show that it is possible to give a sound interpretation of the system interms of the classical BHK interpretation.
inference
We then consider an extension of the system by therules. The resulting system is inherently non-deterministic, and we will show that
it is possible to extend the BHK interpretation and give a sound interpretation
$A$

$B$

$A$

$B$

$p$

$\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{c}\mathrm{h}/\mathrm{t}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{w}$for this system.
By the well-known Curry-Howard isomorphism, it is possible to regard formal derivations in the intuitionistic fragment of our formal system as programsin a typed language. Then our BHK interpretation gives a natural denotationalsemantics to this programming language. It is therefore possible to use thisframework as a basis for constructive programming where programming is replaced by proving.

The classical interpretation2

To make our argument concrete, we will work on a first order language whose
intended domain of interpretation is the set of natural numbers.
So our language contains the constant , a unary function symbol succ (forsuccessor), binary function symbols plus and times. (We also have symbols for
all the primitive recursive functions and associated defining axioms, however, we
etc.
will not mention them explicitly for the sake of simplicity.) We use
as meta variables for individual variables. We define terms as usual using theseetc. as meta variables for terms. We will write $0,1,2,$
symbols. We use
and call these terms numerals. We will identify
for , succ(O), succ
each numeral with the natural number which corresponds to the numeral in an$m,$etc. as meta variables for numerals (and natural
obvious way. We use
numbers). We will write for the set of natural numbers.
$0$

$x,$

$a,$

$0$

$b,$

$c$

$z$

$\ldots$$(\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{C}(\mathrm{O})),$

$k,$

$y,$

$l,$

$\ldots$$n$$\mathrm{N}$30$,$
The only primitive predicate symbol we use is . We will use
form
theand as primitive logical symbols. Atomic formulas are expressions of$a=b$ , and formulas are constructed from atomic formulas by using the above
logical symbols. We use $A,$ $B,$ etc. as meta variables for formulas. We define, respectively.
as abbreviations of succ(O) $=0$ andWe will call an atomic formula of the form $x=k$ a binding. A binding $x=k$binds the variable to the natural number . We define an environment as afinite set of bindings such that for any variable if $x=k$ and $x=k’$ are both inare the same natural number). We use(that is, andthe set thenetc. as meta variables for environments. For an environment and a variable ,to be if $x=k\in\epsilon$ and undefined if no such exists. Let be an
we defineenvironment and $x=k$ be a binding. Then we define an environment $\epsilon[x=k]$
as follows.
$\forall$$=$$\supset,$$\wedge,$$\exists$$C$$A\supset\perp$$\perp \mathrm{a}\mathrm{n}\mathrm{d}\neg A$

$k$

$x$

$x$

$k\equiv k’$

$k’$

$k$

$\delta$$\epsilon,$$x$$\epsilon$

$k$

$k$

$\epsilon.x$$(\epsilon-\{x=k’\})\cup\{x=k\}$$\epsilon[x=k]=\triangle\{$$\epsilon\cup\{x=k\}$$\epsilon$

if $x=k’\in\epsilon$ for someotherwise.

$k’$

be a term and be an environment. We say that covers ifis, wherestands for the set of free variables in andanconcept
thatis defined. We define thethe set of variables such thatsimilarly.
environment covers a formula
Given an environment and a term such that covers , we can associateby induction on as follows. We will say that denotes
a natural numberin the environment .

Let

$a$

$a$

$\mathrm{F}\mathrm{V}(a)$$\mathrm{d}\mathrm{o}\mathrm{m}(\epsilon)$$x$$\mathrm{d}\mathrm{o}\mathrm{m}(\epsilon)$$\epsilon.x$$A$$\epsilon$$a$$\epsilon$$\epsilon$

$a$

$a$

$a$

$\epsilon[a\mathrm{J}$$\epsilon[a\mathrm{I}$

1.
2.
3.
4.
5.

$\mathrm{F}\mathrm{V}(a)\subseteq$$a$$\epsilon$$\epsilon$$\epsilon$$\epsilon \mathbb{I}0\mathrm{J}^{\triangle}=0$.

$\epsilon[x\mathrm{I}^{\triangle}=\epsilon.X$.

$\epsilon \mathbb{I}\mathrm{s}\mathrm{u}\mathrm{C}\mathrm{C}(a)\mathrm{I}^{\triangle}=\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{C}(\epsilon[a\mathrm{J})$.

$\epsilon \mathbb{I}\mathrm{p}\mathrm{I}\mathrm{u}\mathrm{s}(a, b)\mathrm{I}=\triangle\epsilon[a\mathrm{I}+\epsilon[b\mathrm{J}$.

$\epsilon \mathbb{I}\mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}\mathrm{s}(a,b)\mathrm{I}=\triangle\epsilon \mathbb{I}a\mathrm{I}\cdot\epsilon[b\mathrm{I}\cdot$

We have just seen that a term, which is a syntactic entity, denotes a natural
number, which is an abstract mathematical object, under any environment thatcovers the term.
Similarly, we wish to define the denotation of a formula under an environmentthat covers the formula. We first define propositions as certain sets and then we
define the classical BHK interpretation in such a way that each formula will
denote a proposition.
In the classical BHK interpretation, we will use the term ‘function’ in thesame way as we use it in classical mathematics based on set theory. Namely,, ifby a function we understand a set of pairs such that for any objects$(a, b)$ and $(a, c)$ are infor thethen $b=c$ . For a pair , we write
left (right) component of , respectively. If is a function, we put$\{\pi_{0}(p)|p\in f\}$ , and if, then we write $f(a)$ for the unique such that$(a, b)\in f$ . If
is a set and is a mathematical expression (possibly) containing
such that denotes a unique object for any in , then we write$a,$ $b,$

$f$

$f$

$p$

$p$

$\mathrm{d}\mathrm{o}\mathrm{m}(f)=\triangle$

$f$

$b$

$a\in \mathrm{d}\mathrm{o}\mathrm{m}(f)$

$S$

$x$

$e$

$c$

$\pi_{0}(p)(\pi_{1}(p))$

$e$

$x$

$S$

$\lambda x\in S.$

$e$

31

and $f(x)=e$ for any in . Also, wefor the function such thatand $f(p)\in T$ forwill write : $Sarrow T$ if is a function such that
any $p\in S$ .
.
We introduce the following notation. Suppose that $p\in S$ and :$rec(p,f):\mathrm{N}arrow
S$by the following equations.
Then we define a function
$f$

$f$

$f$

$S$

$x$

$\mathrm{d}\mathrm{o}\mathrm{m}(f)=S$$\mathrm{d}\mathrm{o}\mathrm{m}(f)=S$$f$$\mathrm{N}arrow Sarrow S$$rec(p, f)(0)=p$$rec(p, f)(\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{c}(n))=f(n)(rec(p, f)(n))$

Propositions are inductively defined as follows.

is a proposition.
1. For each natural number , the singleton set
2. The empty set is a proposition.
are propositions, then $S\cross T=$ { $(p,$ $q)|p\in S$ and $q\in T$ } is a
3. If andproposition.
4. If and are propositions, then $S+T=\{(0,p)|p\in S\}\cup\{(1, q)|q\in T\}$$k$$\{k\}$$\emptyset$

$S$

$T$

$S$

$T$

is a proposition.
5. If and are propositions, then $Sarrow T$ , the set of functions from to ,is a proposition.
, the set ofis a proposition for each natural number , then
6. If
$f(k)\inS_{k}$, is a proposition.
for eachfunctions from such that$\sum_{k}S_{k}=\{(k,p)|p\in$
7. If
is a proposition for each natural number , then, is a proposition.
$S$

$S$

$T$

$k$

$S_{k}$$f$$T$$\prod_{k}S_{k}$$k\in \mathrm{N}$$\mathrm{N}$$k$$S_{k}$$S_{k}\}$

We write Prop for the set of propositions. We are thus following the principle of$propositi\mathit{0}ns_{-}as-Set_{S}$ since we defined propositions as sets.
Given an environment and a formula such that covers , we can assoby induction on as follows. We will call this interpreciate a proposition
tation the classical $BHK$ interpretation.
$A$$\epsilon$$A$$\epsilon[A\mathrm{I}$

1.
2.
3.

4.
5.
6.

$A$

$\epsilon$$\epsilon[a=b\mathrm{I}=\triangle\{\epsilon[a\mathrm{J}\}\cap\{\epsilon[b\mathrm{J}\}$.

$\epsilon \mathrm{I}^{A\wedge}B\mathrm{I}^{\triangle}=\epsilon[A\mathrm{I}\cross\epsilon[B\mathrm{I}\cdot$$\epsilon[A\vee B\mathrm{I}=[A\mathrm{J}+\triangle_{\epsilon\epsilon}[B\mathrm{I}\cdot$$\epsilon[A\supset B\mathrm{I}^{\triangle_{\epsilon}}=[A\mathrm{J}arrow\epsilon[B\mathrm{J}$.

$\epsilon[\forall x.A\mathrm{I}=\prod_{k}\epsilon\triangle[x=k][A\mathrm{I}\cdot$$\epsilon \mathrm{I}\exists x.A\mathrm{I}=\sum_{k}\epsilon\triangle[x=k][A\mathrm{I}\cdot$

We have the following theorem which establishes a logical equivalence between the classical BHK interpretation and the Tarskian interpretation.

Theorem 1. If an environment covers a formula , thenthe Tarskian interpretation if and only if the proposition
set.
$\epsilon$

$A$

$A$

$\epsilon \mathbb{I}A$

is true in under
I is a non-empty$\epsilon$

Proof. The proof is straightforward if we note the following equivalences.

32$-\{k\}\cap\{l\}\neq\emptyset\Leftrightarrow k=l$$-S\cross T\neq\emptyset\Leftrightarrow S\neq\emptyset$$-S+^{\tau}\neq\emptyset\Leftrightarrow S\neq\emptyset$.

and$T\neq\emptyset$

.

.
or
.
or
for all .
for some .
$T\neq\emptyset$$-Sarrow T\neq\emptyset\Leftrightarrow S=\emptyset$$T\neq\emptyset$$- \prod_{k}S_{k}\neq\emptyset\Leftrightarrow S_{k}\neq\emptyset$

$k$

$k$

$- \sum_{k}S_{k}\neq\emptyset\Leftrightarrow S_{k}\neq\emptyset$

See also exercise 1.3.4 of Troelstra and van Dalen [12].

$\square$We will call elements of propositions proofs. Then, the above theorem says
has a proof.
that a formula is true under if and only if the proposition$\pi(S)$(true) if is non-empty and toto beFor any proposition , we put
for the Tarskian truth value of in .
if is empty. We write
Then, the above theorem can be given as the equation:$A$$\epsilon[A\mathrm{J}$$\epsilon$$S$$\mathrm{b}\mathrm{e}\perp(\mathrm{f}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e})$$\mathrm{T}$

$S$

$S$

$A$

$\epsilon[A]$$\epsilon$$\epsilon[A]=\pi(\epsilon[A\mathrm{I})$In this way, we can decompose the Tarskian interpretation as the compositionof and the BHK interpretation.
$\pi$

3

Interpretation of derivations

In the previous section, we introduced propositions and proofs as abstract mathematical entities (or semantical objects). In this section we define derivations as
syntactic objects that are intended to denote propositions. So, after defining
derivations, we will define an interpretation of a derivation in an environment
by a proof. We also define reduction rules (or computation rules) for derivations
and show that if a derivation reduces to another derivation, then they both denote the same proof (in any environment). In summary, we have the following
table:$\ovalbox{\tt\small REJECT}_{R}^{\mathrm{t}(,),\mathrm{m}}\mathrm{f}\mathrm{o}1\mathrm{m}\mathrm{u}_{\mathrm{X}\mathrm{t}}1\mathrm{C}\iota(A,B,c,)\mathrm{l})1\mathrm{o}_{1)\mathrm{o}\mathrm{S}\mathrm{i},\mathrm{f}}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{I}1(5,)\mathrm{c}\mathrm{o}\mathrm{d}\mathrm{e}1\mathrm{i}\mathrm{V}\mathrm{a}\mathrm{t}\mathrm{i}_{0}\mathrm{n}(P,Q\mathrm{e}\mathrm{l}\mathrm{n}\mathrm{m}\mathrm{t}\mathrm{e}a,b(\Gamma,\Delta)\mathrm{e}\mathrm{n}\mathrm{V}\mathrm{i}_{1}\mathrm{o}\mathrm{n}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}(c)\mathrm{p}_{1}\mathrm{o}\mathrm{O}\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{a}(1\mathrm{n}\mathrm{u}\mathrm{b}\mathrm{e}\mathrm{r}(p,q,r)\epsilon T,\cdot Uk, m, n))$We define derivations in a natural deduction style. We will give inductive rules: ,that are used to derive judgments. A judgment is either of the form
: Prop orwhere is a context, is a term, is a derivation andis a formula. In this way, we will define judgments, contexts and derivations
simultaneously (as well as terms and formulas).
We will define a context as a finite set of declarations, where a declaration is( , a formula). In the first case, we sayeither of the form or of the form
that is declared as a natural number and in the second case, we say thatis declared as a derivation of . Each context will satisfy the condition that for$\Gamma\vdash a$$\Gamma\vdash A$$\Gamma\vdash P:$$A$$\Gamma$$a$$\mathrm{N}$

$P$

$A$

$y^{A}$

$x$

$x$

$A$

$y$

$A$

33
any variable at most one declaration for is in the context. Below, we display
a context by listing its declarations as a sequence. So the empty econtext is
displayed as an (invisible) empty sequence. If andare contexts, thenwill stand for the union of the two contexts, and $\Gamma-x(\Gamma-y^{A})$ will stand forthe context obtained from by removing the declaration $x(y^{A})$ , respectively.
Moreover, when we use the notation
we tacitly assume that and arecompatible, that iscontains at most one declaration for each variable .
If: is derivable, then we will say thathas type
under the context. We say that a context.
is smafler than another context if
First, we give rules for terms.
$x$

$x$

$\Delta$$\Gamma$$\Gamma,$$\Delta$$\Gamma$$\Gamma,$$\Gamma$$\Delta$$\Delta$$\Gamma \mathrm{U}\Delta$$\Gamma\vdash P$

$x$

$A$

$P$

$\Gamma$

1. If
.
3. If
4. If
5. If
$2$

$A$

$\Gamma$$x$

is a variable, then.
, then: and: and$\Delta$$x\vdash x$$\Gamma\subseteq\Delta$: N.

$\vdash 0:\mathrm{N}$$\Gamma\vdash a:\mathrm{N}$: N.
, then, then$\Gamma\vdash \mathrm{s}\mathrm{u}\mathrm{c}\mathrm{C}(a)$$\Gamma\vdash a$$\mathrm{N}$$\Delta\vdash b:\mathrm{N}$$\Gamma\vdash a$$\mathrm{N}$$\Delta\vdash b:\mathrm{N}$

: N.
: N.

$\Gamma,$$\Delta\vdash \mathrm{p}\mathrm{l}\mathrm{u}\mathrm{S}(a, b)$$\Gamma,$$\Delta\vdash \mathrm{t}|\mathrm{m}\mathrm{e}\mathrm{s}(a, b)$

We say that is a term if a judgment of the form:
is derivable byusing the above rules. We also define
as the set of variables such that
occurs in .
Next, we have rules for formulas.
$\Gamma\vdash a$$a$$\mathrm{N}$$x$$\mathrm{F}\mathrm{V}(a)$$\Gamma$

$x$

1. If
2. If
3. If
4. If
5. If
6. If

and
: Prop and: Prop and: Prop andis a variable andis a variable and$\Gamma\vdash a:\mathrm{N}$$\Delta\vdash b:\mathrm{N}$, then$\Gamma\vdash A$$\Delta\vdash B$$\Gamma\vdash A$$\Delta\vdash B$$\Gamma\vdash A$$\Delta\vdash B$

$x$

$x$

$\Gamma,$$\Delta\vdash a=b$

: Prop, then
: Prop, then

: Prop, then$\Gamma\vdash A$$\Gamma\vdash A$: Prop.

: Prop.
: Prop.

$\Gamma,$$\Delta\vdash A\wedge B$$\Gamma,$$\Delta\vdash AB$$\Gamma,$$\Delta\vdash A\supset B$: Prop, then
: Prop, then$\Gamma-x\vdash\forall x.A$$\Gamma-x\vdash\exists x.A$

: Prop.
: Prop.
: Prop.

We say thatis a formula if ajudgment of the form
: Prop is derivable
by using the above rules. We also define
as the set of variables suchthat occurs in . We define substitution operation on formulas as usual, andwe write $A[x=a]$ for the result of substituting for all the free occurrences ofin (after appropriately renaming bound variables in if necessary).
Finally we give rules for derivations. We give these rules as inference rules.
We first give general rules for equality.
$A$$\Gamma\vdash A$$x$$\mathrm{F}\mathrm{V}(A)$$\Gamma$

$x$

$a$

$x$

$A$

$A$

.
$\frac{\Gamma\vdash a.\cdot.\mathrm{N}}{\Gamma\vdash \mathrm{i}\mathrm{d}(a).a=a}(|.\mathrm{d})$$. \frac{\Gamma\vdash P\cdot a=b\Delta\vdash Q..A[x=a]}{\Gamma,\Delta\vdash \mathrm{r}\mathrm{e}\mathrm{p}^{1_{A}(Q}[x=b\mathrm{J}P,)\cdot A[_{X}=b]}$

The rules specific to natural numbers are as follows.
$\frac{\Gamma\vdash.P.a=b}{\Gamma\vdash \mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(P).\mathrm{s}\mathrm{u}\mathrm{C}\mathrm{C}(a)=\mathrm{s}\mathrm{u}\mathrm{C}\mathrm{C}(b)}$(succ)$. \frac{\Gamma\vdash P.\mathrm{s}\mathrm{u}\mathrm{C}\mathrm{C}(a)=0\Delta\vdash A.\mathrm{P}\mathrm{r}\mathrm{o}_{\mathrm{P}}}{\Gamma,\Delta\vdash \mathrm{a}\mathrm{b}_{0}\mathrm{r}\mathrm{t}A(P)\cdot A}.\cdot(\perp E)$(repl)

34$\frac{\Gamma\vdash b.\mathrm{N}}{\Gamma\vdash \mathrm{p}1\mathrm{u}\mathrm{S}(0,b).\mathrm{P}^{1()=b}\mathrm{U}\mathrm{S}\mathrm{o},b}.\cdot(\mathrm{p}^{1\mathrm{u}}\mathrm{s}_{0})$$\frac{\Gamma\vdash a.\mathrm{N}\Delta\vdash b.\mathrm{N}}{\Gamma,\Delta\vdash \mathrm{p}|\mathrm{u}\mathrm{S}(\mathrm{s}\mathrm{u}\mathrm{C}\mathrm{C}(a),b).\mathrm{p}1\mathrm{u}\mathrm{s}(\mathrm{S}\mathrm{u}\mathrm{C}\mathrm{C}(a),b)=\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(\mathrm{P}|\mathrm{u}\mathrm{s}(a,b))}.\cdot.(\mathrm{p}^{1\mathrm{u}}\mathrm{s}_{1})$$\frac{\mathit{1}^{\tau}\vdash b\cdot \mathrm{N}}{\Gamma\vdash \mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}\mathrm{S}(\mathrm{o},b)\cdot \mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}\mathrm{s}(0,b)=0}.\cdot(\mathrm{t}_{1}.\mathrm{m}\mathrm{e}\mathrm{s}\mathrm{o})$$. \frac{\Gamma\vdash a.\mathrm{N}\Delta\vdash b.\mathrm{N}}{\tau,\Delta\vdash \mathrm{t}_{\mathrm{I}}\mathrm{m}\mathrm{e}\mathrm{S}(\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{C}(a),b).\mathrm{t}\mathrm{I}\mathrm{m}\mathrm{e}\mathrm{S}(\mathrm{S}\mathrm{u}\mathrm{C}\mathrm{c}(a),b)=\mathrm{p}^{1}\mathrm{u}\mathrm{s}(b,\mathrm{t}_{\mathrm{I}\mathrm{m}\mathrm{e}}\mathrm{s}(a,b))}.\cdot...(\mathrm{t}1^{\cdot}\mathrm{m}\mathrm{e}\mathrm{S}_{1})$$. \frac{\Gamma\vdash P.A[x=0]\Delta\vdash Q\cdot\forall x.(A\supset.A[X=\mathrm{S}\mathrm{u}\mathrm{C}\mathrm{c}(X)])}{\Gamma,\Delta\vdash \mathrm{r}\mathrm{e}\mathrm{c}(P,Q)\cdot\forall XA}..(\mathrm{l}.\mathrm{n}\mathrm{d})$The rules for logical symbols are as follows.
.

$\frac{\tau,\vdash A\cdot \mathrm{p}_{\mathrm{r}}\mathrm{o}_{\mathrm{P}}}{x^{A}\Gamma\vdash_{X.A}A}$(assume)$\frac{\Gamma\vdash P.A\Delta\vdash.Q.B}{\Gamma,\Delta\vdash_{\mathrm{P}^{\mathrm{a}|\mathrm{r}}}(P,Q).A\wedge B}.(\wedge I)$$\frac{\Gamma\vdash P.A\wedge B}{\Gamma\vdash \mathrm{c}\mathrm{a}\mathrm{r}(P).A}..(\wedge E_{1})$$. \frac{\Gamma\vdash P.A\Delta\vdash B.\mathrm{p}\mathrm{r}\mathrm{o}_{\mathrm{P}}}{\Gamma,\Delta\vdash \mathrm{i}\mathrm{n}\mathrm{I}_{B}(P)\cdot A\mathrm{v}B}.\cdot(\vee I_{1})$$\frac{\Gamma\vdash P.A\wedge..B}{\Gamma\vdash \mathrm{c}\mathrm{d}\mathrm{r}(P)B}.(\wedge E_{2})$$. \frac{\Gamma\vdash P.B\Delta\vdash A.\mathrm{p}\mathrm{r}\mathrm{o}_{\mathrm{P}}}{\tau,\Delta\vdash_{\mathrm{I}\mathrm{n}}\mathrm{r}_{A}(P).A\mathrm{v}B}..\cdot(\vee I_{2})$$. \frac{\Gamma\vdash P.AB\Delta\vdash Q.C\Pi\vdash R.c}{\Gamma,\Delta-x^{A},\Pi-y^{B}\vdash \mathrm{C}\mathrm{a}\mathrm{s}\mathrm{e}(P,XQA.,y.R)B.C}...(\vee E)$$. \frac{\Gamma\vdash P.B\Delta\vdash A.\cdot \mathrm{p}\mathrm{r}\mathrm{o}_{\mathrm{P}}}{\Gamma-x^{A},\Delta\vdash\lambda_{X}A.P\cdot A\supset B}.(\supset I)$$\frac{\Gamma\vdash P.\cdot A}{\Gamma-x\vdash\lambda_{X}P.\forall X.A}..(\forall I)$$. \frac{\Gamma\vdash P\cdot\forall x.A\Delta\vdash a.\mathrm{N}}{\Gamma,\Delta\vdash \mathrm{a}\mathrm{p}\mathrm{P}^{1}\mathrm{y}(P,a)\cdot A[X=a]}.\cdot(\forall E)$$\frac{\tau\vdash P\cdot\exists x.A.\Delta\vdash Q\cdot C}{\Gamma,\Delta-x-y^{A}\vdash \mathrm{S}\mathrm{p}|_{1}\mathrm{t}(P,(X,y)A.Q)\cdot C}...(\exists E)$$. \frac{\Gamma\vdash a.\mathrm{N}.\Delta\vdash P.A[X=a]}{\Gamma,\Delta\vdash \mathrm{p}\mathrm{a}\mathrm{I}\mathrm{r}_{\exists A}x.(a,P)\cdot\exists x.A}..(\exists I)$

derivation if a judgment of the form
We say that is an intuitionis: is derivable by using the above rules. If is in , we say that the derivation.
depends on the assumption
$P$

$P$

$P$

$. \frac{\Gamma\vdash P.A\supset B\Delta\vdash Q.A}{\Gamma,\Delta\vdash \mathrm{a}\mathrm{p}\mathrm{p}^{1}\mathrm{y}(P,Q)\cdot B}.\cdot(\supset E)$$\Gamma\vdash$$\mathrm{t}ic$

$C$

$x$

$x^{A}$$\Gamma$

35
We now add the following rule which formalizes the law of the excluded middle. A derivation which is obtained by possibly using this rule in addition to the.
other rules is called a classical de$7\dot{\tau}vati\mathit{0}n$$\frac{\Gamma\vdash A\cdot..\mathrm{p}_{\mathrm{r}\mathrm{o}_{\mathrm{P}}}}{\Gamma\vdash 1\mathrm{e}\mathrm{m}_{A}A\neg A}.(\mathrm{l}\mathrm{e}\mathrm{m})$We can verify that any formula is derivable in HA (Heyting arithmetic)is derivable in PA (Peanois intuitionistically derivable, and:iff: is classically derivable.
arithmetic)
We have thus defined three kinds of judgments and defined how to derive:these judgments. It is easy to see that if a judgment of the first kind
: Prop is derivable, then is of the formor ajudgment of the second kind
. This means that a term or a formula depends on the variables,, . Therefore, it is in general necessary that covers these variables inare definable.
andorder that
We can easily verify th.e following lemma by induction on the constructionof derivations.
$A$

$A$

$A$

$\vdash P$$\mathrm{i}\mathrm{f}\mathrm{f}\vdash P$$A$$\Gamma\vdash a$$\Gamma$$\Gamma\vdash A$$x_{1}\ldots$

$A$

$a$

$x_{n}$$\mathrm{N}$$\epsilon$$x_{1},$$\ldots$$x_{n}$$\epsilon[A\mathrm{J}$$\epsilon[a\mathrm{J}$Lemma 2. If($\epsilon \mathrm{I}A\mathrm{J}\in$$\epsilon[a\mathrm{I}\in \mathrm{N}$:$\Gamma\vdash a$($\mathrm{N}$: Prop) is derivable and$\Gamma\vdash A$$\epsilon$

covers$\Gamma$, thenProp), respectively.

: is derivable, then each element ofIf ajudgment of the third kind
where is a formula andthe sequence is either of the form or of the form
. In order to interpret such a context, wefor the set of such
we writeneed to extend the definition of binding and environment as follows. A bindingis an expression of the form $x=k$ where is a natural number or of the form
$x=p$ where is a proof. An environment is a finite set of bindings such that foreach variable there exists at most one binding of the form $x=k$ or $x=p$ inis defined in the same way as
the set. For an environment and a variable
is defined. Let
for the set of variables such that
before and we write,
if
be an environment and be a context. We writein .
for eachfor each in , andand, then we can define
is derivable andSuppose thatby the following
as follows. We first define pre-deshow that$C$$\Gamma\vdash P$$A$$x^{A}$$x$$\Gamma$$x’ \mathrm{s}$$\mathrm{d}\mathrm{o}\mathrm{m}(\Gamma)$

$k$

$p$

$x$

$x,$

$\epsilon$$\epsilon.x$$\epsilon.x$$x$$\mathrm{d}\mathrm{o}\mathrm{m}(\epsilon)$$\mathrm{d}\mathrm{o}\mathrm{m}(\Gamma)\subseteq \mathrm{d}\mathrm{o}\mathrm{m}(\epsilon)$$\epsilon\models\Gamma$$\Gamma$$\epsilon$$\epsilon.x\in \mathrm{N}$$x$$\Gamma$$x^{A}$$\epsilon.x\in\epsilon \mathbb{I}A\mathrm{I}$$\Gamma\vdash P:$ $A$$\Gamma$$\epsilon[P\mathrm{I}$$\epsilon\models\Gamma$$r\dot{\tau}va\mathrm{t}ions$$\epsilon[P\mathrm{I}\in\epsilon \mathbb{I}^{A}\mathrm{I}$grammar.
$P::=x||\mathrm{d}(a)|\mathrm{r}\mathrm{e}_{\mathrm{P}^{1}(P},$$Q)|\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(P)|\mathrm{a}\mathrm{b}\mathrm{o}\mathrm{r}\mathrm{t}(P)|\mathrm{r}\mathrm{e}\mathrm{c}(P, Q)$$\mathrm{p}1_{\mathrm{U}}\mathrm{s}(0, b)|\mathrm{p}\mathrm{l}\mathrm{u}\mathrm{s}(\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{C}(a), b)|\mathrm{t}_{\mathrm{I}\mathrm{m}\mathrm{e}}.\mathrm{S}(0, b)|\mathrm{t}_{1\mathrm{m}\mathrm{e}}.\mathrm{S}(\mathrm{S}\mathrm{u}\mathrm{C}\mathrm{c}(a), b)$
$|$

$|$

$|$

$\mathrm{p}\mathrm{a}|\mathrm{r}(P, Q)|\mathrm{p}\mathrm{a}|\mathrm{r}(a, P)|\mathrm{c}\mathrm{a}\mathrm{r}(P)|\mathrm{c}\mathrm{d}\mathrm{r}(P)|\mathrm{s}_{\mathrm{P}^{1_{\mathrm{I}\mathrm{t}}(P}},$$(x, y).Q)$$|\mathrm{n}1(P)||\mathrm{n}\mathrm{r}(P)|\mathrm{c}\mathrm{a}\mathrm{s}\mathrm{e}(P, x.Q, y.R)$$|$$\lambda x^{A}.P|\lambda x.P|\mathrm{a}\mathrm{p}\mathrm{P}^{1}\mathrm{y}(P, Q)|\mathrm{a}\mathrm{p}\mathrm{p}^{[}\mathrm{y}(P, a)$$|$$1\mathrm{e}\mathrm{m}_{A}$of free variables in
we can define the set
For each pre-derivation
as expected. For each pre-derivation and environment such thatinductively as follows.
we define a proof$P$$\mathrm{F}\mathrm{V}(P)$$P$$\mathrm{d}\mathrm{o}\mathrm{m}(\epsilon)$$\epsilon \mathrm{I}^{P}\mathrm{I}$$\epsilon$$P$$\mathrm{F}\mathrm{V}(P)\subseteq$

36

1.
2.
3.
4.
5.
6.

7.
8.
9.
10.
11.
12.
13.
14.
15.
16.
17.
18.

19.
20.
21.
22.
23.

$\epsilon[x\mathrm{I}^{\triangle}=\epsilon.X$.

$\epsilon \mathrm{I}|.\mathrm{d}(a)\mathrm{I}^{\triangle_{\epsilon \mathrm{I}\mathrm{J}}}=a$.

.

$\epsilon \mathrm{I}\mathrm{r}\mathrm{e}\mathrm{p}|(P, Q)\mathrm{I}=\triangle\epsilon \mathrm{I}Q\mathrm{I}$$\epsilon \mathbb{I}\mathrm{s}\mathrm{u}\mathrm{C}\mathrm{C}(P)\mathrm{I}^{\triangle}=\epsilon[P\mathrm{I}\cdot$$\epsilon[\mathrm{a}\mathrm{b}..\mathrm{o}\mathrm{r}\mathrm{t}(P)\mathrm{J}=\triangle$

undefined.

$\epsilon[\mathrm{r}\mathrm{e}\mathrm{c}(P, Q)\mathrm{I}=\triangle rec(\epsilon[P\mathrm{I}, \epsilon[Q\mathrm{I})$.

$\epsilon[\mathrm{p}\mathrm{I}\mathrm{u}\mathrm{s}(0, b)\mathrm{I}^{\triangle}=\epsilon \mathrm{I}^{b}\mathrm{I}\cdot$$\epsilon[\mathrm{p}\mathrm{l}\mathrm{u}\mathrm{s}(\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{c}(a), b)\mathrm{I}=\triangle\epsilon[a\mathrm{J}+1+\epsilon[b\mathrm{I}\cdot$$\epsilon[\mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}\mathrm{S}(0, b)\mathrm{J}=\triangle 0$.
.

$\epsilon[\mathrm{t}\mathrm{i}\mathrm{m}\mathrm{e}\mathrm{S}(\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(a), b)\mathrm{I}=\triangle(\epsilon \mathbb{I}^{a}\mathrm{I}+1)\epsilon \mathbb{I}b\mathrm{J}$$\epsilon[\mathrm{p}\mathrm{a}\mathrm{l}\mathrm{r}(P, Q)\mathrm{I}=\triangle(\epsilon[P\mathrm{I}, \epsilon \mathbb{I}^{Q\mathrm{J}})$$\epsilon[\mathrm{p}\mathrm{a}\mathrm{l}\mathrm{r}(a, P)\mathrm{I}=\triangle(\epsilon \mathbb{I}a\mathrm{I}, \epsilon[P\mathrm{I})$$\epsilon[_{\mathrm{C}\mathrm{a}\mathrm{r}}(P)\mathrm{I}^{\triangle}=\pi 0(\epsilon \mathrm{I}^{P}\mathrm{I})$

.

.

.

.

$\epsilon[\mathrm{C}\mathrm{d}\mathrm{r}(P)\mathrm{I}^{\triangle}=\pi 1(\epsilon \mathrm{I}^{P}\mathrm{I})$$\epsilon[\mathrm{s}\mathrm{p}1_{\mathrm{I}\mathrm{t}}(P, (x, y).Q)\mathrm{J}=\triangle\epsilon[x=k][y=p]\mathrm{I}Q\mathrm{J}$, if$\epsilon[P\mathrm{J}=(k,p)$.

.

$\epsilon[\mathrm{l}\mathrm{n}1(P)\mathrm{I}=\triangle(0, \epsilon\ovalbox{\tt\small REJECT} P\mathrm{I})$$\epsilon[|\mathrm{n}\mathrm{r}(P)\mathrm{I}=\triangle(1, \epsilon[P\mathrm{I})$.
$\epsilon[x=p][Q\mathrm{I}$$\epsilon[\mathrm{c}\mathrm{a}\mathrm{S}\mathrm{e}(P, X.Q, y.R)\mathrm{J}=\triangle\{$$\epsilon[y=p]\mathrm{I}R\mathrm{J}$ifif$\epsilon[P\mathrm{I}=(0_{p},)$,$\epsilon[P\mathrm{I}=(1,p)$.

$\epsilon[\lambda_{X^{A}}.P\mathrm{I}^{\triangle_{\lambda p\in}}=\epsilon[A\mathrm{I}\cdot\epsilon[_{X}=p][P\mathrm{I}\cdot$$\epsilon[\lambda x.P\mathrm{I}=\triangle\lambda k\in \mathrm{N}.\epsilon[x=k]\mathrm{I}^{P}\mathrm{I}\cdot$$\epsilon[\mathrm{a}_{\mathrm{P}\mathrm{P}}[\mathrm{y}(P, Q)\mathrm{I}^{\triangle_{\epsilon \mathbb{I}}}=P\mathrm{I}(\epsilon \mathrm{I}^{Q\mathrm{I})}\cdot$.

$\epsilon[\mathrm{a}_{\mathrm{P}\mathrm{p}[\mathrm{y}(P}, a)\mathrm{I}^{\triangle}=\epsilon \mathrm{I}P\mathrm{I}(\epsilon \mathrm{I}^{a}\mathrm{I})$$(0,p)$ if$\epsilon[1\mathrm{e}\mathrm{m}_{A}\mathrm{I}=\triangle\{$$(1, \emptyset)$

if$p\in\epsilon \mathrm{I}A\mathrm{J}$,$\epsilon[A\mathrm{I}=\emptyset\cdot$. For
We note thatis sometimes undefined even if
is undefined. We also note thatexample,is undefined since
may not be unique if
is non-empty. Even in such a case we canbyuniqueusing
a choice function that selects an element
make the definition.
from the set$\mathrm{F}\mathrm{V}(P)\subseteq \mathrm{d}\mathrm{o}\mathrm{m}(\epsilon)$$\epsilon[P\mathrm{I}$$\pi_{0}(0)$$\epsilon \mathrm{I}\mathrm{c}\mathrm{a}\mathrm{r}(\mathrm{I}\mathrm{d}(0))\mathrm{I}$$\epsilon[A\mathrm{J}$$\epsilon[[\mathrm{e}\mathrm{m}_{A}\mathrm{I}$$\epsilon[A\mathrm{J}$Theorem 3. If$\Gamma\vdash P:$ $A$

is demvable and$\epsilon\models\Gamma$, then$\epsilon[P\mathrm{I}\in\epsilon[A\mathrm{J}$.

may not be a legitimate presuperscripts appropriately,
derivation, but by forgetting its subscripts
we can uniquely translate into a pre-derivation, say, . We therefore understand thatin the statement of the theorem stands for: . Here
We prove the theorem by induction on the derivation of: is derived
we check only the following case. Suppose that

Proof. We first remark that the derivation$P$$\mathrm{a}\mathrm{n}\mathrm{d}/\mathrm{o}\mathrm{r}$

$P$

$Q$

$\epsilon[Q\mathrm{I}\cdot$$\epsilon[P\mathrm{I}$$\Gamma\vdash P$$\Gamma,$$\Delta\vdash \mathrm{a}\mathrm{b}\mathrm{o}\mathrm{r}\mathrm{t}_{A}(P)$

$A$

$A$

37

. Then, since: Prop and thatand:
. Here we, we have by induction hypothesis that
. This is a contradiction, and we see
since succ
have
. So the theorem holds in this case.
that there can be no such thatfrom$\Gamma\vdash P$$\Delta\vdash A$$\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{C}(a)=0$$\epsilon\models\Gamma,$$\Delta$$\epsilon[P\mathrm{I}\in\epsilon[\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{C}(a)=0\mathrm{J}$$\epsilon\models\Gamma$$(\epsilon[a\mathrm{J})\neq 0$$\epsilon[\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(a)=\mathrm{o}\mathrm{I}=\emptyset$$\epsilon\models\Gamma,$$\epsilon$$\square$$\Delta$

We now consider reduction rules for pre-derivations.
1.

$\mathrm{a}\mathrm{p}\mathrm{P}^{[}\mathrm{y}(\mathrm{r}\mathrm{e}\mathrm{c}(P, Q),$$0)\mapsto P$.

2. apply.
3. car.
4.
.
5. case
6. case $(|\mathrm{n}\mathrm{r}(P), X.Q, y.R)\vdasharrow R[y=P]$ .
7. apply $(\lambda xPA., Q)-\succ P[X=Q]$ .
8. apply $(\lambda_{X}.P, a)\mapsto P[x=a]$ .
$(x, y).R)\mapsto R[x=P][y=Q]$ .
9. split$(\mathrm{r}\mathrm{e}\mathrm{c}(P, Q),$$\mathrm{S}\mathrm{u}\mathrm{C}\mathrm{c}(a))\mapsto \mathrm{a}\mathrm{p}\mathrm{p}\mathrm{l}\mathrm{y}(\mathrm{a}_{\mathrm{P}}\mathrm{p}\mathrm{I}\mathrm{y}(Q, a),$$\mathrm{a}_{\mathrm{P}\mathrm{P}}\mathrm{I}\mathrm{y}(\mathrm{r}\mathrm{e}\mathrm{C}(P, Q),$

$a))$

.

$(\mathrm{P}^{\mathrm{a}}\mathrm{I}\mathrm{r}(P, Q))\mapsto P$$\mathrm{C}\mathrm{d}\mathrm{r}(_{\mathrm{P}^{\mathrm{a}}}|.\mathrm{r}(P, Q))\mapsto Q$$(\mathrm{i}\mathrm{n}\mathrm{I}(P), x.Q, y.R)\mapsto Q[x=P]$$(\mathrm{p}\mathrm{a}\mathrm{l}\mathrm{r}(P, Q),$

These reductions enjoy the following subject reduction property.
Theorem4. If has typesome smaller than .

$A$

$P$

under

$\Gamma$

and$P\mapsto Q_{\lambda}$

then

$Q$

has type

$A$

under

$\Gamma$$\Delta$Moreover, we have the following theorem which shows that BHK interpretation is preserved by reductions. We may read this theorem as saying that if aderivation is reducible to another derivation, then although they are syntacticallydistinct, they both denote the same proof.

Theorem 5. Suppose that
have$\Gamma\vdash P:$$A$

is derivable,$\epsilon\models\Gamma$

and $P-\succ Q$ . Then we$\epsilon[P\mathrm{I}=\epsilon[Q\mathrm{I}\cdot$

Proof. We check here only the following case.
$\epsilon[\mathrm{a}\mathrm{p}\mathrm{p}|\mathrm{y}(\lambda x^{A}.P, Q)\mathrm{I}=\epsilon[\lambda X^{A}.P\mathrm{J}(\epsilon[Q\mathrm{I})$$=(\lambda q\in\epsilon[A\mathrm{I}\cdot\epsilon[x=q][P\mathrm{I})(\epsilon[Q\mathrm{I})$$=\epsilon[_{X=\epsilon}[Q\mathrm{I}][P\mathrm{I}$$=\epsilon[P[X=Q]\mathrm{I}$The last equality above comes from Lemma 8, which in turn is based on Lemma 6
and Lemma 7.
$\square$

We need the following lemmas to prove the above theorem.

andLemma6. If
is also derivable, and for any$\Delta\vdash b:\mathrm{N}$$\Gamma\vdash a:\mathrm{N}$$\epsilon[x=\epsilon \mathrm{I}^{b\mathrm{I}][\mathrm{I}}a$such that$\epsilon\models\Gamma-x,$$\Delta_{f}$$\Gamma-x,$ $\Delta\vdash a[x=b]$

we have:$\mathrm{N}$$\epsilon[a[x=b]\mathrm{I}=$.

: are derivable, then $\Gamma-x,$ $\Delta\vdash P[x=$and, we have: $A[x=a]$ is also derivable, and for any such that
andLelnma 7. If$a]$$\epsilon$

are derivable, then$\Gamma\vdash P$:$A$$\epsilon[P[x=a]\mathrm{J}=\epsilon[x=\epsilon \mathbb{I}a\mathrm{J}][P\mathrm{I}$$\Delta\vdash a$$\mathrm{N}$$\epsilon$$\epsilon\llcorner-\Gamma-x,$$\epsilon[A[x=a]\mathrm{I}=\epsilon[x=\epsilon[a\mathrm{J}][A\mathrm{I}\cdot$$\Delta$

38

Lemma8. If$P[x=Q]$ : $A$

are derivable, then $\Gamma-x$ : $B,$:and, we haveis also derivable, and for any such that$\Gamma\vdash P$:$A$$\Delta\vdash Q$$\Delta\vdash$$B$$\epsilon\models\Gamma-x,$ $\Delta$$\epsilon$$\epsilon[P[x=Q]\mathrm{Q}=\epsilon[x--\epsilon[Q\mathrm{I}]\mathrm{I}P\mathrm{I}\cdot$

The catch-throw calculus

4

In this section we extend HA by adding inference rules which correspond tothe catch and throw mechanism used in programming language like Lisp. We.
is logically equivalent tofor the extended calculus.
will write
Such logical calculi were first proposed by Nakano $[5, 6]$ and later modified bySato [11] and Kameyama [3]. Here we use the inference rules introduced in [11],and we refer the reader to $[11, 5]$ for detailed explanations of the motivations
behind these inference rules.
We first extend the language by assuming that there are denumerably many
etc. as meta
tag variables that are used as tags for derivations. We will use
variables for tag variables. We define a tag context as a finite set of declarations
where is a tag variable and $E$ is a formula. If is a context
of the form
is said to be, which we write
and is a tag context, then the pairan -context (extended context).
where is a:
, we will derive judgments of the formIn
is derivable, then we will say:
is a tag context. If
context and$P$is smaller than
. We say that an -context
has type underthat. If is empty, then we will write
andifanother context: for $\Gamma\vdash P:A;\Delta$ .
As we will see later, the reduction rules of derivations are not confluent. To
cope with this situation, we will interpret a derivation in an environment not by
a proof but by a set of proofs.
Now,
is obtained from HA by adding the following two rules.
$\mathrm{P}\mathrm{A}$$\mathrm{P}\mathrm{A}_{c/t}$$\mathrm{P}\mathrm{A}_{c/t}$$u,$ $v,$ $w$$u^{E}$$\Gamma$$u$$\Gamma;\Delta$$(\Gamma, \Delta)$$\Delta$$e$$\Gamma\vdash P$$\mathrm{P}\mathrm{A}_{c/t}$$\Gamma\vdash P$$\Delta$$A$$\Gamma\vdash P$$\Gamma\subseteq\Pi$$\Gamma$$A;\Delta$$\Gamma;\Delta$$\Pi;\Sigma$$A;\Delta$$\Gamma;\Delta$$\mathrm{e}$$\Delta\subseteq\Sigma$$\Delta$$A$$\mathrm{P}\mathrm{A}_{c/t}$.

$\cdot\frac{\Gamma\vdash P.E,\Delta\Pi.\vdash A\cdot \mathrm{p}\mathrm{r}\mathrm{o}_{\mathrm{P}}}{\Gamma,\Pi\vdash!_{A}u^{E}(P)\cdot A}$(throw)$. \frac{\Gamma\vdash P.A,\Delta}{\Gamma\vdash 7uPE..AE\cdot\Delta-uE}.$,(catch)contains a tag context in general, we have to
Since a judgment ofmodify inference rules of HA as well. Tag contexts in the premises are always
rule
inherited in the conclusion of any inference rule. So, for example, thebecomes:$\mathrm{P}\mathrm{A}_{\mathrm{C}}/i$$(\wedge I)$$.. \frac{\Gamma\vdash P\cdot A,\Delta\Pi\vdash Q.B\cdot\Sigma}{\Gamma,\Delta\vdash_{\mathrm{P}^{\mathrm{a}\mathrm{I}}}\mathrm{r}(P,Q)\cdot A\wedge B\cdot\Delta,\Sigma}..\cdot,’(\wedge I)$

and we understand that other rules of HA are similarly modified to those of, except the following rules which we write down explicitly. These rules are, but we restrict tag contexts
also extensions of the corresponding rules inin some judgments to be empty.
$\mathrm{P}\mathrm{A}_{c/t}$$\mathrm{H}\mathrm{A}$$. \frac{\Gamma\vdash P\cdot a=b\Pi\vdash Q\cdot.A[X=a],.\Sigma}{\Gamma,\Pi\vdash \mathrm{r}\mathrm{e}_{\mathrm{P}x}1_{A[=}b](P,Q)\cdot A[X=b],\Sigma}.\cdot$(repI)

39$. \frac{\Gamma\vdash P.A[_{X}=0]\Delta\vdash Q.\forall x.(A\supset A[X=\mathrm{S}\mathrm{u}\mathrm{C}\mathrm{c}(X)])}{\Gamma,\Delta\vdash \mathrm{r}\mathrm{e}\mathrm{C}(P,Q)\cdot\forall X.A}..(|.\mathrm{n}\mathrm{d})$$. \frac{\Gamma\vdash P\cdot A\supset B\cdot\Delta\Pi.\cdot\vdash Q\cdot A}{\Gamma,\Pi\vdash \mathrm{a}\mathrm{p}\mathrm{p}^{1}\mathrm{y}(P,Q)B\cdot\Delta},,\cdot(\supset E)$$. \frac{\Gamma\vdash P.AB\Pi\vdash Q.c\cdot\Sigma\Phi\vdash R.C.\Psi}{\Gamma,\Pi-x^{A},\Phi-y^{B}\vdash \mathrm{C}\mathrm{a}\mathrm{S}\mathrm{e}(P,x^{A}.Q,y^{B}.R).c,\Sigma,\Psi}.,.\cdot,\cdot(\vee E)$$. \frac{\Gamma\vdash P.\exists x.A.\Pi\vdash Q\cdot C,\Sigma}{\Gamma,\Pi-x-y^{A}\vdash \mathrm{s}\mathrm{p}^{1}\mathrm{I}\mathrm{t}(P,(X,yA).Q)\cdot C,\Sigma}.\cdot.\cdot(\exists E)$

is logically equivalent to PA by using Theorem 4
We can show thatasin [11]. In particular, we can derive the law of the excluded middle infollows.
$\mathrm{P}\mathrm{A}_{c/t}$$\mathrm{P}\mathrm{A}_{c/t}$$\frac{\overline{\tau\vdash A\cdot \mathrm{p}_{\mathrm{r}}\mathrm{o}_{\mathrm{P}}}}{x^{A}\Gamma\vdash_{X}A.A}\cdot$.

(assume)(throw)$x^{A}\Gamma\vdash’\overline{!\perp^{u^{A}}(x)A..\perp\cdot,u^{A}}$$\Gamma\vdash’\overline{\lambda_{X^{A}}.!\perp u^{A}(x^{A}).\cdot\neg A\cdot,u^{A}}(\supset I)$(catch)$\overline{\Gamma\vdash 7.u^{A}.\lambda xA.!\perp u^{A}(_{X^{A}})\cdot.\neg A\mathrm{v}A\cdot,}$

which is the same as
It is possible to consider a more liberal system
except that we have the following implication elimination rule instead ofrule above.
the$\mathrm{P}\mathrm{A}_{\mathrm{c}/i}^{+}$$\mathrm{P}\mathrm{A}_{c/t}$$(\supset E)$$. \frac{\Gamma\vdash P.A\supset B\cdot\Delta\Pi..\vdash Q\cdot A,\Sigma}{[^{1},[[\vdash \mathrm{a}\mathrm{P}\mathrm{p}1\mathrm{y}(\int\prime(\mathit{1})\mathcal{B},\Delta,\underline{1}^{1}},,\cdot.\cdot(\supset\Gamma_{J}^{l})^{+}$The difference between these two implication elimination rules is that in
it is possible to apply a function to an argument that has free tag variables, while.
a function can be applied only to an argument that is tag variableinis logically equivalent to PA by the same argument.
We can also show thatis therefore consistent, but we could not find a sound BHK$(\supset E)^{+}$$\mathrm{f}\mathrm{i}\cdot \mathrm{e}\mathrm{e}$$(\supset E)$$\mathrm{P}\mathrm{A}_{c/t}^{+}$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{e}\mathrm{r}\mathrm{p}_{1}\cdot \mathrm{e}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}_{\mathrm{o}\mathrm{n}}$$\mathrm{P}\mathrm{A}_{\mathrm{C}/\mathrm{r}}^{+}$

for$\mathrm{P}\mathrm{A}^{+}$.
wish to give an interpretation of judgments derivable inWe
an e. We will call suchis derivable in:
Suppose thatan -formula. In order to interpretderivation (extended derivation) andthese syntactic entities, we will extend the notions of proposition and proof tothose of -proposition and -proof. In summary, we have the following table.
$c/t\mathrm{n}\mathrm{o}\mathrm{W}$$\mathrm{P}\mathrm{A}_{c/t}$$\Gamma\vdash P$$A;\Delta$$\mathrm{P}\mathrm{A}_{c/t}$$A,\cdot\Delta$$\mathrm{e}$$\mathrm{e}$

$e$

$P$

40

$\ovalbox{\tt\small REJECT}_{\mathrm{e}-}^{\mathrm{t}\mathrm{e}\mathrm{r}}\mathrm{t}\mathrm{e}-\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{m}}\mathrm{u}1\mathrm{a}(A,\Delta)\mathrm{e}_{\mathrm{P}\mathrm{p}}- \mathrm{r}\mathrm{o}\mathrm{o}\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{o}\mathrm{n}(s,\theta)\mathrm{t}\mathrm{a}\mathrm{d}\mathrm{e}\mathrm{r}\mathrm{i}_{\mathrm{V}}\mathrm{g}\mathrm{C}\mathrm{o}\mathrm{n}\mathrm{e}_{\mathrm{i}_{0}\mathrm{n}}\mathrm{x}\mathrm{t}\mathrm{m}(a)\mathrm{n}\mathrm{a}\mathrm{t}\mathrm{u}\mathrm{r}\mathrm{a}_{\mathrm{f}}1\mathrm{n}\mathrm{u}\mathrm{m}\mathrm{a}\mathrm{t}(\Delta(P)\mathrm{p}_{1}\mathrm{o}\mathrm{p}\mathrm{o}\mathrm{s}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}_{\mathrm{i}}\mathrm{n}\mathrm{e}\mathrm{n}\mathrm{v}\mathrm{i}\mathrm{r}\mathrm{o}\mathrm{n}\mathrm{m}\mathrm{e}\mathrm{n}\mathrm{t}(\theta))\mathrm{e}-\mathrm{p}1\mathrm{o}\mathrm{O}(p)\mathrm{b}\mathrm{e}\mathrm{r}(k)$We begin with a preliminary discussion that is necessary to give our interpretation. First, we prepare a notation. Let be a tag variable, be a proof
and be a proposition, then we write $up$ for the pair $(u, p)$ and $uU$ for the set$\{up|p\in U\}$ .
Let be a proposition and $X$ be an arbitrary set. We define a set $S;X$ by
induction on the construction of as follows.
$u$

$p$

$U$

$S$

$S$

or $S=\{k\}$ , then $S;X=\Delta S\cup X$ .
1. If
2. $S\cross T;X=\triangle(S;X\cross T;X)\cup X$ .
3. $S+T;^{x}=\triangle(S;X+T;^{x})\cup X$ .
4. $Sarrow T;X=\triangle(Sarrow(T;X))\cup X$ .
5. $\prod_{k}S_{k;}X=\Delta(\prod k(Sk;x))\cup X$ .
6. $\sum_{k}s_{k;}x=\triangle(\sum_{k}(S_{k;^{x}}))\cup X$ .
$S=\emptyset$

We have the following lemma which we can verify by induction on the construction of .
$U$

Lemma9. If

is a proposition and$U$$X\subseteq Y$, then $U;X\subseteq U;Y$ .

be a function such thatis a finite set of tag variables and. We call such a proposition environment.
is a proposition for any
denotes the
If is a proposition environment and is a tag variable, then.
restriction of to
Suppose that is a proposition environment such that
where are distinct and $U_{i}=\theta(u_{i})(1\leq i\leq n)$ . Then for any set $X$ we associateby putting:another set
Let$\theta$$\theta(u)$$\mathrm{d}\mathrm{o}\mathrm{m}(\theta)$$\theta$$u\in \mathrm{d}\mathrm{o}\mathrm{m}(\theta)$$\theta$$\theta-u$$u$$\theta$$\mathrm{d}\mathrm{o}\mathrm{m}(\theta)-\{u\}$$\mathrm{d}\mathrm{o}\mathrm{m}(\theta)=\{u_{1}, \ldots, u_{n}\}$$\theta$$u_{i}$$\varphi(X)$$\varphi(X)=\triangle u_{1}(U_{1} ; X)\cup\cdots\cup u_{n}(U_{n}; X))$and we define
as the smallest fixed point offollowing set equation.
$|\theta|$$|\theta|=u_{1}\Delta(U_{1}; |\theta|)\cup\cdots\cup u_{n}$$\varphi.$(Un;

Theref.O$|\theta|$$\mathrm{r}\mathrm{e},$$|\theta|$

satisfies the).

If is a proposition and is a proposition environment, then we simply
for
write
and call such a set an -proposition (extended proposition).
be an -proof.
Elements of -propositions will be called -proofs. Let, we putis exceptional if
and proper otherwise. If$V|p$ is exceptional} and{ $p\in V|p$ is proper}.
$S$$\theta$$S;|\theta|$$S;\theta$

$e$

$e$

$\mathrm{e}$$p\in|\theta|$$p\in S;\theta$$V\subseteq S;\theta$$V_{\mathrm{p}}=\triangle$$\mathrm{e}$$p$$V_{\mathrm{e}}=\triangle\{p\in$41. We define a set
Let be an -proof in, thenvariables simultaneously as follows. If, and in this case we put
and$r$$r\in|\theta|$$\{up\}\cup!(p)$$!(r)=\triangle\{$$!(p)$$r\not\in|\theta|$$r$$\mathrm{T}\mathrm{V}(r)$$p\in\theta(u);\theta$$u\in \mathrm{d}\mathrm{o}\mathrm{m}(\theta)$

Ifof tagand a set
where
is of the form $up$$!(r)\subseteq|\theta|$$S;\theta$$\mathrm{e}$ifif$u\not\in \mathrm{T}\mathrm{V}(p)$,$u\in \mathrm{T}\mathrm{V}(p)$.

, then we define $!(r)$ inductively as follows.

.
or $S=\{k\}$ , then $r=k$ and we put
and we put $!(r)=!(p)\cup!\triangle(q)$ .
, thenor $r=(1,p)$ and we put
3. If $r\in S;\theta+T;\theta$ , then
1. If
2. If

$!(r)=\triangle\emptyset$$S=\emptyset$$r=(\mathrm{P}_{)}q)$$r\in S;\theta\cross T;\theta$$!(r)=!(p)\triangle$$r=(\mathrm{O},p)$4. If $r\in Sarrow(T;\theta)$ , then$!(r)= \triangle\bigcup_{p\epsilon S}!(r(p))$

.

.

5. If

$r \in\prod_{k}(S_{k;\theta)}$, then6. If$r \in\sum_{k}(S_{k;}\theta)$, then $r=(k, p)$ and we put $!(r)=!(p)\triangle$ .

We define$!(r)= \triangle\bigcup_{k}!(r(k))$

Ifsay that$\mathrm{T}\mathrm{V}(r)=\emptyset$$u$

by putting:$\mathrm{T}\mathrm{V}(r)\subseteq \mathrm{d}\mathrm{o}\mathrm{m}(\theta)${$\mathrm{T}\mathrm{V}(r)=\triangle$$u\in \mathrm{d}\mathrm{o}\mathrm{m}(\theta)|up\in!(r)$occurs inLemma10. If$r\in S;\theta$

andNext let $r\in S;\theta$ and$r/u$ will be said to be thefor some

is tag va
free and if. We have the following lemma.

, then we say that$\mathrm{T}\mathrm{V}(r)$.

$7\dot{n}a\iota le$$r$$u\not\in \mathrm{T}\mathrm{V}(r)$$u\in \mathrm{d}\mathrm{o}\mathrm{m}(\theta)$

$u$

$p$

}

$u\in \mathrm{T}\mathrm{V}(r)$, then we, then $r\in S;\theta-u$ .

. We define a set$r/u\subseteq\theta(u);\theta$

as follows.

component of .
$r$$r/u=\{\triangle p|up\in^{\mathrm{I}}.(r)\}$if and only if $r/u$ is non-empty. We also have
It is easy to check thatthe following lemma which we can prove by using Lemma 10.
$u\in \mathrm{T}\mathrm{V}(r)$Lelnma 11. $r/u\subseteq\theta(u);\theta-u$ .

If an -proof is in the component of an -proof , then it means that $up$
is a possible exceptional value of . So, unlike ordinary proofs we discussed in
section 3, an -proof denotes a set of its possible values.
We now define the catch and the throw operations on -proofs. Let
be an -proof and be a tag variable. Then, we put
$u$

$p$

$\mathrm{e}$$\mathrm{e}$

$r$

$r$

$\mathrm{e}$$r\in S;\theta$$\mathrm{e}$$\mathrm{e}$$u$$!(u, r)=!(\triangle ur)$andif$\{(1,p)|p\in r/u\}$ if$\{(0, r)\}$$?(u, r)=\triangle\{$$u\not\in \mathrm{T}\mathrm{V}(r)$,$u\in \mathrm{T}\mathrm{V}(r)$.

42
By Lemma 11, we can see that $?(u, r)\subseteq S+U;\theta-u$ and if $r\in U;\theta$ , thenwhere $U=\theta(u)$ , For a set of -proofs, we put $!(u, V)= \Delta\bigcup_{p\in V}!(u, p)$$V$$!(u, r)\subseteq|\theta|$$\mathrm{e}$and $?(u, V)= \Delta\bigcup_{P\in V}?(u,p)$ .
be a tag context and be an environment. We define
Let be a context,,
by putting
a proposition environment whose domain isfor this .
. We will write
where. Thenis derivable in:Now, suppose that the judgmentof -proofs and, we will define a set
for any environment such that.
is non-empty andwill show that$\Delta$$\Gamma$$\epsilon$$\theta(u)=\Delta\epsilon[E\mathrm{I}$$\theta$$u^{E}\in\Delta$$\mathrm{d}\mathrm{o}\mathrm{m}(\Delta)$$\theta$$\epsilon \mathbb{I}\Delta \mathrm{J}$$\Gamma\vdash P$

3.
4.
5.
6.
7.
8.

9.
10.
11.
12.
13.
14.

$\epsilon \mathrm{I}!u(P)\mathrm{I}^{\triangle}=!(u, \epsilon[P\mathrm{I})$$\epsilon \mathrm{I}^{7}.u$

.

.

.

$\epsilon \mathbb{I}|.\mathrm{d}(a)1=\triangle\{\epsilon[a\mathrm{I}\}$.

$\epsilon \mathrm{I}\mathrm{r}\mathrm{e}_{\mathrm{P}}|(P, Q)\mathrm{I}^{\triangle_{\epsilon}}=\mathbb{I}^{Q\mathrm{I}}$$\epsilon \mathrm{I}\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(P)\mathrm{I}=\{k\triangle+1|k\in\epsilon \mathbb{I}^{P}\mathrm{J}_{\mathrm{p}^{\}\cup}}\epsilon[P\mathrm{I}\mathrm{e}\cdot$$\epsilon[\mathrm{a}\mathrm{b}\mathrm{o}\mathrm{r}\mathrm{t}(P)\mathrm{I}=\epsilon \mathrm{I}\triangle P\mathrm{I}\cdot$$\epsilon \mathbb{I}\mathrm{r}\mathrm{e}\mathrm{c}(P, Q)\mathrm{I}=\triangle${ $rec(p,$$\epsilon \mathbb{I}\mathrm{p}\mathrm{I}\mathrm{u}\mathrm{S}(0, b)\mathrm{I}=\{\triangle\epsilon[b\mathrm{I}\}$$q)|p\in\epsilon \mathrm{I}P\mathrm{J}$

and

{

.

.

$\epsilon[\mathrm{t}[\mathrm{m}\mathrm{e}\mathrm{s}(\mathrm{S}\mathrm{u}\mathrm{c}\mathrm{c}(a), b)\mathrm{I}=\triangle\{(\epsilon[a\mathrm{I}+1)\epsilon[b\mathrm{I}\}$$\epsilon[\mathrm{p}\mathrm{a}|\mathrm{r}(P, Q)\mathrm{I}=\triangle$}.

.

$\epsilon[\mathrm{p}\mathrm{l}\mathrm{u}\mathrm{s}(\mathrm{S}\mathrm{U}\mathrm{c}\mathrm{c}(a), b)\mathrm{J}=\triangle\{\epsilon[a\mathrm{J}+1+\epsilon \mathrm{I}b\mathrm{J}\}$$\epsilon[\mathrm{t}[\mathrm{m}\mathrm{e}\mathrm{s}(0, b)\mathrm{J}=\triangle\{0\}$$q\in\epsilon[Q\mathrm{J}$and$(p,$ $q)|p\in\epsilon[P\mathrm{I}$.
$q\in\epsilon[Q\mathrm{I}$}$\cup\epsilon[P\mathrm{I}\mathrm{e}\cup\epsilon[Q\mathrm{J}_{\mathrm{e}}$$\epsilon[\mathrm{c}\mathrm{a}’(P)\mathrm{I}^{\triangle}=\{\pi_{0}(p)|p\in\epsilon[P\mathrm{J}_{\mathrm{p}}\}\cup\epsilon[P\mathrm{J}_{\mathrm{e}}$.

16.

$\epsilon[\mathrm{c}\mathrm{d}\mathrm{r}(P)\mathrm{J}=\triangle\{\pi_{1}(p)|p\in\epsilon[P\mathrm{I}_{\mathrm{P}}\}\cup\epsilon[P\mathrm{J}_{\mathrm{e}}$.

17.

$\epsilon[\mathrm{s}\mathrm{p}^{1}|.\mathrm{t}(P, (x, y).Q)\mathrm{J}=\triangle\bigcup_{(p},q)\in\epsilon \mathbb{I}P\mathrm{I}\epsilon[x=p][y=q][Q\mathrm{I}\cdot$

18.

$\epsilon[|\mathrm{n}1(P)\mathrm{I}=\triangle\{(0,p)|p\in\epsilon \mathbb{I}P\mathrm{I}\}\cup\epsilon[P\mathrm{I}\mathrm{e}\cdot$

21.

$\epsilon[\mathrm{I}\mathrm{n}\mathrm{r}(P)\mathrm{I}=\triangle\{(1,p)|p\in\epsilon \mathbb{I}P\mathrm{I}\}\cup\epsilon[P\mathrm{I}\mathrm{e}\cdot$$\epsilon[\mathrm{c}\mathrm{a}\mathrm{S}\mathrm{e}(P, x.Q, y.R)\mathrm{I}=\triangle\bigcup_{(0,p)\in}\epsilon \mathbb{I}P\mathrm{I}\epsilon[X=p][Q\mathrm{J}\cup\bigcup_{(1,p)\in\epsilon}\mathbb{I}P\mathrm{I}\epsilon[y=p][R\mathrm{I}\cdot$$\epsilon[\lambda_{X^{A}}.P\mathrm{J}=\Delta${$f|\mathrm{d}\mathrm{o}\mathrm{m}(f)=\epsilon \mathbb{I}A\mathrm{I}$$\bigcup_{p\in\epsilon\beta}A1\epsilon[x=\mathrm{P}][P\mathrm{J}_{\mathrm{e}}$22.

$\epsilon[\lambda x.P\mathrm{I}=\triangle$$\bigcup_{k}\epsilon[x=k]$

23.

24.

.

$\epsilon[\mathrm{p}\mathrm{a}|\mathrm{r}(a, P)\mathrm{J}=\triangle\{(\epsilon[a\mathrm{I},p)|p\in\epsilon[P\mathrm{J}\}\cup\epsilon \mathbb{I}P\mathrm{I}\mathrm{e}\cdot$

15.

19.
20.

$\mathrm{e}$.

$P\mathrm{J}=?(u, \epsilon \mathbb{I}P\mathrm{I}\triangle)$$\epsilon \mathbb{I}x\mathrm{J}^{\Delta}=\{\epsilon.x\}$$\epsilon[P\mathrm{I}$$\epsilon[P\mathrm{I}\subseteq\epsilon[A\mathrm{J};\epsilon[\Delta \mathrm{J}$$\epsilon[P\mathrm{J}$2.

$\mathrm{P}\mathrm{A}_{c/t}$$\epsilon\models\Gamma$$\epsilon$

1.

$A;\Delta${

and$f(p)\in\epsilon[x=p]\mathrm{I}P\mathrm{J}$for all.

$f|\mathrm{d}\mathrm{o}\mathrm{m}(f)=\mathrm{N}$and $f(k)\in\epsilon[x=k][P\mathrm{I}$ for all[PIe .

$\epsilon[\mathrm{a}\mathrm{p}\mathrm{P}^{1}\mathrm{y}(P, Q)\mathrm{I}=\triangle$$\epsilon[\mathrm{a}\mathrm{p}\mathrm{p}^{1}\mathrm{y}(P, a)\mathrm{I}=\triangle${{$p\in\epsilon[A\mathrm{I}$$p(q)|p\in\epsilon[P\mathrm{I}_{\mathrm{P}}$and$p(k)|p\in\epsilon[P\mathrm{I}_{\mathrm{P}}$and$q\in\epsilon[Q\mathrm{I}$$k\in\epsilon[a\mathrm{I}$}}$\cup\epsilon[P\mathrm{I}\mathrm{e}\cdot$$\cup\epsilon \mathbb{I}P\mathrm{I}\mathrm{e}\cdot$$k\in \mathrm{N}$}$\cup$}$\cup$

43

We have the following soundness theorem for

Theorem 12. If
and$\Gamma\vdash P:A;\Delta$

is de vable in$\mathrm{P}\mathrm{A}_{\mathrm{c}/t}$$7\dot{\mathrm{Y}}$$\mathrm{P}\mathrm{A}_{c/t}$

;

.

and

$\epsilon\models\Gamma$, then$\epsilon[P\mathrm{I}\neq\emptyset$.

$\epsilon[P\mathrm{I}\subseteq\epsilon[A\mathrm{I};\epsilon[\Delta \mathrm{J}$Proof. By induction on the construction of derivations. We check typical cases

only. Since the verification of the non-emptiness ofthat
Case (throw): The rule we consider is as follows.

is easy, we only verify$\epsilon[P\mathrm{J}$$\epsilon[P\mathrm{I}\subseteq\epsilon[A\mathrm{I};\epsilon[\Delta \mathrm{I}\cdot$$\cdot\frac{\Gamma\vdash P.E,\Delta\Pi.\vdash A\cdot \mathrm{p}\mathrm{r}\mathrm{o}_{\mathrm{P}}}{\Gamma_{)}\Pi\vdash!_{A}u^{E}(P)\cdot A\cdot\Delta,u^{E}}$,Suppose that$\epsilon\models\Gamma,$$\epsilon[P\mathrm{I}\subseteq\epsilon[E\mathrm{J};\epsilon[\Delta \mathrm{I}\cdot$$\Pi$

So, if. Then(throw)and by induction hypothesis, we have,
, then we have$\epsilon\models\Gamma$$p\in\epsilon \mathbb{I}P\mathrm{J}$$p\in\epsilon \mathbb{I}E\mathrm{I};\epsilon \mathbb{I}\Delta \mathrm{I}\subseteq\epsilon \mathbb{I}E\mathrm{I};\epsilon[\Delta,$$u\mathrm{J}E$

so thatCase (catch): We consider the following rule:$!(u,p)\subseteq\epsilon \mathbb{I}\Delta,$ $u^{E}\mathrm{I}\subseteq\epsilon[A\mathrm{I};\epsilon[\Delta,$$u^{E}\mathrm{I}\cdot$$. \frac{\Gamma\vdash P.A\cdot\Delta}{\Gamma\vdash 7u^{E}.P\cdot A\mathrm{v}E\cdot\Delta-uE}.’$,

Suppose that
Suppose that$\epsilon\models\Gamma$(catch). Then, by induction hypothesis, we. We have two cases to consider.

$\mathrm{h}\mathrm{a}\mathrm{v}\mathrm{e}\epsilon[P\mathrm{I}\subseteq\epsilon[A\mathrm{I};\epsilon[\Delta \mathrm{I}\cdot$$r\in\epsilon \mathrm{I}P\mathrm{J}$-Case: does not occur in . In this case, we have
Lemma 10. So, we have $?(u, r)=\{(0, r)\}$ where-Case: occurs in . By Lemma 11, we havefor any $p\in r/u$ .
we have$r\in\epsilon \mathbb{I}A\mathrm{I};\epsilon[\Delta-u^{E}\mathrm{I}$

$r$

$u$

by

.
Hence,$(0, r)\in\epsilon \mathrm{I}A\vee E\mathrm{I};\epsilon \mathrm{I}\Delta-u^{E}\mathrm{I}$$r/u\subseteq\epsilon \mathbb{I}E\mathrm{J};\epsilon[\Delta-u^{E}\mathrm{I}\cdot$

$r$

$u$

$(1, p)\in\epsilon[AE\mathrm{I};\epsilon[\Delta-u^{E}\mathrm{I}$So, the theorem holds in this case.
rule in: The
Case$(\vee E)$$(\vee E)$$\mathrm{P}\mathrm{A}_{c/t}$

takes the following form.

$. \frac{\Gamma\vdash P\cdot A\vee B\Pi\vdash Q.c,\Sigma\Phi\vdash R.C.\Psi}{\Gamma,\Pi-x^{A},\Phi-y^{B}\vdash \mathrm{c}\mathrm{a}\mathrm{s}\mathrm{e}(P,X^{A}.Q,y^{B}.R).C,\Sigma,\Psi}...\cdot,\cdot(\vee E)$

Suppose that
we have$\epsilon\models\Gamma,$$\Pi-x^{A},$ $\Phi-y^{B}$$\epsilon[P\mathrm{J}\subseteq\epsilon \mathrm{I}A\vee B\mathrm{I}\cdot$$p\in\epsilon \mathrm{I}A$

I or $r=(1,p)$ andTake any$p\in\epsilon \mathrm{I}B\mathrm{I}$. Then$r\in\epsilon \mathbb{I}P\mathrm{I}$. So, by induction hypothesis,. Then we have either $r=(0,p)$ and$\epsilon\models\Gamma$. In the first case, we have $\epsilon[x=p]\models\Pi$ andby induction hypothesis we have$\epsilon[x=p][Q\mathrm{I}\subseteq\epsilon[X=p][C\mathrm{I}).\epsilon[x=p][\Sigma \mathrm{I}=\epsilon[C\mathrm{I};\epsilon[\Sigma \mathrm{I}\subseteq\epsilon[c\mathrm{I};\epsilon[\Sigma,$$\Psi \mathrm{I}\cdot$

We can handle the second case similarly. Hence we have the theorem in this case.
: The rule in question is:Case$(\supset I)$$.. \frac{\Gamma\vdash P.B,\Delta\Pi\vdash.\cdot A.\mathrm{p}\mathrm{r}\mathrm{o}_{\mathrm{P}}}{\Gamma-x^{A},\Pi\vdash\lambda x^{A}.PA\supset B,\Delta}..(\supset I)$

Suppose that$\epsilon\models\Gamma-x^{A},$ $\Pi$. Take any$r\in\epsilon[\lambda x^{A}.P\mathrm{I}\cdot$

There are two possibilities.

44

is a function such that
Then, we have. Let
we have
hypothesis,
Hence, by induction-Case$\mathrm{d}\mathrm{o}\mathrm{m}(r)=\epsilon[A$$r$$r(p)\in\epsilon[x=p][P\mathrm{I}$$r(p)\in\epsilon[x=p]\mathrm{I}P\mathrm{J}$$p\in\epsilon[A\mathrm{I}\cdot$$p\in\epsilon[A\mathrm{J}$

I and

and

for all$\epsilon[x=p]\models\Gamma$.

$r(p)\in\epsilon[x=p]\mathrm{I}B\mathrm{I};\epsilon[_{X=}p][\Delta \mathrm{I}=\epsilon \mathrm{I}B\mathrm{I};\epsilon[\Delta \mathrm{I}\cdot$

Therefore, we have$r\in\epsilon \mathrm{I}^{A}\mathrm{I}arrow(\epsilon[B\mathrm{J};\epsilon[\Delta \mathrm{I})=(\epsilon[A\mathrm{I}arrow\epsilon[B\mathrm{I});\epsilon[\Delta \mathrm{J}=\epsilon[A\supset B\mathrm{I};\epsilon[\Delta \mathrm{J}$-Case:
some

In this case, we haveHence, by induction hypothesis, we have$r \in\bigcup_{p\in\epsilon \mathbb{I}A}$$p\in\epsilon[A\mathrm{I}\cdot$

I$r\in\epsilon[x=p][P\mathrm{I}\mathrm{e}$$\epsilon[x=p][P\mathrm{J}\mathrm{e}\cdot$$r\in\epsilon[x=p][B\mathrm{J};\epsilon[x=p][\Delta \mathrm{I}=\epsilon \mathbb{I}B\mathrm{I};\epsilon[\Delta \mathrm{J}$

But, sinceCaseis exceptional, we have$r$$(\supset E)$

.

for

.

$r\in|\epsilon[\Delta \mathrm{I}|\subseteq\epsilon \mathbb{I}A\supset B\mathrm{I};\epsilon \mathrm{I}\Delta \mathrm{J}$.

: The rule in question is:$.. \frac{\Gamma\vdash P.A\supset B,\Delta\Pi.\vdash Q.A}{\Gamma,\Pi\vdash \mathrm{a}_{\mathrm{P}\mathrm{p}^{1}\mathrm{y}}(P,Q).B\cdot\Delta},\cdot(\supset E)$

Suppose that$\epsilon\models\Gamma,$$\Pi$

and take any$r\in\epsilon\square \mathrm{a}\mathrm{p}\mathrm{p}\mathrm{l}\mathrm{y}(P, Q)\mathrm{I}$such that-Case: $r=p(q)$ for someinduction hypothesis, we have$p,$ $q$. Then we have two cases.
andand$q\in\epsilon[Q\mathrm{I}\cdot$$p\in\epsilon[P\mathrm{J}_{\mathrm{P}}$$p\in\epsilon[A\mathrm{J}arrow(\epsilon[B\mathrm{J};\epsilon[\Delta \mathrm{I})$

Then, by, so that$q\in\epsilon \mathbb{I}A\mathrm{J}$$r=p(q)\in\epsilon \mathrm{I}B\mathrm{J};\epsilon[\Delta \mathrm{I}\cdot$-Case:$r\in\epsilon[P\mathrm{I}\mathrm{e}\cdot$

In this case, we have$r\in|\epsilon[\Delta \mathrm{J}|\subseteq\epsilon \mathrm{I}B\mathrm{J})\epsilon[\Delta \mathrm{J}$.
$\square$We give a simple example. Let be the empty environment and suppose that
: Prop, that is, is a closed formula. Then, as we saw before, the judgment$\epsilon$$A$$\vdash A$$\vdash 7_{u^{A.A}}.\lambda x.!\perp^{u^{A}}(x^{A})$is derivable inthat:$\mathrm{P}\mathrm{A}_{c/t}$$\epsilon[^{7}.u$.

: $\neg AA$. By the definition of our BHK interpretation, it follows$\lambda x^{A}.!\perp^{u(}x^{A}$)$\{(0, \emptyset)\}$$\mathrm{I}=\{$$\{(1,p)|p\in\epsilon \mathbb{I}A\mathrm{J}\}$

if
if$\epsilon[A\mathrm{I}=\emptyset$,$\epsilon[A\mathrm{I}\neq\emptyset\cdot$

So, if the proposition (denoted by) is false, then the derivation denotes the left
, that is the left injection
injection of the unique proof of (the denotation of)of the empty function, and if is true, then the derivation denotes the rightinjection of the set of all proofs of .
derivations. We have the following
Let us consider the reduction of. Via the Curry-Howardin addition to those forrules.
can be seen as functional programs and these
lsomorphism, derlvations in
reduction rules can be thought of as giving operational semantics to these func$A$$\neg A$$A$

$A$$\mathrm{P}\mathrm{A}_{c/t}$.eduction$\mathrm{r}$fo.rtional programs.

$\mathrm{H}\mathrm{A}$$\mathrm{P}\mathrm{A}_{c/t}$$\mathrm{P}\mathrm{A}_{c/t}$

45, then 7. .
1. If.
, then
2. If
3. $!v(!u(P))\mapsto!u(P)$ .
.
4.
.
5.
.
6.
$u$

$u\not\in \mathrm{F}\mathrm{V}(P)$$7_{u}.$$u\not\in \mathrm{F}\mathrm{V}(P)$$P\mapsto|\mathrm{n}1(P)$.

$!u(P)\mapsto\dot{|}\cap \mathrm{r}(P)$.

$\mathrm{a}\mathrm{b}_{\mathrm{o}\mathrm{r}\mathrm{t}}(!u(P))\mapsto!u(P)$$\mathrm{p}\mathrm{a}\mathrm{I}^{\cdot}\mathrm{r}(!u(P), Q)\mapsto!u(P)$$\mathrm{p}\mathrm{a}\mathrm{I}^{\cdot}\mathrm{r}(P, !u(Q))\mapsto!u(Q)$7.
8. car $(!u(P))\mapsto!u(P)$ .
.
9.
10. $|\mathrm{n}1(!u(P))\mapsto!u(P)$ .
.
11.

$\mathrm{p}\mathrm{a}|.\mathrm{r}(a, !u(P))\mapsto!u(Q)$.

$\mathrm{c}\mathrm{d}\mathrm{r}(!u(P))\mapsto!u(P)$$\dot{\mathrm{I}}\mathrm{n}\mathrm{r}(!u(P))\mapsto!u(P)$.
12.
$(!u(P),a)\mapsto!u(P)$.
13. apply$\mathrm{a}\mathrm{p}\mathrm{p}^{1}\mathrm{y}(!u(P), Q)\mapsto!u(P)$Then these reduction rules enjoy the following subject reduction property.

Theorem 13. If has type under.
smaller than
some
$A$

$P$

$\Pi;\Sigma$$\Gamma;\Delta$

and $P\mapsto Q$ , then$Q$

has type

$A$

under

$\Gamma;\Delta$

Moreover, the BHK interpretation respects these reduction rules in the following

way.
Theoreln 14. If$P$

has type

$A$

under

$\Gamma;\Delta,$$\epsilon\models\Gamma$

and$P\mapsto Q_{f}$then$\epsilon[P\mathrm{J}\supseteq$$\epsilon[Q\mathrm{I}\cdot$

5

Concluding remarks

In this paper, we defined propositions and proofs as abstract mathematical entities and showed that formulas and derivations, which are introduced as formal
counterparts to propositions and proofs, can be interpreted by the classical version of BHK interpretation. As a concrete example of classical BHK interpre. Thistation, we gave an interpreration for classical first order arithmetic
interpretation is almost constructive, since the interpretation of a derivation is
the same as the interpretation for constructive arithmetic HA if the derivation is obtained without using the law of the excluded middle. We showed thatthe interpretation is sound and the denotation of derivation is preserved under
reductions of derivations.
of theWe also gave an interpretation for the system
calculus which is obtained from HA by adding the rules for the catch and throw, the law of the excluded middle is derivable by using theoperations. In
rules. If we look at such a derivation as a program, then we cannot
compute (reduce) it in a constructive way. However, Murthy [4] formulated PA
control operator which(as a progranuning language), roughly, as HA
serves as a witness of the law of the double negation elimination, and showed
can be computed constructively.
sentence , if : , thenthat for any
We take this as a hint that we might be able to extract constructive contents$\mathrm{P}\mathrm{A}$$\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{c}\mathrm{h}/\mathrm{t}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{w}$$\mathrm{P}\mathrm{A}_{c/t}$$\mathrm{P}\mathrm{A}_{c/t}$$\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{h}/\mathrm{t}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{w}$$+\mathrm{t}\mathrm{h}\mathrm{e}$$\Pi_{2}^{0}$

$A$

$P$

$A$

$P$

$C$

46

, since the law of the double negationfrom classical derivations derived in.
elimination is certainly derivable in
In order to pursue the possibility of extracting constructive contents from
calculus, we do a case study using an example given in [4]. We
theinformally. We consider the sentence
will work in$\mathrm{P}\mathrm{A}_{c/t}$$\mathrm{P}\mathrm{A}_{c/t}$$\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{c}\mathrm{h}/\mathrm{t}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{w}$$\mathrm{P}\mathrm{A}_{c/t}^{+}$$A=\triangle\exists n$. $prime(n)\wedge n<100$

be a derivation of prime (3)be a derivation of prime (2) $\wedge 2<100$ and: . We writeand:$3<100$ , so that we havefor these derivations. Then, we can derive the followand P3 ::ing judgmentl, where the first abort is) and the second abort is
.
Let

$A$

$\vdash \mathrm{P}^{\mathrm{a}1\mathrm{r}_{A(2,P_{2})}}$$\vdash \mathrm{P}_{2}$$\wedge$$P_{3}$$P_{2}$$A$$A$$\vdash \mathrm{P}^{\mathrm{a}1\mathrm{r}_{A(3,P_{3})}}$$A$$\vdash$$\mathrm{a}\mathrm{b}\mathrm{o}\mathrm{r}\mathrm{t}_{pe(10}rim2$$\mathrm{a}\mathrm{b}\mathrm{o}\mathrm{r}\mathrm{t}_{\mathrm{l}0}2<100$$\vdash\lambda X^{\urcorner A}$.

$X(\mathrm{p}\mathrm{a}|\mathrm{r}_{A}(102, \mathrm{P}\mathrm{a}\mathrm{i}\mathrm{r}(\mathrm{a}\mathrm{b}\mathrm{o}\mathrm{r}\mathrm{t}(X(\mathrm{p}_{2})), \mathrm{a}\mathrm{b}\mathrm{o}\mathrm{r}\mathrm{t}(x(\mathrm{P}3)))))$:$\neg\neg A$

We can also derive the following judgment.
.

$\vdash\lambda y^{\neg\neg A}..u^{A}$$y(7\lambda_{X^{A}}.

We
that we$\mathrm{w}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{e}\vdash Y$:$:\perp\vee A$$X=\lambda_{X}\triangle A$.

$1_{\perp^{u(x)}}.$:$\neg\neg A\supset\perp\vee A$

for the above two judgments2 so. We can compute $C(Y)$ as follows, where we put$\neg\neg A\mathrm{a}\mathrm{n}\mathrm{d}\vdash C$$\mathrm{h}\mathrm{a}\mathrm{v}\mathrm{e}\vdash C(Y)$!_{\perp^{u}}(x))$:$\neg\neg A\supset\perp\vee A$.

$C(Y)arrow 7_{u^{A}.Y(\lambda X^{A}}.$.

$!_{\perp^{u}}(x))$( $X$ (P3)) $)))$$arrow 7.u^{A}$.

$x(\mathrm{p}\mathrm{a}|\mathrm{r}_{A}(102, \mathrm{p}\mathrm{a}\mathrm{I}\mathrm{r}(\mathrm{a}\mathrm{b}_{\mathrm{o}\mathrm{r}\mathrm{t}(X(}\mathrm{P}2)),$$arrow 7.u^{A}$.

$X(\mathrm{p}\mathrm{a}|\mathrm{r}_{A}(102, \mathrm{P}\mathrm{a}\mathrm{i}\mathrm{r}(\mathrm{a}\mathrm{b}_{0}r\mathrm{t}(!u(\mathrm{p}_{2})), \mathrm{a}\mathrm{b}_{0}\mathrm{r}\mathrm{t}(!u(\mathrm{p}_{3})))))$$\mathrm{a}\mathrm{b}\mathrm{o}\mathrm{r}\mathrm{t}$$arrow 7_{u^{A}.X(\mathrm{P}}.\mathrm{a}|\mathrm{r}_{A}(102, \mathrm{p}\mathrm{a}|\mathrm{r}(!u(\mathrm{P}_{2}), \mathrm{a}\mathrm{b}\mathrm{o}\mathrm{r}\mathrm{t}(!u(\mathrm{p}_{3})))))$$arrow 7_{u^{A}.x(\mathrm{r}_{A}}.\mathrm{p}\mathrm{a}\dot{|}(102, !u(\mathrm{P}2)))$$arrow 7_{u^{A}.X(!(}.u\mathrm{p}_{2}))$$arrow 7_{u^{A}}.$.

$!u(\mathrm{p}_{2})$$arrow\dot{|}\mathrm{n}\mathrm{r}(^{\mathrm{p}_{2}})$

We could thus read off the constructive content of the classical derivation $C(Y)$similarly.
. We can also get
By the above observation, we saw that it is possible to extract constructive. However, at present, we do notcontent from some classical derivations inknow whether we can extract constructive content from any derivation of. Also, we do not know if we can give a sound BHK interpretasentence in, the argument of any functional application. Note that intion for$\mathrm{o}\mathrm{f}\perp\vee A$$C(Y)arrow|\mathrm{n}\mathrm{r}(\mathrm{p}_{3})$$\mathrm{P}\mathrm{A}_{c/t}^{+}$$\Pi_{2}^{0}$$\mathrm{P}\mathrm{A}_{c/t}^{+}$$\mathrm{P}\mathrm{A}_{c/t}$$\mathrm{P}\mathrm{A}_{c/t}^{+}$

1
2

simplicity.
We write $a(b)$ for apply, since in
We note that is not a valid derivation ina function to an argument having a free tag variable.
$(a, b)\mathrm{f}\mathrm{o}\mathrm{i}$$C$$\mathrm{P}\mathrm{A}_{c/t}$$\mathrm{P}\mathrm{A}_{c}/\iota$

we cannot apply

47

must be tag variable free, and the soundness of the BHK interpretation forcomes from this restriction.
A number of classical logical systems have been introduced recently andmost of them are explicitly designed to extract constructive contents of classicalderivations ([1, 2, 4, 7, 8, 9, 10]). We hope that the classical BHK interpretation
is useful for the analysis ofthese systems.
$\mathrm{P}\mathrm{A}_{c/t}$

Acknowledgment s
We thank Yukiyoshi Kameyama and Izumi Takeuti for discussions on BHK
interpretaion and Susumu Hayashi for drawing our attention to Troelstra and-Aid for thevan Dalen [12]. This work was supported in part by the
Science Research of Ministry of Education, Science and Culture (No. 08558023).
$\mathrm{G}\mathrm{r}\mathrm{a}\mathrm{n}\mathrm{t}_{-}\mathrm{i}\mathrm{n}$References
1. Barbanera, F. and Berardi, S., A symmetric lambda calculus for “classical” program extraction, pp. 495-515, in Theoretical Aspects of Computer Software, Lecture
Note in Computer Science 789, Hagiya, M. and Mitchell, J.C. (eds.), SpringerVerlag, 1994.
-types notion of control, pp. 47-58, in Proc. 17th A CM
2. Griffin, T., A
Symp. on Principle of Programming Languages, ACM Press, 1990.
Mechanism, pp. 106-122,
Y., A New Formulation of the
Kameyama,3.
in Second Fuji International Workshop on Functional and Logic Programming, Ida,
T., Ohori, A. and Takeichi, M. (eds.), World Scientific, 1997.
4. Murthy, C., An evaluation semantics for classical prook, pp. 96-107, Proc. 5thIEEE Symp. Logic in Computer Science, IEEE Computer Society Press, 1991.
5. Nakano, H., A constructive formalization of the catch and throw mechanism, pp.
82-89, in Proc. 7th Ann. IEEE Symp. on Logic in Computer Science, 1992.
6. Nakano, H., The non-deterministic catch and throw mechanism and its subject
reduction property, pp. 61-72, in Logic, Language and Computation, Lecture Notes
in Computer Science 792, Jones, N. D., Hagiya, M. and Sato, M. (eds.), SpringerVerlag, 1994.
7. Ong, C.-H.L., A semantic view of classical proofs, pp. 230-241, in Proc. 11th IEEE
Ann. Symp. of Logic in Computer Science, Computer Science Press, 1996.
8. Ong, C.-H.L. and Stewart, C.A., A Curry-Howard foundation for functional computation with control, pp. 215-227, in Proc. 24th Ann. ACM Symp. on Principles
of Programming Languages, ACM Press, 1997.
9. Parigot, M., An algorithmic interpretation of classical natural deduction, pp. 190210, in Proc. International Conf. on Logic Programming and Automated Reasoning,
Lecture Notes in Artificial Intelligence 624, Springer-Verlag, 1992.
10. Rehof, N.J. and Sorensen, pp. 516-542, in Theoretical Aspects of Computer Software, Lecture Note in Computer Science 789, Hagiya, M. and Mitchell, J.C. (eds.),
Springer-Verlag, 1994.
11. Sato, M., Intuitionistic and classical natural deduction systems with the catch andthe throw rules, pp. 75-92, in Theoretical Computer Science 175, 1997.
12. Troelstra, A.S. and van Dalen, D., Constructivism in $Mathemati_{Cs,}$ An Introduction, Studies in Logic and the Foundation of Mathematics 121, North-Holland,$\mathrm{f}_{\mathrm{o}\mathrm{r}\mathrm{m}\mathrm{u}}1\mathrm{a}\mathrm{e}-\mathrm{a}S$$\mathrm{c}_{\mathrm{a}\mathrm{t}\mathrm{C}}\mathrm{h}/\mathrm{T}\mathrm{h}\mathrm{r}\mathrm{o}\mathrm{w}$1988.