Feature request: persistency aka monotonic accessibility checkbox

[Jean-Luc-Picard-2021]

I wanted to experiment with a certain Kripke semantics for intuitionistic logic. But I am missing a check box to choose a persistency condtion for the accessibility relation.

This would be a property that can be expressed by this axiom schema, but you can also express it directly with the accessibility relation, see here:

P => []P

The workaround is currently to do for example this, i.e. manually instantiate and box prefix the axiom schema for each propositional variable and use the standard translation S(_):

(□(p→□p) ∧ □(q→□q)) → (□(□(p→q) → p) → p) is invalid. https://www.umsu.de/trees/#~8(p~5~8p)~1~8(q~5~8q)~5(~8(~8(p~5q)~5p)~5p)||reflexivity|transitivity

Or alternatively use the Gödel translation T(_):

□(□(□p → □q) → □p) → □p is invalid. https://www.umsu.de/trees/#~8%28~8%28~8p~5~8q%29~5~8p%29~5~8p||reflexivity|transitivity

The models under the Gödel translation T(_) do not directly correspond to models from the Kripke semantics for intuitionistic logic with the persistency condtion.

So the advantage of the S(_) translation plus persistency condition is focus on different counter models.

[Jean-Luc-Picard-2021]

P.S.: There is a kind of Galois Connection between the standard translation S(_) and the Gödel translation T(_).

See also:

Modal Logic - Logic Guides 35 Lemma 3.81 (Skeleton) Chagrov & Zakharyaschev - 1997 https://www.amazon.de/dp/0198537794

But I might be a little rusty, could be also the wrong reference. And maybe there are new and more educational references around? the geometric intuition

is rather simple. Lets show the idea by a simple modal model that has consecutive worlds w0, w1, w2, .., wk, ..., wn-1, wn, and all of these worlds are freely true or false for a

propositional variable p, there is no persistency condition, the index k is chosen such that it marks the start of a 1's run, and we have transitivity and reflexivity as well:

w0, w1, w2, .., wk, ..., wn-1, wn
0   1 0  ....  1 ... 1  1

Then p sees the above, but []p sees the below:

w0, w1, w2, .., wk, ..., wn-1, wn
0   0  0  ....  1 ... 1  1

Which the persistency condition would filter out from the beginning as a candidate model, allowing to use p instead of []p in a standard translation instead.

[wo]

Thanks for the suggestion. It's not trivial to implement. At the moment, my countermodel finder uses the standard translation to turn modal sentences into first-order sentences; accessibility conditions are translated into further premises. I don't think the persistency condition is first-order definable, so I couldn't handle it in this way. (I'd also need a new tree rule.)

[Jean-Luc-Picard-2021]

It depends how you translate. If you translate a propositional variable p into p(w) its a little bit more effort. If you translate a propositional variable p into D(p,w) then its a little bit less effort:

ALL(p):ALL(w):ALL(v):[D(w,p) & R(w,v) => D(v,p)]

For p(w) you can collect all propositional variables from the given input A, lets say they are p1,..,pn. And then generate:

ALL(w):ALL(v):[p1(w) & R(w,v) => p1(v)]
[...]
ALL(w):ALL(v):[pn(w) & R(w,v) => pn(v)]

My claims are based on this short wiki definition:

Semantics of intuitionistic logic https://en.wikipedia.org/wiki/Kripke_semantics#Semantics_of_intuitionistic_logic

In the above D(p,w) is written as w ⊩ p . But to have D(p,w) usable, maybe you need also pi ≠ pj for i ≠ j as axioms? Some Unique name assumption? Not 100% sure.

[wo]

The problem is that propositional quantification is second-order quantification.

[Jean-Luc-Picard-2021]

Well you reify the propositional variables. So the propositional variables p1,..,pn land in some domain P, the forcing conditions, and for every propositional variable pj there is a forcing condition Pj,

which is member of P. So basically this here, would be rather a multisorted thing, were W is the sort of the possible worlds, and P are the forcing conditions. So turn this:

ALL(p):ALL(w):ALL(v):[D(w,p) & R(w,v) => D(v,p)]

Into this:

ALL(p):[P(p) => ALL(w):[W(w) => ALL(v):[W(v) => [D(w,p) & R(w,v) => D(v,p)]]]

But you don't run into this problem if you use the alternate translation. Just manually collect the proposional variables p1,..,pn of a formula A, which is queried, before you try to prove it or find a counter model, and then add

before you try to prove it or find a counter model:

ALL(w):ALL(v):[p1(w) & R(w,v) => p1(v)]
[...]
ALL(w):ALL(v):[pn(w) & R(w,v) => pn(v)]

This is single sorted. You don't need a sort P, and a sort W is also not necessary. The domain of discourse is basically the sort W. No need to go multi sorted.