# Proof-Theoretic Validity for Generalized Atomic Systems

We now consider atomic systems which are not restricted to first-level atomic rules but which can contain atomic rules that can also discharge assumptions of a certain kind. One can show that intuitionistic logic is not complete for a notion of prooftheoretic validity based on such generalized atomic systems (see [16]).

To motivate such a generalization one might argue that since the device of assumption discharge is available at the level of logical rules (e.g., in the rules of implication introduction and disjunction elimination of natural deduction), it should be available at the level of atomic rules, too. However, from the point of view of attempting a justification of a certain logic by giving a semantics based on atomic systems, such a generalization might be conceived as being counterproductive, as it introduces a feature of implication already at the level of atomic rules.

## Generalized Atomic Systems

We generalize the notion of first-level atomic system to higher-level atomic systems by allowing for atomic rules that can discharge atomic assumptions (cf. [16]).

**Definition 9** A *second-level atomic system S* is a (possibly empty) set of atomic rules of the form

[*Γ*1]

*a*1 *...*

*b* [*Γn* ]

*an*

where the *ai* and *b* are atoms, and the *Γi* are finite sets of atoms. The sets *Γi* may be empty, in which case the rule is a *first-level rule*. The set of premises {*a*1*,..., an* } can be empty as well; in this case the rule is an axiom.

Such a rule can be applied as follows: If the premises *a*1*,..., an* have been derived in *S* from certain assumptions, then one may conclude *b*, where, for each *i* , in the branch of the subderivation leading to *ai* assumptions belonging to *Γi* may be discharged.

Second-level atomic systems are now further generalized to the higher-level case by allowing for atomic rules which can discharge not only atoms but atomic rules as assumptions (see Schroeder-Heister [29, 32] and Olkhovikov and SchroederHeister [15]; cf. [16]). We use the following linear notation for atomic higher-level rules:

**Definition 10** (i) Every atom *a* is a rule of level 0.

(ii) If *R*1*,..., Rn* are rules (*n* ≥ 1), whose maximal level is *£*, and *a* is an atom, then *(R*1*,..., Rn ✄ a)* is a rule of level *£* + 1.

**Definition 11** A *higher-level atomic system S* is a (possibly empty) set of atomic rules of the form

[*Γ*1]

*a*1 *...*

*b* [*Γn* ]

*an*

(in linear notation: *(Γ*1 *✄ a*1*),..., (Γn ✄ an ) ✄ b*), where the *ai* and *b* are atoms,

and the *Γi* are now finite sets {*Ri ,..., Ri* } of rules, which may be empty. The set of

1 *k*

premises {*a*1*,..., an* } of such a rule can also be empty, in which case the rule is an

axiom.

In the higher-level case atomic *rules* can be used as (dischargeable) assumptions, whereas in the second-level case only atoms could be used in that way. This difference requires a definition of the notion of *derivation* of an atom *a* from rules *R*1*,..., Rn* :

**Definition 12** For a level-0 rule *a*,

*a a*

is a *derivation* of *a* from {*a*}.

Now consider a level-*(£* + 1*)* rule *(Γ*1 *✄ a*1*), . . . , (Γn ✄ an ) ✄ b*. Suppose that for

each *i (*1 ≤ *i* ≤ *n)* a derivation

*Σi* ∪ *Γi*

*Di*

*ai*

of *ai* from *Σi* ∪ *Γi* is given. Then

*Σ*1

*D*1

*a*1 *...*

*b Σn*

*Dn*

*an (Γ*1 *✄ a*1*),..., (Γn ✄ an ) ✄ b*

is a *derivation* of *b* from *Σ*1 ∪ *...* ∪ *Σn* ∪ {*(Γ*1 *✄ a*1*),..., (Γn ✄ an ) ✄ b*}.

An atom *b* is *derivable* from *Σ* in a higher-level atomic system *S*, symbolically

*Σ* f-*S b*, if there is a derivation of *b* from *Σ* ∪ *S*.

As an example, consider the atomic system *S* = {*((b✄e)✄ f ), (((a ✄b)✄c)✄e)*}

and the set of assumptions *Σ* = {*((a ✄b)✄d), ((b, d)✄c)*}. The following derivation

shows that *Σ* f-*S f* :

*b* [*b*]3

*c*

*a*

[*a*]1

*b* [*a ✄ b*]2

1 *d (a ✄ b) ✄ d*

*b, d ✄ c*

2 *e* (*((a ✄ b) ✄ c) ✄ e*)

3 *f* (*(b ✄ e) ✄ f* )

Angle brackets () are used to indicate the rules of *S*, and square brackets [ ] with numerals indicate the discharge of assumptions.