On a definition of Frege

Over the last few weekends I’ve been reading Frege’s “The Foundations of Arithmetic”, a wonderful book mixing philosophy, logic and mathematics from 1884. I hope I will find time to post on the book more generally, but for now I was intrigued enough by this interesting passage to want to play a little with it.

Frege writes:

The proposition

“if every object to which x stands in the relation to \phi falls under the concept F, and if from the proposition that d falls under the concept F it follows universally, whatever d may be, that every object to which d stands in the relation to \phi falls under the concept F, then y falls under the concept F, whatever concept F may be”

is to mean the same as

y follows in the \phi-series after x

G. Frege, “The Foundations of Arithmetic”, Section 79.

Let’s write “y follows in the \phi-series after x” as (x,y) \in G. Then I read Frege’s definition as:

(x,y) \in G iff

\forall F. (\forall a. (x,a) \in \phi \to F(a)) \wedge (\forall d. F(d) \to (\forall e. (d,e) \in \phi \to F(e))) \to F(y)

Frege’s definition appears to be a characterisation of the transitive closure of \phi, that is the smallest transitive relation containing \phi. Or is it? Perhaps this is not immediately apparent. I thought it might be a fun exercise to formalise this and explore it in Coq, a formal proof assistant I’ve played with a little in the past.

I enclose the Coq code I wrote below (note I am very much an amateur with Coq) that shows that Frege’s definition, once tying down an object universe ({\mathtt A} in the code) indeed (i) contains \phi, (ii) is transitive and (iii) is contained in any other transitive relation containing \phi.

I hope you enjoy.

(* Coq analysis of a definition of Frege                                                  *)
(* Formalises Frege’s ‘follows’ definition and proves it equivalent to transitive closure *)
(* George A. Constantinides, 25/03/23                                                     *)

Require Import Coq.Relations.Relation_Definitions. (* for inclusion and transitive *)
Require Import Coq.Relations.Relation_Operators.

Variable A : Type.
Variable phi : AAProp.

Definition FregeFollows (x : A) (y : A) :=
  (F : AProp),
  ( (a : A), (phi x a) → (F a)) ∧
  ( (d : A), (F d) → ( (e : A), (phi d e) → (F e)))
  → (F y).

(* We will separately show:                                                    *)
(* 1. phi is included in FregeFollows                                          *)
(* 2. FregeFollows is transitive                                               *)
(* 3. Amongst all relations meeting conditions 1 & 2, FregeFollows is minimal. *)

(* 1. phi is included in Frege’s relation *)

Theorem IncludesPhi : inclusion A phi FregeFollows.
  unfold inclusion.
  intros x y.
  unfold FregeFollows.
  intros H F.
  intros H1.
  destruct H1. (* we only need base case *)
  apply (H0 y).

(* 2. Frege’s relation is transitive *)

Theorem IsTransitive : transitive A FregeFollows.
  unfold transitive.
  intros x y z.
  unfold FregeFollows.
  intros H0 H1.
  intros F.
  specialize (H0 F).
  specialize (H1 F).
  intros H2.

  apply H1.

  pose proof H2 as G. (* keep a copy of H2 to use to prove F y *)

  apply H0 in G.

  destruct H2.
  2: assumption.

  intros a.
  intros H3.

  specialize (H2 y).

  specialize (H2 G).
  specialize (H2 a).
  specialize (H2 H3).


(* 3. Amongst all transitive relations including phi, Frege’s relation is minimal *)

Theorem IsMinimal : R : relation A,
  (inclusion A phi R) ∧ (transitive A R) → (inclusion A FregeFollows R).
  intros R.
  intros H.
  unfold inclusion.
  intros x y.
  unfold FregeFollows.
  intros H1.

  specialize (H1 (R x)). (* Choose F to be R(x,.) *)
  apply H1.


  destruct H.
  unfold inclusion in H.

  specialize (H x).
  1: assumption.

  intros d Rxd e.

  destruct H.
  unfold transitive in H0.
  specialize (H0 x d e).
  apply H0.
  1: assumption.

  unfold inclusion in H.
  specialize (H d e).

  apply H.

Redundant Life Totals

It’s nearly Christmas, and despite illness hitting our house this year, we’re still managing to play games. One of the games I enjoy playing with my family is Star Realms, however the built-in mechanism for keeping track of life total – known in this game as “Authority” – is a little clunky, and so my son and I quickly decided to use spin-down life counters from Magic: The Gathering instead.

Authority starts at 50, and it can go up and down during a game of Star Realms. This means we need at least three spin down life counters to represent our Authority, assuming that the total authority is equal to the sum of the values displayed on the life counters. We did briefly consider using one to represent tens and one to represent units, but this was too fiddly to operate in practice.

Two ways of representing 22 Authority: 12+10 and 20+2.

