Logical Equivalence Ontology

FLOW ALGEBRA
TITLE: Logical Equivalence Ontology
DOMAIN: Discrete Mathematics / Logic
SOURCE_URL: https://kirethresearch.org/booksai-core/discrete-mathematics-ontologies/logic/logical-equivalence-ontology-2.html
VERSION: 1.0
LANGUAGE: en-GB
AUTHORS: Mark Higgins — Sky (Recursive AI)
SITE: https://kirethresearch.org
STATUS: Formal mathematical model; source page not independently verified

1. PURPOSE
Represent logical equivalence as a typed, verifiable relationship between formulas that have identical truth values under every admissible interpretation in a specified logical system.

2. TYPES
LogicSystem := {classical_propositional, classical_first_order, other_explicit_system}
Formula := well_formed_expression(LogicSystem)
Interpretation := admissible_semantic_structure(LogicSystem)
Assignment := valuation_of_free_variables(Interpretation)
TruthValue := {true, false}  # for classical systems
EquivalenceClaim := (Formula, Formula, LogicSystem, Context)
Proof := finite_sequence_of_justified_steps
Countermodel := (Interpretation, Assignment)

3. CORE SEMANTICS
EQUIVALENT(P, Q, L) := forall admissible I and assignments s: evaluate(P,I,s) = evaluate(Q,I,s)
NOT_EQUIVALENT(P,Q,L) := exists admissible I,s: evaluate(P,I,s) != evaluate(Q,I,s)
CLASSICAL_PROPOSITIONAL_EQUIVALENCE(P,Q) <=> TAUTOLOGY(P <-> Q)
NOTE: Equivalence is metalogical; the biconditional is an object-language connective. Their relationship depends on the chosen logic.

4. RELATION PROPERTIES
REFLEXIVE: P ≡ P
SYMMETRIC: P ≡ Q => Q ≡ P
TRANSITIVE: (P ≡ Q and Q ≡ R) => P ≡ R
CONGRUENCE: replacing an equivalent subformula within a truth-functional context preserves equivalence.

5. CLASSICAL EQUIVALENCE LAWS
DOUBLE_NEGATION: not(not P) ≡ P
DE_MORGAN_1: not(P and Q) ≡ (not P or not Q)
DE_MORGAN_2: not(P or Q) ≡ (not P and not Q)
COMMUTATIVE_AND: (P and Q) ≡ (Q and P)
COMMUTATIVE_OR: (P or Q) ≡ (Q or P)
ASSOCIATIVE_AND: ((P and Q) and R) ≡ (P and (Q and R))
ASSOCIATIVE_OR: ((P or Q) or R) ≡ (P or (Q or R))
DISTRIBUTIVE_AND: (P and (Q or R)) ≡ ((P and Q) or (P and R))
DISTRIBUTIVE_OR: (P or (Q and R)) ≡ ((P or Q) and (P or R))
IMPLICATION: (P -> Q) ≡ (not P or Q)
CONTRAPOSITION: (P -> Q) ≡ (not Q -> not P)
BICONDITIONAL: (P <-> Q) ≡ ((P -> Q) and (Q -> P))
IDEMPOTENCE: (P and P) ≡ P; (P or P) ≡ P
ABSORPTION: (P or (P and Q)) ≡ P; (P and (P or Q)) ≡ P
IDENTITY: (P and true) ≡ P; (P or false) ≡ P
DOMINATION: (P or true) ≡ true; (P and false) ≡ false

6. QUANTIFIER EQUIVALENCES (CLASSICAL FIRST-ORDER LOGIC)
not(forall x P(x)) ≡ exists x not P(x)
not(exists x P(x)) ≡ forall x not P(x)
forall x (P(x) and Q(x)) ≡ (forall x P(x)) and (forall x Q(x))
exists x (P(x) or Q(x)) ≡ (exists x P(x)) or (exists x Q(x))
ALPHA_EQUIVALENCE: bound-variable renaming preserves meaning when capture is avoided.
SIDE_CONDITION: transformations must preserve scope and avoid variable capture; do not freely interchange unlike quantifiers.

