This article aims to study, proof-theoretically and semantically, Gentzen-style sequent calculi (including possibly Cut-free and Identity-free systems), containing combinations of canonical and cocanonical rules, i.e. Gentzen systems for sequents, with well-behaved forms of left and right introduction and elimination rules for logical expressions. Our main goals are to provide soundness and completeness results for the derivability relations of the target systems in terms of 2-, 3-, or 4-valued non-deterministic semantics, and to give sufficient conditions under which these calculi are prone to produce well-behaved normal derivations of a structurally-atomic analytic-synthetic kind.
The scheme that Gentzen designed to specify the definitions of logical connectives has a wider reach than is usually recognized, extending naturally to terms that Gentzen did not treat explicitly, including predicate symbols. After explaining (§2) how the introduction and elimination rules of natural deduction calculi provide a relational definition of a term through a universal construction, we will describe how to provide similar constructions of, first, the binary predicate symbol for identity (§3) and, second, the monadic predicate symbol for being a natural number (§4). The main result of §3 is the interderivability of the introduction rule for identity (=I) with the law of reflexivity. This result greatly simplifies the analysis of the former rule. Further, it explains why attempts either to reject =I as unsound or to justify it only relative to specific background assumptions have systematically missed its decontextualized role in inference. In §4 we review the realization, observed by Martin-Löf and Parsons, of the principle of mathematical induction as an elimination rule (\(\mathbb{N}\)E) for the natural number predicate. Noting the universal construction underlying this realization clarifies the relationship between the induction principle and the number concept, at least when the latter is relationally specified, by resituating induction as an integral part of the very definition of the natural numbers. The common motif tying these and other results together is the fact that a term’s introduction and elimination rules are a presentation of a single concept, the term’s universal construction.
In this paper, we show that Frege's approach to classes and the relation of being an element was influential in Leśniewski's formalisation of these notions in a collective version. This was further influenced by Leśniewski's attempt to solve Russell's paradox. This happened even though Frege and Russell wrote about distributive classes, while Leśniewski recognised collective classes. We will present this in terms of Frege's approach to classes and the relation of being an element of. It allows us to discuss Russell's paradox in its form as Leśniewski saw it.
In this paper, the concepts of commutativity relation, commutant of a subset, center and solvable pseudo BL-algebras are defined and their properties are investigated. The notion of n-Engel pseudo BL-algebras as a natural generalization of BL-algebras is introduced, and we discuss Engel pseudo BL-algebra, which is defined by left and right normed commutators.
We show that partially ordered sets, lattices, semilattices, Boolean algebras, Heyting algebras with a further coarser or finer partial order, or a linearization, or an auxiliary relation have the strong amalgamation property, Fraïssé limits and, in many cases, an \(\omega\)-categorical model completion with quantifier elimination. The same applies to causal spaces, introduced by Kronheimer and Penrose in connection with foundational problems in general relativity. Our main tool is the superamalgamation property, thus we provide arguments suggesting the usefulness of the superamalgamation property also in pure model theory, not only in algebraic logic.
