Quantifier Ontology

FLOW ALGEBRA
TITLE: Quantifier Ontology
DOMAIN: Discrete Mathematics / Logic / Predicate Logic
SOURCE_URL: https://kirethresearch.org/booksai-core/discrete-mathematics-ontologies/logic/quantifier-ontology-2.html
VERSION: 1.0
LANGUAGE: en-GB
AUTHORS: Mark Higgins — Sky (Recursive AI)
PROJECT: Kireth Semantic Library

1. ONTOLOGY PURPOSE
Represent universal and existential quantification, their scope, variable binding, semantic evaluation, and sound inference in first-order logic.

2. TYPED ENTITIES
Sort := nonempty domain type
Domain[D:Sort] := nonempty collection of individuals
Variable[D] := symbol ranging over D
Term[D] := variable | constant | well-typed function application
Formula := atomic predicate | NOT Formula | AND(Formula,Formula) | OR(Formula,Formula) | IMPLIES(Formula,Formula) | FORALL(Variable,Formula) | EXISTS(Variable,Formula)
Quantifier := Universal | Existential
Assignment := map from free variables to domain elements
Structure := nonempty domain plus interpretations of predicates, functions and constants
BoundVariable := variable occurrence governed by a quantifier
FreeVariable := variable occurrence not governed by a quantifier
Scope := subformula governed by a quantifier
Witness := domain element satisfying an existential formula
Counterexample := domain element falsifying a universal formula

3. CORE FORMAL SEMANTICS
M,s |= FORALL(x,phi) iff for every d in D, M,s[x:=d] |= phi.
M,s |= EXISTS(x,phi) iff some d in D satisfies M,s[x:=d] |= phi.
Free occurrences of x in phi are bound by FORALL(x,phi) or EXISTS(x,phi).
Quantification ranges over the explicitly declared sort/domain of x.
A closed formula (sentence) has no free variables.

4. TRANSFORMATIONS AND EQUIVALENCES
NOT FORALL(x,phi) <=> EXISTS(x,NOT phi).
NOT EXISTS(x,phi) <=> FORALL(x,NOT phi).
FORALL(x,FORALL(y,phi)) <=> FORALL(y,FORALL(x,phi)).
EXISTS(x,EXISTS(y,phi)) <=> EXISTS(y,EXISTS(x,phi)).
FORALL(x,phi AND psi) <=> FORALL(x,phi) AND FORALL(x,psi).
EXISTS(x,phi OR psi) <=> EXISTS(x,phi) OR EXISTS(x,psi).
If x is not free in psi:
  FORALL(x,phi AND psi) <=> FORALL(x,phi) AND psi.
  EXISTS(x,phi OR psi) <=> EXISTS(x,phi) OR psi.
In nonempty domains, if x is not free in phi:
  FORALL(x,phi) <=> phi; EXISTS(x,phi) <=> phi.
In general, FORALL(x,EXISTS(y,R(x,y))) is NOT equivalent to EXISTS(y,FORALL(x,R(x,y))).

5. INFERENCE RULES
UNIVERSAL_ELIMINATION: FORALL(x,phi) -> phi[t/x], provided t is free for x in phi.
UNIVERSAL_INTRODUCTION: derive phi(x) for an arbitrary x not occurring free in any undischarged assumption -> FORALL(x,phi).
EXISTENTIAL_INTRODUCTION: phi[t/x] -> EXISTS(x,phi), provided substitution is capture-avoiding.
EXISTENTIAL_ELIMINATION: from EXISTS(x,phi), assume phi(c) for a fresh witness c; if psi follows without c in psi or other open assumptions, infer psi.
COUNTEREXAMPLE: if phi(d) is false for some d in D, then FORALL(x,phi) is false.
WITNESS: if phi(d) is true for some d in D, then EXISTS(x,phi) is true.