7. OPERATIONS
NORMALISE(formula, target_form, logic) -> Formula | Error
CHECK_TRUTH_TABLE(P,Q) -> Equivalent | Countervaluation  # finite propositional variables
CHECK_MODEL(P,Q,model) -> Agreement | Counterexample
PROVE_EQUIVALENCE(P,Q,calculus) -> Proof | Unknown
FIND_COUNTERMODEL(P,Q,logic) -> Countermodel | Unknown
REWRITE(P,law,position) -> Formula | InvalidRewrite

8. INFERENCE RULES
EQ_INTRO: infer P ≡ P.
EQ_SYMMETRY: from P ≡ Q infer Q ≡ P.
EQ_TRANSITIVITY: from P ≡ Q and Q ≡ R infer P ≡ R.
EQ_SUBSTITUTION: from P ≡ Q infer C[P] ≡ C[Q] for valid formula contexts C.
COUNTEREXAMPLE: if any admissible interpretation assigns distinct truth values, reject equivalence.

9. VALIDATION
CHECK_WELL_FORMED: both expressions parse in the same declared logic.
CHECK_FREE_VARIABLES: compare under a shared assignment and declared vocabulary.
CHECK_SCOPE: prevent quantifier scope changes and variable capture.
CHECK_SYSTEM: do not transfer classical laws automatically to intuitionistic, modal, fuzzy, or paraconsistent logics.
CHECK_EVIDENCE: accept a sound proof or exhaustive valid decision procedure; distinguish timeout/unknown from false.
CHECK_REWRITE: each rewrite records the applied law and its side conditions.

10. SEMANTIC RELATIONSHIPS
LogicalEquivalence --is_a--> SemanticRelation
LogicalEquivalence --relates--> Formula
LogicalEquivalence --validated_by--> Proof
LogicalEquivalence --refuted_by--> Countermodel
LogicalEquivalence --supports--> FormulaNormalisation
LogicalEquivalence --enables--> SemanticsPreservingRewrite
LogicalEquivalence --distinct_from--> SyntacticIdentity
LogicalEquivalence --associated_with--> Biconditional

11. SEMANTIC_EQUIVALENCE
canonical_relation: logical_equivalence
aliases: [semantic_equivalence_of_formulas, truth_functional_equivalence]
notation: [≡, ⊨ (P ↔ Q)]
qualification: truth-functional equivalence is the propositional case; contextual and non-classical equivalences require their own semantics.

12. CONFIDENCE
mathematical_definition: 1.0 (within declared classical semantics)
proved_claim: 1.0 (subject to sound verifier and assumptions)
model_sample_agreement: insufficient_to_establish_global_equivalence
unverified_claim: unknown
confidence_policy: never treat a heuristic score as a formal proof.

13. FLOW_HASH
algorithm: SHA-256
input: canonical_serialisation(version, logic_system, formula_A, formula_B, assumptions, normalisation_rules)
value: compute_at_runtime
note: No hash is asserted without performing canonical serialisation and hashing.

14. UPDATE_MODEL
on_formula_change: invalidate_cached_proofs_and_checks
on_logic_change: revalidate_all_equivalence_claims
on_rule_change: version_rule_set_and_rerun_validation
on_countermodel_found: set_status_not_equivalent_and_store_witness
on_proof_verified: set_status_equivalent_and_store_provenance

15. AI_CONSUMPTION
input: {formula_A, formula_B, logic_system, assumptions, requested_check}
output: {status: equivalent|not_equivalent|unknown, proof?, countermodel?, law_trace?, confidence?, provenance?}
constraints: preserve semantics, declare logic, track side conditions, expose uncertainty, never fabricate a proof or countermodel.

END FLOW ALGEBRA