Logical Variable Ontology

FLOW ALGEBRA
LOGICAL VARIABLE ONTOLOGY
Kireth Semantic Library | Mathematical Entities | Logical Entities
Source: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/logical-entities/logical-variable-ontology-2.html
Version: 1.0 | Locale: en-GB | Status: proposed formalisation; source text not independently verified
Authors: Mark Higgins — Sky (Recursive AI)
Website: https://kirethresearch.org

1. PURPOSE
Represent logical variables as typed symbols whose interpretation depends on a formal language, assignment, scope and logical semantics. Distinguish propositional variables from first-order individual variables, and free from bound occurrences.

2. ENTITY TYPES
LogicalVariable := {id, symbol, variable_kind, sort?, domain?, scope?, binding_status, provenance?}
variable_kind := PROPOSITIONAL | INDIVIDUAL | SORTED | META_VARIABLE
binding_status := FREE | BOUND | CONTEXT_DEPENDENT
Assignment := mapping from variables to appropriate semantic values
Formula := well-formed expression with explicitly specified signature and logic
Quantifier := FORALL | EXISTS
Binder := {quantifier, variable, body, scope}
Interpretation := {domain, symbols, predicates, functions, constants}

3. TYPE CONSTRAINTS
PROPOSITIONAL variable: assignment value in {TRUE,FALSE} under classical two-valued semantics.
INDIVIDUAL variable: assignment value in interpretation domain D, with D nonempty for standard first-order logic.
SORTED variable: assignment value in the declared sort domain.
META_VARIABLE: denotes syntax objects at the metalanguage level; do not conflate with object-language variables.
Variables are symbols; occurrences in formulae carry binding and scope information.

4. FORMAL SEMANTICS
For propositional valuation v: v(p) in {T,F}.
v(NOT phi) = NOT v(phi).
v(phi AND psi) = v(phi) AND v(psi).
v(phi OR psi) = v(phi) OR v(psi).
v(phi IMPLIES psi) = (NOT v(phi)) OR v(psi).
For first-order assignment g: Var -> D.
M,g |= P(x) iff g(x) belongs to the interpretation of unary predicate P.
M,g |= FORALL x phi iff for every d in D, M,g[x:=d] |= phi.
M,g |= EXISTS x phi iff for some d in D, M,g[x:=d] |= phi.
The truth of a closed formula is assignment-independent under standard first-order semantics.

5. FREE AND BOUND VARIABLES
FV(P(x,y)) = {x,y}.
FV(NOT phi) = FV(phi).
FV(phi AND psi) = FV(phi) union FV(psi).
FV(FORALL x phi) = FV(phi) minus {x}.
FV(EXISTS x phi) = FV(phi) minus {x}.
A variable is bound only at occurrences governed by its binder; the same symbol can have both free and bound occurrences in a formula.
Alpha-equivalence permits consistent renaming of bound variables provided variable capture is avoided.

6. TYPED RELATIONSHIPS
LogicalVariable --OCCURS_IN--> Formula
LogicalVariable --HAS_SORT--> Sort
LogicalVariable --RANGES_OVER--> Domain
LogicalVariable --ASSIGNED_BY--> Assignment
Quantifier --BINDS_OCCURRENCE_OF--> LogicalVariable
Formula --HAS_FREE_VARIABLE--> LogicalVariable
Interpretation --SUPPLIES_DOMAIN_FOR--> LogicalVariable
Substitution --REPLACES_FREE_OCCURRENCES_OF--> LogicalVariable

7. EXECUTABLE INFERENCE FLOWS (PSEUDOCODE)
flow ValidateVariable(v, signature, logic):
  require unique(v.id) and valid_identifier(v.symbol)
  require v.variable_kind in permitted_kinds(logic)
  if v.variable_kind == SORTED: require sort_declared(v.sort, signature)
  return VALID or diagnostics

flow FreeVariables(ast):
  match ast:
    Atom(args) -> union of variable symbols in args
    Not(phi) -> FreeVariables(phi)
    Binary(phi,psi) -> FreeVariables(phi) union FreeVariables(psi)
    Quantified(q,x,phi) -> FreeVariables(phi) minus {x}
  return set

flow EvaluateQuantifier(q,x,phi,M,g):
  require finite(M.domain) for direct enumeration
  if q == FORALL: return all(Evaluate(phi,M,g[x:=d]) for d in M.domain)
  if q == EXISTS: return any(Evaluate(phi,M,g[x:=d]) for d in M.domain)
  otherwise return UNSUPPORTED

flow CaptureAvoidingSubstitute(phi,x,t):
  require term_well_typed(t)
  rename conflicting bound variables before substitution
  replace free occurrences of x with t
  return resulting_formula

8. INFERENCE RULES AND GUARDED CLAIMS
If x not in FV(phi), then FORALL x phi is equivalent to phi in standard first-order semantics with a nonempty domain.
If x not in FV(phi), then EXISTS x phi is equivalent to phi in standard first-order semantics with a nonempty domain.
If two formulae differ only by capture-free renaming of bound variables, they are alpha-equivalent.
A free variable must be resolved by assignment or binding before evaluating an open formula as a closed proposition.
Never infer independence, causality, or universal validity merely from variable naming.

9. SEMANTIC EQUIVALENCE AND DISTINCTIONS
propositional variable != individual variable
variable symbol != variable occurrence
free occurrence != bound occurrence
assignment != interpretation
logical variable != statistical random variable
logical variable != programming-language mutable storage
alpha-equivalence != arbitrary textual substitution

10. VALIDATION
Check symbol identity and namespace; declared sort and domain; AST well-formedness; quantifier scope; free-variable extraction; capture-avoiding substitution; assignment completeness; semantic type correctness; logic-system assumptions; and reproducibility of evaluations.
Example: FV(FORALL x (P(x,y) AND Q(z))) = {y,z}.
Example: FORALL x P(x) and FORALL y P(y) are alpha-equivalent when renaming is capture-free.

11. CONFIDENCE AND PROVENANCE
CONFIDENCE: high for standard classical propositional and first-order definitions; context-dependent for alternative logics.
PROVENANCE: canonical source URL above; mathematical definitions proposed independently, not a verbatim transcription.
SEMANTIC_EQUIVALENCE: permit only when signature, types, binder scopes and logical system agree.

12. FLOW HASH AND UPDATE MODEL
FLOW_HASH: compute SHA-256 over canonical UTF-8 serialisation of ontology content excluding the FLOW_HASH field itself; no hash is claimed until calculated by a consuming system.
UPDATE_MODEL: version changes must record changes to entity types, signatures, inference semantics, validation rules and provenance; invalidate dependent inferences when assumptions change.

13. AI CONSUMPTION
Parse typed entities and ASTs; resolve binding and scope; validate assignments; perform capture-avoiding substitutions; execute guarded inference rules; attach provenance and confidence; preserve distinction between object-language and metalanguage variables; reject ambiguous or ill-typed inferences.

END FLOW ALGEBRA