Negation Ontology

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

1. DOMAIN AND PURPOSE
flow "NegationOntology" v1.0
  domain: MathematicalEntities.LogicalEntities
  entity: Negation
  notation: ¬P
  semantics: classical propositional and predicate logic by default
  objective: Represent truth-functional negation, its typing, laws, inference, and validation.

2. TYPED ENTITIES
  Proposition := Formula with Boolean truth value under an interpretation
  Negation := UnaryLogicalConnective(Proposition -> Proposition)
  TruthValue := {TRUE, FALSE}
  Interpretation := Mapping(AtomicProposition -> TruthValue)
  Formula := Atomic | Not(Formula) | And(Formula,Formula) | Or(Formula,Formula) | ...
  Predicate := Formula with zero or more free individual variables
  Quantifier := Universal | Existential
  Proof := Sequence(WellFormedFormula, InferenceRule)

3. CORE SEMANTICS
  eval(Not(P), I) := not eval(P,I)
  truth_table:
    P=TRUE  => Not(P)=FALSE
    P=FALSE => Not(P)=TRUE
  syntax: ¬ : Formula -> Formula
  scope: Not(P) negates the entire scoped subformula P
  prerequisite: P is well-formed and I assigns truth to its atoms

4. CLASSICAL IDENTITIES
  double_negation: ¬¬P ≡ P
  excluded_middle: P ∨ ¬P ≡ TRUE
  non_contradiction: P ∧ ¬P ≡ FALSE
  de_morgan_and: ¬(P ∧ Q) ≡ (¬P ∨ ¬Q)
  de_morgan_or: ¬(P ∨ Q) ≡ (¬P ∧ ¬Q)
  implication_negation: ¬(P → Q) ≡ (P ∧ ¬Q)
  biconditional_negation: ¬(P ↔ Q) ≡ (P ⊕ Q)
  constants: ¬TRUE ≡ FALSE; ¬FALSE ≡ TRUE
  quantifier_duality_1: ¬∀x P(x) ≡ ∃x ¬P(x)
  quantifier_duality_2: ¬∃x P(x) ≡ ∀x ¬P(x)
  note: Quantifier identities require a shared domain and standard classical semantics.

5. TYPED RELATIONSHIPS
  Negation --is_a--> LogicalConnective
  Negation --has_arity--> 1
  Negation --operates_on--> Proposition
  Negation --produces--> Proposition
  Negation --inverts--> ClassicalTruthValue
  Negation --dualises_quantifiers--> Quantifier
  Negation --participates_in--> DeMorganLaw
  Negation --contrasts_with--> Affirmation
  Negation --used_by--> ProofRule

6. EXECUTABLE INFERENCE FLOWS (PSEUDOCODE)
  flow "EvaluateNegation"(P:Formula, I:Interpretation) -> TruthValue:
    require well_formed(P)
    return boolean_not(evaluate(P,I))

  flow "SimplifyNegation"(F:Formula) -> Formula:
    if F = Not(Not(P)): return Simplify(P)
    if F = Not(And(P,Q)): return Or(Not(P),Not(Q))
    if F = Not(Or(P,Q)): return And(Not(P),Not(Q))
    if F = Not(Implies(P,Q)): return And(P,Not(Q))
    if F = Not(ForAll(x,P)): return Exists(x,Not(P))
    if F = Not(Exists(x,P)): return ForAll(x,Not(P))
    return F

  flow "ContradictionDetection"(Gamma:Set[Formula]) -> Boolean:
    return exists P such that P in Gamma and Not(P) in Gamma

  flow "NegationIntroduction"(Gamma:Set[Formula], P:Formula) -> Formula:
    require derivation_of_contradiction(Gamma union {P})
    return Not(P)

  flow "NegationElimination"(Gamma:Set[Formula], P:Formula) -> Contradiction:
    require P in Gamma and Not(P) in Gamma
    return BOTTOM

7. VALIDATION AND INVARIANTS
  V01: every Not node has exactly one well-formed formula operand
  V02: evaluation of ¬P is Boolean when P is Boolean
  V03: for every classical interpretation I, eval(¬¬P,I)=eval(P,I)
  V04: de Morgan rewrites preserve truth under all classical interpretations
  V05: distinguish logical negation from inequality, set complement and arithmetic minus
  V06: do not infer ¬P from failure to prove P under open-world semantics
  V07: do not assume excluded middle or double-negation elimination in intuitionistic logic
  V08: do not assume classical two-valued truth tables for fuzzy or paraconsistent logics

8. SEMANTIC_EQUIVALENCE
  canonical: logical negation
  equivalent_labels: NOT; propositional negation; Boolean complement (Boolean context)
  context_sensitive: denial; complement; opposite
  non_equivalent: logical contradiction; absence of evidence; numerical subtraction
  confidence: 1.0 for classical truth-table identities; context-dependent for synonyms

9. EXAMPLES
  example_1: P=TRUE => ¬P=FALSE
  example_2: ¬(P ∧ Q) => ¬P ∨ ¬Q
  example_3: ¬∀x Human(x) => ∃x ¬Human(x) [under a fixed classical domain]
  example_4: ¬(P → Q) => P ∧ ¬Q

10. FLOW_HASH AND UPDATE_MODEL
  canonicalisation: UTF-8; normalise line endings to LF; stable field ordering
  flow_hash: SHA-256(canonicalised_flow_content_excluding_flow_hash_field)
  update_model:
    versioning: semantic
    breaking_change: change to typing, semantics or inference contracts
    compatible_change: new examples, annotations or relationships
    provenance: retain source URL, version, authors and review status

11. AI_CONSUMPTION
  parsing: typed logical entities and relations
  reasoning_mode: classical unless explicitly overridden
  outputs: truth-value evaluation; normalisation; contradiction checks; proof support
  safeguards: report logical system assumptions and distinguish syntax from semantics
  audit: retain applied rewrite rules, input formula, output formula and interpretation

END FLOW ALGEBRA