(Semi)automatic translated theroems and defintions

Stream: new members

[Ryan McManus]

structure LogicalContext where
  Statement : Type u
  truth : Statement → Bool
  possible : Set (Statement → Bool)
  truth_possible : truth ∈ possible
  /--
  You can combine an arbitrary possible : Set (Statement → Bool) number of statements with a boolean function.
  -/
  apply {ι} :
    (ι → Statement) →
    (f : (ι → Bool) → Bool) →
    Statement

  --axiom of closure
  apply_spec {ι}
   (T : ι → Statement)
   (f : (ι → Bool) → Bool) :
    ∀ a ∈ possible,
      a (apply T f) = f (a ∘ T)

I have been working on translating a book by "Assumptions of Physics" and this is the Logical Context is the base of this entire thing. It was described as a set of Statements internal to the Context, with a set of functions assigning statements to truth values (represented by Bools) with the truth being one of them.

Another thing added (and why I am posting this) is that these statements are in a sense closed. What I mean is that you can take any function from an arbitrary number of bools to bool and turn that into a function from an arbitrary number of Statements to Statement, and Statement will be closed under that. In addition this transformation is structure preserving e.g.:

$$\forall a \in possible, a(f (s_1, s_2,\cdots) ) = f_\mathbb B(a(s_1),a(s_2),\cdots)$$

my question on this is if I am intending to prove a ton of algebraic properties of Statement, particularly reproving properties of bool, is there a good way to do it or do I have to do everything by had?

[Ryan McManus]

I was thinking if there was a way to automatically take theorems and defs from bools to theorems and defs on statements that would be nice

[Ryan McManus]

I don't want to define And, Or, Not, Le, and equality on statements, and then have to prove all of the sensible ways to combine them if it is not something of substance

[Ryan McManus]

For my other question. I have an equivalence relation defined on these statements as well as a partial order. Statement modulo the equivalence forms a complete Boolean Algebra. My question is do I have to redefine all of the definitions and theorems in terms of the Quotient or is there a way to skirt around that without to much of a headache.

If I do have to I will still try my best to prove as much out of it as I can so I would like to decrease the code duplication if I can.