Higher inductive types are a class of type-forming rules, introduced to provide basic (and not-so-basic) homotopy-theoretic constructions in a type-theoretic style. They have proven very fruitful for the “synthetic” development of homotopy theory within type theory, as well as in formalising ordinary set-level mathematics in type theory. In this paper, we construct models of a wide range of higher inductive types in a fairly wide range of settings.

We introduce the notion of cell monad with parameters: a semantically-defined scheme for specifying homotopically well-behaved notions of structure. We then show that any suitable model category has weakly stable typal initial algebras for any cell monad with parameters. When combined with the local universes construction to obtain strict stability, this specialises to give models of specific higher inductive types, including spheres, the torus, pushout types, truncations, the James construction and general localisations.

Our results apply in any sufficiently nice Quillen model category, including any right proper, simplicially locally cartesian closed, simplicial Cisinski model category (such as simplicial sets) and any locally presentable locally cartesian closed category (such as sets) with its trivial model structure. In particular, any locally presentable locally cartesian closed (∞, 1)-category is presented by some model category to which our results apply.

A multiset consists of elements, but the notion of a multiset is distinguished from that of a set by carrying information of how many times each element occurs in a given multiset. In this work we will investigate the notion of iterative multisets, where multisets are iteratively built up from other multisets, in the context Martin–Löf Type Theory, in the presence of Voevodsky’s Univalence Axiom.

In his 1978 paper, “the type theoretic interpretation of constructive set theory” Aczel introduced a model of constructive set theory in type theory, using a W-type quantifying over a universe, and an inductively defined equivalence relation on it. Our investigation takes this W-type and instead considers the identity type on it, which can be computed from the univalence axiom. Our thesis is that this gives a model of multisets. In order to demonstrate this, we adapt axioms of constructive set theory to multisets, and show that they hold for our model.

A new generalized class of fuzzy implications, called ($h,f,g$)-implications, is introduced and discussed in this paper. The results show that the new fuzzy implications possess some good properties, such as the left neutrality property and the exchange principle.

We construct an increasing ${\it\omega}$ -sequence $\langle \boldsymbol{a}_{n}\rangle$ of Turing degrees which forms an initial segment of the Turing degrees, and such that each $\boldsymbol{a}_{n+1}$ is diagonally nonrecursive relative to $\boldsymbol{a}_{n}$ . It follows that the DNR principle of reverse mathematics does not imply the existence of Turing incomparable degrees.

The form of information presented can influence its utility for the conveying of knowledge by affecting an interpreter’s ability to reason with the information. There are distinct types of representational systems (for example, symbolic versus diagrammatic logics), various sub-systems (for example, propositional versus predicate logics), and even within a single representational system there may be different means of expressing the same piece of information content. Thus, to display information, choices must be made between its different representations, depending upon many factors such as: the context, the reasoning tasks to be considered, user preferences or desires (for example, for short symbolic sentences or minimal clutter within diagrammatic systems). The identification of all equivalent representations with the same information content is a sensible precursor to attempts to minimise a metric over this class. We posit that defining notions of semantic redundancy and identifying the syntactic properties that encapsulate redundancy can help in achieving the goal of completely identifying equivalences within a single notational system or across multiple systems, but that care must be taken when extending systems, since refinements of redundancy conditions may be necessary even for conservative system extensions. We demonstrate this theory within two diagrammatic systems, which are Euler-diagram-based notations. Such notations can be used to represent logical information and have applications including visualisation of database queries, social network visualisation, statistical data visualisation, and as the basis of more expressive diagrammatic logics such as constraint languages used in software specification and reasoning. The development of the new associated machinery and concepts required is important in its own right since it increases the growing body of knowledge on diagrammatic logics. In particular, we consider Euler diagrams with shading, and then we conservatively extend the system to include projections, which allow for a much greater degree of flexibility of representation. We give syntactic properties that encapsulate semantic equivalence in both systems, whilst observing that the same semantic concept of redundancy is significantly more difficult to realise as syntactic properties in the extended system with projections.

