Hyper Natural Deduction for Godel Logic-A natural deduction system for parallel reasoning

摘要

We introduce a system of Hyper Natural Deduction for Godel Logic as an extension of Gentzen's system of Natural Deduction. A deduction in this system consists of a finite set of derivations which uses the typical rules of Natural Deduction, plus additional rules providing means for communication between derivations. We show that our system is sound and complete for infinite-valued propositional Godel Logic, by giving translations to and from Avron's Hypersequent Calculus. We provide conversions for normalization extending usual conversions for Natural Deduction and prove the existence of normal forms for Hyper Natural Deduction for Godel Logic. We show that normal deductions satisfy the subformula property.