Closed Jean-Luc-Picard-2021 closed 4 months ago
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.
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.)
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.
The problem is that propositional quantification is second-order quantification.
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.
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:
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(_)
:Or alternatively use the Gödel translation
T(_)
: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.