This paper aims at formulating a condition neccssary and sufficient for the existing of a prime filter preserving enumerable infinite joins and meets in a distributive lattice.

Rauszer and Sabalski proved in [2] that distributivity with respect to infi- nite joins and meets is a sucient and necessary condition making the RasiowaSikorski Lemma valid in distributive lattices. The main part of their proof is a direct construction of a required filter under distributivity. In this note we show that a generalization of the result can be obtained from the Rasiowa-Sikorski Lemma for Boolean algebras by using Gornemann’s result in [1] instead of a direct con- ¨ struction. (...) Suppose A is a distributive lattice and Q; R 2 A f;g. We call A complete if 8M 2 Q9 M 2 A and 8N 2 R9 F N 2 A. M 2 Q is -dis if 9 M 2 A and 8a 2 A a t M = m2M. N 2 R is F -dis if 9 F N 2 A and 8a 2 A a u F N = F n2N. is called distributive if every M 2 Q is -dis and every N 2 R is F -dis. Suppose A is complete and C; D A. By rC we mean the filter in A generated by C, in particular, let r; = ; = ;. is called complete if and , where 8M 2 Q 9m 2 MrC \ D[fmg = ;) 8N 2 R 9n 2 NrC[fng \ D = ;). (shrink)

Bi-intuitionistic logic is the union of intuitionistic and dual intuitionistic logic, and was introduced by Rauszer as a Hilbert calculus with algebraic and Kripke semantics. But her subsequent ‘cut-free’ sequent calculus has recently been shown to fail cut-elimination. We present a new cut-free sequent calculus for bi-intuitionistic logic, and prove it sound and complete with respect to its Kripke semantics. Ensuring completeness is complicated by the interaction between intuitionistic implication and dual intuitionistic exclusion, similarly to future and past modalities (...) in tense logic. Our calculus handles this interaction using derivations and refutations as first class citizens. We employ extended sequents which pass information from premises to conclusions using variables instantiated at the leaves of refutations, and rules which compose certain refutations and derivations to form derivations. Automated deduction using terminating backward search is also possible, although this is not our main purpose. (shrink)

Negation often reinforces problematic habits of othering, but rethinking negation can make good on feminist hopes for logic as a transformative space for inclusion. As Plumwood argues in her 1993 paper, not all uses of negation in the context of social identity are inherently problematic, but the widespread implicit use of classical negation has limited our options with respect to representing difference, ultimately reinforcing dualisms that essentialize social differences in problematic ways. In response to these limitations, I take inspiration from (...) Dembroff’s recent work on the metaphysics of genderqueer identity to build models of social identity using the Heyting-Brouwer logic developed by Rauszer in her 1974 paper. Ultimately, I argue that these models demonstrate both how classical negation reinforces problematic habits of othering and how alternative forms of negation can transform our treatment of social identity altogether. (shrink)

We consider a “polarized” version of bi-intuitionistic logic [5, 2, 6, 4] as a logic of assertions and hypotheses and show that it supports a “rich proof theory” and an interesting categorical interpretation, unlike the standard approach of C. Rauszer’s Heyting-Brouwer logic [28, 29], whose categorical models are all partial orders by Crolard’s theorem [8]. We show that P.A. Melliès notion of chirality [21, 22] appears as the right mathematical representation of the mirror symmetry between the intuitionistic and co-intuitionistc (...) sides of polarized bi-intuitionism. Philosophically, we extend Dalla Pozza and Garola’s pragmatic interpretation of intuitionism as a logic of assertions [10] to bi-intuitionism as a logic of assertions and hypotheses. We focus on the logical role of illocutionary forces and justification conditions in order to provide “intended interpretations” of logical systems that classify inferential uses in natural language and remain acceptable from an intuitionistic point of view. Although Dalla Pozza and Garola originally provide a constructive interpretation of intuitionism in a classical setting, we claim that some conceptual refinements suffice to make their “pragmatic interpretation” a bona fide representation of intuitionism. We sketch a meaning-asuse interpretation of co-intuitionism that seems to fulfil the requirements of Dummett and Prawitz’s justificationist approach. We extend the Brouwer-Heyting-Kolmogorov interpretation to bi-intuitionism by regarding co-intuitionistic formulas as types of the evidence for them: if conclusive evidence is needed to justify assertions, only a scintilla of evidence suffices to justify hypotheses. (shrink)

