We consider a logic which is semantically dual (in some precise sense of the term) to intuitionistic. This logic can be labeled as “falsification logic”: it embodies the Popperian methodology of scientific discovery. Whereas intuitionistic logic deals with constructive truth and non-constructive falsity, and Nelson's logic takes both truth and falsity as constructive notions, in the falsification logic truth is essentially non-constructive as opposed to falsity that is conceived constructively. We also briefly clarify the relationships of our falsification logic to (...) some other logical systems. (shrink)

We construct an extension P of the standard language of classical propositional logic by adjoining to the alphabet of a new category of logical-pragmatic signs. The well formed formulas of are calledradical formulas (rfs) of P;rfs preceded by theassertion sign constituteelementary assertive formulas of P, which can be connected together by means of thepragmatic connectives N, K, A, C, E, so as to obtain the set of all theassertive formulas (afs). Everyrf of P is endowed with atruth value defined classically, (...) and everyaf is endowed with ajustification value, defined in terms of the intuitive notion of proof and depending on the truth values of its radical subformulas. In this framework, we define the notion ofpragmatic validity in P and yield a list of criteria of pragmatic validity which hold under the assumption that only classical metalinguistic procedures of proof be accepted. We translate the classical propositional calculus (CPC) and the intuitionistic propositional calculus (IPC) into the assertive part of P and show that this translation allows us to interpret Intuitionistic Logic as an axiomatic theory of the constructive proof concept rather than an alternative to Classical Logic. Finally, we show that our framework provides a suitable background for discussing classical problems in the philosophy of logic. (shrink)

The sequent system LDJ is formulated using the same connectives as Gentzen's intuitionistic sequent system LJ, but is dual in the following sense: (i) whereas LJ is singular in the consequent, LDJ is singular in the antecedent; (ii) whereas LJ has the same sentential counter-theorems as classical LK but not the same theorems, LDJ has the same sentential theorems as LK but not the same counter-theorems. In particular, LDJ does not reject all contradictions and is accordingly paraconsistent. To obtain a (...) more precise mapping, both LJ and LDJ are extended by adding a "pseudo-difference" operator which is the dual of intuitionistic implication. Cut-elimination and decidability are proved for the extended systems and , and a simply consistent but -inconsistent Set Theory with Unrestricted Comprehension Schema based on LDJ is sketched. (shrink)

Reviewed Works:Gaisi Takeuti, Proof Theory.Georg Kreisel, Proof Theory: Some Personal Recollections.Wolfram Pohlers, Contributions of the Schutte School in Munich to Proof Theory.Stephen G. Simpson, Subsystems of $\mathbf{Z}_2$ and Reverse Mathematics.Solomon Feferman, Proof Theory: A Personal Report.

We present a natural deduction system for dual-intuitionistic logic. Its distinctive feature is that it is a single-premise multiple-conclusions system. Its relationships with the natural deduction systems for intuitionistic and classical logic are discussed.