Intuitionistic Existential Instantiation and Epsilon Symbol

Abstract

A natural deduction system for intuitionistic predicate logic with existential instantiation rule presented here uses Hilbert’s $\epsilon$-symbol. It is conservative over intuitionistic predicate logic. We provide a completeness proof for a suitable Kripke semantics, sketch an approach to a normalization proof, survey related work and state some open problems. Our system extends intuitionistic systems with $\epsilon$-symbol due to Dragalin and Maehara.

Prof. Mints passed away May 29, 2014

9.1 Introduction

In natural deduction formulations of classical and intuitionistic logic, the existence-elimination rule is usually taken in the form

where $a$ is a fresh variable. Existential instantiation is the rule

where $a$ is a fresh constant. It is sound and complete (with suitable restrictions) in the role of existence-elimination rule in classical predicate logic but is not sound intuitionistically, since it makes possible for example the following derivation:

There are several approaches in the literature to introduction of restrictions making this rule conservative over intuitionistic predicate calculus.

We present an approach using intuitionistic version of Hilbert’s epsilon-symbol and strengthening works by Dragalin Dragalin (1974) and Maehara (1970) where $\epsilon$-terms are treated as partially defined. Then a survey of extensions and related approaches including the important paper by Shirai (1971) is given and some problems are stated. There is an obvious connection with the problem of Skolemization of quantifiers. The role of existence conditions in that connection is prominent in the work by Baaz and Iemhoff (2006).

We do not include equality since in this case adding of $\epsilon$-symbol with natural axioms is not conservative over intutionistic logic (Mints 1974; Osswald 1975). A simple counterexample due (in other terms) to Smorynski (1977) is

$$ \forall x\exists yP(x,y)\rightarrow \forall xx'\exists yy'( Pxy \& Px'y' \& (x=x'\rightarrow y=y')) $$

In our natural deduction system NJ$\epsilon$ axioms and propositional inference rules are the same as in ordinary intuitionistic natural deduction, the same holds for $\forall$-introduction. The remaining rules are as follows:

(9.1)

existential instantiation,

(9.2)

where

$$\begin{aligned} \epsilon xA(x)\downarrow := \exists y(\exists xA(x)\rightarrow A(y)), \end{aligned}$$

(9.3)

and ${{\!\!}\downarrow }:=\top$ (the constant “true”) if $t$ is a variable or constant.

Two semantics are given for NJ$\epsilon$, or more precisely to an equivalent Gentzen-style system $\mathrm {IPC}\epsilon$ (Sect. 9.2). The first semantics, which is incomplete but convenient for a proof of conservative extension property over IPC is defined in Sect. 9.3.

The second semantics with a completeness proof for $\mathrm {IPC}\epsilon$ is given in Sect. 9.4.

Section 9.4.1 presents a sketch of a possible proof of a normal form theorem. Section 9.5 surveys some of the previous work and Sect. 9.6 outlines some open problems.

9.2 Gentzen-Style System IPC$\epsilon$

Let us state our Gentzen-style rules for the intuitionistic predicate calculus IPC$\epsilon$ with $\epsilon$-symbol. For simplicity we assume that the language does not have function symbols except constants. Formulas and terms are defined by familiar inductive definition plus one additional clause:

If $A(x)$ is a formula then $\epsilon xA(x)$ is a term.

Derivable objects of IPC$\epsilon$ are sequents $\Gamma \Rightarrow A$ where $\Gamma$ is a finite set of formulas, $A$ is a formula. This means in particular that structural rules are implicitly included below.

First, let’s list the rules of the intuitionistic predicate calculus IPC without $\epsilon$-symbol.

Axioms:

$$\begin{aligned} \Gamma ,A \Rightarrow A, \quad \Gamma ,\bot \Rightarrow A\ . \end{aligned}$$

Inference rules:

For IPC$\epsilon$ quantifier-inferences $\Rightarrow \exists ,\forall \Rightarrow$ are modified by requirement that the term $t$ substituted in the rule should be “defined” (cf. (9.3)).

(9.4)

$\exists \Rightarrow$-rule is also changed for IPC$\epsilon$:

(9.5)

A routine proof shows that IPC$\epsilon$ is equivalent to a Hilbert-style system obtained by weakening familiar axioms for quantifiers to

$$ (\epsilon Q1)\ {{\!\!}\downarrow } \& \forall xA(x)\rightarrow A(t) $$

$$ \begin{aligned} (\epsilon Q2)\ {{\!\!}\downarrow } \& A(t)\rightarrow \exists xA(x) \end{aligned}$$

