Orthomodular logic is a weakening of quantum logic in the sense of Birkhoff and von Neumann. Orthomodular logic is shown to be a nonlinear noncommutative logic. Sequents are given a physically motivated semantics that is consistent with exactly one semantics for propositional formulas that use negation, conjunction, and implication. In particular, implication must be interpreted as the Sasaki arrow, which satisfies the deduction theorem in this logic. As an application, this deductive system is extended to two systems of predicate logic: the first is sound for Takeuti’s quantum set theory, and the second is sound for a variant of Weaver’s quantum logic.

We generalize the notion of consequence relation standard in abstract treatments of logic to accommodate intuitions of relevance. The guiding idea follows the use criterion, according to which in order for some premises to have some conclusion(s) as consequence(s), the premises must each be used in some way to obtain the conclusion(s). This relevance intuition turns out to require not just a failure of monotonicity, but also a move to considering consequence relations as obtaining between multisets. We motivate and state basic definitions of relevant consequence relations, both in single conclusion (asymmetric) and multiple conclusion (symmetric) settings, as well as derivations and theories, guided by the use intuitions, and prove a number of results indicating that the definitions capture the desired results (at least in many cases).

The present note was prompted by Weber’s approach to proving Cantor’s theorem, i.e., the claim that the cardinality of the power set of a set is always greater than that of the set itself. While I do not contest that his proof succeeds, my point is that he neglects the possibility that by similar methods it can be shown also that no non-empty set satisfies Cantor’s theorem. In this paper unrestricted abstraction based on a cut free Gentzen type sequential calculus will be employed to prove both results. In view of the connection between Priest’s three-valued logic of paradox and cut free Gentzen calculi this, a fortiori, has an impact on any paraconsistent set theory built on Priest’s logic of paradox.

I discuss problems with Martin-Löf’s distinction between analytic and synthetic judgments in constructive type theory and propose a revision of his views. I maintain that a judgment is analytic when its correctness follows exclusively from the evaluation of the expressions occurring in it. I argue that Martin-Löf’s claim that all judgments of the forms $a : A$ and $a = b : A$ are analytic is unfounded. As I shall show, when A evaluates to a dependent function type $(x : B) \to C$, all judgments of these forms fail to be analytic and therefore end up as synthetic. Going beyond the scope of Martin-Löf’s original distinction, I also argue that all hypothetical judgments are synthetic and show how the analytic–synthetic distinction reworked here is capable of accommodating judgments of the forms $A \> \mathsf {type}$ and $A = B \> \mathsf {type}$ as well. Finally, I consider and reject an alternative account of analyticity as decidability and assess Martin-Löf’s position on the analytic grounding of synthetic judgments.

This paper proves the finite axiomatizability of transitive modal logics of finite depth and finite width w.r.t. proper-successor-equivalence. The frame condition of the latter requires, in a rooted transitive frame, a finite upper bound of cardinality for antichains of points with different sets of proper successors. The result generalizes Rybakov’s result of the finite axiomatizability of extensions of $\mathbf {S4}$ of finite depth and finite width.

It is widely thought that chance should be understood in reductionist terms: claims about chance should be understood as claims that certain patterns of events are instantiated. There are many possible reductionist theories of chance, differing as to which possible pattern of events they take to be chance-making. It is also widely taken to be a norm of rationality that credence should defer to chance: special cases aside, rationality requires that one’s credence function, when conditionalized on the chance-making facts, should coincide with the objective chance function. It is a shortcoming of a theory of chance if it implies that this norm of rationality is unsatisfiable. The primary goal of this paper is to show, on the basis of considerations concerning computability and inductive learning, that this shortcoming is more common than one would have hoped.

In this note we study a counterpart in predicate logic of the notion of logical friendliness, introduced into propositional logic in [15]. The result is a new consequence relation for predicate languages with equality using first-order models. While compactness, interpolation and axiomatizability fail dramatically, several other properties are preserved from the propositional case. Divergence is diminished when the language does not contain equality with its standard interpretation.

The paper investigates from a proof-theoretic perspective various non-contractive logical systems, which circumvent logical and semantic paradoxes. Until recently, such systems only displayed additive quantifiers (Grišin and Cantini). Systems with multiplicative quantifiers were proposed in the 2010s (Zardini), but they turned out to be inconsistent with the naive rules for truth or comprehension. We start by presenting a first-order system for disquotational truth with additive quantifiers and compare it with Grišin set theory. We then analyze the reasons behind the inconsistency phenomenon affecting multiplicative quantifiers. After interpreting the exponentials in affine logic as vacuous quantifiers, we show how such a logic can be simulated within a truth-free fragment of a system with multiplicative quantifiers. Finally, we establish that the logic for these multiplicative quantifiers (but without disquotational truth) is consistent, by proving that an infinitary version of the cut rule can be eliminated. This paves the way to a syntactic approach to the proof theory of infinitary logic with infinite sequents.

We explain and explore class-theoretic potentialism—the view that one can always individuate more classes over a set-theoretic universe. We examine some motivations for class-theoretic potentialism, before proving some results concerning the relevant potentialist systems (in particular exhibiting failures of the $\mathsf {.2}$ and $\mathsf {.3}$ axioms). We then discuss the significance of these results for the different kinds of class-theoretic potentialists.

