Search

The extensionality of ⊤-convergence spaces is verified for a complete residuated lattice L with the top element ⊤. And also the E -connectedness of ⊤-convergence spaces for a class E of ⊤-convergence spaces is proposed by generalizing Preuss's connectedness of topological spaces. Then we establish a necessary and sufficient condition that for a class K of ⊤-convergence spaces, there exists a class E of ⊤-convergence spaces such that each space of K is E -connected, where we stress the point that the conclusion benefits from the extensionality of the category of ⊤-convergence spaces. We further present a deep relationship between E -connectedness and T 1 -separation for ⊤-convergence spaces, that is, the E -connectedness of each subset in a ⊤-convergence space implies that of its closure if and only if E precisely is a class of ⊤-convergence spaces being T 1 -separated, and as a natural result, the product theorem for E -connected ⊤-convergence spaces is obtained.

We investigate some non-normal variants of well-studied paraconsistent and paracomplete modal logics that are based on N. Belnap’s and M. Dunn’s four-valued logic. Our basic non-normal modal logics are characterized by a weak extensionality rule, which reflects the four-valued nature of underlying logics. Aside from introducing our basic framework of bi-neighbourhood semantics, we develop a correspondence theory in order to prove completeness results with respect to our neighbourhood semantics for non-normal variants of $$\mathsf {BK}$$ , $$\mathsf {BK^{FS}}$$ and $$\mathsf {MBL}$$ .

In this work we provide an alternative, and equivalent, formulation of the concept of λ-theory without introducing the notion of substitution and the sets of all, free and bound variables occurring in a term. We call α β-relations our alternative versions of λ-theories. We also clarify the actual role of α-renaming in the lambda calculus: it expresses a property of extensionality for a certain class of terms. To motivate the necessity of α-renaming, we construct an unusual denotational model of the lambda calculus that validates all structural and beta conditions but not α-renaming. The article also has a survey character.

On the occasion of the 50th anniversary of the publication of Zadeh's significant paper Similarity Relations and Fuzzy Orderings, an account of the development of similarity relations during this time will be given. Moreover, the main topics related to these fuzzy relations will be reviewed.

We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free$$\lambda $$λ-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus’s two predecessors, new challenges arise from the interplay between$$\lambda $$λ-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.

This paper studies local indistinguishability operators, i.e., symmetric and transitive fuzzy relations that do not need to be reflexive. This is an important generalization of global indistinguishability relations (fuzzy relations satisfying the reflexivity property in addition) because there are interesting families of fuzzy relations that are non-reflexive. One case are decomposable relations, that are generated by a fuzzy subset and contains the t-norms as an important subfamily. Also the relations associated naturally to fuzzy subgroups are local indistinguishability operators. In this paper these relations will be studied stressing the way they can be generated. A representation theorem will be proved and related to the concepts of extensionality and of fuzzy rough set. Decomposable local indistinguishability operators will also be studied and related with one-dimensional ones in the sense of the previous representation theorem. The presence of these relations in the study of fuzzy subgroups will also be analyzed.

The setoid model is a model of intensional type theory that validates certain extensionality principles, like function extensionality and propositional extensionality, the latter being a limited form of univalence that equates logically equivalent propositions. The appeal of this model construction is that it can be constructed in a small, intensional, type theoretic metatheory, therefore giving a method to boostrap extensionality. The setoid model has been recently adapted into a formal system, namely Setoid Type Theory (SeTT). SeTT is an extension of intensional Martin-Löf type theory with constructs that give full access to the extensionality principles that hold in the setoid model.Although already a rich theory as currently defined, SeTT currently lacks a way to internalize the notion of type beyond propositions, hence we want to extend SeTT with a universe of setoids. To this aim, we present the construction of a (non-univalent) universe of setoids within the setoid model, first as an inductive-recursive definition, which is then translated to an inductive-inductive definition and finally to an inductive family. These translations from more powerful definition schemas to simpler ones ensure that our construction can still be defined in a relatively small metatheory which includes a proof-irrelevant identity type with a strong transport rule.

