Set Theory INC# ∞# Based on Infinitary Intuitionistic Logic with Restricted Modus Ponens Rule (Part.II) Hyper Inductive Definitions

In this paper intuitionistic set theory INC# ∞# in infinitary set theoretical language is considered. External induction principle in nonstandard intuitionistic arithmetic were derived. Non trivial application in number theory is considered.The Goldbach-Euler theorem is obtained without anyreferences to Catalan conjecture.

Unifying Decidable Entailments in Separation Logic with Inductive Definitions

The entailment problem $$\upvarphi \models \uppsi $$ φ ⊧ ψ in Separation Logic [12, 15], between separated conjunctions of equational ($$x \approx y$$ x ≈ y and $$x \not \approx y$$ x ≉ y ), spatial ($$x \mapsto (y_1,\ldots ,y_\upkappa )$$ x ↦ ( y 1 , … , y κ ) ) and predicate ($$p(x_1,\ldots ,x_n)$$ p ( x 1 , … , x n ) ) atoms, interpreted by a finite set of inductive rules, is undecidable in general. Certain restrictions on the set of inductive definitions lead to decidable classes of entailment problems. Currently, there are two such decidable classes, based on two restrictions, called establishment [10, 13, 14] and restrictedness [8], respectively. Both classes are shown to be in $$\mathsf {2\text {EXPTIME}}$$ 2 EXPTIME by the independent proofs from [14] and [8], respectively, and a many-one reduction of established to restricted entailment problems has been given [8]. In this paper, we strictly generalize the restricted class, by distinguishing the conditions that apply only to the left- ($$\upvarphi $$ φ ) and the right- ($$\uppsi $$ ψ ) hand side of entailments, respectively. We provide a many-one reduction of this generalized class, called safe, to the established class. Together with the reduction of established to restricted entailment problems, this new reduction closes the loop and shows that the three classes of entailment problems (respectively established, restricted and safe) form a single, unified, $$\mathsf {2\text {EXPTIME}}$$ 2 EXPTIME -complete class.

Entailment Checking in Separation Logic with Inductive Definitions is 2-EXPTIME hard

The entailment between separation logic formulæ with inductive predicates, also known as sym- bolic heaps, has been shown to be decidable for a large class of inductive definitions [7]. Recently, a 2-EXPTIME algorithm was proposed [10, 14] and an EXPTIME-hard bound was established in [8]; however no precise lower bound is known. In this paper, we show that deciding entailment between predicate atoms is 2-EXPTIME-hard. The proof is based on a reduction from the membership problem for exponential-space bounded alternating Turing machines [5].

Beyond Symbolic Heaps: Deciding Separation Logic With Inductive Definitions

Symbolic-heap separation logic with inductive definitions is a popular formalism for reasoning about heap-manipulating programs. The fragment SLIDbtw introduced by Iosif, Rogalewicz and Simacek, is one of the most expressive fragments with a decidable entailment problem. In recent work, we improved on the original decidability proof by providing a direct model-theoretic construction, obtaining a 2-Exptime upper bound. In this paper, we investigate separation logics built on top of the inductive definitions from SLIDbtw, i.e., logics that feature the standard Boolean and separation-logic operators. We give an almost tight delineation between decidability and undecidabilty. We establish the decidability of the satisfiability problem (in 2-Exptime) of a separation logic with conjunction, disjunction, separating conjunction and guarded forms of negation, magic wand, and septraction. We show that any further generalization leads to undecidabilty (under mild assumptions).

Embeddings of Bishop spaces

We develop the basic constructive theory of embeddings of Bishop spaces in parallel to the basic classical theory of embeddings of topological spaces. The theory of Bishop spaces is a constructive approach to point-function topology and a natural constructive alternative to the classical theory of the rings of continuous functions. Our most significant result is the translation of the classical Urysohn extension theorem within the theory of Bishop spaces. The related theory of the zero sets of a Bishop topology is also included. We work within $\textrm{BISH}^{\ast }$, Bishop’s informal system of constructive mathematics $\textrm{BISH}$ equipped with inductive definitions with rules of countably many premises.

Constructing Infinitary Quotient-Inductive Types

This paper introduces an expressive class of quotient-inductive types, called QW-types. We show that in dependent type theory with uniqueness of identity proofs, even the infinitary case of QW-types can be encoded using the combination of inductive-inductive definitions involving strictly positive occurrences of Hofmann-style quotient types, and Abel’s size types. The latter, which provide a convenient constructive abstraction of what classically would be accomplished with transfinite ordinals, are used to prove termination of the recursive definitions of the elimination and computation properties of our encoding of QW-types. The development is formalized using the Agda theorem prover.