CONCEPT DOMAIN - Predication Substrate
| Description | Pattern Domain The Predication Substrate defines the compositional system of Element, Class of Element, and local predicates (Linkage) from which SysFEAT's ontological structures are grown. It provides the internal structure of predication - classification, specialization, powertyping, and Compositionality - as a single, universe-stratified, mechanically verified engine that every higher layer inherits. Unlike predicate logic (where a predicate is not a term) and graph theory (where an edge is not a node), a Linkage is simultaneously the mechanism of relating an Element that can be classified, specialized, and related to other entities. This self-applicability is what allows the framework to provide a theory of Relation - not just relations, but the ability to classify relations, specialize them, and compose them, using the same machinery that applies to the Entitys they relate. |
|---|---|
| External references |
 OMG - KerML - Root
 SysFEAT-TheoraticalFoundations-LocalityPrinciple.pdf
Wikipedia - Upper ontology
|
| Dictionary | 
SysFEAT Upper Ontology |
| Parent Domain | 
Upper Ontology |
DOMAIN CONCEPT GRAPH
CONCEPT DESCRIPTIONS
ABSTRACT CONCRETE
| Concept | Description |
|---|---|
Class of Element |
A Class of Element is an Element whose inhabitants are themselves Elements: a type one universe level above its members. Formally, ClassOfElement u = Element (lsuc u), so a class at level u is a type whose instances are Element u things. This universe gap is what separates a class from its members and prevents the self-reference paradoxes of naive set theory - while still allowing, through cross-level reasoning (metaInstanceOf), the class of all classes to be an instance of itself. A Class of Element is the Predication Substrate's answer to the question "what is a category of things?" - not a predicate that returns true or false, but a type that collects its instances as inhabitants.
|
Element |
Element is the most primitive concept in the Predication Substrate: anything that can be the subject or object of predication. Formally, Element u = Set u - a type at universe level u. An Element makes no ontological commitment: it is neither an Entity nor a Relation, neither concrete nor abstract. It is simply something that can be talked about - classified, linked, composed. Every concept in SysFEAT is an Element at some universe level; what distinguishes concepts is the level at which they live and the Linkages they participate in.
|
|
Linkage |
Linkage is the structural primitive of predication: a fibered, proof-relevant, compositional local predicate between a source Element and a target Element. A Linkage from S to T assigns to each source s : S a local type of evidence (localType s) and a projection (ref) that determines the target from the evidence. The reconstructed predicate s =[ L ]= t is then a dependent pair: a witness e : localType s together with a proof that ref e ≡ t. Linkage is simultaneously a generalized graph edge (with source, target, and composable edge data), a proof-relevant predicate (where two different edges between the same endpoints are distinguished), and an Element at a higher universe level (meaning it can itself be classified, specialized, and linked). This triple nature — edge, predicate, entity — is what resolves the polysemy that traditional frameworks impose between things-that-are and things-that-connect.
|
|
Mixed-Order Element |
An Mixed-Order Element is an Element that can belong to multiple metamodeling order (mixed universes in Agda). Example: |
|
Ordered Element |
An Ordered Element is an Element that can belong to only to a single metamodeling order (fixed universe in Agda). Example: |
LOGICAL FORMULATION
AGDA RDF