A common misconception among logicians is to think that intuitionism is necessarily tied-up with single conclusion calculi. Single conclusion calculi can be used to model intuitionism and they are convenient, but by no means are they necessary. This has been shown by such influential textbook authors as Kleene, Takeuti and Dummett, to cite only three. If single conclusions are not necessary, how do we guarantee that only intuitionistic derivations are allowed? Traditionally one insists on restrictions on particular rules: implication right, (...) negation right and universal quantification right are required to be single conclusion rules. In this note we show that instead of a cardinality restriction such as one-conclusion-only, we can use a notion of dependency between formulae to enforce the constructive character of derivations. The system we obtain, called FIL for full intuitionistic logic, satisfies basic properties such as soundness, completeness and cut elimination. We present two motivating applications of FIL and discuss some future work. (shrink)

In Logical Forms Chateaubriand offers a realist semantics for false elementary propositions and for true negative propositions that appeals to negative facts. Although he does not refer to Wittgenstein, he rules out “possibilist” solutions such as that of the Tractatus. In this paper I will critically discuss Chateaubriand’s solution and compare it with the semantics of the Tractatus.

A natural extension of Natural Deduction was defined by Schroder-Heister where not only formulas but also rules could be used as hypotheses and hence discharged. It was shown that this extension allows the definition of higher-level introduction and elimination schemes and that the set $\{ \vee, \wedge, \rightarrow, \bot \}$ of intuitionist sentential operators forms a {\it complete} set of operators modulo the higher level introduction and elimination schemes, i.e., that any operator whose introduction and elimination rules are instances of (...) the higher-level schemes can be defined in terms of $\{ \vee, \wedge, \rightarrow, \bot \}$.The aim of the present work is to extend the well-known connections between Proof Theory and Category Theory to higher-level Natural Deduction. To be precise, we will show how an adjointness between cartesian closed categories with finite coproducts can be associated, in a systematic way, with any operator $\phi$ defined by the higher-level schemes. The objects in the categories will be rules instead of formulas. (shrink)