A wordless proof

Advertisements

The Isabelle logo as end-of-proof symbol

In a recent research paper, I formalised some of my theorems in the proof assistant Isabelle, but left some of them as just proved 'by hand'. I found it helpful to use a different 'QED' symbol depending on which method I had used. Below is an enlarged version of the 'three cubes' symbol in the snippet…

A star operator for functions

If $latex f$ and $latex g$ are functions, what does $latex f*g$ mean? Definition 1. A separation algebra (citation) is a triple $latex (M, \circ, u)$, where $latex M$ is a set, $latex \circ$ has type $latex M \times M \rightharpoonup M$ and is commutative, associative and cancellative, and $latex u\in M$ is the unit…

A comment on ‘Abstract Separation Logic’

Abstract Separation Logic (citation) is based on a partial composition operator, $latex \circ$, which has the following type: $latex \circ : \Sigma \times \Sigma \rightharpoonup \Sigma$ We shall concentrate henceforth on the simplest incarnation of this operator: disjoint union. Here are two useful theorems about disjoint union. Theorem 1. If $latex a\subseteq a'$ and $latex…

A little theorem about odd powers

Here's an interesting little theorem I came across in number theory. By instantiating $latex n$, one can generate an unlimited of exercises for maths students! Theorem. When two numbers are raised to the same odd power, the sum is divisible by the sum of the two numbers; that is: $latex a+b\mid a^{2n+1}+b^{2n+1}$ for any natural…

A proof environment for LaTeX

The johnproof style file provides an environment for typesetting proofs. Features include: It automatically handles page breaks, for those occasions when a long proof splits over multiple pages. It deals with assumptions and case splits. It assigns a label to each step in the proof, for referencing. It indicates the scope of each assumption using…

A new notation for building sets?

We write $latex \forall x\in\mathbb{R}\ldotp x^2 \ge 0$ to express that the square of any real number is non-negative. We write $latex \exists x\in\mathbb{Z} \ldotp x \ge 0 \land x \le 0$ to express that there exists an integer that is both non-negative and non-positive. We write $latex \lambda x:\mathsf{int} \ldotp x+1$ to denote the…