In generic realizability for set theories, realizers treat unbounded quantifiers generically. To this form of realizability, we add another layer of extensionality by requiring that realizers ought to act extensionally on realizers, giving rise to a realizability universe $\mathrm{V_{ex}}(A)$ in which the axiom of choice in all finite types ${\sf AC}_{{\sf FT}}$ is realized, where $A$ stands for an arbitrary partial combinatory algebra. This construction furnishes 'inner models' of many set theories that additionally validate ${\sf AC}_{{\sf FT}}$, in particular it provides a self-validating semantics for $\sf CZF$ (Constructive Zermelo-Fraenkel set theory) and $\sf IZF$ (Intuitionistic Zermelo-Fraenkel set theory). One can also add large set axioms and many other principles., Comment: Revised version. To appear in JLC

We present a way of constructing a Quillen model structure on a full subcategory of an elementary topos, starting with an interval object with connections and a certain dominance. The advantage of this method is that it does not require the underlying topos to be cocomplete. The resulting model category structure gives rise to a model of homotopy type theory with identity types, $\Sigma$- and $\Pi$-types, and functional extensionality. We apply the method to the effective topos with the interval object $\nabla 2$. In the resulting model structure we identify uniform inhabited objects as contractible objects, and show that discrete objects are fibrant. Moreover, we show that the unit of the discrete reflection is a homotopy equivalence and the homotopy category of fibrant assemblies is equivalent to the category of modest sets. We compare our work with the path object category construction on the effective topos by Jaap van Oosten., Comment: v2: The section "A non-contractible uniform object." was removed due to an error in Lemma 6.5, Proposition 7.3 was changed to account for the fact that only the "only if" direction holds

Extensionality is explored form different points of view. Extensional fuzzy subsets from a fuzzy equivalence relation E are considered as observable subsets with respect to the granularity generated by E. Interestingly, they are characterized as the fuzzy subsets that can be obtained as combinations of the fuzzy equivalence classes of E. Extensional mappings are characterized topologically and the set of extensional mappings between two universes are algebraically determined. Specifying the results to fuzzy mappings from a universe X onto [0, 1] an interpretation of type-2 fuzzy subsets of X as fuzzification of its type-1 fuzzy subsets is provided.

A semantics of realizability based on hyperarithmetical predicates of membership is introduced for formulas of the language of set theory. It is proved that the constructive set theory without the extensionality axiom is sound with this semantics.

Purpose Graham Priest has recently argued that the distinctive trait of classical mathematics is that the conditional of its underlying logic—that is, classical logic—is extensional. In this article, I aim to present an alternate explanation of the specificity of classical mathematics (and actually for L-mathematics, for a significative amount of instances of 'L').

The word problem for a finite set of ground identities is known to be decidable in polynomial time, and this is also the case if some of the function symbols are assumed to be commutative. We show that decidability in P is preserved if we also assume that certain function symbols f are extensional in the sense that \(f(s_1,\ldots ,s_n) \mathrel {\approx }f(t_1,\ldots ,t_n)\) implies \(s_1 \mathrel {\approx }t_1,\ldots ,s_n \mathrel {\approx }t_n\). In addition, we investigate a variant of extensionality that is more appropriate for commutative function symbols, but which raises the complexity of the word problem to coNP.

We present a refutationally complete superposition calculus for a version of higher-order logic based on the combinatory calculus. We also introduce a novel method of dealing with extensionality. The calculus was implemented in the Vampire theorem prover and we test its performance against other leading higher-order provers. The results suggest that the method is competitive.

International audience; We introduce setoid type theory, an intensional type theory with a proof-irrelevant universe of propositions and an equality type satisfying function extensionality, propositional extensionality and a definitional computation rule for transport. We justify the rules of setoid type theory by a syntactic translation into a pure type theory with a universe of propositions. We conjecture that our syntax is complete with regards to this translation.