Over the years, I’ve had many disputes with my son and wife over how I choose to represent my Authority total. If they have a total Authority of n, then they like to have d = \lceil n/20 \rceil spin-downs on the battlefield. For d > 1, if n is not a multiple of 20, then they keep precisely d-1 of these spin downs at 20 Authority, with the remaining one at n \mod 20. They get very annoyed with me, as that’s not how I keep them at all: I choose a seemingly random collection of values that adds up to n.

But there is method in my madness. When I want to deduct, say, 10 authority from a total represented as 20+3, it’s easy for me: I find a spin down with at least the amount I wish to deduct (if one exists) and deduct it from only that one, so I’d get 10+3. In the same position, they’d to deduct the 3, remove that spin down from the battlefield, and then deduct the remaining 7 from the final spin down to get a single spin down showing 13.

They complain that it’s hard to figure out how much Authority I have and whether I’m in the lead or not. And they’re right. In my system, arithmetic tends to be easier – I tend to need to flip fewer spin downs – but comparison is harder.

This is exactly the same situation, for essentially exactly the same reason, as one is faced with in computer arithmetic. They have chosen a canonical number representation, leading to efficient storage (few spin downs on the table) and efficient comparison. I have chosen a redundant number system, leading to fast computation but complex comparison.

Such redundant number systems have a long history. My friend and colleague Miloš Ercegovac, who is an expert in this field, has pointed out to me that an account of such a system was described in a 1726 paper by Mr John Colson FRS (please do download the PDF – the language is a joy). More recently, Miloš developed a deep and profoundly appealing system known as online arithmetic based on exploiting the properties of redundancy in computer arithmetic, a topic we continue to work on to this day. I strongly recommend Miloš’s book for details on this arithmetic and much much more.

Computer arithmetic pops up everywhere. Even when ill and on a Christmas holiday!

(Fellow gamers who also like spin down life counters might also be interested in this paper my son and I published some years ago.)

St. Anselm’s Ontological Argument

Over the past few weeks, my son has been telling me about St. Anselm’s ontological argument for the existence of God. Last weekend I decided to play around with trying to formalise a version of this argument mathematically. This post briefly records my thoughts on the matter. I make no claim to originality, nor have I undertaken a review of what other people have done in this area; this was just a fun way to spend some of the weekend. I would also caution that I am neither a philosopher nor a logician, however I am a user of formal logic. If any philosophers or logicians happen across this blog post and strongly disagree with anything I’ve said, it would be fun to hear about it and I’d love to learn more. It is entirely possible that I’ve committed some cardinal sin. Pun intended.

The version of the argument given in the Internet Encyclopaedia of Philosophy is as follows:

  1. It is a conceptual truth (or, so to speak, true by definition) that God is a being than which none greater can be imagined (that is, the greatest possible being that can be imagined).
  2. God exists as an idea in the mind.
  3. A being that exists as an idea in the mind and in reality is, other things being equal, greater than a being that exists only as an idea in the mind.
  4. Thus, if God exists only as an idea in the mind, then we can imagine something that is greater than God (that is, a greatest possible being that does exist).
  5. But we cannot imagine something that is greater than God (for it is a contradiction to suppose that we can imagine a being greater than the greatest possible being that can be imagined.)
  6. Therefore, God exists.

Our first challenge is to understand what it means to be “an idea in the mind”. I tend to think of an idea in the mind as a description of something and, formally, as a logical formula defining a predicate. (I am not sure if this is what others think!) For the sake of simplicity, I will consider in the below “an idea in the mind” to simply mean a predicate defined on “physical things”, but keep in mind that when I refer to a predicate below, I’m really referring to the equivalence class of formulae defining this predicate.

The reading of ideas as formulae (or predicates) makes it hard to say what we mean when we compare two things, one which exists and one which doesn’t, in Line 3 of Anselm’s argument, though, an issue we will address below.

Finally, to my way of thinking, there appears to be an unnecessary implicit focus on uniqueness in the way the argument presented above is given, so let’s strip that away to simplify matters, so we just want to focus on a predicate which may be taken to describe ‘godliness’, or ‘godlike things’ – call it \Theta.


Taking the above arguments together, I will redefine the first premise as “the concept of godliness is a concept of which there is none greater.”

The other unnecessary element in this argument seems to be the use of language to draw the reader into trying to define ‘greater’ as some kind of second-order predicate denoting an order (of some kind) on first-order predicates. We will see below that this is not necessary, so we will consider ‘greater’ as simply referring here to an arbitrary 2-place second-order predicate G. Thus we obtain

1. \neg \exists P G( P, \Theta ).

We obtain Premise 2 directly by simply stating Premise 1 formally, given our conception of ‘an idea in the mind’.

Premise 3 is interesting. In our reformulation, we have a few approaches to this premise depending on what is meant by “other things being equal”. It seems that the weakest interpretation would be “for any concept describing something that doesn’t exist, there’s some greater concept”:

3a. \forall P. (\neg \exists x P x) \rightarrow \exists Q G(Q, P).