and adding the axiom

$$ \exists xA(x)\rightarrow A(\epsilon xA(x)) $$

9.2.1 Equivalence of IPC$\epsilon$ and NJ$\epsilon$

Let us recall that in natural deduction a sequent

$$ A_1,\ldots ,A_n\Rightarrow A $$

is used to indicate that A is deducible from assumptions $A_1,\ldots ,A_n$.

Theorem 9.1

A sequent is provable in NJ$\epsilon$ iff it is provable in IPC$\epsilon$.

Proof

The proof is routine: every rule of one of these systems is directly derivable in the other system. Let’s show derivations of the rules $\exists i$ and $\exists \Rightarrow$ from each other using abbreviation $e:=\epsilon xF(x)$.

9.3 A Kripke Semantics for Intuitionistic $\epsilon$-symbol

To prove that IPC$\epsilon$ is conservative over IPC we present an incomplete semantics modifying a semantics from Dragalin (1974). The main modification is in the definition of ${{\!\!}\downarrow }$ and treatment of atomic formulas containing $\epsilon$-terms $\epsilon x A$.

Definition 9.1

Let $w$ be a world in a Kripke model. Denote

$$ \epsilon xA(x)\downarrow w:\equiv \ w \models \epsilon xA(x)\downarrow . $$

We say that a term $\epsilon xA$ is defined in $w$ iff $\epsilon xA(x)\downarrow w$.

The symbol $\bot$ in the next definition indicates the condition (9.6) below.

Definition 9.2

An intuitionistic Kripke $\epsilon \bot$-model (or simply model in this section)

$$ \mathcal {M}=(W,<,D,\models ,V) $$

has to satisfy the following conditions:

$(W,<)$ is a Kripke frame with a strict partial ordering $<$,

$D$ is a domain function assigning to every $w\in W$ a non-empty set $D(w)$ monotone with respect to $<$,

$w\models A$ is a relation between worlds $w\in W$ and atomic formulas $A$ with constants from

$$ D:= \cup _{w\in W}D(w) $$

monotonic with respect to $\le$ and such that

$$\begin{aligned} w\not \models A~\mathrm{{if }} A~\mathrm{{contains\, at\, least\, one\, constant~ in~}} D-D(w). \end{aligned}$$

(9.6)

$V$ is a valuation function assigning a constant $V(e,w)\in D$ to any $\epsilon$-term $e$ (possibly containing constants from $D$) and $w\in W$.

The relation $\models$ is extended to composite formulas in the familiar way. The components of an $\epsilon$-model have to satisfy the following conditions.

$$\begin{aligned} V(\epsilon xB(x,\epsilon y C),w)=V(\epsilon xB(x,V(\epsilon yC,w)),w), \end{aligned}$$

(9.7)

$$\begin{aligned} w\models A(\epsilon y C)\leftrightarrow w\models A(x,V(\epsilon yC)), \end{aligned}$$

(9.8)

where substitution of $\epsilon yC$ is safe, that is no free variable of $\epsilon yC$ becomes bound. Also, if $e\downarrow w$ for a term $e:=\ \epsilon xA(x)$, then

