A natural deduction system of indexical logic.
Rolf Schock · Notre Dame Journal of Formal Logic · 1980
In a previous study, 1 a system L of indexical logic sound and complete with respect to a certain semantic theory was developed.However, L is an axiomatic logic.As usual, or perhaps even more than usual because of the complexity of indexical reasoning, the logic is unintuitively cumbersome since it is of the axiomatic type.For wrestling with problems of situational dependence in an adequate way, a natural deduction system of indexical logic is therefore needed.So far, no such system seems to exist in the literature.The present study consists of a formulation of the rules of a natural deduction system N of indexical logic and of a proof that N and L are equivalent.1 The system N N is an improved and extended version of the system N of [1].S is the auxiliary word "Show".It is assumed that no variable or constant occurs in S. A show line is a sequence SF and a line is either a show line or a formula.Crossing out the "Show" in front of F gives us F; that is, &F = F. Given a finite sequence p of lines, the conjunction of p is the c such that c is F -> F with F the first sentential constant if no line of p is a formula, F if F is the only line of p which is a formula, and the result of conjoining in order those lines of p which are formulas otherwise, p consists of a show line just in case the only line of p is a show line.If q is also a finite sequence of lines, then the following terminology is assumed:1. q is obtainable from p by adding a show line just when q is p with a show line added at its end.2. q is obtainable from p by adding an assumption just when there are formulas F x and F 2 such that the last line of p is SF 1? q is p with F 2 added at its end, and one of the following holds (each clause is prefixed with its notation, name, and diagram): a Rule of assumption for the proof of conditionals and disjunctions