Murdoch J. Gabbay

Gilles Dowek, Murdoch J. Gabbay

We define a model of predicate logic in which every term and predicate, open or closed, has an absolute denotation independently of a valuation of the variables. For each variable a, the domain of the model contains an element [[a]] which is the denotation of the term a (which is also a variable symbol). Similarly, the algebra interpreting predicates in the model directly interprets open predicates. Because of this models must also incorporate notions of substitution and quantification. These notions are axiomatic, and need not be applied only to sets of syntax. We prove soundness and show how every 'ordinary' model (i.e. model based on sets and valuations) can be translated to one of our nominal models, and thus also prove completeness.

Murdoch J. Gabbay

Call a semantics for a language with variables absolute when variables map to fixed entities in the denotation. That is, a semantics is absolute when the denotation of a variable a is a copy of itself in the denotation. We give a trio of lattice-based, sets-based, and algebraic absolute semantics to first-order logic. Possibly open predicates are directly interpreted as lattice elements / sets / algebra elements, subject to suitable interpretations of the connectives and quantifiers. In particular, universal quantification "forall a.phi" is interpreted using a new notion of "fresh-finite" limit and using a novel dual to substitution. The interest of this semantics is partly in the non-trivial and beautiful technical details, which also offer certain advantages over existing semantics---but also the fact that such semantics exist at all suggests a new way of looking at variables and the foundations of logic and computation, which may be well-suited to the demands of modern computer science.

Murdoch J. Gabbay

We illustrate how to formally specify distributed algorithms as declarative axiomatic theories in a modal logic, using as illustrative examples a simple voting protocol, a simple broadcast protocol (Bracha Broadcast), and a simple agreement protocol (Crusader Agreement). The methods scale well and have been used to find errors in a proposed industrial protocol. The key novelty is to use modal logic to capture a declarative, high-level representation of essential system properties -- the logical essence of the algorithm -- while abstracting away from explicit state transitions of an abstract machine that implements it. It is like the difference between specifying code in a functional or logic programming language, versus specifying code in an imperative one. Thus we present axiomatisations of Declarative Bracha Broacast and Declarative Crusader Agreement. A logical axiomatisation in the style we propose provides a precise, compact, human-readable specification that abstractly captures essential system properties, while eliding low-level implementation details; it is more precise than a natural language description, yet more abstract than source code or a logical specification thereof. This creates new opportunities for reasoning about correctness, resilience, and failure, and could serve as a foundation for human- and machine verification efforts, design improvements, and even alternative protocol implementations. The proofs in this paper have been formalised in Lean 4.

Lars Brunjes, Murdoch J. Gabbay

We implement two versions of a simple but illustrative smart contract: one in Solidity on the Ethereum blockchain platform, and one in Plutus on the Cardano platform, with annotated code excerpts and with source code attached. We get a clearer view of the Cardano programming model in particular by introducing a novel mathematical abstraction which we call Idealised EUTxO. For each version of the contract, we trace how the architectures of the underlying platforms and their mathematics affects the natural programming styles and natural classes of errors. We prove some simple but novel results about alpha-conversion and observational equivalence for Cardano, and explain why Ethereum does not have them. We conclude with a wide-ranging and detailed discussion in the light of the examples, mathematical model, and mathematical results so far.