The framework of Porphyry’s Isagoge may be summarized as follows:

Kinds are genera and species. Kinds may be within kinds, in which case the broader kind is relatively called a genus, and the narrower kind is relatively called a species. But there are ultimate genera (genus generalissimum) which are not species of any genera, and there are ultimate species (species specialissima) which are not genera of any species. There may be a single ultimate genus, as for Plato, for whom the ultimate genus is Being. There may alternatively be more than one, as for Aristotle, for whom there are ten ultimate genera (the categories). If someone is a haecceitist, they will believe that an ultimate species will always have a single member, but not otherwise. Kinds are defined by predicates called differences, which the theorist believes to jointly exhaust reality (in the case of ultimate genera) or a given genus (in the case of coordinate genera subordinate to that genus), but it is not required that these predicates be logically guaranteed to be jointly exhaustive, as happens in the Porphyrean tree, where the differences that constitute coordinate genera are predicates which are negations of each other, such as “mortal” and “immortal”, “living” and “nonliving”, etc. A predicate which is not a difference, if it is only present within a kind, is called an inseparable accident with respect to that kind; a predicate which is not a difference, if it is coextensive with a kind, is called a proper accident or property (proprium) with respect to that kind; a predicate which is not a difference, if it is neither inseparable nor proper to a kind, it is called simply an accident with respect to that kind.

Axiomatize a modern version of this for use as a formal tool in theorizing.

A modern axiomatization of Porphyry’s framework

Below is a compact, modular axiomatization you can drop into first-order logic with sorts. It keeps Porphyry’s spirit but is clean enough to mechanize (e.g., in Coq/Lean as sets of individuals) and to extend for different metaphysical “packages” (Platonist, Aristotelian, haecceitist, Porphyrean tree, etc.).

0) Signature (three-sorted FOL)

Sorts
- ι (individuals)
- κ (kinds)
- π (unary predicates/properties on individuals)
Primitive symbols
- E(x:ι, K:κ) : “x instantiates K” (write $x \in K$)
- Sub(K:κ, L:κ) : “K is a subkind of L” (write $K \le L$)
- Ext(P:π, x:ι) : predicate truth (write $P(x)$)
- Diff(P:π, G:κ) : “P is a difference at genus G”
- ∩ : κ×κ → κ : kind intersection
Defined/abbrev
- $K < L :!!\iff K \le L \land \lnot(L \le K)$ (proper subkind)
- $x \in K\cap L :!!\iff x \in K \land x \in L$
- Extensional equality of kinds: $K=L :!!\iff \forall x,(x\in K \leftrightarrow x\in L)$
- Immediate subkind: $\mathrm{Imm}(S,G) :!!\iff S<G \land \lnot\exists M,(S<M<G)$

1) Core axioms (kind lattice + differences + accidents)

A1 (Kind extensionality). $\forall K,L.\ [(\forall x.\ x\in K \leftrightarrow x\in L) \rightarrow K=L]$.

A2 (Order is inclusion). $\forall K,L.\ [K\le L \leftrightarrow \forall x.\ (x\in K \rightarrow x\in L)]$.

A3 (Closure under intersection). $\forall K,L.\ \forall x.\ x\in (K\cap L) \leftrightarrow (x\in K \land x\in L)$.

A4 (Ultimate genera/species—purely relative notions).

Ultimate genus: $\mathrm{UG}(G) :!!\iff \lnot\exists H.\ G<H$.
Ultimate species: $\mathrm{US}(S) :!!\iff (\exists x.\ x\in S)\ \land\ \lnot\exists T.\ [(\exists x.\ x\in T)\ \land\ T<S]$.

A5 (Genus/species are relative terms).

$\mathrm{GenusOf}(G,S) :!!\iff S<G$.
$\mathrm{SpeciesOf}(S,G) :!!\iff S<G$.

A6 (Differences carve subkinds nontrivially). $\forall P,G.\ \mathrm{Diff}(P,G) \rightarrow$ (i) $\exists x.\ x\in G \land P(x)$ and $\exists y.\ y\in G \land \lnot P(y)$ (nontrivial on $G$); (ii) $\exists S.\ [\forall x.\ x\in S \leftrightarrow (x\in G \land P(x))]\ \land\ S<G$. (Write $S = G{\restriction}P$ for that unique $S$ by A1.)

A7 (Coordinate subkinds from complementary differences—local Porphyry). If $\mathrm{Diff}(P,G)$ and $\mathrm{Diff}(Q,G)$ and $\forall x,(x\in G \rightarrow (P(x)\leftrightarrow \lnot Q(x)))$, then (i) $\mathrm{Imm}(G{\restriction}P,\ G)$ and $\mathrm{Imm}(G{\restriction}Q,\ G)$; (ii) $\forall x.\ x\in G \leftrightarrow (x\in G{\restriction}P \lor x\in G{\restriction}Q)$; (iii) $\forall x.\ \lnot(x\in G{\restriction}P \land x\in G{\restriction}Q)$.

Intuition: complementary differences within a genus produce coordinate species that are disjoint and jointly cover that genus.

A8 (Accident taxonomy relative to a kind). For any property $P$ and kind $K$:

Proper accident (proprium): $\mathrm{PropAcc}(P,K) :!!\iff [\forall x.\ (x\in K \leftrightarrow P(x))] \land \lnot\mathrm{Diff}(P,K)$.
Inseparable accident (of K): $\mathrm{InsepAcc}(P,K) :!!\iff [\forall x.\ P(x) \rightarrow x\in K]\ \land\ \lnot\mathrm{PropAcc}(P,K)\ \land\ \lnot\mathrm{Diff}(P,K)$.
(Mere) accident (of K): $\mathrm{Acc}(P,K) :!!\iff \lnot\mathrm{Diff}(P,K)\ \land\ \lnot\mathrm{PropAcc}(P,K)\ \land\ \lnot\mathrm{InsepAcc}(P,K)$.

