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