Mixing
Prove that structure M is not Herbrand structure
$begingroup$
I've been trying to solve the following problem, but I get a bit confused with the solution I get.
Here's the problem:
Let's M be a structure with an universe all the terms with no variables. We know that the value of the term f(x) in M given evaluation v is v(x).
Prove that M is not Herbrand structure.
My attempt to prove it:
By definition structure H is Herbrand if for every functional symbol f and elements of the Universe (which contains only terms with no variables)
$t_1, ... , t_n$ we have that $f^H(t_1, ...,t_n)=f(t_1,...,t_n)$
On the other hand we know evaluation functions are functions mapping elements of the Universe to variables.
So
$[![f(x)]!]^Hv=$(by definition of evaluation)$=f^H([![x]!]^Hv)=f^H(v(x))$
On the other hand we want
$f^H(x)=f(x)$ By the definition of Herbrand structure.
So here I get confused by the fact that the evalution v may be such that v(x)=x.
Any suggestions how to prove it?
logic first-order-logic predicate-logic
edited Jan 28 at 10:42
Mauro ALLEGRANZA
67.5k449117
asked Jan 28 at 10:13
ZarrieZarrie
103
$endgroup$
add a comment |
$begingroup$
I've been trying to solve the following problem, but I get a bit confused with the solution I get.
Here's the problem:
Let's M be a structure with an universe all the terms with no variables. We know that the value of the term f(x) in M given evaluation v is v(x).
Prove that M is not Herbrand structure.
My attempt to prove it:
By definition structure H is Herbrand if for every functional symbol f and elements of the Universe (which contains only terms with no variables)
$t_1, ... , t_n$ we have that $f^H(t_1, ...,t_n)=f(t_1,...,t_n)$
On the other hand we know evaluation functions are functions mapping elements of the Universe to variables.
So
$[![f(x)]!]^Hv=$(by definition of evaluation)$=f^H([![x]!]^Hv)=f^H(v(x))$
On the other hand we want
$f^H(x)=f(x)$ By the definition of Herbrand structure.
So here I get confused by the fact that the evalution v may be such that v(x)=x.
Any suggestions how to prove it?
logic first-order-logic predicate-logic
edited Jan 28 at 10:42
Mauro ALLEGRANZA
67.5k449117
asked Jan 28 at 10:13
ZarrieZarrie
103
$endgroup$
add a comment |
$begingroup$
I've been trying to solve the following problem, but I get a bit confused with the solution I get.
Here's the problem:
Let's M be a structure with an universe all the terms with no variables. We know that the value of the term f(x) in M given evaluation v is v(x).
Prove that M is not Herbrand structure.
My attempt to prove it:
By definition structure H is Herbrand if for every functional symbol f and elements of the Universe (which contains only terms with no variables)
$t_1, ... , t_n$ we have that $f^H(t_1, ...,t_n)=f(t_1,...,t_n)$
On the other hand we know evaluation functions are functions mapping elements of the Universe to variables.
So
$[![f(x)]!]^Hv=$(by definition of evaluation)$=f^H([![x]!]^Hv)=f^H(v(x))$
On the other hand we want
$f^H(x)=f(x)$ By the definition of Herbrand structure.
So here I get confused by the fact that the evalution v may be such that v(x)=x.
Any suggestions how to prove it?
logic first-order-logic predicate-logic
edited Jan 28 at 10:42
Mauro ALLEGRANZA
67.5k449117
asked Jan 28 at 10:13
ZarrieZarrie
103
$endgroup$
I've been trying to solve the following problem, but I get a bit confused with the solution I get.
Here's the problem:
Let's M be a structure with an universe all the terms with no variables. We know that the value of the term f(x) in M given evaluation v is v(x).
Prove that M is not Herbrand structure.
My attempt to prove it:
By definition structure H is Herbrand if for every functional symbol f and elements of the Universe (which contains only terms with no variables)
$t_1, ... , t_n$ we have that $f^H(t_1, ...,t_n)=f(t_1,...,t_n)$
On the other hand we know evaluation functions are functions mapping elements of the Universe to variables.
So
$[![f(x)]!]^Hv=$(by definition of evaluation)$=f^H([![x]!]^Hv)=f^H(v(x))$
On the other hand we want
$f^H(x)=f(x)$ By the definition of Herbrand structure.
So here I get confused by the fact that the evalution v may be such that v(x)=x.
Any suggestions how to prove it?
logic first-order-logic predicate-logic
logic first-order-logic predicate-logic
edited Jan 28 at 10:42
Mauro ALLEGRANZA
67.5k449117
asked Jan 28 at 10:13
ZarrieZarrie
103
edited Jan 28 at 10:42
Mauro ALLEGRANZA
67.5k449117
asked Jan 28 at 10:13
ZarrieZarrie
103
edited Jan 28 at 10:42
Mauro ALLEGRANZA
67.5k449117
edited Jan 28 at 10:42
Mauro ALLEGRANZA
67.5k449117
edited Jan 28 at 10:42
Mauro ALLEGRANZA
67.5k449117
67.5k449117
asked Jan 28 at 10:13
ZarrieZarrie
103
asked Jan 28 at 10:13
ZarrieZarrie
103
asked Jan 28 at 10:13
ZarrieZarrie
103
103
add a comment |
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Let $S$ be a set of formulas (more exactly : clauses).
Let $H$ the Herbrand universe of $S$ (the domain of all ground (i.e. closed) terms) and $I$ an interpretation of $S$ over $H$.
In order that $I$ is an Herbrand model of $S$ we need that :
1) $I$ maps all constants in $S$ to themselves;
2) If $f$ is an $n$-place function symbol and $h_1, ldots, h_n$ are elements of $H$, then $I$ must assign to $f$ a function $f^{H}$ that maps $(h_1, ldots, h_n)$ to
$f^H(h_1, ldots, h_n)$ (an element of $H$).
But the variable $x$ is not in the Herbrand universe $H$, because it is not a closed term.
Thus, $v(x)$ is an element of the domain $D$ of the structure $mathcal M$, and again $v(x)$ is not an element of $H$.
answered Jan 28 at 10:41
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
$endgroup$
$begingroup$
Thank you! Clear and simple explanation!
$endgroup$
– Zarrie
Jan 28 at 11:03
$begingroup$
@Zarrie - you are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 28 at 11:41
add a comment |
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',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3090683%2fprove-that-structure-m-is-not-herbrand-structure%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Let $S$ be a set of formulas (more exactly : clauses).
Let $H$ the Herbrand universe of $S$ (the domain of all ground (i.e. closed) terms) and $I$ an interpretation of $S$ over $H$.
In order that $I$ is an Herbrand model of $S$ we need that :
1) $I$ maps all constants in $S$ to themselves;
2) If $f$ is an $n$-place function symbol and $h_1, ldots, h_n$ are elements of $H$, then $I$ must assign to $f$ a function $f^{H}$ that maps $(h_1, ldots, h_n)$ to
$f^H(h_1, ldots, h_n)$ (an element of $H$).
But the variable $x$ is not in the Herbrand universe $H$, because it is not a closed term.
Thus, $v(x)$ is an element of the domain $D$ of the structure $mathcal M$, and again $v(x)$ is not an element of $H$.
answered Jan 28 at 10:41
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
$endgroup$
$begingroup$
Thank you! Clear and simple explanation!
$endgroup$
– Zarrie
Jan 28 at 11:03
$begingroup$
@Zarrie - you are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 28 at 11:41
add a comment |
$begingroup$
Let $S$ be a set of formulas (more exactly : clauses).
Let $H$ the Herbrand universe of $S$ (the domain of all ground (i.e. closed) terms) and $I$ an interpretation of $S$ over $H$.
In order that $I$ is an Herbrand model of $S$ we need that :
1) $I$ maps all constants in $S$ to themselves;
2) If $f$ is an $n$-place function symbol and $h_1, ldots, h_n$ are elements of $H$, then $I$ must assign to $f$ a function $f^{H}$ that maps $(h_1, ldots, h_n)$ to
$f^H(h_1, ldots, h_n)$ (an element of $H$).
But the variable $x$ is not in the Herbrand universe $H$, because it is not a closed term.
Thus, $v(x)$ is an element of the domain $D$ of the structure $mathcal M$, and again $v(x)$ is not an element of $H$.
answered Jan 28 at 10:41
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
$endgroup$
$begingroup$
Thank you! Clear and simple explanation!
$endgroup$
– Zarrie
Jan 28 at 11:03
$begingroup$
@Zarrie - you are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 28 at 11:41
add a comment |
$begingroup$
Let $S$ be a set of formulas (more exactly : clauses).
Let $H$ the Herbrand universe of $S$ (the domain of all ground (i.e. closed) terms) and $I$ an interpretation of $S$ over $H$.
In order that $I$ is an Herbrand model of $S$ we need that :
1) $I$ maps all constants in $S$ to themselves;
2) If $f$ is an $n$-place function symbol and $h_1, ldots, h_n$ are elements of $H$, then $I$ must assign to $f$ a function $f^{H}$ that maps $(h_1, ldots, h_n)$ to
$f^H(h_1, ldots, h_n)$ (an element of $H$).
But the variable $x$ is not in the Herbrand universe $H$, because it is not a closed term.
Thus, $v(x)$ is an element of the domain $D$ of the structure $mathcal M$, and again $v(x)$ is not an element of $H$.
answered Jan 28 at 10:41
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
$endgroup$
Let $S$ be a set of formulas (more exactly : clauses).
Let $H$ the Herbrand universe of $S$ (the domain of all ground (i.e. closed) terms) and $I$ an interpretation of $S$ over $H$.
In order that $I$ is an Herbrand model of $S$ we need that :
1) $I$ maps all constants in $S$ to themselves;
2) If $f$ is an $n$-place function symbol and $h_1, ldots, h_n$ are elements of $H$, then $I$ must assign to $f$ a function $f^{H}$ that maps $(h_1, ldots, h_n)$ to
$f^H(h_1, ldots, h_n)$ (an element of $H$).
But the variable $x$ is not in the Herbrand universe $H$, because it is not a closed term.
Thus, $v(x)$ is an element of the domain $D$ of the structure $mathcal M$, and again $v(x)$ is not an element of $H$.
answered Jan 28 at 10:41
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
edited Jan 28 at 10:50
answered Jan 28 at 10:41
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
answered Jan 28 at 10:41
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
answered Jan 28 at 10:41
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
67.5k449117
$begingroup$
Thank you! Clear and simple explanation!
$endgroup$
– Zarrie
Jan 28 at 11:03
$begingroup$
@Zarrie - you are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 28 at 11:41
add a comment |
$begingroup$
Thank you! Clear and simple explanation!
$endgroup$
– Zarrie
Jan 28 at 11:03
$begingroup$
@Zarrie - you are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 28 at 11:41
$begingroup$
Thank you! Clear and simple explanation!
$endgroup$
– Zarrie
Jan 28 at 11:03
$begingroup$
Thank you! Clear and simple explanation!
$endgroup$
– Zarrie
Jan 28 at 11:03
$begingroup$
@Zarrie - you are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 28 at 11:41
$begingroup$
@Zarrie - you are welcome :-)
$endgroup$
– Mauro ALLEGRANZA
Jan 28 at 11:41
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3090683%2fprove-that-structure-m-is-not-herbrand-structure%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
Required, but never shown
