search

Brandon-Rozek / vspursuer

Verify Relevance Properties for Matrix Models with Implicative Connectives
2 stars 0 forks source link

Discard models with a single designated value #7

Closed Brandon-Rozek closed 2 weeks ago

Brandon-Rozek commented 4 months ago

We can immediately throw out any matrix in which there is exactly one designated value.

In all models and for the logics MaGIC deals with, we want x = y to ensure that x -> y is designated, and so for any a,b in a model with exactly one designated value d, a ->a=d=b->b will hold. Thus, (a->a) -> (b->b)=d, and VSP fails.

In other words, if we take any pair of distinct atomic formulas p, q, the value of (p-> p) -> (q-> q) will be designated breaking VSP

Brandon-Rozek commented 4 months ago

Thinking through a possible edge case: Q: What if there are no implications that are designated? A: All logics satisfy implications of the form A->A