It is shown that a simple deduction engine can be developed for a propositional logic that follows the normal rules of classical logic in symbolic form, but the description of what is known about a proposition uses two numeric state variables that conveniently describe unknown and inconsistent, as well as true and false. Partly true and partly false can be included in deductions. The multi-valued logic is easily understood as the state variables relate directly to true and false. The deduction engine provides a convenient standard method for handling multiple or complicated logical relations. It is particularly convenient when the deduction can start with different propositions being given initial values of true or false. It extends Horn clause based deduction for propositional logic to arbitrary clauses. The logic system used has potential applications in many areas. A comparison with propositional logic makes the paper self-contained.

We introduce perfect effect algebras and we show that every perfect algebra is an interval in the lexicographical product of the group of all integers with an Abelian directed interpolation po-group. To show this we introduce prime ideals of effect algebras with the Riesz decomposition property (RDP). We show that the category of perfect effect algebras is categorically equivalent to the category of Abelian directed interpolation po-groups. Moreover, we prove that any perfect effect algebra is a subdirect product of antilattice effect algebras with the RDP.

Free algebras with an arbitrary number of free generators in varieties of BL-algebras generated by one BL-chain that is an ordinal sum of a finite MV-chain Ln, and a generalized BL-chain B are described in terms of weak Boolean products of BL-algebras that are ordinal sums of subalgebras of Ln, and free algebras in the variety of basic hoops generated by B. The Boolean products are taken over the Stone spaces of the Boolean subalgebras of idempotents of free algebras in the variety of MV-algebras generated by Ln.

2000 Mathematics subject classification: primary 03G25, 03B50, 03B52, 03D35, 03G25, 08B20.

We show that monotone σ -complete effect algebras under some conditions are σ - homomorphic images of effect-tribes (as monotone σ -complete effect algebras), which are nonempty systems of fuzzy sets closed under complements, sums of fuzzy sets less than 1, and containing all pointwise limits of nondecreasing fuzzy sets. Because effect-tribes are generalizations of Boolean σ -algebras of subsets, we present a generlization of the Loomis-Sikorski theorem for such effect algebras. We show that we can choose an effect-tribe to be a system of affin fuzzy sets. In addition, we present a new version of the Loomis-Sikorski theorem for σ-complete MV-algebras.

Pseudo-effect algebras are partial algebras (E; +, 0, 1) with a partially defined addition + which is not necessary commutative and with two complements, left and right ones. We define central elements of a pseudo-effect algebra and the centre, which in the case of MV-algebras coincides with the set of Boolean elements and in the case of effect algebras with the Riesz decomposition property central elements are only characteristic elements. If E satisfies general comparability, then E is a pseudo MV-algebra. Finally, we apply central elements to obtain a variation of the Cantor-Bernstein theorem for pseudo-effect algebras.

We show that any pseudo MV-algebra is isomorphic with an interval Γ(G, u), where G is an ℓ-group not necessarily Abelian with a strong unit u. In addition, we prove that the category of unital ℓ-groups is categorically equivalent with the category of pseudo MV-algebras. Since pseudo MV-algebras are a non-commutative generalization of MV-algebras, our assertions generalize a famous result of Mundici for a representation of MV-algebras by Abelian unital ℓ-groups. Our methods are completely different from those of Mundici. In addition, we show that any Archimedean pseudo MV-algebra is an MV-algebra.

We show that every σ-complete MV-algebra is an MV-σ-homomorphic image of some σ-complete MV- algebra of fuzzy sets, called a tribe, which is a system of fuzzy sets of a crisp set Ω containing 1Ω and closed under fuzzy complementation and formation of min {∑nfn, 1}. Since a tribe is a direct generalization of a σ-algebra of crisp subsets, the representation theorem is an analogue of the Loomis-Sikorski theorem for MV-algebras. In addition, this result will be extended also for Dedekind σ-complete ℓ-groups with strong unit.

An alternative approach is proposed to the basic definitions of the lassical lambda calculus. A proof is sketched of the equivalence of the approach with the classical case. The new formulation simplifies some aspects of the syntactic theory of the lambda calculus. In particular it provides a justification for omitting in syntactic theory discussion of changes of bound variable.