truth_eval_implies_identity

formal source

  31  nontrivial : NonTrivial C
  32
  33/-- Truth-evaluability of self-statements gives identity. -/
  34theorem truth_eval_implies_identity
  35    (C : ComparisonOperator)
  36    (hT : TruthEvaluableComparison C) :
  37    Identity C :=
  38  hT.self_evaluable
  39
  40/-- Truth-evaluability of reordered pair-statements gives non-contradiction. -/
  41theorem truth_eval_implies_non_contradiction
  42    (C : ComparisonOperator)
  43    (hT : TruthEvaluableComparison C) :
  44    NonContradiction C :=
  45  hT.reorder_single_valued
  46
  47/-- Truth-evaluability of every positive pair gives totality/continuity on the
  48open positive quadrant. -/
  49theorem truth_eval_implies_totality
  50    (C : ComparisonOperator)
  51    (hT : TruthEvaluableComparison C) :
  52    ExcludedMiddle C :=
  53  hT.determinate_continuous
  54
  55/-- Truth-evaluability of composite comparison-statements gives finite pairwise
  56composition. -/
  57theorem truth_eval_implies_composition
  58    (C : ComparisonOperator)
  59    (hT : TruthEvaluableComparison C) :
  60    FinitePairwisePolynomialClosure C :=
  61  hT.composite_determinate
  62
  63/-- Truth-evaluable comparisons are operative positive-ratio comparisons. -/
  64theorem truth_eval_to_operative