truth_eval_implies_totality

formal source

  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
  65    (C : ComparisonOperator)
  66    (hT : TruthEvaluableComparison C) :
  67    OperativePositiveRatioComparison C where
  68  identity := truth_eval_implies_identity C hT
  69  non_contradiction := truth_eval_implies_non_contradiction C hT
  70  continuous := truth_eval_implies_totality C hT
  71  scale_invariant := hT.scale_free
  72  non_trivial := hT.nontrivial
  73
  74/-- Truth-evaluable comparisons satisfy the encoded laws of logic. -/
  75theorem reality_satisfies_logic
  76    (C : ComparisonOperator)
  77    (hT : TruthEvaluableComparison C) :
  78    SatisfiesLawsOfLogic C :=
  79  operative_to_laws_of_logic C