Local deductions theorems (Q1090668): Difference between revisions

Kripke's system K with MP and necessitation has the following indeterminate deduction theorem: X,A\(\vdash B\) iff for some n \(X\vdash \square^ nA\to B\). Similarly, Łukasiewicz's infinite valued logic has an indeterminate deduction theorem: X,A\(\vdash B\) iff for some n \(X\vdash A\to_ nB\). The author generalizes from these cases of indeterminate deduction theorems to develop the notion of local deduction theorem. He then investigates conditions for a logic to have a local deduction theorem. A major result is that a finitary logic L has a local deduction theorem iff the class of all matrices validating L has the L- filter extension property. The paper is clearly presented, but reading it is greatly faciliated by having familiarity with the algebraic treatment of logic so commonly used by Polish logicians.