(Note that here, and in the following, I’ve used the convention that a ‘dot’ indicates an opening bracket that is closed at the end of the statement.)


The proof then follows Lines 4-6 directly:

From Premise 3a, conclude \neg \exists x. \Theta x \to \exists Q G(Q,\Theta) via universal instantiation. Then using Premise 1 and modus tollens, one obtains \exists x. \Theta x.

In English: we may conclude from Premise 3a that if a god does not exist then there exists a concept greater than godliness. But since there is no concept greater than godliness (Premise 1), a god exists.

What does this mean?

This argument is valid, but what is its semantic content? Let’s try to build some ‘unorthodox’ models to see if we can satisfy these premises and understand the rigidity these premises provide. In this section I will use \llbracket \phi \rrbracket to denote the interpretation of a formula \phi in a model, and I will use \Xi to denote the false predicate, i.e. \llbracket \Xi \rrbracket(x) is false for all x.

One simple model has (M1) \llbracket G( P, \Xi ) \rrbracket true for any predicate P with different interpretation to \Xi, (M2) \llbracket G( P, Q ) \rrbracket false for all other predicate pairs, and (M3) \llbracket \Theta \rrbracket(x) true for all x. Let’s verify the premises under this model. Since \Theta and \Xi differ in interpretation, Premise 1 is true by (M2 + M3). Equally, Premise 3a is true by (M1). What’s this model (one of several) actually saying? “Everything is godlike! A godlike thing exists!”. So quite reasonable logically, but perhaps not in line with a typical reading – perhaps it can be taken as a pantheistic reading!

Another simple model has all the same interpretations as above but with \llbracket \Theta \rrbracket(x) true for exactly one element. This model is saying “There’s a unique existent God! But the concept of God is no greater than the concept of any other existent thing.”

Both of these models do actually have G as a partial order, though there are also models where it is not. Even if we were to impose strict totality on G, then there are minimal restrictions on the order: we require only that godliness is at the top.

In general, in every model, the interpretation of G is one for which there is an epimorphism \delta from \llbracket G \rrbracket onto a specific relation on \{\top, \bot\}. Then the relation in question is \Gamma = \{ (\top,\bot), (\bot,\bot) \}. We also require \delta(\Theta) = \top and \delta(\Xi) = \bot. Another way of saying this is that any relation G will do, so long as its digraph can be partitioned into two vertex subsets: a nonempty set containing zero indegree nodes (including \Theta), and a nonempty subset containing the rest (including \Xi). Note that to achieve this, the interpretation of \Theta and \Xi must necessarily differ, i.e. a god must exist.

It appears that Anselm’s argument has basically shifted the problem ‘existence of God’ onto the problem of “what does ‘greater’ mean?” The special relation described in the preceding paragraph forms the archetype of acceptable answers to the latter question: ideas that are greatest must be those that describe an existing thing.

“Other things being equal”

Let’s go back to the line ‘other things being equal’. The best I can muster here as an alternative interpretation of Premise 3 taking this line into account is that “for every concept P describing something that doesn’t exist, there’s some greater concept describing only those things described by P that also exist”:

3b. \forall P. (\neg \exists x P x) \rightarrow \exists Q. G(Q, P) \wedge \exists x Q(x) \wedge \forall x. Q(x) \rightarrow P(x).

However, (3b) is clearly unsatisfiable: For an arbirary predicate \Pi, assume the antecedent \neg \exists x \Pi x. Then the third conjunct enforces \neg \exists x Q(x), which directly contradicts the second conjunct.


I have provided two readings of St. Anselm’s argument, based on simplification away of uniqueness of “things possessing godliness” and using formulas (second-order predicates) to discuss “ideas in the mind”. The difference of these two readings hinges on the interpretation of the phrase “other things being equal”. One reading leads to a variety of models, including a model in which every (real) thing has godliness. The other reading renders Premise 3 of St. Anselm’s argument unsound. Neither reading makes strong use of any order properties relating to the phrase ‘greater than’, however the first reading is satisfiable exactly when existence is encoded within the concept ‘greater than’.

Quite an interesting way to spend a few hours – thanks to my son for interesting me in this!

Highlights from FPGA 2020


Here are a few personal highlights from the FPGA 2020 conference, which took place this week in Seaside, California. (Main photo credit: George Constantinides.)

Jakub Szefer‘s invited talk on “Thermal and Voltage Side Channels and Attacks in Cloud FPGAs” described a rather nifty side-channel through which secrets could be leaked in the context of cloud-based FPGAs. The context is that one user of an FPGA would like to transmit information secretly to the next user of the same FPGA. Jakub suggests transmitting this information via the physical temperature of the FPGA. His proposal is that if the first user would like to transmit a ‘1’, they heat up the FPGA by running a circuit that uses a lot of current, such as a ring oscillator; if they would like to transmit a ‘0’, they don’t. The second user, once they arrive, measures the temperature of…

View original post 1,412 more words