$$V(e,w)\in D(w) \text { and } V(e,w')=V(e,w) \text { for every } w'\ge w. $$

Note. The requirement (9.6) is sound as we prove at the rest of this section, but it leads to incompleteness. For example the formula

$$ P(\epsilon xP(x))\rightarrow \exists xP(x) $$

is valid: if $\epsilon xP(x)$ is undefined in a world $w$ then the premise is false in $w$, otherwise the conclusion is true. However this formula is not derivable, since its instance

$$\begin{aligned} (C\rightarrow P(e))\rightarrow \exists x(C\rightarrow P(x)) \end{aligned}$$

(9.9)

where $C$ is a propositional variable and $e=\epsilon x(C\rightarrow P(x))$, implies

$$\begin{aligned} (C\rightarrow \exists xP(x))\rightarrow \exists x(C\rightarrow P(x)). \end{aligned}$$

(9.10)

Indeed, the following figure (where $e_0=\epsilon xP(x)$) is a derivation, and one application of (9.9) yields (9.10).

(9.11)

We continue the proof of soundness. The proofs of the next lemmata are routine.

Lemma 9.1

Let $t$ be a closed term, $A$ a closed formula with constants from $D$. Then

$$ w\le w' \rightarrow \ ({{\!\!}\downarrow } w\rightarrow {{\!\!}\downarrow } w' \& \ (w\models A \rightarrow w'\models A)) $$

Proof

Simultaneous induction on $t,A$.

Lemma 9.2

If $\Gamma$ is a set of formulas, $G$ a formula then $\Gamma \vdash G$ in $\mathrm {IPC}\epsilon$ implies $\Gamma \models G$.

Proof

Induction on derivations. Checking the rule $\exists \Rightarrow$ uses the fact that $\exists xA(x)$ implies $\epsilon xA(x)\downarrow$. It may be interesting to check whether any other properties of the formula ${{\!\!}\downarrow }$ are used. $\square$

Theorem 9.2

If $A,B$ are formulas without $\epsilon$-symbol then $A\vdash B$ in $\mathrm {IPC}\epsilon$ implies $A\vdash B$ in intuitionistic predicate logic IPC.

Proof

We need to prove that for every Kripke model

$$ \mathcal {M}_0=(W,<,D,\models _0) $$

for intutionistic predicate logic refuting $A\rightarrow B$ there is an $\mathrm {IPC}\epsilon$-model refuting $A\rightarrow B$. Before applying the construction from Dragalin (1974), let us recall a refinement of a completeness theorem for intuitionistic predicate logic IPC.

Lemma 9.3

The following additional requirements to the definition of a Kripke frame $(W,<,D)$ for IPC are still complete:

• 1. $W$ is a countable tree with a root $\mathbf 0$ such that each $w\in W$ except $\mathbf 0$ has unique immediate $<$-predecessor and the number of predecessors of $w$ is finite.

• 2. domains D(w) are strictly increasing: if $w<w'$ then $D(w)$ is a proper subset of $D(w')$.

Proof

The requirement 1 is satisfied by the canonical proof search tree for a given sequent, see for example Mints (2000). To satisfy the second requirement, note that an infinite branch of the canonical proof search tree does not have “leaf worlds”: for every $w\in W$ there exists a $w'>w$. Now take a fixed element $e\in D(w_0)$ and duplicate it by a fresh element, say $e_w$ in every world $w$. More precisely for the new domain function $D'$ define

$$e_w\in D'(w)-D'(w^-), $$

where $w^-$ is the immediate predecessor of $w$. Let’s extend the relation $\models$ by identifying $e_w$ and $e$, more precisely define for atomic formulas $P(c_1,\ldots ,c_n)$ with constants $c_i\in D'(w)$

$$ w\models P(c_1,\ldots ,c_n)\ := w\models P(c_1^-,\ldots ,c_n^-) $$

where $c_i^-=e$, if $c_i=e_w$ and $c_i^-=c_i$ otherwise. It is easily proved by induction on formulas that this property extends to all formulas:

$$ w\models A(c_1,\ldots ,c_n)\text { implies } w\models A(c_1^-,\ldots ,c_n^-) $$

so that the new model verifies (and refutes) the same formulas.      $\dashv$

Proof of the Theorem 9.2. We extend the model for IPC satisfying the previous Lemma by the definition of values for $\epsilon$-terms without changing domains $D(w)$, which is done by induction on construction of the term. Assume that the elements of $D$ are well-ordered by a relation $\prec$ in some arbitrary way. In view of the condition (9.7) it enough to define $V(\epsilon xA,w)$ when $\epsilon xA$ does not have proper non-closed $\epsilon$-subterms. In that case,

if $\epsilon xA(x)\downarrow w$, take the $<$-minimal element $v\le w$ such that $\epsilon xA\downarrow v$, then define

$$ V(\epsilon xA(x),w):=\ \mathrm{{the}}\prec \mathrm{{-first}}\, d\in D(v) (v\models (\exists xA(x)\rightarrow A(d))) $$

If not $\epsilon xA(x)\downarrow w$, define $V(\epsilon xA(x),w)$ as the $\prec$-first $d\in D-D(w)$. $\square$

9.4 Completeness Proof for $\mathrm {IPC}\epsilon$

We prove that removing condition (9.6) but preserving familiar monotonicity requirement

$$\begin{aligned} w\le w'\rightarrow \ (w\models A\rightarrow w'\models A) \end{aligned}$$

(9.12)

leads to a complete semantics for $\mathrm {IPC}\epsilon$.

For simplicity consider term models where individual domain $D(w)$ for every world $w$ consists of terms, and the evaluation function for terms is identity: value of a term $t$ is $t$. In particular the value of $\epsilon xA$ is $\epsilon xA$.

Definition 9.3