This paper examines the relationships between the many-valued logics G~ and Gn~ of Esteva, Godo, Hajek, and Navara, i.e., Godel logic G enriched with Łukasiewicz negation, and neighbors of intuitionistic logic. The popular fragments of Rauszer's Heyting-Brouwer logic HB admit many-valued extensions similar to G which may likewise be enriched with Łukasiewicz negation; the fuzzy extensions of these logics, including HB, are equivalent to G ~, as are their n-valued extensions equivalent to Gn~ for any n ≥ 2. These (...) enriched systems extend Wansing's logic I4C4, showing that Łukasiewicz negation is a species of Nelson's negation of constructible falsity and yielding a Kripke-style semantics for G~ and Gn~ to complement the many-valued semantics. (shrink)

We give topological proofs of Görnemann’s adaptation to Heyting algebras of the Rasiowa-Sikorski Lemma for Boolean algebras; and of the Rauszer-Sabalski generalisation of it to distributive lattices. The arguments use the Priestley topology on the set of prime filters, and the Baire category theorem. This is preceded by a discussion of criteria for compactness of various spaces of subsets of a lattice, including spaces of filters, prime filters etc.

This paper is a proposal of continuation of the work of C. Rauszer. The logic of falsehood created by her may constitute the starting point for construction of logic formalising reductive reasonings. The extension of Heyting-Brouwer logic to its deductive-reductive form sheds new light upon those classical tautologies which are rejected in intuitionism. It turns out that among HBtautologies there can be found all the classical ones. Some of them are characteristic for deductive reasoning and they are accepted by (...) intuitionism. Others formulate the laws of reductive reasoning. Many of them, including the law of excluded middle has been rejected in Heyting’s intuitionism. Intuitionism only permits for those reductive tautologies, which at the same time bear deductive character. Thus, the complete HB intuitionism does not reject any of the classical tautologies. Every classical tautology appears in HB logic in its deductive or reductive part. Some are even present in both parts. At the end it is shown that the law of excluded middle α∨¬α is a law of the reductive part of the traditional, Heyting’s intuitionistic propositional calculus. (shrink)

In this article we show that bi-intuitionistic predicate logic lacks the Craig Interpolation Property. We proceed by adapting the counterexample given by Mints, Olkhovikov and Urquhart for intuitionistic predicate logic with constant domains [13]. More precisely, we show that there is a valid implication $\phi \rightarrow \psi $ with no interpolant. Importantly, this result does not contradict the unfortunately named ‘Craig interpolation’ theorem established by Rauszer in [24] since that article is about the property more correctly named ‘deductive interpolation’ (...) (see Galatos, Jipsen, Kowalski and Ono’s use of this term in [5]) for global consequence. Given that the deduction theorem fails for bi-intuitionistic logic with global consequence, the two formulations of the property are not equivalent. (shrink)

We explore a relation we call 'anticipation' between formulas, where A anticipates B (according to some logic) just in case B is a consequence (according to that logic, presumed to support some distinguished implicational connective →) of the formula A → B. We are especially interested in the case in which the logic is intuitionistic (propositional) logic and are much concerned with an extension of that logic with a new connective, written as "a", governed by rules which guarantee that for (...) any formula B, aB is the (logically) strongest formula anticipating B. The investigation of this new logic, which we call ILa, will confront us on several occasions with some of the finer points in the theory of rules and with issues in the philosophy of logic arising from the proposed explication of the existence of a connective (with prescribed logical behaviour) in terms of the conservative extension of a favoured logic by the addition of such a connective. Other points of interest include the provision of a Kripke semantics with respect to which ILa is demonstrably sound, deployed to establish certain unprovability results as well as to forge connections with C. Rauszer's logic of dual intuitionistic negation and dual intuitionistic implication, and the isolation of two relations (between formulas), head-implication and head-linkage, which, though trivial in the setting of classical logic, are of considerable significance in the intuitionistic context. (shrink)