Goodman's theorem (1976) states that intuitionistic finite-type arithmetic plus the axiom of choice plus the axiom of relativized dependent choice is conservative over Heyting arithmetic. The same result applies to the extensional variant. This is due to Beeson (1979). In this paper we modify Goodman realizability (1978) and provide a new proof of the extensional case., Comment: 25 pages. Updated. To appear in NDJFL

The delay datatype was introduced by Capretta (Logical Methods in Computer Science, 1(2), article 1, 2005) as a means to deal with partial functions (as in computability theory) in Martin-Löf type theory. The delay datatype is a monad. It is often desirable to consider two delayed computations equal, if they terminate with equal values, whenever one of them terminates. The equivalence relation underlying this identification is called weak bisimilarity. In type theory, one commonly replaces quotients with setoids. In this approach, the delay datatype quotiented by weak bisimilarity is still a monad–a constructive alternative to the maybe monad. In this paper, we consider the alternative approach of Hofmann (Extensional Constructs in Intensional Type Theory, Springer, London, 1997) of extending type theory with inductive-like quotient types. In this setting, it is difficult to define the intended monad multiplication for the quotiented datatype. We give a solution where we postulate some principles, crucially proposition extensionality and the (semi-classical) axiom of countable choice. With the aid of these principles, we also prove that the quotiented delay datatype delivers free ω-complete pointed partial orders (ωcppos).Altenkirch et al. (Lecture Notes in Computer Science, vol. 10203, Springer, Heidelberg, 534–549, 2017) demonstrated that, in homotopy type theory, a certain higher inductive–inductive type is the free ωcppo on a type X essentially by definition; this allowed them to obtain a monad of free ωcppos without recourse to a choice principle. We notice that, by a similar construction, a simpler ordinary higher inductive type gives the free countably complete join semilattice on the unit type 1. This type suffices for constructing a monad, which is isomorphic to the one of Altenkirch et al. We have fully formalized our results in the Agda dependently typed programming language.

Contact algebra is one of the main tools in the region-based theory of space. It is an extension of Boolean algebra with a relation called contact. The elements of the Boolean algebra are considered as formal representations of physical bodies. The contact relation is used also to define some other important mereotopological relations like non-tangential inclusion, dual contact, external contact. Most of these definitions are given by means of the operation of Boolean complementation. There are, however, some problems related to the motivation of this operation. In order to avoid these problems we propose a generalization of the notion of contact algebra by dropping the operation of complement. In this paper we consider as non-definable primitives the relations of contact, nontangential inclusion and dual contact. Part I of the paper is devoted to a suitable axiomatization called extended distributive contact lattice (EDCL) by means of universal first-order axioms true in all contact algebras. EDCL may be considered also as an algebraic tool for certain subarea of mereotopology, called in this paper distributive mereotopology. The main result of Part I of the paper is a representation theorem, stating that each EDCL can be embedded into a contact algebra, showing in this way that the presented axiomatization preserves the meaning of mereotopological relations without considering Boolean complementation. Part II of the paper is devoted to topological representation theory of EDCL, transferring into the distributive case important results from the topological representation theory of contact algebras. It is shown that under minor additional assumptions on distributive lattices as extensionality of the definable relations of overlap or underlap one can preserve the good topological interpretations of regions as regular closed or regular open sets in topological space., Comment: The final publication is available at Springer via http://dx.doi.org/10.1007/s10472-016-9499-5

Cubical type theory provides a constructive justification to certain aspects of homotopy type theory such as Voevodsky's univalence axiom. This makes many extensionality principles, like function and propositional extensionality, directly provable in the theory. This paper describes a constructive semantics, expressed in a presheaf topos with suitable structure inspired by cubical sets, of some higher inductive types. It also extends cubical type theory by a syntax for the higher inductive types of spheres, torus, suspensions,truncations, and pushouts. All of these types are justified by the semantics and have judgmental computation rules for all constructors, including the higher dimensional ones, and the universes are closed under these type formers., Comment: 24 pages

