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 stands in the relation to falls under the concept , and if from the proposition that falls under the concept it follows universally, whatever may be, that every object to which stands in the relation to falls under the concept , then falls under the concept , whatever concept may be”

is to mean the same as

“ follows in the -series after “

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

Let’s write “ follows in the -series after ” as . Then I read Frege’s definition as:

iff

Frege’s definition appears to be a characterisation of the transitive closure of , that is the smallest transitive relation containing . 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 ( in the code) indeed (i) contains , (ii) is transitive and (iii) is contained in any other transitive relation containing .

I hope you enjoy.

(* 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 : A → A → Prop.

Definition FregeFollows (x : A) (y : A) :=

∀ (F : A → Prop),

(∀ (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.

Proof.

unfold inclusion.

intros x y.

unfold FregeFollows.

intros H F.

intros H1.

destruct H1. (* we only need base case *)

apply (H0 y).

auto.

Qed.

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

Theorem IsTransitive : transitive A FregeFollows.

Proof.

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.

split.

2: assumption.

intros a.

intros H3.

specialize (H2 y).

specialize (H2 G).

specialize (H2 a).

specialize (H2 H3).

assumption.

Qed.

(* 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).

Proof.

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.

split.

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).

intros.

apply H0.

1: assumption.

unfold inclusion in H.

specialize (H d e).

apply H.

assumption.

Qed.