Logical Formula Ontology

FLOW ALGEBRA
LOGICAL FORMULA ONTOLOGY
Kireth Semantic Library | Mathematical Entities > Logical Entities
Source: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/logical-entities/logical-formula-ontology.html
Authors: Mark Higgins — Sky (Recursive AI)
Version: 1.0 | Date: 2026-10-14
Status: Proposed mathematical formalisation; source page wording not independently verified.

1. PURPOSE
Represent well-formed logical formulae, their syntax, typing, binding, interpretation, inference and semantic relationships in a machine-consumable ontology. Distinguish syntactic formula identity from semantic equivalence.

2. ENTITY TYPES
LogicalFormula : SyntaxTree
AtomicFormula : LogicalFormula
CompoundFormula : LogicalFormula
Term : SyntaxTree
Variable : Term
Constant : Term
FunctionApplication : Term
PredicateSymbol : Symbol[arity:n]
Connective : {NOT, AND, OR, IMPLIES, IFF}
Quantifier : {FORALL, EXISTS}
Interpretation : (Domain, SymbolAssignments)
VariableAssignment : Variable -> DomainElement
TruthValue : {TRUE, FALSE}
Proof : Sequence[Judgement]

3. TYPED CONSTRUCTORS
atom(P:PredicateSymbol[n], args:Term[n]) -> AtomicFormula
not(phi:LogicalFormula) -> LogicalFormula
and(phi:LogicalFormula, psi:LogicalFormula) -> LogicalFormula
or(phi:LogicalFormula, psi:LogicalFormula) -> LogicalFormula
implies(phi:LogicalFormula, psi:LogicalFormula) -> LogicalFormula
iff(phi:LogicalFormula, psi:LogicalFormula) -> LogicalFormula
forall(x:Variable, phi:LogicalFormula) -> LogicalFormula
exists(x:Variable, phi:LogicalFormula) -> LogicalFormula

4. FORMATION RULES
F1: If P has arity n and t1,...,tn are well-typed terms, P(t1,...,tn) is a formula.
F2: If phi is a formula, NOT(phi) is a formula.
F3: If phi and psi are formulae, (phi AND psi), (phi OR psi), (phi -> psi), (phi <-> psi) are formulae.
F4: If phi is a formula and x is a variable, FORALL x.phi and EXISTS x.phi are formulae.
F5: Nothing else is a well-formed formula unless admitted by an explicitly declared logic extension.

5. SEMANTICS (CLASSICAL FIRST-ORDER LOGIC)
Evaluate(I,g, P(t1,...,tn)) = TRUE iff (value(I,g,t1),...,value(I,g,tn)) belongs to I(P).
Evaluate(I,g, NOT phi) = not Evaluate(I,g,phi).
Evaluate(I,g, phi AND psi) = Evaluate(I,g,phi) and Evaluate(I,g,psi).
Evaluate(I,g, phi OR psi) = Evaluate(I,g,phi) or Evaluate(I,g,psi).
Evaluate(I,g, phi -> psi) = (not Evaluate(I,g,phi)) or Evaluate(I,g,psi).
Evaluate(I,g, phi <-> psi) = (Evaluate(I,g,phi) = Evaluate(I,g,psi)).
Evaluate(I,g, FORALL x.phi) = TRUE iff for every d in Domain(I), Evaluate(I,g[x:=d],phi)=TRUE.
Evaluate(I,g, EXISTS x.phi) = TRUE iff some d in Domain(I) satisfies Evaluate(I,g[x:=d],phi)=TRUE.
Assume nonempty domains in standard first-order semantics.

6. VARIABLE BINDING AND SUBSTITUTION
freeVars(P(t1,...,tn)) = union of free variables in its terms.
freeVars(NOT phi) = freeVars(phi).
freeVars(phi OP psi) = freeVars(phi) union freeVars(psi) for binary OP.
freeVars(Q x.phi) = freeVars(phi) minus {x}, for Q in {FORALL, EXISTS}.
Sentence(phi) iff freeVars(phi) is empty.
Substitute(phi,x,t) must avoid variable capture; alpha-rename bound variables as necessary.
Alpha-equivalent formulae differ only by consistent renaming of bound variables.