We present a model of dependent type theory ( DTT ) with Π-, 1-, Σ- and intensional Id -types, which is based on a slight variation of the (call-by-name) category of AJM-games and history-free winning well-bracketed strategies. The model satisfies Streicher's criteria of intensionality and refutes function extensionality. The principle of uniqueness of identity proofs is satisfied. We show it contains a submodel as a full subcategory which gives a faithful interpretation of DTT with Π-, 1-, Σ- and intensional Id -types and, additionally, finite inductive type families. This smaller model is fully (and faithfully) complete with respect to the syntax at the type hierarchy built without Id -types, as well as at the more general class of types where we allow for one strictly positive occurrence of an Id -type. Definability for the full type hierarchy with Id -types remains to be investigated.

The paper concerns Grzegorczyk's non-Fregean logics that are intended to be a formal representation of the equimeaning relation defined on descriptions. We argue that the main Grzegorczyk logics discussed in the literature are too strong and we propose a new logical system, $${\mathsf{MGL}}$$MGL, which satisfies Grzegorczyk's fundamental requirements. We present a sound and complete semantics for $${\mathsf{MGL}}$$MGL and we prove that it is decidable. Finally, we show that many non-classical logics are extensions of $${\mathsf{MGL}}$$MGL, which makes it a generic non-Fregean logic.

The notion of extensionality, introduced by Hohle and Blanchard, and the notion of compatibility, as coined by Bi¾?lohlavek, of a fuzzy relation with respect to a fuzzy equality are trivially equivalent. Here, this compatibility property is dissected into left and right compatibility, mimicking the original twofold definition of extensionality, and studied in detail in the context of arbitrary fuzzy relations. Relying on the notions of left and right traces of a fuzzy relation, it is shown that compatibility can be characterized in terms of inclusions, shedding another light on the matter.

We study fuzzy quantifiers of type 〈 1 , 1 〉 defined using fuzzy measures and integrals. Residuated lattices are considered as structures of truth values. We present basic notions on fuzzy measures over algebras of fuzzy subsets of a given fuzzy set, and the definition and necessary properties of so-called ⊙-fuzzy integrals. Residuated lattice operations are established to derive operations between fuzzy sets describing degrees in which formulas expressing relations between fuzzy sets are true. Finally, a general definition of type 〈 1 , 1 〉 fuzzy quantifiers determined by fuzzy measures and integrals is introduced and several examples of important natural language quantifiers are modeled using this approach.

Along the line of Hirst-Mummert [9] and Dorais [4], we analyze the relationship between the classical provability of uniform versions Uni(S) of Π2-statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π2-statement S of some syntactical form, if its uniform version derives the uniform variant of over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong semi-intuitionistic systems including bar induction in all finite types but also nonconstructive principles such as Kőnig's lemma and uniform weak Kőnig's lemma . Our result is applicable to many mathematical principles whose sequential versions imply .

In this paper we extend the traditional set-theoretic notion of standard models and nonstandard models going up to α levels in the cumulative hierarchy, α any given limit ordinal. A proof of the representation theorem is given and the structure of nonstandard models is studied where the ”transfer principle” holds for every (not necessarily bounded) formula. These models preserve a stratified structure which is investigated by means of ”pseudo-rank” functions taking linearly ordered values (hyperordinals). In particular, such functions show a ”rigidity” property of the internal sets, in that each external set has a pseudo-rank which is greater than the pseudo-rank of any internal set. 1 Nonstandard α-Models We shall work in ZF−C, i.e. in Zermelo-Fraenkel axiomatic set theory ZF with choice but without the axiom Fnd of foundation (regularity). Thus the axioms of our set theory are precisely: Ext (Extensionality); Pair (Pairing); Sep (Separation Schema); Un (Union); Pow (Power Set); Rep (Replacement Schema); Inf (Infinity) and AC (Choice). For unexplained set-theoretic and model-theoretic notions and notations we refer to [J] and [CK] respectively.

