0

I am trying to prove that some preconditions don't introduce an inconsistency to my (constructive) system. I would like to know if this is possible with the set-up below, and how to do this, and what additionally i need to include/specify to make this happen. What do I need to specify about isThisTrue?

Inductive myThing : Type :=
  | a : myThing
  | b : myThing.

Inductive isThisTrue : myThing -> Prop :=
  | is_a : isThisTrue a
  | is_b : isThisTrue b.


Definition somethingIsTrue := ~ (forall x, ~ isThisTrue x).


Definition nothingIsFalse := forall x, ~~ isThisTrue x.

So, I want show something like -

Definition consistent := somethingIsTrue /\ nothingIsFalse ... does not introduce inconsistency

Polina
  • 1
  • The idea is that we have no additional information about isThisTrue, but we want to say something about the conjunction of the two propositions somethingIsTrue and nothingIsFalse, showing that they dont contradict themselves or each other. But for that we need some additional assumptions about isThisTrue or maybe a complete re-statement of the problem? – Polina Dec 29 '22 at 19:56
  • What do you mean by “does not introduce inconsistency”? We are simply introducing new notation. How would that create inconsistency? – Mark Saving Dec 31 '22 at 05:53
  • My first thought would be to try to prove that ~ ~ somethingIsTrue /\ nothingIsFalse, which would be trivial for example, if I was instead proving ~~ (somethingIsTrue \/ ~ somethingIsTrue). My goal is to prove additional results implied by somethingIsTrue /\ nothingIsFalse but I am not sure that these two do not contradict each other (I actually have slightly different definitions which are more involved, but I am interested in how I would approach this in general) – Polina Jan 05 '23 at 03:29
  • Perhaps I could scrap the definition of isThisTrue and parametrize somethingIsTrue and nothingIsFalse, so that I would instead try to prove something like, exists (isThisTrue : myThing -> Prop), (somethingIsTrue isThisTrue /\ nothingIsFalse isThisTrue) – Polina Jan 05 '23 at 03:49

0 Answers0