search

Brandon-Rozek / matmod

Matrix Model Generator for Implicative Connectives
2 stars 0 forks source link

Possible VSP Optimization: Discard models with a single designated value #7

Open Brandon-Rozek opened 1 month ago

Brandon-Rozek commented 1 month 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 1 month 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