Incorporating extensional equality into a dependent intensional type system such as the Calculus of Constructions provides with stronger type-checking capabilities and makes the proof development closer to intuition. Since strong forms of extensionality lead to undecidable type-checking, a good trade-off is to extend intensional equality with a decidable first-order theory T, as done in CoqMT, which uses matching modulo T for the weak and strong elimination rules, we call these rules T-elimination. So far, type-checking in CoqMT is known to be decidable in presence of a cumulative hierarchy of universes and weak T-elimination. Further, it has been shown by Wang with a formal proof in Coq that consistency is preserved in presence of weak and strong elimination rules, which actually implies consistency in presence of weak and strong T-elimination rules since T is already present in the conversion rule of the calculus.We justify here CoqMT’s type-checking algorithm by showing strong normalization as well as the Church-Rosser property of β-reductions augmented with CoqMT’s weak and strong T -elimination rules. This therefore concludes successfully the meta-theoretical study of CoqMT.

We study idempotents in intensional Martin-L\"of type theory, and in particular the question of when and whether they split. We show that in the presence of propositional truncation and Voevodsky's univalence axiom, there exist idempotents that do not split; thus in plain MLTT not all idempotents can be proven to split. On the other hand, assuming only function extensionality, an idempotent can be split if and only if its witness of idempotency satisfies one extra coherence condition. Both proofs are inspired by parallel results of Lurie in higher category theory, showing that ideas from higher category theory and homotopy theory can have applications even in ordinary MLTT. Finally, we show that although the witness of idempotency can be recovered from a splitting, the one extra coherence condition cannot in general; and we construct "the type of fully coherent idempotents", by splitting an idempotent on the type of partially coherent ones. Our results have been formally verified in the proof assistant Coq., Comment: 24 pages. v2: final version, to appear in LMCS

Viscosity is considered to be a significant indicator of the metallurgical property of blast furnace slag. An improved model for viscosity prediction based on the Chou model was presented in this article. The updated model has optimized the selection strategy of distance algorithm and negative weights at the reference points. Therefore, the extensionality prediction disadvantage in the original model was ameliorated by this approach. The model prediction was compared with viscosity data of slags of compositions typical to BF operations obtained from a domestic steel plant. The results show that the approach can predict the viscosity with average error of 9.23 pct and mean standard deviation of 0.046 Pa s.

International audience; We define the class of relational graph models and study the induced order-and equational-theories. Using the Taylor expansion, we show that all λ-terms with the same Böhm tree are equated in any relational graph model. If the model is moreover extensional and satisfies a technical condition, then its order-theory coincides with Morris's observational pre-order. Finally, we introduce an extensional version of the Taylor expansion, then prove that two λ-terms have the same extensional Taylor expansion exactly when they are equivalent in Morris's sense.

We shall try to defend two non-standard views that run counter to two well-entrenched familiar views. The standard views are (1) the universal and existential quantifiers of first-order logic are not modal operators, and (2) the quantifiers are extensional. If that is correct then the counterclaims create genuine problems for some traditional philosophical doctrines.

This paper gives the strong reduction of the combinatory calculus SCL, which was introduced as a combinatory calculus corresponding to the untyped Lambda-mu calculus. It proves the confluence of the strong reduction. By the confluence, it also proves the conservativity of the extensional equality of SCL over the combinatory calculus CL, and the consistency of SCL.

A graph G is said to be a set graph if it admits an acyclic orientation that is also extensional, in the sense that the out-neighborhoods of its vertices are pairwise distinct. Equivalently, a set graph is the underlying graph of the digraph representation of a hereditarily finite set. In this paper, we continue the study of set graphs and related topics, focusing on computational complexity aspects. We prove that set graph recognition is NP-complete, even when the input is restricted to bipartite graphs with exactly two leaves. The problem remains NP-complete if, in addition, we require that the extensional acyclic orientation be also slim, that is, that the digraph obtained by removing any arc from it is not extensional. Our approach in fact allows us to also show that the counting variants of the above problems are #P-complete, and prove similar complexity results for problems related to a generalization of extensional acyclic digraphs, the so-called hyper-extensional digraphs, which were proposed by Aczel to describe hypersets. Our proofs are based on reductions from variants of the Hamiltonian Path problem. We also consider a variant of the well-known notion of a separating code in a digraph, the so-called open-out-separating code, and show that it is NP-complete to determine whether an input extensional acyclic digraph contains an open-out-separating code of given size.

