Predicate Ontology

FLOW ALGEBRA
PREDICATE ONTOLOGY
Kireth Semantic Library — Mathematical Entities / Logical Entities
Version: 1.0
Authors: Mark Higgins — Sky (Recursive AI)
Source: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/logical-entities/predicate-ontology-2.html
Status: Proposed formalisation; source page wording not independently verified.

1. PURPOSE
Represent predicates as typed expressions whose interpretation yields truth values under variable assignments and logical structures. Preserve distinctions among predicates, propositions, relations, functions and quantified formulae.

2. ENTITY TYPES
Predicate: symbol or formula with zero or more typed argument positions.
PredicateSymbol: identifier P with arity n and signature D1 × ... × Dn → Bool.
Argument: term occupying a typed position in a predicate application.
Term: variable, constant or function application.
Variable: typed placeholder evaluated under an assignment.
Domain: set of permissible values for a variable or argument.
Interpretation: mapping of predicate symbols to relations over their domains.
Structure: domains and interpretations for non-logical symbols.
Assignment: mapping of free variables to domain elements.
AtomicFormula: P(t1,...,tn).
Formula: atomic formula or expression built with connectives and quantifiers.
Quantifier: universal ∀ or existential ∃ binding a variable.
TruthValue: true or false in classical two-valued semantics.
Relation: subset of D1 × ... × Dn corresponding to the extension of an n-ary predicate.

3. TYPE SIGNATURES
predicate(P, n, [D1,...,Dn]) : Predicate
apply(P, [t1,...,tn]) : AtomicFormula
interpret(M, P) : Relation
assign(g, x) : Element
satisfies(M, g, φ) : Bool
free_variables(φ) : Set[Variable]
substitute(φ, x, t) : Formula
quantify(Q, x, φ) : Formula

4. CORE SEMANTICS
Let M be a structure, g an assignment and P a predicate of arity n.
M,g ⊨ P(t1,...,tn) iff (⟦t1⟧M,g,...,⟦tn⟧M,g) ∈ P^M.
M,g ⊨ ¬φ iff not(M,g ⊨ φ).
M,g ⊨ (φ ∧ ψ) iff (M,g ⊨ φ) and (M,g ⊨ ψ).
M,g ⊨ (φ ∨ ψ) iff (M,g ⊨ φ) or (M,g ⊨ ψ).
M,g ⊨ (φ → ψ) iff not(M,g ⊨ φ) or (M,g ⊨ ψ).
M,g ⊨ ∀x φ iff for every a in domain(x), M,g[x↦a] ⊨ φ.
M,g ⊨ ∃x φ iff some a in domain(x) satisfies M,g[x↦a] ⊨ φ.
A formula with no free variables is a sentence, whose truth in M does not depend on g.

5. AXIOMS AND INVARIANTS
A1: Arity consistency — application of an n-ary predicate has exactly n arguments.
A2: Sort safety — each argument belongs to its declared domain or sort.
A3: Classical bivalence — each fully interpreted formula is true or false under M,g.
A4: Bound-variable renaming (alpha equivalence) preserves meaning when capture is avoided.
A5: Substitution must be capture-avoiding and type-correct.
A6: Predicate extension P^M is a subset of the Cartesian product of argument domains.
A7: Zero-ary predicates behave as propositional constants under an interpretation.
A8: Free variables must be assigned before evaluating an open formula.

6. TYPED RELATIONSHIPS
Predicate --HAS_ARITY--> NaturalNumber
Predicate --HAS_ARGUMENT_SORT--> Domain
Predicate --APPLIED_TO--> Term
Predicate --DENOTES_UNDER_INTERPRETATION--> Relation
AtomicFormula --USES_PREDICATE--> Predicate
Formula --HAS_FREE_VARIABLE--> Variable
Quantifier --BINDS--> Variable
Formula --EVALUATED_IN--> Structure
Formula --EVALUATED_UNDER--> Assignment
Formula --HAS_TRUTH_VALUE--> TruthValue
Predicate --SPECIALISES--> LogicalEntity

7. EXECUTABLE INFERENCE FLOWS (PSEUDOCODE)
flow PredicateTypeCheck(P, args):
  require length(args) == arity(P)
  for i in 1..arity(P): require type(args[i]) compatible_with signature(P)[i]
  return VALID

flow EvaluateAtomic(M, g, P, args):
  require PredicateTypeCheck(P,args) == VALID
  values := [evaluate_term(M,g,t) for t in args]
  return tuple(values) in interpret(M,P)

flow UniversalInstantiation(M, g, x, φ, a):
  require a in domain(x)
  require satisfies(M,g,forall(x,φ))
  infer satisfies(M,g[x:=a],φ)

flow ExistentialWitness(M, g, x, φ, a):
  require a in domain(x)
  require satisfies(M,g[x:=a],φ)
  infer satisfies(M,g,exists(x,φ))

flow CaptureAvoidingSubstitution(φ,x,t):
  require sort(t) compatible_with sort(x)
  alpha_rename_bound_variables_if_needed(φ,t)
  return replace_free_occurrences(φ,x,t)

8. SEMANTIC DISTINCTIONS
Predicate versus proposition: an open predicate expression can depend on variable assignment; a closed proposition/sentence has a truth value in a structure.
Predicate versus function: predicates denote truth-valued conditions or relations; ordinary functions denote values in a codomain.
Predicate versus relation: predicate symbols are syntactic; their interpretations are semantic relations.
Free versus bound variable: free variables depend on assignment; bound variables are scoped by quantifiers.
Validity versus satisfiability: validity means true in every admissible structure; satisfiability means true in at least one structure and assignment.

9. EXAMPLE
Domain: integers. P(x): x > 0.
P(3) = true; P(-2) = false.
∃x P(x) = true; ∀x P(x) = false.
Binary predicate LessThan(x,y): x < y; LessThan(2,5) = true.

10. VALIDATION
Check declared arities and sorts; reject unbound or unassigned free variables during evaluation; enforce quantifier scope and capture avoidance; distinguish syntax from interpretation; record chosen logic (classical first-order by default); ensure proof rules are sound under stated semantics.

11. CONFIDENCE AND PROVENANCE
CONFIDENCE: high for standard classical first-order semantics; source-page alignment unverified.
PROVENANCE: mathematical logic reference knowledge; source URL provided by user.
SEMANTIC_EQUIVALENCE: alpha-renamed quantified formulae equivalent when renaming is capture-free.
SEMANTIC_DIFFERENCE: P(x) is not identical to ∀x P(x) or ∃x P(x).

12. FLOW HASH / UPDATE MODEL
FLOW_HASH: SHA-256 of canonical UTF-8 content excluding the FLOW_HASH value itself; calculate during publication, not prefilled.
UPDATE_MODEL: versioned, append-only change history; recalculate hash after canonical content changes.

13. AI CONSUMPTION
AI_CONSUMPTION:
  representation: typed_first_order_logic
  tasks: [semantic_parsing, knowledge_graph_mapping, theorem_proving, rule_validation, logical_querying]
  safeguards: [arity_check, sort_check, scope_check, interpretation_required, no_unjustified_inference]
  output: [formula, typing, free_variables, truth_under_model, provenance, confidence]

END FLOW ALGEBRA