Observational equality: now for good

Building on the recent extension of dependent type theory with a universe of definitionally proof-irrelevant types, we introduce TTobs, a new type theory based on the setoidal interpretation of dependent type theory. TTobs equips every type with an identity relation that satisfies function extensionality, propositional extensionality, and definitional uniqueness of identity proofs (UIP). Compared to other existing proposals to enrich dependent type theory with these principles, our theory features a notion of reduction that is normalizing and provides an algorithmic canonicity result, which we formally prove in Agda using the logical relation framework of Abel et al. Our paper thoroughly develops the meta-theoretical properties of TTobs, such as the decidability of the conversion and of the type checking, as well as consistency. We also explain how to extend our theory with quotient types, and we introduce a setoidal version of Swan's Id types that turn it into a proper extension of MLTT with inductive equality.

Quantum Information in Relativity: The Challenge of QFT Measurements

Proposed quantum experiments in deep space will be able to explore quantum information issues in regimes where relativistic effects are important. In this essay, we argue that a proper extension of quantum information theory into the relativistic domain requires the expression of all informational notions in terms of quantum field theoretic (QFT) concepts. This task requires a working and practicable theory of QFT measurements. We present the foundational problems in constructing such a theory, especially in relation to longstanding causality and locality issues in the foundations of QFT. Finally, we present the ongoing Quantum Temporal Probabilities program for constructing a measurement theory that (i) works, in principle, for any QFT, (ii) allows for a first- principles investigation of all relevant issues of causality and locality, and (iii) it can be directly applied to experiments of current interest.

Four-valued expansions of Dunn-Belnap's logic (I): Basic characterizations

Basic results of the paper are that any four-valued expansion L4 of Dunn-Belnap's logic DB4 is defined by a unique (up to isomorphism) conjunctive matrix with exactly two distinguished values over an expansion 𝔄4 of a De Morgan non-Boolean four-valued diamond, but by no matrix with either less than four values or a single [non-]distinguished value, and has no proper extension satisfying Variable Sharing Property (VSP). We then characterize L4's having a theorem / inconsistent formula, satisfying VSP and being [inferentially] maximal / subclassical / maximally paraconsistent, in particular, algebraically through ℳ4|𝔄4's (not) having certain submatrices|subalebras. Likewise, [providing 𝔄4 is regular / has no three-element subalgebra] L4 has a proper consistent axiomatic extension if[f] ℳ4 has a proper paraconsistent / two-valued submatrix [in which case the logic of this submatrix is the only proper consistent axiomatic extension of L4 and is relatively axiomatized by the Excluded Middle law axiom]. As a generic tool (applicable, in particular, to both classically-negative and implicative expansionsof DB4), we also prove that the lattice of axiomatic extensions of the logic of an implicative matrix ℳ with equality determinant is dual to the distributive lattice of lower cones of the set of all submatrices of ℳ with non-distinguished values.

New Extensions of Kannan’s and Reich’s Fixed Point Theorems for Multivalued Maps Using Wardowski’s Technique with Application to Integral Equations

The metric function generalizes the concept of distance between two points and hence includes the symmetric property. The aim of this article is to introduce a new and proper extension of Kannan’s fixed point theorem to the case of multivalued maps using Wardowski’s F-contraction. We show that our result is applicable to a class of mappings where neither the multivalued version of Kannan’s theorem nor that of Wardowski’s can be applied to determine the existence of fixed points. Application of our result to the solution of integral equations has been provided. A multivalued Reich type generalized version of the result is also established.

Two Aspects of Relevance in Structured Argumentation: Minimality and Paraconsistency

