Desktop version

Home arrow Philosophy arrow Advances in Proof-Theoretic Semantics

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]

a1 ...

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 {a1,..., 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 a1,..., 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 R1,..., Rn are rules (n ≥ 1), whose maximal level is £, and a is an atom, then (R1,..., 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]

a1 ...

b [Γn ]

an

(in linear notation: 1 ✄ a1),..., (Γ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 {a1,..., 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 R1,..., 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 ✄ a1), . . . , (Γn ✄ an ) ✄ b. Suppose that for

each i (1 ≤ in) a derivation

ΣiΓi

Di

ai

of ai from ΣiΓi is given. Then

Σ1

D1

a1 ...

b Σn

Dn

an (Γ1 ✄ a1),..., (Γn ✄ an ) ✄ b

is a derivation of b from Σ1 ∪ ...Σn ∪ {1 ✄ a1),..., (Γ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.

 
Found a mistake? Please highlight the word and press Shift + Enter  
< Prev   CONTENTS   Next >

Related topics