These are definitions (no extra axioms needed).

2) Optional “packages” you can toggle

Pick any combination to match your metaphysics or application.

P-Plat (Platonist top)

Introduce a constant 𝟙:κ and add:

U1: $\forall x.\ x\in \mathbf{1}$ (𝟙 is the universal kind).
U2: $\mathrm{UG}(\mathbf{1})$ and $\forall K.\ K\le \mathbf{1}$.

Effect: single ultimate genus (“Being”). All kinds live under 𝟙.

P-Cat$_n$ (Aristotelian categories, typically $n=10$)

Introduce constants $C_1,\dots,C_n:κ$ and add:

C1 (tops): $\forall i.\ \mathrm{UG}(C_i)$.
C2 (cover): $\forall x.\ \bigvee_{i=1}^{n} x\in C_i$.
C3 (pairwise disjoint in extension): $\forall i\neq j.\ \lnot\exists x.\ (x\in C_i \land x\in C_j)$.

Effect: multiple ultimate genera that jointly exhaust reality and do not overlap.

P-Hex (Haecceitism)

H1: $\forall S.\ \mathrm{US}(S) \rightarrow \exists ! x.\ x\in S$.

Effect: ultimate species are singletons. Omit H1 for anti-haecceitist settings.

P-Exh (Exhaustive difference bases)

E1 (local exhaustivity): $\forall G.\ (\exists x.\ x\in G) \rightarrow \forall x.\ x\in G \Rightarrow \exists P.\ \mathrm{Diff}(P,G)\ \land\ P(x)$.

Effect: every member of a genus falls under at least one admissible difference for that genus. Drop E1 if you want open-ended taxonomies.

P-Por (Porphyrean binary tree schema)

B1: $\forall G.\ \exists P.\ \mathrm{Diff}(P,G) \land \mathrm{Diff}(Q_G,G)\ \land\ \forall x\in G.\ [P(x)\leftrightarrow \lnot Q_G(x)]$.
B2 (well-foundedness): No infinite $<$-descending chain of kinds.
B3 (branching minimality): Every non-ultimate genus has exactly two immediate subkinds, both produced by a complementary pair as in A7.

Effect: you recover a Porphyrean tree (binary, exhaustive, disjoint, well-founded).

3) Useful definitions & lemmas (derivable)

Coordinate under $G$: $\mathrm{Coord}(S,T;G) :!!\iff \mathrm{Imm}(S,G)\land \mathrm{Imm}(T,G)\land S\neq T\land \forall x.\ \lnot(x\in S\land x\in T)$.
Genus/Sigma-algebra closure (optional convenience axiom). Add closure under finite unions or set difference by definability (e.g., introduce $K\setminus L$ with the obvious membership axiom) if you want fast proofs about partitions.
Difference-induced species uniqueness. From A1+A6, for each $\mathrm{Diff}(P,G)$ there is a unique $G{\restriction}P$.
Proper accidents behave like definitions. If $\mathrm{PropAcc}(P,K)$, then $P$ is extensionally identical to $K$ but not designated as a difference at $K$ (e.g., being a triangle vs. having interior angles summing to 180° in Euclidean settings).

4) How to use the tool in practice

Model choice. Fix a domain $I$ of individuals. Interpret kinds as subsets of $I$ (so $x\in K$ is ordinary membership). Interpret properties $P\in \pi$ as subsets of $I$ as well (so $P(x)$ is membership). Then take $\le$ as $\subseteq$, and $\cap$ as set intersection. Add whichever package axioms you want.
Designate differences. Choose which predicates count as admissible Diff(·,G) at each genus $G$. This separates “structural” cuts (differences) from background properties (accidents).
Check the accident calculus. Given any predicate $P$ and kind $K$, its status is computed by the definitions in A8 relative to your chosen Diff-base.

5) Tiny worked toy model (just to see it run)

Let $I={\text{Socrates},\ \text{Pegasus}}$. Let $G=\text{Animal}\subseteq I={\text{Socrates},\ \text{Pegasus}}$. Let $P=\text{Mortal}$ with $P(\text{Socrates})$, $\lnot P(\text{Pegasus})$. Declare $\mathrm{Diff}(P,G)$ and $\mathrm{Diff}(Q,G)$ with $Q=\text{Immortal}$ and $Q$ complementary to $P$ on $G$.

Then by A6–A7:

$G{\restriction}P={\text{Socrates}}$ and $G{\restriction}Q={\text{Pegasus}}$ are immediate, disjoint, and jointly cover $G$.
If you add P-Hex, both are ultimate species (singletons).
A predicate like $R=\text{Feathered}$ with $R(\text{Pegasus})$ only and $\lnot R(\text{Socrates})$ is an Accident relative to $G$ unless you declare it as a difference.

6) Why this setup is useful

Modular: flip on/off Platonist vs. Aristotelian tops; Porphyrean binary vs. open-ended refinement; haecceitism vs. plurality in ultimate species.
Mechanical: everything is first-order over three sorts; in proof assistants you can reduce to sets of individuals.
Relativized predicates: proprium / (in)separable accident are relative to a kind, matching Porphyry’s intent.
Pragmatic taxonomy: you can designate which cuts are essential by setting Diff; the rest fall into the accident trichotomy by definition.

If you want, I can provide a Lean or Coq skeleton that instantiates these axioms and shows sample derivations (e.g., “complementary differences yield coordinate species,” “haecceitism ⇒ all ultimate species are singletons,” etc.).

Thiago’s ChatGPT Blog

Friday, September 12, 2025

Modern formal axiomatic Isagoge