Easy example of a herbrand structure
$begingroup$
Can someone give me an easy example of a Herbrand structure?
I can't really visualise the difference between a Herbrand and a normal structure.
logic examples-counterexamples first-order-logic predicate-logic
$endgroup$
add a comment |
$begingroup$
Can someone give me an easy example of a Herbrand structure?
I can't really visualise the difference between a Herbrand and a normal structure.
logic examples-counterexamples first-order-logic predicate-logic
$endgroup$
$begingroup$
See the post Logic - Satisfaction of a statement.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 15:46
$begingroup$
I read it but the difference is still not really clear. A structure/Interpretation for me is just a domain (non-empty set) in which we give values to non-logical symbols. ( This can be object symbols, function symbols and predicate symbols ). But I can't understand Herbrand structure intuitively even when I check multiple websites and stackposts.
$endgroup$
– Ayoub Rossi
Jan 24 at 16:00
$begingroup$
It exactly what you said : syntactical objects (like e.g. individual constants) are used also as elements of the domain of the interpretation. Thus, the term $c$ is the "name" of the object $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:29
$begingroup$
In the linked example, we have a formula that is satisfiable in an interpretation with domain having as elements the numbers $0$ and $1$ but it is not in the Herbrand structure having the domain with only one object : the constant $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:30
$begingroup$
Can you explain me shortly what a Herbrand structure is? Of course I checked thé définition on wikipedia but I don’t really get it..
$endgroup$
– Ayoub Rossi
Jan 24 at 18:37
add a comment |
$begingroup$
Can someone give me an easy example of a Herbrand structure?
I can't really visualise the difference between a Herbrand and a normal structure.
logic examples-counterexamples first-order-logic predicate-logic
$endgroup$
Can someone give me an easy example of a Herbrand structure?
I can't really visualise the difference between a Herbrand and a normal structure.
logic examples-counterexamples first-order-logic predicate-logic
logic examples-counterexamples first-order-logic predicate-logic
edited Feb 18 at 14:29
Mauro ALLEGRANZA
67.2k449115
67.2k449115
asked Jan 24 at 15:38
Ayoub RossiAyoub Rossi
11110
11110
$begingroup$
See the post Logic - Satisfaction of a statement.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 15:46
$begingroup$
I read it but the difference is still not really clear. A structure/Interpretation for me is just a domain (non-empty set) in which we give values to non-logical symbols. ( This can be object symbols, function symbols and predicate symbols ). But I can't understand Herbrand structure intuitively even when I check multiple websites and stackposts.
$endgroup$
– Ayoub Rossi
Jan 24 at 16:00
$begingroup$
It exactly what you said : syntactical objects (like e.g. individual constants) are used also as elements of the domain of the interpretation. Thus, the term $c$ is the "name" of the object $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:29
$begingroup$
In the linked example, we have a formula that is satisfiable in an interpretation with domain having as elements the numbers $0$ and $1$ but it is not in the Herbrand structure having the domain with only one object : the constant $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:30
$begingroup$
Can you explain me shortly what a Herbrand structure is? Of course I checked thé définition on wikipedia but I don’t really get it..
$endgroup$
– Ayoub Rossi
Jan 24 at 18:37
add a comment |
$begingroup$
See the post Logic - Satisfaction of a statement.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 15:46
$begingroup$
I read it but the difference is still not really clear. A structure/Interpretation for me is just a domain (non-empty set) in which we give values to non-logical symbols. ( This can be object symbols, function symbols and predicate symbols ). But I can't understand Herbrand structure intuitively even when I check multiple websites and stackposts.
$endgroup$
– Ayoub Rossi
Jan 24 at 16:00
$begingroup$
It exactly what you said : syntactical objects (like e.g. individual constants) are used also as elements of the domain of the interpretation. Thus, the term $c$ is the "name" of the object $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:29
$begingroup$
In the linked example, we have a formula that is satisfiable in an interpretation with domain having as elements the numbers $0$ and $1$ but it is not in the Herbrand structure having the domain with only one object : the constant $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:30
$begingroup$
Can you explain me shortly what a Herbrand structure is? Of course I checked thé définition on wikipedia but I don’t really get it..
$endgroup$
– Ayoub Rossi
Jan 24 at 18:37
$begingroup$
See the post Logic - Satisfaction of a statement.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 15:46
$begingroup$
See the post Logic - Satisfaction of a statement.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 15:46
$begingroup$
I read it but the difference is still not really clear. A structure/Interpretation for me is just a domain (non-empty set) in which we give values to non-logical symbols. ( This can be object symbols, function symbols and predicate symbols ). But I can't understand Herbrand structure intuitively even when I check multiple websites and stackposts.
$endgroup$
– Ayoub Rossi
Jan 24 at 16:00
$begingroup$
I read it but the difference is still not really clear. A structure/Interpretation for me is just a domain (non-empty set) in which we give values to non-logical symbols. ( This can be object symbols, function symbols and predicate symbols ). But I can't understand Herbrand structure intuitively even when I check multiple websites and stackposts.
$endgroup$
– Ayoub Rossi
Jan 24 at 16:00
$begingroup$
It exactly what you said : syntactical objects (like e.g. individual constants) are used also as elements of the domain of the interpretation. Thus, the term $c$ is the "name" of the object $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:29
$begingroup$
It exactly what you said : syntactical objects (like e.g. individual constants) are used also as elements of the domain of the interpretation. Thus, the term $c$ is the "name" of the object $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:29
$begingroup$
In the linked example, we have a formula that is satisfiable in an interpretation with domain having as elements the numbers $0$ and $1$ but it is not in the Herbrand structure having the domain with only one object : the constant $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:30
$begingroup$
In the linked example, we have a formula that is satisfiable in an interpretation with domain having as elements the numbers $0$ and $1$ but it is not in the Herbrand structure having the domain with only one object : the constant $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:30
$begingroup$
Can you explain me shortly what a Herbrand structure is? Of course I checked thé définition on wikipedia but I don’t really get it..
$endgroup$
– Ayoub Rossi
Jan 24 at 18:37
$begingroup$
Can you explain me shortly what a Herbrand structure is? Of course I checked thé définition on wikipedia but I don’t really get it..
$endgroup$
– Ayoub Rossi
Jan 24 at 18:37
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
Example
Consider the very simple FOL formula : $R(c)$.
The domain of the Herbrand structure is :
the set of all ground terms [i.e. closed terms] of the language.
In the above case, we have only the individual constant $c$ as gorund term. Thus, the domain is $H = { c }$.
With it, we define the Herbrand interpretation :
an interpretation in which all constants and function symbols are assigned very simple meanings. Specifically, every constant is interpreted as itself, and every function symbol is interpreted as the function that applies it. The interpretation also defines predicate symbols as denoting a subset of the relevant Herbrand base, effectively specifying which ground atoms are true in the interpretation. This allows the symbols in a set of clauses to be interpreted in a purely syntactic way, separated from any real instantiation.
Again, we have a very simple Herbrand inerpretation $H_S$ :
$H_S = (H, R^H)$,
where $H$ is the domain defiend above and $R^H$ is the subset of $H$ interpreting the relation symbol $R$.
Obviously, $R^H = { c }$.
$endgroup$
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%2f3086002%2feasy-example-of-a-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$
Example
Consider the very simple FOL formula : $R(c)$.
The domain of the Herbrand structure is :
the set of all ground terms [i.e. closed terms] of the language.
In the above case, we have only the individual constant $c$ as gorund term. Thus, the domain is $H = { c }$.
With it, we define the Herbrand interpretation :
an interpretation in which all constants and function symbols are assigned very simple meanings. Specifically, every constant is interpreted as itself, and every function symbol is interpreted as the function that applies it. The interpretation also defines predicate symbols as denoting a subset of the relevant Herbrand base, effectively specifying which ground atoms are true in the interpretation. This allows the symbols in a set of clauses to be interpreted in a purely syntactic way, separated from any real instantiation.
Again, we have a very simple Herbrand inerpretation $H_S$ :
$H_S = (H, R^H)$,
where $H$ is the domain defiend above and $R^H$ is the subset of $H$ interpreting the relation symbol $R$.
Obviously, $R^H = { c }$.
$endgroup$
add a comment |
$begingroup$
Example
Consider the very simple FOL formula : $R(c)$.
The domain of the Herbrand structure is :
the set of all ground terms [i.e. closed terms] of the language.
In the above case, we have only the individual constant $c$ as gorund term. Thus, the domain is $H = { c }$.
With it, we define the Herbrand interpretation :
an interpretation in which all constants and function symbols are assigned very simple meanings. Specifically, every constant is interpreted as itself, and every function symbol is interpreted as the function that applies it. The interpretation also defines predicate symbols as denoting a subset of the relevant Herbrand base, effectively specifying which ground atoms are true in the interpretation. This allows the symbols in a set of clauses to be interpreted in a purely syntactic way, separated from any real instantiation.
Again, we have a very simple Herbrand inerpretation $H_S$ :
$H_S = (H, R^H)$,
where $H$ is the domain defiend above and $R^H$ is the subset of $H$ interpreting the relation symbol $R$.
Obviously, $R^H = { c }$.
$endgroup$
add a comment |
$begingroup$
Example
Consider the very simple FOL formula : $R(c)$.
The domain of the Herbrand structure is :
the set of all ground terms [i.e. closed terms] of the language.
In the above case, we have only the individual constant $c$ as gorund term. Thus, the domain is $H = { c }$.
With it, we define the Herbrand interpretation :
an interpretation in which all constants and function symbols are assigned very simple meanings. Specifically, every constant is interpreted as itself, and every function symbol is interpreted as the function that applies it. The interpretation also defines predicate symbols as denoting a subset of the relevant Herbrand base, effectively specifying which ground atoms are true in the interpretation. This allows the symbols in a set of clauses to be interpreted in a purely syntactic way, separated from any real instantiation.
Again, we have a very simple Herbrand inerpretation $H_S$ :
$H_S = (H, R^H)$,
where $H$ is the domain defiend above and $R^H$ is the subset of $H$ interpreting the relation symbol $R$.
Obviously, $R^H = { c }$.
$endgroup$
Example
Consider the very simple FOL formula : $R(c)$.
The domain of the Herbrand structure is :
the set of all ground terms [i.e. closed terms] of the language.
In the above case, we have only the individual constant $c$ as gorund term. Thus, the domain is $H = { c }$.
With it, we define the Herbrand interpretation :
an interpretation in which all constants and function symbols are assigned very simple meanings. Specifically, every constant is interpreted as itself, and every function symbol is interpreted as the function that applies it. The interpretation also defines predicate symbols as denoting a subset of the relevant Herbrand base, effectively specifying which ground atoms are true in the interpretation. This allows the symbols in a set of clauses to be interpreted in a purely syntactic way, separated from any real instantiation.
Again, we have a very simple Herbrand inerpretation $H_S$ :
$H_S = (H, R^H)$,
where $H$ is the domain defiend above and $R^H$ is the subset of $H$ interpreting the relation symbol $R$.
Obviously, $R^H = { c }$.
answered Jan 25 at 12:20
Mauro ALLEGRANZAMauro ALLEGRANZA
67.2k449115
67.2k449115
add a comment |
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%2f3086002%2feasy-example-of-a-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
$begingroup$
See the post Logic - Satisfaction of a statement.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 15:46
$begingroup$
I read it but the difference is still not really clear. A structure/Interpretation for me is just a domain (non-empty set) in which we give values to non-logical symbols. ( This can be object symbols, function symbols and predicate symbols ). But I can't understand Herbrand structure intuitively even when I check multiple websites and stackposts.
$endgroup$
– Ayoub Rossi
Jan 24 at 16:00
$begingroup$
It exactly what you said : syntactical objects (like e.g. individual constants) are used also as elements of the domain of the interpretation. Thus, the term $c$ is the "name" of the object $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:29
$begingroup$
In the linked example, we have a formula that is satisfiable in an interpretation with domain having as elements the numbers $0$ and $1$ but it is not in the Herbrand structure having the domain with only one object : the constant $c$.
$endgroup$
– Mauro ALLEGRANZA
Jan 24 at 16:30
$begingroup$
Can you explain me shortly what a Herbrand structure is? Of course I checked thé définition on wikipedia but I don’t really get it..
$endgroup$
– Ayoub Rossi
Jan 24 at 18:37