Logical Argument Ontology

FLOW ALGEBRA
TITLE: Logical Argument Ontology
VERSION: 1.0
DOMAIN: Mathematical Entities / Logical Entities
SOURCE: https://kirethresearch.org/booksai-core/entity-graph/mathematical-entities/logical-entities/logical-argument-ontology.html
AUTHORS: Mark Higgins — Sky (Recursive AI)
STATUS: Proposed mathematical formalisation; source-page wording not independently verified.

1. PURPOSE
Represent a logical argument as an ordered or unordered collection of premises and a distinguished conclusion, with explicit syntax, semantics, proof obligations, validity checks, and machine-consumable inference provenance.

2. TYPED ENTITIES
sort Formula; sort Proposition <: Formula; sort Premise <: Formula;
sort Conclusion <: Formula; sort Argument; sort Interpretation;
sort Proof; sort InferenceRule; sort Countermodel; sort Context.
Argument = {id: Identifier, premises: FiniteSequence<Formula>, conclusion: Formula, logic: LogicSystem, context: Context}.
Judgement = {argument: Argument, status: VALID | INVALID | UNKNOWN, evidence: Proof | Countermodel | None}.

3. CORE RELATIONSHIPS
HAS_PREMISE(Argument, Formula)
HAS_CONCLUSION(Argument, Formula)
USES_RULE(Proof, InferenceRule)
DERIVES(PremiseSet, Conclusion)
ENTAILS(PremiseSet, Conclusion)
SATISFIES(Interpretation, Formula)
COUNTEREXAMPLE_TO(Countermodel, Argument)
CONTEXT_OF(Argument, Context)

4. FORMAL SEMANTICS
Let A = (Gamma, phi), with Gamma a set of premises and phi a conclusion.
SEMANTIC_VALID(A) iff for every interpretation M, if M satisfies every gamma in Gamma, then M satisfies phi.
Notation: Gamma |= phi.
SYNTACTIC_DERIVABLE(A) iff a proof exists from Gamma to phi under the declared proof calculus.
Notation: Gamma |- phi.
For a sound calculus: Gamma |- phi implies Gamma |= phi.
For a complete calculus: Gamma |= phi implies Gamma |- phi.
These implications are conditional on the calculus and logic system.

5. CLASSICAL PROPOSITIONAL LOGIC RULES
MODUS_PONENS: [P, (P -> Q)] => Q.
MODUS_TOLLENS: [(P -> Q), not Q] => not P.
CONJUNCTION_INTRODUCTION: [P, Q] => (P and Q).
CONJUNCTION_ELIMINATION: [(P and Q)] => P; [(P and Q)] => Q.
DISJUNCTION_INTRODUCTION: [P] => (P or Q).
HYPOTHETICAL_SYLLOGISM: [(P -> Q), (Q -> R)] => (P -> R).
DISJUNCTIVE_SYLLOGISM: [(P or Q), not P] => Q.
Each rule is interpreted under classical logic; other logics require separate rule declarations.

6. ARGUMENT CLASSIFICATION
DEDUCTIVE_VALID: no interpretation makes every premise true and conclusion false.
DEDUCTIVE_INVALID: at least one such counterinterpretation exists.
SOUND: deductively valid and every premise is true under the intended interpretation.
UNSOUND: not sound; does not by itself establish invalidity.
CONSISTENT_PREMISES: Gamma has at least one model.
INCONSISTENT_PREMISES: Gamma has no model.
INDUCTIVE_SUPPORT: graded evidential support; not equivalent to deductive entailment.
ABDUCTIVE_INFERENCE: candidate explanatory conclusion; not automatically deductively valid.

7. EXECUTABLE FLOW
flow LogicalArgumentValidation(argument: Argument) -> Judgement:
  require well_formed(argument.premises, argument.conclusion, argument.logic)
  require scoped_variables(argument)
  normalised := normalise_formulas(argument)
  if supported_decidable_fragment(normalised.logic):
    countermodel := solve(SAT(Gamma AND NOT phi))
    if countermodel exists: return INVALID with Countermodel(countermodel)
    if UNSAT certified: return VALID with proof_or_unsat_certificate
    return UNKNOWN with reason="solver inconclusive"
  proof := attempt_proof(Gamma, phi, declared_rules)
  if proof is verified: return VALID with Proof(proof)
  return UNKNOWN with reason="no complete decision procedure applied"

8. INFERENCE AND CONSTRAINTS
R1: HAS_PREMISE(A,P) and HAS_CONCLUSION(A,Q) do not alone imply ENTAILS({P},Q).
R2: VERIFIED_PROOF(Gamma,phi) and SOUND_CALCULUS => ENTAILS(Gamma,phi).
R3: COUNTERMODEL(M,Gamma,phi) => INVALID(Argument(Gamma,phi)).
R4: VALID(A) and ALL_PREMISES_TRUE(A,M) => CONCLUSION_TRUE(A,M).
R5: INCONSISTENT_PREMISES(Gamma) => Gamma entails phi in classical logic (explosion); do not generalise to paraconsistent logics.
R6: VALID(A) does not imply SOUND(A).

9. SEMANTIC EQUIVALENCE AND DISTINCTIONS
SEMANTIC_EQUIVALENCE: "valid argument" ~= "premises entail conclusion" under specified logic.
DISTINGUISH: entailment (semantic) vs derivability (syntactic).
DISTINGUISH: truth of conclusion vs validity of inference.
DISTINGUISH: validity vs soundness.
DISTINGUISH: deductive argument vs inductive or abductive argument.
DISTINGUISH: argument as formal object vs rhetorical disagreement.

10. VALIDATION
V1: Every argument has at least one designated conclusion.
V2: All formulas parse in the declared formal language.
V3: Free variables, domains and quantifier scope are recorded.
V4: Proof steps cite licensed inference rules and prior lines.
V5: Countermodels satisfy every premise and falsify the conclusion.
V6: Never label UNKNOWN as INVALID merely because proof search failed.
V7: For classical finite propositional arguments, SAT(Gamma and not phi) decides validity when solver terminates correctly.
V8: Truth and soundness claims identify intended interpretation and evidence.

11. CONFIDENCE
confidence.semantic_status = CERTAIN only for verified formal proof or certified countermodel.
confidence.source_alignment = UNVERIFIED until compared with source-page text.
confidence.heuristic_inference = CALIBRATED_SCORE; never substitute for proof validity.

12. UPDATE_MODEL
On changes to premises, conclusion, interpretation, logic, or inference rules:
  invalidate cached validity status and proofs as required;
  recompute normal form and dependency graph;
  revalidate derivations and countermodels;
  increment version and record provenance.

13. FLOW_HASH
FLOW_HASH = SHA256(canonical_utf8(serialised_flow_without_flow_hash)).
Canonicalisation must specify stable field ordering, normalised line endings, Unicode NFC and exact whitespace handling. Compute the hash after publication; no uncomputed digest is claimed here.

14. AI_CONSUMPTION
input: typed Argument, declared logic, context, optional proof and interpretations.
output: classification, derivation trace, countermodel or uncertainty, semantic links, provenance.
policy: distinguish logically guaranteed conclusions from plausible claims; preserve assumptions and scope; reject unsupported entailment.

END FLOW ALGEBRA