Existential Quantifier Ontology

FLOW ALGEBRA
EXISTENTIAL QUANTIFIER ONTOLOGY
Kireth Semantic Library | Mathematical Entities / Logical Entities
Source: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/logical-entities/existential-quantifier-ontology-2.html
Version: 1.0 | 2026-10-14 | Locale: en-GB
Authors: Mark Higgins — Sky (Recursive AI)
Status: Proposed mathematical formalisation; source-page wording not independently verified.

1. PURPOSE
Represent existential quantification as a typed, scoped, interpretable logical operation. Preserve the distinction between existence, witness construction, proof of existence and unique existence.

2. TYPED ENTITIES
entity Domain<D> { members: Set<D>; nonempty: Bool? }
entity Variable<D> { name: Identifier; domain: Domain<D> }
entity Predicate<D> { expression: Formula; free_variables: Set<Variable> }
entity ExistentialQuantifier { symbol: "∃"; bound_variable: Variable; body: Formula; scope: Formula }
entity Interpretation { domain: Domain; predicate_meaning: Relation; assignment: Map<Variable,Element> }
entity Witness<D> { value: D; validates: Formula }
entity ExistentialClaim { formula: Formula; truth: Bool?; provenance: Evidence? }
entity Proof { premises: Set<Formula>; conclusion: Formula; rules: Sequence<Rule> }

3. SYNTAX AND SEMANTICS
syntax: if x:D and φ(x) is a formula, then ∃x:D.φ(x) is a formula.
free_variables(∃x.φ) = free_variables(φ) \ {x}.
semantics: M,s ⊨ ∃x:D.φ iff there exists d∈D such that M,s[x↦d] ⊨ φ.
finite_domain: truth(∃x∈{d1,...,dn}.φ(x)) = OR_i truth(φ(di)).
empty_domain: ∃x∈∅.φ(x) is false (standard first-order semantics with explicit restricted domain).

4. CORE EQUIVALENCES (CLASSICAL LOGIC)
¬∃x φ(x) ↔ ∀x ¬φ(x).
∃x φ(x) ↔ ¬∀x ¬φ(x).
∃x(φ(x)∨ψ(x)) ↔ (∃x φ(x))∨(∃x ψ(x)).
∃x(φ(x)∧ψ(x)) ⇒ (∃x φ(x))∧(∃x ψ(x)); converse is not valid generally.
∃x(φ(x)∧Q) ↔ (∃x φ(x))∧Q when x is not free in Q.
∃x(φ(x)∨Q) ↔ (∃x φ(x))∨Q when x is not free in Q AND the domain is nonempty; if the domain may be empty, preserve the nonemptiness guard.
Alpha conversion: ∃x φ(x) ≡α ∃y φ[y/x] when substitution is capture-avoiding and y is fresh.
Quantifier order: ∃x∃y φ ↔ ∃y∃x φ (with matching independent domains); ∀x∃y φ does not generally imply ∃y∀x φ.

5. INFERENCE RULES
EXISTS_INTRO: from φ(t), infer ∃x φ(x), provided t is admissible for x and substitution is capture-avoiding.
EXISTS_ELIM: from ∃x φ(x) and a subproof deriving ψ from φ(c), infer ψ, provided c is fresh and occurs neither in ψ nor in undischarged assumptions outside that subproof.
COUNTEREXAMPLE_TO_UNIVERSAL: from ¬φ(t), infer ¬∀x φ(x) for admissible t.
EXISTENCE_FROM_NONEMPTY: if D is nonempty, infer ∃x:D. True.
Do not infer a specific witness solely from an existential claim without an additional witness-extraction rule or constructive evidence.

6. RELATIONSHIPS
ExistentialQuantifier --BINDS--> Variable
ExistentialQuantifier --SCOPES_OVER--> Formula
Variable --RANGES_OVER--> Domain
Witness --SATISFIES--> Predicate
ExistentialClaim --EVALUATED_UNDER--> Interpretation
ExistentialClaim --DUAL_UNDER_NEGATION--> UniversalQuantifier
Proof --JUSTIFIES--> ExistentialClaim

7. EXECUTABLE FLOW
flow EvaluateExistential(input: Formula, interpretation: M, assignment: s):
  require formula.kind == EXISTS
  let D = resolve_domain(formula.bound_variable, M)
  if D.is_finite_and_enumerable:
    for d in D:
      if evaluate(formula.body, M, s.with(formula.variable,d)) == TRUE:
        return {truth: TRUE, witness: d, confidence: 1.0}
    return {truth: FALSE, witness: NONE, confidence: 1.0}
  else:
    return symbolic_or_solver_check(formula, M, s)
    # Solver UNKNOWN is not FALSE; preserve undecidability and resource limits.

flow ValidateWitness(claim, candidate, M):
  require candidate ∈ domain(claim.bound_variable)
  return evaluate(claim.body, M, assignment(claim.variable,candidate))

8. VALIDATION CONSTRAINTS
- Bound variables must be typed and scoped.
- Substitution must prevent variable capture.
- Domains and interpretation must be declared or explicitly unresolved.
- Truth, satisfiability, provability and constructibility must not be conflated.
- UNKNOWN is distinct from FALSE.
- Unique existence (∃!) requires existence AND uniqueness, not merely ∃.
- An existential statement may be true without a supplied named witness.
- Classical equivalences must be tagged with their logic-system assumptions.

9. SEMANTIC EQUIVALENCE AND DISTINCTIONS
aliases: existential quantifier; exists; there exists; ∃.
not_equivalent_to: universal quantifier (∀); uniqueness quantifier (∃!); possibility modality (◇); probabilistic existence claim.
semantic_equivalence requires compatible domains, interpretations, variable binding and logical assumptions.

10. CONFIDENCE AND PROVENANCE
confidence: 1.0 for formally checked derivations under explicit axioms; otherwise report evidence-based confidence, not arbitrary certainty.
provenance: retain source URL, formalisation version, assumptions, solver identity (if used), verification result and revision timestamp.

11. FLOW_HASH / UPDATE_MODEL
canonicalise: UTF-8 NFC; stable entity identifiers; sorted unordered relationship sets; capture-avoiding alpha-normalisation; preserve quantifier order and scope.
FLOW_HASH = SHA256(canonical_serialisation(ontology_content, version, assumptions)).
UPDATE_MODEL: semantic-version changes; revalidate dependent flows when quantifier semantics, scope, domain assumptions or inference rules change.

12. AI_CONSUMPTION
export: typed entities, logical formula AST, inference-rule IDs, preconditions, truth status, proof/witness references, provenance and FLOW_HASH.
reasoning_policy: require explicit domain and logic; distinguish proof from plausible natural-language explanation; return UNKNOWN when not established.

END FLOW ALGEBRA