6. OPERATIONS
PARSE_QUANTIFIER(formula) -> quantifier, bound_variable, scope.
FREE_VARIABLES(formula) -> Set[Variable].
BOUND_VARIABLES(formula) -> Set[Variable].
ALPHA_RENAME(formula,old,new) -> logically equivalent formula with safe bound-variable renaming.
SUBSTITUTE(formula,x,term) -> capture-avoiding substitution.
EVALUATE(formula,structure,assignment) -> Boolean when interpretations are fully specified.
NORMALISE_NEGATION(formula) -> formula with quantifier negations pushed inward.
FIND_WITNESS(EXISTS(x,phi),model) -> witness | unknown.
FIND_COUNTEREXAMPLE(FORALL(x,phi),model) -> counterexample | unknown.

7. SEMANTIC RELATIONSHIPS
Quantifier --binds--> Variable
Quantifier --has_scope--> Formula
Variable --ranges_over--> Domain
UniversalQuantifier --requires--> AllDomainMembersSatisfy
ExistentialQuantifier --requires--> AtLeastOneDomainMemberSatisfies
ExistentialStatement --may_have--> Witness
UniversalStatement --may_have--> Counterexample
QuantifiedFormula --evaluated_in--> Structure
Formula --has_free_variables--> Set[Variable]

8. VALIDATION CONSTRAINTS
V01: Quantified variables must have declared domains or sorts.
V02: Domain must be nonempty under conventional first-order semantics.
V03: Predicate and function arities/types must match their signatures.
V04: Substitution must avoid variable capture.
V05: Universal introduction must satisfy the arbitrary-variable restriction.
V06: Existential elimination must use a fresh witness with correct discharge restrictions.
V07: Quantifier order must be preserved unless equivalence is proven.
V08: A witness/counterexample must belong to the quantified domain.
V09: An unbounded finite test cannot establish universal truth over an infinite domain.
V10: Do not confuse logical validity with truth in one specific model.

9. EXAMPLES
D={1,2,3}; P(x): x>0.
FORALL(x in D,P(x)) = TRUE.
EXISTS(x in D,x=2) = TRUE; witness=2.
FORALL(x in D,x<3) = FALSE; counterexample=3.
EXISTS(x in D,x>3) = FALSE.
FORALL(x,EXISTS(y,y>x)) is true over integers but false over {1,2,3}.

10. SEMANTIC_EQUIVALENCE
FORALL(x,phi) ~= "for every x, phi" (with explicit domain and scope).
EXISTS(x,phi) ~= "there is at least one x such that phi".
"For all" and "each" can be paraphrases under matching scope.
"Some" means at least one in standard existential logic, not necessarily 'some but not all'.
Equivalence is conditional on consistent domain, binding, scope and interpretation.

11. CONFIDENCE
FORMAL_THEOREM: 1.00 when checked against stated first-order semantics and side conditions.
MODEL_EVALUATION: 1.00 when model is complete and evaluation is exact.
NATURAL_LANGUAGE_MAPPING: variable; requires disambiguation of scope and domain.
UNVERIFIED_SOURCE_CONTENT: do not claim exact correspondence with source page without verification.

12. FLOW_HASH
Canonicalise typed declarations, operator definitions, formulas, side conditions and ordered sections as UTF-8 NFC with LF line endings; compute SHA-256 over canonical bytes. Populate FLOW_HASH only after final file freeze; do not fabricate a digest.
FLOW_HASH: PENDING_CANONICAL_HASH

13. UPDATE_MODEL
On update: increment version; record date, author, changed rules, affected dependencies, proof checks and new canonical hash. Reject updates violating V01-V10.

14. AI_CONSUMPTION
READ -> TYPE_CHECK -> RESOLVE_SCOPE -> NORMALISE -> APPLY_RULES -> VERIFY_SIDE_CONDITIONS -> EVALUATE_OR_PROVE -> EMIT_RESULT.
Output: formula, interpretation, domain, proof or countermodel, assumptions, confidence and provenance.
Never present finite sampling as a general proof. Mark missing domain/model details as unresolved.

15. PROVENANCE
Based on standard first-order predicate logic. This file is an independently authored formalisation, not a verified transcription of the linked webpage.