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

Published by George Constantinides

View all posts by George Constantinides

Published March 26, 2023

Share this:

Like this:

Related

Published by George Constantinides

Leave a Reply Cancel reply