Given a three-valued definition of validity, which choice of three-valued truth tables for the connectives can ensure that the resulting logic coincides exactly with classical logic? We give an answer to this question for the five monotonic consequence relations $st$, $ss$, $tt$, $ss\cap tt$, and $ts$, when the connectives are negation, conjunction, and disjunction. For $ts$ and $ss\cap tt$ the answer is trivial (no scheme works), and for $ss$ and $tt$ it is straightforward (they are the collapsible schemes, in which the middle value acts like one of the classical values). For $st$, the schemes in question are the Boolean normal schemes that are either monotonic or collapsible.

The present review paper has several objectives. Its primary aim is to give an idea of the general features of virtual element methods (VEMs), which were introduced about a decade ago in the field of numerical methods for partial differential equations, in order to allow decompositions of the computational domain into polygons or polyhedra of a very general shape.

Nonetheless, the paper is also addressed to readers who have already heard (and possibly read) about VEMs and are interested in gaining more precise information, in particular concerning their application in specific subfields such as ${C}^1$ -approximations of plate bending problems or approximations to problems in solid and fluid mechanics.

This article surveys research on the application of compatible finite element methods to large-scale atmosphere and ocean simulation. Compatible finite element methods extend Arakawa’s C-grid finite difference scheme to the finite element world. They are constructed from a discrete de Rham complex, which is a sequence of finite element spaces linked by the operators of differential calculus. The use of discrete de Rham complexes to solve partial differential equations is well established, but in this article we focus on the specifics of dynamical cores for simulating weather, oceans and climate. The most important consequence of the discrete de Rham complex is the Hodge–Helmholtz decomposition, which has been used to exclude the possibility of several types of spurious oscillations from linear equations of geophysical flow. This means that compatible finite element spaces provide a useful framework for building dynamical cores. In this article we introduce the main concepts of compatible finite element spaces, and discuss their wave propagation properties. We survey some methods for discretizing the transport terms that arise in dynamical core equation systems, and provide some example discretizations, briefly discussing their iterative solution. Then we focus on the recent use of compatible finite element spaces in designing structure preserving methods, surveying variational discretizations, Poisson bracket discretizations and consistent vorticity transport.

One of the main challenges in molecular dynamics is overcoming the ‘timescale barrier’: in many realistic molecular systems, biologically important rare transitions occur on timescales that are not accessible to direct numerical simulation, even on the largest or specifically dedicated supercomputers. This article discusses how to circumvent the timescale barrier by a collection of transfer operator-based techniques that have emerged from dynamical systems theory, numerical mathematics and machine learning over the last two decades. We will focus on how transfer operators can be used to approximate the dynamical behaviour on long timescales, review the introduction of this approach into molecular dynamics, and outline the respective theory, as well as the algorithmic development, from the early numerics-based methods, via variational reformulations, to modern data-based techniques utilizing and improving concepts from machine learning. Furthermore, its relation to rare event simulation techniques will be explained, revealing a broad equivalence of variational principles for long-time quantities in molecular dynamics. The article will mainly take a mathematical perspective and will leave the application to real-world molecular systems to the more than 1000 research articles already written on this subject.

Floating-point numbers have an intuitive meaning when it comes to physics-based numerical computations, and they have thus become the most common way of approximating real numbers in computers. The IEEE-754 Standard has played a large part in making floating-point arithmetic ubiquitous today, by specifying its semantics in a strict yet useful way as early as 1985. In particular, floating-point operations should be performed as if their results were first computed with an infinite precision and then rounded to the target format. A consequence is that floating-point arithmetic satisfies the ‘standard model’ that is often used for analysing the accuracy of floating-point algorithms. But that is only scraping the surface, and floating-point arithmetic offers much more.

In this survey we recall the history of floating-point arithmetic as well as its specification mandated by the IEEE-754 Standard. We also recall what properties it entails and what every programmer should know when designing a floating-point algorithm. We provide various basic blocks that can be implemented with floating-point arithmetic. In particular, one can actually compute the rounding error caused by some floating-point operations, which paves the way to designing more accurate algorithms. More generally, properties of floating-point arithmetic make it possible to extend the accuracy of computations beyond working precision.

We discuss the modelling framework of port-Hamiltonian descriptor systems and their use in numerical simulation and control. The structure is ideal for automated network-based modelling since it is invariant under power-conserving interconnection, congruence transformations and Galerkin projection. Moreover, stability and passivity properties are easily shown. Condensed forms under orthogonal transformations present easy analysis tools for existence, uniqueness, regularity and numerical methods to check these properties.

After recalling the concepts for general linear and nonlinear descriptor systems, we demonstrate that many difficulties that arise in general descriptor systems can be easily overcome within the port-Hamiltonian framework. The properties of port-Hamiltonian descriptor systems are analysed, and time discretization and numerical linear algebra techniques are discussed. Structure-preserving regularization procedures for descriptor systems are presented to make them suitable for simulation and control. Model reduction techniques that preserve the structure and stabilization and optimal control techniques are discussed.

The properties of port-Hamiltonian descriptor systems and their use in modelling simulation and control methods are illustrated with several examples from different physical domains. The survey concludes with open problems and research topics that deserve further attention.

Low-rank tensor representations can provide highly compressed approximations of functions. These concepts, which essentially amount to generalizations of classical techniques of separation of variables, have proved to be particularly fruitful for functions of many variables. We focus here on problems where the target function is given only implicitly as the solution of a partial differential equation. A first natural question is under which conditions we should expect such solutions to be efficiently approximated in low-rank form. Due to the highly nonlinear nature of the resulting low-rank approximations, a crucial second question is at what expense such approximations can be computed in practice. This article surveys basic construction principles of numerical methods based on low-rank representations as well as the analysis of their convergence and computational complexity.