Glivenko’s theorem states that an arbitrary propositional formula is classically provable if and only if its double negation is intuitionistically provable. The result does not extend to full first-order predicate logic, but does extend to first-order predicate logic without the universal quantifier. A recent paper by Zdanowski shows that Glivenko’s theorem also holds for second-order propositional logic without the universal quantifier. We prove that Glivenko’s theorem extends to some versions of simple type theory without the universal quantifier. Moreover, we prove that Kuroda’s negative translation, which is known to embed classical first-order logic into intuitionistic first-order logic, extends to the same versions of simple type theory. We also prove that the Glivenko property fails for simple type theory once a weak form of functional extensionality is included.

Modal propositional logic can be obtained either by extending non-modal propositional logic (this is the case of Lewis’ systems) or by using many-valued logic as the basic system. The second route was taken by Jan Łukasiewicz, who proved that modalities cannot be defined within two-valued logic. The principle of extensionality was a tacit Łukasiewicz’s assumption. If we compare Lewis’ modal systems with that of Łukasiewicz, we see that both solutions share most logical principles. Perhaps the most important difference concerns the formula ◊( A ^ ¬ A ), in words ( A and ¬A ) is possible. Łukasiewicz argued that this formula has the value 1/2, if A and ¬ A have this value as well. I argue that Łukasiewicz’s argument is not correct.

We provide a co-free construction which adds elementary structure to a primary doctrine. We show that the construction preserves comprehensions and all the logical operations which are in the starting doctrine, in the sense that it maps a first order many-sorted theory into a the same theory formulated with equality. As a corollary it forces an implicational doctrine to have an extentional entailment.

The paper discusses Grzegorczyk’s logic LD of descriptive equivalence, some of its extensions (logics LDD and LDT), and its more recent modifications, which are the logic of equimeaning LE and the logic of descriptions with Suszko’s axioms LDS. We present an improved semantics for LD and prove a corresponding extended soundness and completeness theorem. We also show that LD is paraconsistent. These results generalize to LDD, LDT, and LDS as well. We briefly study the properties of LE. Furthermore, we compare the strengths of the logics and prove, in particular, that LD is uncomparable with LE and LDS, and the logic LDD—the extension of LD with the so called Delusion Axiom—is the strongest among the logics in question. Next we show that descriptive equivalence can be defined in terms of descriptive implication in LDT but not in LD. We prove also that if we identify the descriptive equivalence with the implication of the other logics, then LD, LDD, and LDT are different from intuitionistic logic and relevance logics T, E, R, EM, RM. Moreover, descriptive equivalence cannot be identified with necessary equivalence in any class of Kripke frames. Finally, we study different ways to formulate the idea of extensionality, presenting three different extensionality principles and exploring which logics satisfy each of them.

The naive theory of properties states that for every condition there is a property instantiated by exactly the things which satisfy that condition. The naive theory of properties is inconsistent in classical logic, but there are many ways to obtain consistent naive theories of properties in nonclassical logics. The naive theory of classes adds to the naive theory of properties an extensionality rule or axiom, which states roughly that if two classes have exactly the same members, they are identical. In this paper we examine the prospects for obtaining a satisfactory naive theory of classes. We start from a result by Ross Brady, which demonstrates the consistency of something resembling a naive theory of classes. We generalize Brady’s result somewhat and extend it to a recent system developed by Andrew Bacon. All of the theories we prove consistent contain an extensionality rule or axiom. But we argue that given the background logics, the relevant extensionality principles are too weak. For example, in some of these theories, there are universal classes which are not declared coextensive. We elucidate some very modest demands on extensionality, designed to rule out this kind of pathology. But we close by proving that even these modest demands cannot be jointly satisfied. In light of this new impossibility result, the prospects for a naive theory of classes are bleak.

