Jos De Roo

Higher-order look, first-order heart

Intuition

• Intension = the named property/relation (e.g., a URI like ex:likes).
• Extension = the set of tuples that satisfy it.
• The Hayes–Menzel move: treat relation names as ordinary first-order objects, and mediate application with fixed first-order predicates Holdsₙ (and Appₙ for function application). This yields a truth-preserving translation of the higher-order-looking syntax into orthodox FOL.
• On the Web this fits naturally: URIs are logical constants (intensions); property extensions are given by an interpretation map IEXT from property-resources to sets of pairs (their extensions). (W3C)

---

Signature (pure FOL)

For each arity n ≥ 1, add a predicate:

• Holdsₙ(r, x₁, …, xₙ) (“the relation named by r holds of those args”). Everything you “apply” (predicates, classes, properties) is just a term naming an intension; Holdsₙ links that name to its extension.

Optional but common:

• ExtEqₙ(r, s) := ∀x₁…xₙ( Holdsₙ(r,x₁,…,xₙ) ↔ Holdsₙ(s,x₁,…,xₙ) ) for extensional equality (distinct from intensional identity r = s). This intension/extension separation is emphasized by Menzel. (jfsowa.com)

---

Translation schema (HO → FO)

• Predicate application P(t₁,…,tₙ) ↦ Holdsₙ(P, T(t₁), …, T(tₙ)).
• Quantification over predicates ∀P φ ↦ ∀p T(φ) (now p ranges over objects naming relations).
• Predicate equality intensional P = Q stays p = q; extensional equality becomes ExtEqₙ(p,q). (jfsowa.com)

A concise third-party summary of the same “Holdsₙ” trick appears in Horrocks et al., describing Hayes–Menzel’s translation explicitly.

---

Micro-examples

CLIF-style

;; r is a first-order variable ranging over relation-names (intensions)
(def Reflexive (r) (forall (x) (Holds2 r x x)))

;; extensional vs intensional equality
(forall (x y) (iff (Holds2 likes x y) (Holds2 admires x y)))   ; ExtEq2(likes,admires)
(= likes admires)                                              ; intensional identity (different claim)

RDF intuition → FOL core

RDF triple

ex:Alice ex:likes ex:Bob .

reads as

Holds2(likes, Alice, Bob)

since URIs are constants and property extensions are given by IEXT. (W3C)

---

What you can do (cleanly) in FOL

• Quantify over “predicates” (really: over names of predicates).
• Define meta-properties (reflexive, transitive, functional, …) using only Holdsₙ.
• Keep Web-style naming (URIs/IRIs) first-class while retaining a first-order model theory (as in Common Logic).

---

Pitfalls & notes

• You need one Holdsₙ per arity you use (a schema; any given theory uses finitely many).
• Row/sequence variables (variably-polyadic tricks) do push you beyond FOL; the FO story here is the Holdsₙ part.
• Comprehension/λ (creating new relation-names from formulas) isn’t automatic in FOL; CL handles this conservatively while including full FOL with equality and supporting IRIs as names for open networks.

---

TL;DR

Name relations (URIs/IRIs) = talk about intensions as first-order objects; use Holdsₙ to tie them to extensions. Then your “higher-order” quantification is just FOL.

---

References (handy pointers)

• Hayes & Menzel (2001), “A Semantics for the Knowledge Interchange Format (SKIF)” — proves that quantification over relations is possible in FOL and gives the explicit Holdsₙ/Appₙ translation. See “Mapping SKIF into conventional logic.”
• Menzel (2011), “Knowledge representation, the Web, and the evolution of logic,” Synthese — explains the type-free, name-centric approach; separates denotation vs relation-extension (e.g., rext('Married')) and motivates the Web’s reliance on URIs as names. (jfsowa.com)
• W3C RDF Semantics (2004) — treats URI references as logical constants and models properties as first-class objects with extensions via IEXT (the intension/extension split for Web vocabularies). (W3C)
• ISO/IEC 24707:2018 — Common Logic — includes full FOL with equality, permits Web-friendly naming (IRIs as names), and supports open networks, while allowing “higher-order-looking” surface features without abandoning a first-order model theory.
• Horrocks et al., “Three Theses of Representation in the Semantic Web” (2003) — independent summary of the Hayes–Menzel Holdsₙ translation (how HO-looking syntax is embedded in FOL).