David Corfield ontology

Idea

Application: PhACT

• Define their problem with multiple formal criteria (of the kind that could in principle be encoded in a proof assistant such as Lean 4), likely in addition to informal criteria

• Mention related past work and identify on which criteria they fall short

• Differentiate the problem from the normal course of their research going forward were it not for ARIA, and explain why

• Identify and contrast two or three potential approaches to the problem

Answers

• Integrate philosophical reflection on ontology into a category-theoretic framework. Philosophy as providing store house, both system-building and cautions. Many cautions come from inadequacy of FOL. Dependent type theory as addressing cautions of Brandom that much inference is material. Bede on ‘and’. Patterson on cautions of Cartwright about Dappled World. Process ontology.

• Fall short: systems too reliant on FOL – cautions too limited by FOL. Analytic philosophy’s limitation to first-order logic.

• Direct: DOLCE as engaging with philosophy.

• ARIA enabling: Unable to develop, PhACT. If we find a good language this will allow dramatic increase in communication. Collaboration with other researchers. Expertise in setting the background. Useful role in connecting bodies of ideas.

• Experience with many aspects of CT, machine learning, Bayesian inference, causality.

Suitability

Pitch myself as uniquely placed:

1. Access to philosophy, Cartwright Dappled World, Dupre Promiscuous realism and Process, neat FOL, and opponents.

2. Know category theory from 1990s. Category Cafe, gauge theory, but proto-applied category theory.

3. Know dependent type theory: with modalities. Modal HoTT book

To combine the work by category-theoretic and type-theoretic approaches to ontology (Patterson, Spivak, etc.) with the linguistic and philosophically informed formal ontology (DOLCE).

Decades of good philosophy to mine, often limited through formalism chosen.

I’ve been held back by need to appeal to philosophical referees.

Provide a bridge to import further philosophical insight.

Graded monads ‘Type structure is a syntactic discipline for enforcing levels of abstraction.’ – J. C. Reynolds

Details

“That it should be possible to identify particulars of a given type seems a necessary condition of the inclusion of that type in our ontology.” (P. F. Strawson, Individuals, 1959, p. 16)

“we are in the dark about the nature of philosophical problems and methods if we are in the dark about types and categories.” (Ryle 1938, 189)

Ulrik Buchholtz, Higher Structures in Homotopy Type Theory,

Quine’s

1. To be is to be the value of a variable, and
2. No entity without identity. Quine, W.V.O.: Ontological relativity and other essays. Columbia University Press (1969)

Become

1. To be is to be an element of a type
2. No type without an identity type.

“to be is to be an element of a type”:

DOLCE

DOLCE (Descriptive Ontology for Linguistic and Cognitive Engineering) set of basic classes: Prop, Thing, PT, AB, R, TR, T, PR, …, STV, ST, PRO, 2308.01597

What if there were systems in refinement relations to each other? So Montague is very coarse.

Carried out in first-order logic.

Basic Formal Ontology, BFO, Arp.

Lai et al.

dependent type theory is sufficiently expressive to represent constructs from OWL, RDFS and RIF as well. Future work will reproduce these constructs for carrying out more sophisticated reasoning on DTKGs.

References

• Zhangsheng Lai, Aik Beng Ng, Liang Ze Wong, Simon See, Shaowei Lin, Dependently Typed Knowledge Graphs (arXiv:2003.03785)

• Nicholas Harley, Abstract Representation of Music: A Type-Based Knowledge Representation Framework, §8.3 describes the Dependent Type Ontology

• Patrick Barlatier, Richard Dapoigny, A Type-Theoretical Approach for Ontologies: the Case of Roles, Applied Ontology 20 (2012) 1–31. (K-DTT)

• Richard Dapoigny, Patrick Barlatier, Formal foundations for situation awareness based on dependent type theory, 2013, Information Fusion 14(1), 87-107

• Richard Dapoigny and Patrick Barlatier. Formalizing context for domain ontologies in coq. In Context in computing, pages 437–454. Springer, 2014.

• Richard Dapoigny and Patrick Barlatier. Towards ontological correctness of part-whole relations with dependent types. In FOIS, volume 2010, pages 45–58, 2010.

• Consensus-Free Spreadsheet Integration, https://arxiv.org/pdf/2209.14457

• Pérez, Marco A., Spivak, David I. ,Toward formalizing ologs: Linguistic structures, instantiations, and mappings

• R. E. Kent and D. I. Spivak, Ologs: A categorical framework for knowledge representation

• Evan Patterson, Knowledge Representation in Bicategories of Relations, https://arxiv.org/abs/1706.00526

• Michael Lambert, Evan Patterson Representing Knowledge and Querying Data using Double-Functorial Semantics, https://arxiv.org/abs/2403.19884

• Angeline Aguinaldo, Evan Patterson, James Fairbanks, William Regli, Jaime Ruiz, A Categorical Representation Language and Computational System for Knowledge-Based Planning, https://arxiv.org/abs/2305.17208

• Spencer Breiner Sarala Padi Eswaran Subrahmanian RamD. Sriram, Deconstructing UML, Part 1: Modeling Classes with Categories, https://nvlpubs.nist.gov/nistpubs/ir/2021/NIST.IR.8358.pdf

• Alexey Potapov, Vitaly Bogdanov, Univalent foundations of AGI are (not) all you nee