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

Evaluating very complex sentences #27

Closed mbuit82 closed 6 months ago

mbuit82 commented 6 months ago

Some of the "test cases" I've been using so far for debugging involve very complex sentences, which we can define to be sentence that are counterfactual and don't have boxright as their main operator (or have some other complex mix of operators, where its "type" (viz, extensional, modal, or cf) isn't the type of the main operator). I've been using them because they used to make the entire thing crash, so I've just been working on them until they don't crash, and then looking at the output and seeing if it makes sense. Here are some outputs:

There is a 3-model of:

Premise:
1. (A \boxright ((B \boxright C) \wedge (D \boxright E)))

Conclusion:
2. F

Possible states:
  #b000 = □
  #b001 = a (world)

The evaluation world is a:
  B, E  (True in a)
  A, C, D, F  (False in a)

Interpreted premise:

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

Interpreted conclusion:

2.  |F| = < ∅, {a} >  (False in a)
There is a 3-model of:

Premise:
1. (A \boxright (B \boxright C))

Conclusion:
2. F

Possible states:
  #b000 = □
  #b001 = a (world)

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

Interpreted premise:

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

Interpreted conclusion:

2.  |F| = < ∅, {a} >  (False in a)

I don't know if these are awfully simple because I simply made the conclusion a new sentence or if there's actually something fundamentally wrong about the way it's printing things. I think the latter may be true because the first one doesn't given any A-alternatives to the antecedent, so the output is very short.

benbrastmckie commented 6 months ago

Those look good! The printouts are short because it's making them true in the most trivial way (that's what it should do). Nice work!

mbuit82 commented 6 months ago

Changed the conclusion from F to C and got more substantive results:

There is a 3-model of:

Premise:
1. (A \boxright ((B \boxright C) \wedge (D \boxright E)))

Conclusion:
2. C

Possible states:
  #b000 = □
  #b001 = a
  #b010 = b
  #b011 = a.b (world)
  #b100 = c (world)

The evaluation world is c:
  D, E  (True in c)
  A, B, C  (False in c)

Interpreted premise:

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

Interpreted conclusion:

2.  |C| = < ∅, {a, a.b, c} >  (False in c)
mbuit82 commented 6 months ago

I guess I makes sense then—a random sentence F is easy to trivially make false

benbrastmckie commented 6 months ago

If you want it to be less trivial, you could add A as a premise to the first one.

benbrastmckie commented 6 months ago

Hey I'm just testing the new merge. Seems like it is catching some errors since world_bits is not an attribute for the Proposition class. I added them from (coming from the model_structure argument). There were a few missing arguments, but they were easy to add. Just booking keeping here so you know what changes I made.

mbuit82 commented 6 months ago

Sounds good!

benbrastmckie commented 6 months ago

Oh looks like you fixed those as well! Seems to be working great.

benbrastmckie commented 6 months ago

I just managed to get the antecedent of a counterfactual to accept nonextensional sentences. Seems to be working great.

benbrastmckie commented 6 months ago

This has been resolved.