An intuitionistic Kripke (term) $\epsilon$-model (or simply $\epsilon$-model)

$$ \mathcal {M}=(W,<,D,\models ,V) $$

has to satisfy the following conditions.

$(W,<)$ is a Kripke frame with a strict partial ordering $<$,

$D$ is a domain function assigning to every $w\in W$ a non-empty set $D(w)$ (of terms) monotone with respect to $<$,

$w\models A$ is a relation between worlds $w$ and atomic formulas $A$ with constants from

$$ D:= \cup _{w\in W}D(w) $$

monotonic with respect to $\le$ .

$V$ is a valuation function assigning a constant $V(e,w)\in D$ to any $\epsilon$-term $e$ (possibly containing constants from $D$) and $w\in W$. (In a term model $V(e,w)=e$.)

The relation $\models$ is extended to composite formulas in the familiar way. The components of an $\epsilon$-model have to satisfy the following conditions.

$$\begin{aligned} V(\epsilon xB(x,\epsilon y C),w)=V(\epsilon xB(x,V(\epsilon yC,w)),w) \end{aligned}$$

(9.13)

$$\begin{aligned} w\models A(\epsilon y C)\leftrightarrow w\models A(x,V(\epsilon yC)) \end{aligned}$$

(9.14)

where substitution of $\epsilon yC$ is safe, that is no free variable of $\epsilon yC$ becomes bound. Also if $e\downarrow w$ for a term $e:=\ \epsilon xA(x)$, then

