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...

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...

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...

The Naoyuki Tamura seqprover for classical first-order logic invents a new variables, no Russell Paradox, which would read d(d): ------------------------------------------- Ax-c d(X1),d(Z) --> d(X1),d(Y1),X#(d(X)->Y@d(Y)) -------------------------------------------- R@ d(X1),d(Z) --> d(X1),Y@d(Y),X#(d(X)->Y@d(Y)) ---------------------------------------------...