This paper studies two issues concerning relevance in structured argumentation in the context of the ASPIC+ framework, arising from the combined use of strict and defeasible inference rules. One issue arises if the strict inference rules correspond to classical logic. A longstanding problem is how the trivialising effect of the classical Ex Falso principle can be avoided while satisfying consistency and closure postulates. In this paper, this problem is solved by disallowing chaining of strict rules, resulting in a variant of the ASPIC+ framework called ASPIC*, and then disallowing the application of strict rules to inconsistent sets of formulas. Thus in effect Rescher & Manor's paraconsistent notion of weak consequence is embedded in ASPIC*. Another issue is minimality of arguments. If arguments can apply defeasible inference rules, then they cannot be required to have subset-minimal premises, since defeasible rules based on more information may well make an argument stronger. In this paper instead minimality is required of applications of strict rules throughout an argument. It is shown that under some plausible assumptions this does not affect the set of conclusions. In addition, circular arguments are in the new ASPIC* framework excluded in a way that satisfies closure and consistency postulates and that generates finitary argumentation frameworks if the knowledge base and set of defeasible rules are finite. For the latter result the exclusion of chaining of strict rules is essential. Finally, the combined results of this paper are shown to be a proper extension of classical-logic argumentation with preferences and defeasible rules.

Quasi-linear Cycle Sets and the Retraction Problem for Set-theoretic Solutions of the Quantum Yang-Baxter Equation

Cycle sets were introduced to reduce non-degenerate unitary Yang-Baxter maps to an algebraic system with a single binary operation. Every finite cycle set extends uniquely to a finite cycle set with a compatible abelian group structure. Etingof et al. introduced affine Yang-Baxter maps. These are equivalent to cycle sets with a specific abelian group structure. Abelian group structures have also been essential to get partial results for the still unsolved retraction problem. We introduce two new classes of cycle sets with an underlying abelian group structure and show that they can be transformed into each other while keeping the group structure fixed. This leads to a proper extension of the retractibility conjecture and new evidence for its truth.

Predicate Logic with Anaphora

In this paper I make a case for a separate treatment of (singular) anaphoric pronouns within a predicate logic with anaphora (PLA). Discourse representation theoretic results (from Kamp 1981) can be formulated in a compositional way, without fid­dling with orthodox notions of scope and binding. In contrast with its predecessor dynamic predicate logic (Groenendijk and Stokhof 1991), the system of PLA is a proper extension of ordinary predicate logic and it has a genuine update semantics. Moreover, in contrast with other compositional reformulations of DRT, the seman­tics of PLA remains well within the bounds of ordinary, extensional type theory.

Constrained regular expressions for answering RDF-path queries modulo RDFS

Purpose – The paper aims to discuss extensions of SPARQL that use regular expressions to navigate RDF graphs and may be used to answer queries considering RDFS semantics (in particular, nSPARQL and our proposal CPSPARQL). Design/methodology/approach – The paper is based upon a theoretical comparison of the expressiveness and complexity of both nSPARQL and the corresponding fragment of CPSPARQL, that we call cpSPARQL. Findings – The paper shows that nSPARQL and cpSPARQL (the fragment of CPSPARQL) have the same complexity through cpSPARQL, being a proper extension of SPARQL graph patterns, is more expressive than nSPARQL. Research limitations/implications – It has not been possible to the authors to compare the performance of our CPSPARQL implementation with other proposals. However, the experimentation has allowed to make interesting observations. Practical implications – The paper includes implications for implementing the SPARQL RDFS entailment regime. Originality/value – The paper demonstrates the usefulness of cpSPARQL language. In particular, cpSPARQL, which is sufficient for capturing RDFS semantics, admits an efficient evaluation algorithm, while the whole CPSPARQL language is in theory as efficient as SPARQL is. Moreover, using such a path language within the SPARQL structure allows for properly extending SPARQL.

Fixed Points Of F-Weak Contractions On Complete Metric Spaces

In this paper, we introduce the notion of an F-weak contraction and prove a fixed point theorem for F-weak contractions. Examples are given to show that our result is a proper extension of some results known in the literature

Fixed Point Theorems for Nonlinear Contractions in Menger Spaces

The main purpose of this paper is to introduce a new class of Ćirić-type contraction and to present some fixed point theorems for this mapping as well as for Caristi-type contraction. Several examples are given to show that our results are proper extension of many known results.