An elementary rheory of concatenation is introduced and used to establish mutual interpretability of Robinson arithmetic, Minimal Predicative Set Theory, the quantifier-free part of Kirby's finitary set theory, and Adjunctive Set Theory, with or without extensionality., Comment: 61 pages

This chapter studies the undirected graphs underlying the membership graphs of sets, which we call set graphs. Set graphs comprise two well-known classes of graphs: as shown in this chapter, • every graph which has a Hamiltonian path is a set graph; • claw-free graphs form the largest hereditary class of graphs every connected member of which is a set graph.We also present two graph transformations under which the class of set graphs is closed: substitution of a vertex by a set graph, and removal of a cut vertex accompanied by addition of certain edges between its neighbors.Then we discuss the algorithmic complexity of establishing whether or not a given undirected graph G is a set graph. This amounts to establishing whether an orientation can be imposed on the edges of G in a way that reflects the properties of membership over ordinary sets: well-foundedness and extensionality. To wit, neither cycles nor distinct vertices endowed with the same set of out-neighbors are permitted in the graph resulting from the orientation. The said problem turns out to be NP-complete, much like the analogous problem arising for hypersets: Does a given G admit a hyperextensional orientation?

The notion of extensionality means in plain sense that properties of complex things can be expressed by means of their simple components, in particular, that two things are identical if and only if certain of their components or features are identical; e.g., the Leibniz Identitas Indiscernibilium Principle: two things are identical if each applicable to them operator yields the same result on either; or, extensionality for sets, viz., two sets are identical if and only if they consist of identical elements. In mereology, this property is expressed by the statement that two things are identical if their parts are the same. However, building a thing from parts may proceed in various ways and this, unexpectedly, yields various extensionality principles. Also, building a thing may lead to things identical with respect to parts but distinct with respect, e.g., to usage. We address the question of extensionality for artifacts, i.e., things produced in some assembling or creative process in order to satisfy a chosen purpose of usage, and, we formulate the extensionality principle for artifacts which takes into account the assembling process and requires for identity of two artifacts that assembling graphs for the two be isomorphic in a specified sense. In parallel, we consider the design process and design things showing the canonical correspondence between abstracta as design products and concreta as artifacts. In the end, we discuss approximate artifacts as a result of assembling with spare parts which analysis does involve rough mereology.

In response to the paper by Cotnoir and Bacon published in RSL 2/2012, we would like to add some remarks regarding supplementation principles. It is known that in a classical mereology, the Strong Supplementation Principle (SSP) together with antisymmetry enforces the Weak Supplementation Principle (WSP). Instead, in the nonwellfounded mereology, the failure of extensionality causes the failure of antisymmetry (Cotnoir, 2010), hence the investigated model is also nonantisymmetric. Cotnoir supposes that the failure of antisymmetry implies the failure of (WSP) when (PP1) is applied, however gives no explicit argument, which we would like to supply in this paper. Additionally, when (PP2) is applied, (SSP) implies (WSP), hence the failure of antisymmetry does not necessarily imply the failure of (WSP).

Axiomatic set theory is almost universally accepted as the basic theory which provides the foundations of mathematics, and in which the whole of present day mathematics can be developed. As such, it is the most natural framework for Mathematical Knowledge Management. However, in order to be used for this task it is necessary to overcome serious gaps that exist between the "official" formulations of set theory (as given e.g. by formal set theory ZF) and actual mathematical practice. In this work we present a new unified framework for formalizations of axiomatic set theories of different strength, from rudimentary set theory to full ZF. It allows the use of set terms, but provides a static check of their validity., Comment: In Proceedings LSFA 2011, arXiv:1203.5423