$$V(e,w)\in D(w) \text { and } V(e,w')=V(e,w) \text { for every } w'\ge w. $$

Let’s present a completeness proof along familiar lines.

Definition 9.4

An infinite sequent is a pair of sets $\Gamma ,\Delta$ of formulas such that there is an infinite number of variables not in $\Gamma \cup \Delta$. An infinite sequent $w$ is written as $\Gamma \Rightarrow \Delta$ and notation

$$ w_a:=\Gamma ,\ w_s:=\Delta $$

is used for its antecedent and succedent.

$L_w$ denotes the set of all terms and formulas with free variables and constants occurring in formulas of $w$.

$D(w)$ is the set of all terms $t\in L_w$ such that $({{\!\!}\downarrow })\in w_a$. In other worlds $D(w)$ consists of all free variables and constants in $w$ plus all $\epsilon$-terms $\epsilon xA(x)$ such that $\exists y(\exists xA(x)\rightarrow A(y))\in \ w_a$.

An infinite sequent $w$ is consistent, if it is underivable, that is if no finite sequent $\Gamma \Rightarrow \Delta$ with $\Gamma \subset w_a,\ \Delta \subset w_s$ is derivable in IPC$\epsilon$.

A consistent infinite sequent $w$ is maximal consistent if $w_a\cup w_s$ is the whole set of formulas in $L_w$.

Lemma 9.4

Every consistent infinite sequent $w_0$ can be extended to a maximal consistent sequent.

Proof

Enumerate all formulas containing only free variables and constants in $L_{w_0}$, then add them one by one to $w_a$ or $w_s$ preserving consistency. At the $n$-th stage of this process a sequent $w_n$, an extension of $w_0$ by a finite number of formulas is generated.

It cannot happen that at some stage $n$ of this process a formula $A$ fits none of $w^n_a,w^n_s$, i.e., both of

$$ w^n_a\Rightarrow w^n_s,A_n\qquad A_n,w^n_a\Rightarrow w^n_s $$

are inconsistent, since in that case $w^n_a\Rightarrow w^n_s$ is inconsistent by a cut rule. $\square$

Important example. If $w$ is $\forall xP(x)\Rightarrow P(\epsilon xQ(x))$ with $P\ne Q$, and the first “undecided” formula is $\exists y(\exists xQ(x)\rightarrow Q(y))$ then this formula is added to the succedent, since adding it to the antecedent results in an inconsistent sequent.

Lemma 9.5

Every maximal consistent infinite sequent $w$ is closed under invertible rules of multiple-succedent version of  $\mathrm {IPC}\epsilon$, that is under all rules except $\Rightarrow \forall , \Rightarrow \rightarrow$. More precisely

$$ (A \& B)\in w_a\text { implies } A\in w_a\text { and } B\in w_a, $$

$$(A\rightarrow B)\in w_a \text { implies } A\in w_s\text { or } B\in w_a, $$

$$(A\vee B)\in w_a \text { implies } A\in w_a\text { or } B\in w_a, $$

$$(\forall xA(x))\in w_a \text { implies } (\forall t\in D(w))(A(t)\in w_a) $$

$$ (A\vee B)\in w_s\text { implies } A\in w_a\text { and } B\in w_a, $$

$$ (A \& B)\in w_s \text { implies } A\in w_a\text { or } B\in w_a, $$

Proof

Suppose $(A \& B)\in w_a$. If $A\not \in w_a$ then by maximality $A\in w_s$. Therefore $w$ is inconsistent.

Suppose $\forall xA\in \ w_a$. If $A(t)\not \in w_a$ for some $t\in D(w)$ then by maximality $A(t)\in w_s$. Therefore $\forall xA\Rightarrow A(t)$ is derived by one application of the $\forall \Rightarrow$-rule, and hence $w$ is inconsistent. Note that additional premise ${{\!\!}\downarrow }$ of this rule is available by $t\in D(w)$.

Other cases are similar. $\square$

Definition 9.5

For infinite sequents $w,w'$ define

$$ w<w'\text { iff } w_a\subseteq w'_a \text { and } D(w)\subseteq D(w') $$

Lemma 9.6

The set of maximal consistent sequents is closed under non-invertible rules $\Rightarrow \rightarrow ,\Rightarrow \forall$. More precisely,

For every maximal consistent sequent $w$, if $(A\rightarrow B)\in w_s$ then there exists a maximal consistent sequent $w'>w$ with $A\in w'_a,\ B\in w'_s$.

For every maximal consistent sequent $w$, if $\forall xA(x)\in w_s$ then there exists a maximal consistent sequent $w'>w$ with $A(a)\in w'_s$ for some variable $a$, $a\in D(w')$.

Proof

If $(A\rightarrow B)\in w_s$ then the sequent $A,w_a\Rightarrow B$ is consistent, since otherwise one application of the rule $\Rightarrow \rightarrow$ leads to inconsistency of $w$. Now extend $A,w_a\Rightarrow B$ to a complete consistent sequent.

If $\forall xA(x) \in w_s$ then the sequent $w_a\Rightarrow A(a)$ for a fresh variable $a$ is consistent, since otherwise one application of the rule $\Rightarrow \forall$ leads to inconsistency of $w$. Now extend $A,w_a\Rightarrow B$ to a complete consistent sequent. $\square$

Definition 9.6

(Canonical model) Consider the following model

$$ M=(W,<,V,\models ). $$

$W$ is the set of all maximal complete sequents, $<,V$ are as above,

$w\models A$ iff $A\in w_a$ for atomic formulas $A$.

This definition implies that $w\not \models A$ for atomic $A\in w_s$, since otherwise $w$ is inconsistent.

Lemma 9.7

The relation $\models$ for atomic formulas and the function $D$ is monotonic.

Proof

Consider only $D(w)$. Let $w<w'$. All variables and constants in $D(w)$ are in $D(w')$ by the definition of $<$. Assume $\epsilon xA(x)\in D(w)$, that is $\epsilon xA(x)\downarrow \ \in w_a$. Then $\epsilon x A(x)\downarrow \in w'_a$ by $w<w'$, and hence $\epsilon xA(x)\in D(w')$. $\square$

Lemma 9.8

For every formula $A\in L_w$

• 1. $A\in w_a$ implies $w\models A$,

• 2. $A\in w_s$ implies $w\not \models A$,

Proof

Induction on formulas using Lemmata 9.5 and 9.6. For example, if $A \& B\in w_a$ then $A,B\in w_a$, therefore $w\models A, w\models B$ by induction hypothesis, and hence $w\models A \& B$.

If $\forall xA\in w_s$ then there exists $w'>w$ such that $A(a)\in w'_s$ for some variable $a\in D(w')$. Therefore $w'\not \models A(a)$ and hence $w\not \models \forall xA(x)$. $\square$

Theorem 9.3

The system IPC$\epsilon$ is sound and complete.

Proof

Soundness is checked as before. For completeness take an arbitrary underivable formula $A$, then extend sequent $\Rightarrow A$ to a maximal consistent set $w$. By the previous Lemma $w\not \models A$. $\square$

9.4.1 About a Cut-Free Formulation

It is plausible that the completeness proof for the rules with cut given above can be modified to provide completeness of a cut-free formulation. As our example (9.11) shows, complete cut-elimination is impossible. One may need to admit cuts for formulas of the form $\epsilon xA(x)\downarrow$ where $\epsilon xA(x)$ occurs in the conclusion, and subformulas of such formulas. The following proof where $e:=\epsilon xP(x)$ is another example.

9.5 Comparison with Previous Work

9.5.1 System $IPC\Omega \epsilon$

Let $\exists \epsilon xA(x):= \exists xA(x)$.

A. Dragalin’s system $IPC\Omega \epsilon$ from Dragalin (1974) for a given language $\Omega \epsilon$ is obtained by weakening familiar axioms for quantifiers

and adding the axiom

A. Dragalin (Dragalin 1974) tried to avoid as much as possible dealing with a value of an $\epsilon$-term in a world $w$ where the term is not defined. Values (in a given world $w$) are assigned only to $\epsilon$-terms defined in $w$, and many intermediate results are proved only for the case when all relevant $\epsilon$-terms are defined. Nevertheless soundness is established for all formulas, without any restrictions. As pointed out earlier, this system is not complete.

In Sect. 9.3 we changed the definition of a model from Dragalin (1974) to a more uniform version: $\epsilon$-term $e$ which is not defined at the world $w$ is assigned a value at $w$, but this value does not belong to the individual domain $D(w)$. To make this possible, the Kripke frame underlying the model and the domain function should satisfy additional conditions that still guarantee completeness.

Let us consider other systems in the literature.

9.5.2 Systems with $\exists y(\exists xA(x)\rightarrow A(y))$ as Existence Condition

In systems due to Maehara (1970) and Shirai (1971), instead of using $\exists xA(x)$ as a discriminating criterion, a weaker formula $\exists y(\exists xA(x)\rightarrow A(y))$ is employed. This still allows to anticipate a correct future value of the term $\epsilon xA(x)$ in a world $w$ even if $\exists xA(x)$ fails in $w$.

Sh. Maehara treats a weaker language than ours: $\epsilon xA(x)$ is a syntactically correct term only if it is closed. He proves (using partial cut-elimination and other syntactic transformations) conservativity over IPC of the rules

(9.15)

where

(9.16)

Here $\top$ is the constant true, $a$ is an arbitrary variable.

Note that the first of these rules contains a hidden cut. This conservativity result is used to establish a kind of completeness theorem for IPC over a modification of Kripke semantics, although this modification is not stated explicitly. More precisely, Sh. Maehara proves Kripke-style soundness and completeness results for the relation $A\in \alpha$ between formulas $A$ and complete consistent (in his sense) subsets $\alpha$ of the set of formulas. Only his condition for $\forall$ is not standard:

To establish this condition he uses admissibility of the following rule in his system:

This rules approximates equivalence

$$ \forall xA(x)\leftrightarrow A(\epsilon x\lnot A(x)) $$

which is valid only classically.

Shirai (1971) removes the restriction to closed $\epsilon$-terms. He considers a language with the existence predicate denote by $D$. Instead of the rules used by Maehara he considers the following axioms:

$$\begin{aligned} D(t),\exists y(\exists xA(x,t)\rightarrow A(y,t)\Rightarrow D(\epsilon xA(x)) \end{aligned}$$

(9.17)

$$ D(t),\exists xA(x,t)\Rightarrow A(\epsilon xA(x,t),t) $$

plus standard modifications of quantifier rules for the system with existence predicate $D$.

He proves conservativity of his system over IPC by a combination of a partial cut-elimination and Maehara’s argument.

Leivant (1973) and Smirnov (1979) define logical systems with $\epsilon$-symbol conservative over IPC by requiring that assumptions discharged in natural deduction rules contain no $\epsilon$-symbol. These systems are probably much weaker than $\mathrm {IPC}\epsilon$. The system introduced by the author (Mints 1974) is certainly weaker than $\mathrm {IPC}\epsilon$: a sequent containing subterm $\epsilon xA(x,y)$ with a bound variable $y$ is syntactically correct only provided $\forall y\exists xA(x,y)$ is a member of the antecedent.

9.6 Further Work

Complete the proof of cut-elimination for IPC$\epsilon$ and of the normal form theorem for NJ$\epsilon$.

Give a syntactic proof of cut-elimination for IPC$\epsilon$ and of normalization for NJ$\epsilon$.

Provide a semantics for the systems by Maehara (1970) and Shirai (1971) and find out whether these systems admit cut-elimination. It seems that the system by Shirai provides the most general formulation of the idea that $\epsilon$-terms are partially defined in some arbitrary way. The restriction $D(t)$ allowing to quantify over value of $t$ can be an arbitrary predicate with the only condition (9.17).