Home Philosophy Advances in Proof-Theoretic Semantics

## Proof-Theoretic Validity for Generalized Atomic SystemsWe 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 SystemsWe 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]).
[
where the Such a rule can be applied as follows: If the premises 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:
(ii) If
[
(in linear notation: and the 1 premises { axiom. In the higher-level case atomic
is a Now consider a level- each
of
is a An atom
As an example, consider the atomic system and the set of assumptions shows that
1
2 3 Angle brackets () are used to indicate the rules of |

< Prev | CONTENTS | Next > |
---|

Related topics |

Academic library - free online college e textbooks - info{at}ebrary.net - © 2014 - 2019