benbrastmckie / ModelChecker

A hyperintensional theorem prover for counterfactual conditional, modal, constitutive explanatory, relevance, and extensional operators.
https://pypi.org/project/model-checker/
7 stars 0 forks source link

False Premise and True Conclusion Models #34

Open benbrastmckie opened 4 months ago

benbrastmckie commented 4 months ago

The testing.py file contains various examples which either include a false premise or true conclusion. For instance, consider the following cases:

False Premise

There is a 2-model of:

Premises:
1. (A \boxright X)
2. \neg ((A \wedge B) \boxright X)
3. (((A \wedge B) \wedge C) \boxright X)
4. \neg ((((A \wedge B) \wedge C) \wedge D) \boxright X)

State Space:
  #b00 = □
  #b01 = a (world)
  #b10 = b (world)

The evaluation world is: b
  A, B, X  (True in b)
  C, D  (False in b)

INTERPRETED PREMISES:

1.  |(A \boxright X)| = < {□}, ∅ >  (True in b)
    |A| = < {□}, ∅ >  (True in b)
    A-alternatives to b = {b}
      |X| = < {b}, {a} >  (True in b)

2.  |\neg ((A \wedge B) \boxright X)| = < {□}, ∅ >  (True in b)
    |((A \wedge B) \boxright X)| = < ∅, {□} >  (False in b)
      |(A \wedge B)| = < {a, b}, ∅ >  (True in b)
        |A| = < {□}, ∅ >  (True in b)
        |B| = < {a, b}, ∅ >  (True in b)
      (A \wedge B)-alternatives to b = {a, b}
        |X| = < {b}, {a} >  (False in a)
        |X| = < {b}, {a} >  (True in b)

3.  |(((A \wedge B) \wedge C) \boxright X)| = < {□}, ∅ >  (True in b)
    |((A \wedge B) \wedge C)| = < ∅, {□} >  (False in b)
      |(A \wedge B)| = < {a, b}, ∅ >  (True in b)
        |A| = < {□}, ∅ >  (True in b)
        |B| = < {a, b}, ∅ >  (True in b)
      |C| = < ∅, {□} >  (False in b)
    ((A \wedge B) \wedge C)-alternatives to b = {}

4.  |\neg ((((A \wedge B) \wedge C) \wedge D) \boxright X)| = < ∅, {□} >  (F
alse in b)
    |((((A \wedge B) \wedge C) \wedge D) \boxright X)| = < {□}, ∅ >  (True i
n b)
      |(((A \wedge B) \wedge C) \wedge D)| = < ∅, {b, □} >  (False in b)
        |((A \wedge B) \wedge C)| = < ∅, {□} >  (False in b)
          |(A \wedge B)| = < {a, b}, ∅ >  (True in b)
            |A| = < {□}, ∅ >  (True in b)
            |B| = < {a, b}, ∅ >  (True in b)
          |C| = < ∅, {□} >  (False in b)
        |D| = < {a}, {b} >  (False in b)
      (((A \wedge B) \wedge C) \wedge D)-alternatives to b = {}

Run time: 0.027 seconds

True Conclusion

There is a 3-model of:

Conclusion:
1. ((A \wedge (B \vee C)) \equiv ((A \wedge B) \vee (A \wedge C)))

State Space:
  #b000 = □
  #b001 = a
  #b010 = b
  #b011 = a.b (world)
  #b100 = c
  #b110 = b.c (world)

The evaluation world is: a.b
  C  (True in a.b)
  A, B  (False in a.b)

INTERPRETED CONCLUSION:

1.  |((A \wedge (B \vee C)) \equiv ((A \wedge B) \vee (A \wedge C)))| = < {□
}, ∅ >  (True in a.b)
    |(A \wedge (B \vee C))| = < {b.c}, {a.b} >  (False in a.b)
      |A| = < {b.c}, {a.b} >  (False in a.b)
      |(B \vee C)| = < {a.b, c}, ∅ >  (True in a.b)
        |B| = < {c}, {a} >  (False in a.b)
        |C| = < {a.b}, {b.c} >  (True in a.b)
    |((A \wedge B) \vee (A \wedge C))| = < {b.c}, {a.b} >  (False in a.b)
      |(A \wedge B)| = < {b.c}, {a, a.b} >  (False in a.b)
        |A| = < {b.c}, {a.b} >  (False in a.b)
        |B| = < {c}, {a} >  (False in a.b)
      |(A \wedge C)| = < ∅, {a.b, b.c} >  (False in a.b)
        |A| = < {b.c}, {a.b} >  (False in a.b)
        |C| = < {a.b}, {b.c} >  (True in a.b)

Run time: 0.1348 seconds

I'm not sure what explains either of these cases.

benbrastmckie commented 2 weeks ago

These were all resolved previously, but I'm now getting false premise models for the following:

# FALSE PREMISE
N = 3
premises = ["(A \\leftrightarrow B)", "\\possible A"]
conclusions = ["C"]
contingent_bool = False
disjoint_bool = False

# FALSE PREMISE
# CF_CM19: COUNTERFACTUAL EXPORTATION WITH POSSIBILITY
N = 3
premises = ['((A \\wedge B) \\boxright C)','\\possible (A \\wedge B)']
conclusions = ['(A \\boxright (B \\boxright C))']
contingent_bool = True
disjoint_bool = False

Whereas before the false premise models were eliminated without finding their cause, perhaps these examples will be some clue to what is causing this behavior.