7. SEMANTIC RELATIONSHIPS
HAS_SUBFORMULA(LogicalFormula,LogicalFormula)
USES_PREDICATE(LogicalFormula,PredicateSymbol)
HAS_FREE_VARIABLE(LogicalFormula,Variable)
BINDS_VARIABLE(QuantifiedFormula,Variable)
HAS_OPERATOR(CompoundFormula,Connective)
IS_SATISFIED_BY(LogicalFormula,Interpretation)
LOGICALLY_ENTAILS(Set[LogicalFormula],LogicalFormula)
LOGICALLY_EQUIVALENT(LogicalFormula,LogicalFormula)
ALPHA_EQUIVALENT(LogicalFormula,LogicalFormula)
IS_NEGATION_OF(LogicalFormula,LogicalFormula)

8. INFERENCE FLOWS
flow ParseAndTypeCheck(source):
  tokens := lexical_parse(source)
  ast := parse_formula(tokens)
  require arity_consistent(ast) and terms_well_typed(ast)
  return ast

flow EvaluateFormula(phi,I,g):
  require well_formed(phi)
  return Evaluate(I,g,phi)

flow InferModusPonens(premises):
  if contains(premises,phi) and contains(premises,implies(phi,psi)):
    derive(psi, rule="modus_ponens")

flow QuantifierNegation(phi):
  rewrite NOT(FORALL x.phi) <=> EXISTS x.NOT(phi)
  rewrite NOT(EXISTS x.phi) <=> FORALL x.NOT(phi)

flow VerifyEquivalence(phi,psi):
  require same_signature(phi,psi)
  return valid(IFF(phi,psi))  # validity requires a sound decision/proof method;
                              # unrestricted first-order validity is undecidable.

9. AXIOMS / INVARIANTS
A1: Well-formedness is decidable for a fixed effective grammar and signature.
A2: A formula may have free variables; a sentence has none.
A3: Syntactic equality implies semantic equivalence, but not conversely.
A4: Alpha-equivalence preserves truth under corresponding assignments.
A5: Sound inference preserves semantic entailment.
A6: Contradictory formulae cannot both be true under the same interpretation and assignment in classical logic.
A7: Formula satisfiability and validity depend on the selected logic and interpretation class.

10. SEMANTIC DISTINCTIONS
Formula != Proposition: an open formula may depend on variable assignment.
Formula != Term: terms denote objects; formulae evaluate to truth values.
Syntactic equivalence != Logical equivalence.
Satisfiable != Valid: satisfiable means true in at least one model; valid means true in all models.
Entailment (semantic) != Derivability (proof-theoretic), except under applicable soundness/completeness assumptions.
First-order logic != Propositional logic: first-order logic adds quantifiers, terms and interpretations.

11. VALIDATION
CHECK grammar and symbol arities.
CHECK sort/type constraints for terms and predicate arguments.
CHECK lexical scope and capture-avoiding substitution.
CHECK provenance of every inference rule.
CHECK classical versus nonclassical semantic regime is declared.
CHECK any equivalence assertion has proof or appropriately scoped model-checking evidence.
CHECK undecidable tasks are not falsely labelled universally decidable.

12. CONFIDENCE / PROVENANCE
CONFIDENCE: 0.98 for standard definitions under classical first-order semantics; 0.70 for mapping to the linked page without verified page text.
PROVENANCE: Kireth Semantic Library target URL; standard mathematical logic formalisation.
SEMANTIC_EQUIVALENCE: Only assert with explicit logic, signature and supporting derivation/model semantics.

13. FLOW_HASH / UPDATE_MODEL
FLOW_HASH: SHA-256(canonical_utf8(normalise(ontology_id,version,axioms,types,rules,relations)))
FLOW_HASH_VALUE: Compute at ingestion; not precomputed in this document.
UPDATE_MODEL: versioned; invalidate dependent proofs and embeddings when grammar, typing, axioms or semantics change.

14. AI_CONSUMPTION
Input: typed formula AST, signature, logic profile, interpretation or premises.
Output: parsed formula, free/bound variables, semantic evaluation or derived conclusions with provenance.
Never infer truth from grammatical well-formedness alone.
Keep proof status separate from conjecture and model-specific evaluation.
Emit uncertainty and unresolved proof obligations explicitly.

END FLOW ALGEBRA