A natural deduction system NI, for the full propositional intuitionistic logic, is proposed. The operational rules of NI are obtained by the translation from Gentzen’s calculus LJ and the normalization is proved, via translations from sequent calculus derivations to natural deduction derivations and back.
This paper presents a way of formalising definite descriptions with a binary quantifier ℩, where ℩x[F, G] is read as `The F is G'. Introduction and elimination rules for ℩ in a system of intuitionist negative free logic are formulated. Procedures for removing maximal formulas of the form ℩x[F, G] are given, and it is shown that deductions in the system can be brought into normal form.
Sentences containing definite descriptions, expressions of the form `The F', can be formalised using a binary quantier that forms a formula out of two predicates, where ℩x[F;G] is read as `The F is G'. This is an innovation over the usual formalisation of definite descriptions with a term forming operator. The present paper compares the two approaches. After a brief overview of the system INF℩ of...
We upgrade  to a complete proof of the conjecture NP = PSPACE that is known as one of the fundamental open problems in the mathematical theory of computational complexity; this proof is based on . Since minimal propositional logic is known to be PSPACE complete, while PSPACE to include NP, it suﬃces to show that every valid purely implicational formula ρ has a proof whose weight (= total number...
Financed by the National Centre for Research and Development under grant No. SP/I/1/77065/10 by the strategic scientific research and experimental development program:
SYNAT - “Interdisciplinary System for Interactive Scientific and Scientific-Technical Information”.