Is my Skolem normal form of $(forall x exists yexists zT(x,y)land S(y,z))land(lnotforall yP(y))$ correct?

The name of the pictureThe name of the pictureThe name of the pictureClash Royale CLAN TAG#URR8PPP











up vote
0
down vote

favorite












Is my skolem normal form of $(forall x exists y exists z T(x,y)land S(y,z))land (lnot forall yP(y))$ correct?



$$
beginarray
hline
( forall x exists y exists z ; T(x,y) land S(y,z) )
land (neg forall y ; P(y))
& leftarrowtextGiven formula
\
hline
( forall x exists y exists z ; T(x,y) land S(y,z))
land (neg forall y ; P(y))
& textRename variables and
\

& textchange quantors
\
hline
( forall x exists y exists z ; (T(x,y) land S(y,z)) )
land (exists v ; neg P(v))
& textRemove $()$ and move
\

& text$exists v$ to the left side
\
hline
forall x exists y exists z exists u
; T(x,y) land S(y,z) land neg P(u)
& textIt is in PNF. Do:
\

& exists y = i(x);
exists z = k(x);
\

& exists u = h(x)
\
hline
forall x ; T(x, i(x)) land Q(f(x), k(x)) land neg P(h(x))
& textIt is in SNF.
\
hline
endarray
$$
(Original picture of the calculation here.)







share|cite|improve this question






















  • Thanks for your corrections @Bernard - did you also check the calculations?
    – user3352632
    Aug 26 at 20:42










  • It's beyond my capabilities, unfortunately.
    – Bernard
    Aug 26 at 20:45














up vote
0
down vote

favorite












Is my skolem normal form of $(forall x exists y exists z T(x,y)land S(y,z))land (lnot forall yP(y))$ correct?



$$
beginarray
hline
( forall x exists y exists z ; T(x,y) land S(y,z) )
land (neg forall y ; P(y))
& leftarrowtextGiven formula
\
hline
( forall x exists y exists z ; T(x,y) land S(y,z))
land (neg forall y ; P(y))
& textRename variables and
\

& textchange quantors
\
hline
( forall x exists y exists z ; (T(x,y) land S(y,z)) )
land (exists v ; neg P(v))
& textRemove $()$ and move
\

& text$exists v$ to the left side
\
hline
forall x exists y exists z exists u
; T(x,y) land S(y,z) land neg P(u)
& textIt is in PNF. Do:
\

& exists y = i(x);
exists z = k(x);
\

& exists u = h(x)
\
hline
forall x ; T(x, i(x)) land Q(f(x), k(x)) land neg P(h(x))
& textIt is in SNF.
\
hline
endarray
$$
(Original picture of the calculation here.)







share|cite|improve this question






















  • Thanks for your corrections @Bernard - did you also check the calculations?
    – user3352632
    Aug 26 at 20:42










  • It's beyond my capabilities, unfortunately.
    – Bernard
    Aug 26 at 20:45












up vote
0
down vote

favorite









up vote
0
down vote

favorite











Is my skolem normal form of $(forall x exists y exists z T(x,y)land S(y,z))land (lnot forall yP(y))$ correct?



$$
beginarray
hline
( forall x exists y exists z ; T(x,y) land S(y,z) )
land (neg forall y ; P(y))
& leftarrowtextGiven formula
\
hline
( forall x exists y exists z ; T(x,y) land S(y,z))
land (neg forall y ; P(y))
& textRename variables and
\

& textchange quantors
\
hline
( forall x exists y exists z ; (T(x,y) land S(y,z)) )
land (exists v ; neg P(v))
& textRemove $()$ and move
\

& text$exists v$ to the left side
\
hline
forall x exists y exists z exists u
; T(x,y) land S(y,z) land neg P(u)
& textIt is in PNF. Do:
\

& exists y = i(x);
exists z = k(x);
\

& exists u = h(x)
\
hline
forall x ; T(x, i(x)) land Q(f(x), k(x)) land neg P(h(x))
& textIt is in SNF.
\
hline
endarray
$$
(Original picture of the calculation here.)







share|cite|improve this question














Is my skolem normal form of $(forall x exists y exists z T(x,y)land S(y,z))land (lnot forall yP(y))$ correct?



$$
beginarray
hline
( forall x exists y exists z ; T(x,y) land S(y,z) )
land (neg forall y ; P(y))
& leftarrowtextGiven formula
\
hline
( forall x exists y exists z ; T(x,y) land S(y,z))
land (neg forall y ; P(y))
& textRename variables and
\

& textchange quantors
\
hline
( forall x exists y exists z ; (T(x,y) land S(y,z)) )
land (exists v ; neg P(v))
& textRemove $()$ and move
\

& text$exists v$ to the left side
\
hline
forall x exists y exists z exists u
; T(x,y) land S(y,z) land neg P(u)
& textIt is in PNF. Do:
\

& exists y = i(x);
exists z = k(x);
\

& exists u = h(x)
\
hline
forall x ; T(x, i(x)) land Q(f(x), k(x)) land neg P(h(x))
& textIt is in SNF.
\
hline
endarray
$$
(Original picture of the calculation here.)









share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








edited Aug 26 at 20:47









Jendrik Stelzner

7,63121037




7,63121037










asked Aug 26 at 20:23









user3352632

827




827











  • Thanks for your corrections @Bernard - did you also check the calculations?
    – user3352632
    Aug 26 at 20:42










  • It's beyond my capabilities, unfortunately.
    – Bernard
    Aug 26 at 20:45
















  • Thanks for your corrections @Bernard - did you also check the calculations?
    – user3352632
    Aug 26 at 20:42










  • It's beyond my capabilities, unfortunately.
    – Bernard
    Aug 26 at 20:45















Thanks for your corrections @Bernard - did you also check the calculations?
– user3352632
Aug 26 at 20:42




Thanks for your corrections @Bernard - did you also check the calculations?
– user3352632
Aug 26 at 20:42












It's beyond my capabilities, unfortunately.
– Bernard
Aug 26 at 20:45




It's beyond my capabilities, unfortunately.
– Bernard
Aug 26 at 20:45















active

oldest

votes











Your Answer




StackExchange.ifUsing("editor", function ()
return StackExchange.using("mathjaxEditing", function ()
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix)
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
);
);
, "mathjax-editing");

StackExchange.ready(function()
var channelOptions =
tags: "".split(" "),
id: "69"
;
initTagRenderer("".split(" "), "".split(" "), channelOptions);

StackExchange.using("externalEditor", function()
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled)
StackExchange.using("snippets", function()
createEditor();
);

else
createEditor();

);

function createEditor()
StackExchange.prepareEditor(
heartbeatType: 'answer',
convertImagesToLinks: true,
noModals: false,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
);



);













 

draft saved


draft discarded


















StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2895482%2fis-my-skolem-normal-form-of-forall-x-exists-y-exists-ztx-y-land-sy-z-la%23new-answer', 'question_page');

);

Post as a guest



































active

oldest

votes













active

oldest

votes









active

oldest

votes






active

oldest

votes















 

draft saved


draft discarded















































 


draft saved


draft discarded














StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2895482%2fis-my-skolem-normal-form-of-forall-x-exists-y-exists-ztx-y-land-sy-z-la%23new-answer', 'question_page');

);

Post as a guest













































































這個網誌中的熱門文章

Is there any way to eliminate the singular point to solve this integral by hand or by approximations?

Why am i infinitely getting the same tweet with the Twitter Search API?

Carbon dioxide