Define a relation $\equiv$ on the set of modal formulas by

$\phi \equiv \psi \Leftrightarrow (\forall M\forall w, M,w \models \phi\Leftrightarrow M,w \models \psi)$ (so it is an equivalence relation)

Define boolean combination by combining the formulas use only boolean connectives, namely $\lnot$ and $\lor$ (certainly we can involve $\land$ also, but only these two are primitive).

My goal is to prove:

Give a set $S$ of formulas, suppose its set of equivalence classes under $\equiv$ is finite, then take the set of boolean combinations of the formulas of this set, then we obtain a set with its set of equivalence classes under $\equiv$ finite.

The stuff below is the relative information in HOL 4. (I am proving it in the theorem prover HOL 4.)

The definition of the relation is:

∀f1 f2. equiv f1 f2 ⇔ ∀M w. satis M w f1 ⇔ satis M w f2

The definition of boolean combination is:

∀a0 a1. IBC a0 a1 ⇔ (∃f1 f2. a0 = DISJ f1 f2 ∧ IBC f1 a1 ∧ IBC f2 a1) ∨ a0 = ⊥ ∨ (∃f. a0 = ¬f ∧ IBC f a1) ∨ a0 ∈ a1

Where "IBC" stands for boolean combination. Saying "IBC a0 a1" is saying that a0 is a formula which can be obtained by boolean combination using the formulas in the set a1."DISJ" stands for "$\lor$". So "(∃f1 f2. a0 = DISJ f1 f2 ∧ IBC f1 a1 ∧ IBC f2 a1)" is read as "exists modal formulas f1 f2 such that the formula a0 is the disjunction of f1 and f2, and each of the formulas f1 and f2 can be obtained by boolean combination using elements in the set a1."

The goal I want to prove is:

∀s. FINITE (partition equiv s) ⇒ FINITE (partition equiv {phi | IBC phi s}))

Where "partition R s" denotes the set obtained by partitioning the set s under the relation R.

My thoughts:

I attempted by induction, I have solved the base case and the step case is:

FINITE (partition equiv {phi | IBC phi s})

  1. FINITE p

  2. ∀s. p = partition equiv s ⇒ FINITE (partition equiv {phi | IBC phi s})

  3. e ∉ p

  4. e INSERT p = partition equiv s

The 0,1,2,3 under the lines are assumptions, and the statement above the line is the goal.

I admit that this fact is obvious, but I need a proof which is as rigorous as possible since I want to convince my theorem prover. I have thought about it for long without progress. Any attempt of helping me would be very appreciate! Thank you.


Your Answer

By clicking "Post Your Answer", you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.