Mixing
What is the difference between value and constant literal in first order logic syntax?
$begingroup$
In FOL, there are two values true and false;
In FOL, there are two constant literals : T and F;
Is there any difference between the both (values and constant literals)?
Can I say that true value is same as constant literal T and false value as F?
first-order-logic predicate-logic
edited Feb 18 at 11:57
Mauro ALLEGRANZA
68k449117
asked Feb 3 at 5:03
hanugmhanugm
878621
$endgroup$
add a comment |
$begingroup$
In FOL, there are two values true and false;
In FOL, there are two constant literals : T and F;
Is there any difference between the both (values and constant literals)?
Can I say that true value is same as constant literal T and false value as F?
first-order-logic predicate-logic
edited Feb 18 at 11:57
Mauro ALLEGRANZA
68k449117
asked Feb 3 at 5:03
hanugmhanugm
878621
$endgroup$
1
$begingroup$
See also the post Verum, Falsum, Atoms.
$endgroup$
– Mauro ALLEGRANZA
Feb 3 at 13:30
$begingroup$
Can you give a link to a development of FOL that includes two such constant literals? Note that's FOL, not propositional logic! Also note that an exposition where we see those two symbols doesn't suuffice; they have to be explicitly included as "constant literals" in the language.
$endgroup$
– David C. Ullrich
Feb 3 at 15:46
$begingroup$
@DavidC.Ullrich delivery.acm.org/10.1145/1800000/1795140/… Page no 2 sec 3.1
$endgroup$
– hanugm
Feb 3 at 16:53
$begingroup$
Thanks, but that just gives "An error occurred while processing your request."
$endgroup$
– David C. Ullrich
Feb 3 at 17:59
$begingroup$
@DavidC.Ullrich See the paper titled "First-Order Mixed Integer Linear Programming" by Gordon et al in google scholar
$endgroup$
– hanugm
Feb 3 at 18:03
add a comment |
$begingroup$
In FOL, there are two values true and false;
In FOL, there are two constant literals : T and F;
Is there any difference between the both (values and constant literals)?
Can I say that true value is same as constant literal T and false value as F?
first-order-logic predicate-logic
edited Feb 18 at 11:57
Mauro ALLEGRANZA
68k449117
asked Feb 3 at 5:03
hanugmhanugm
878621
$endgroup$
In FOL, there are two values true and false;
In FOL, there are two constant literals : T and F;
Is there any difference between the both (values and constant literals)?
Can I say that true value is same as constant literal T and false value as F?
first-order-logic predicate-logic
first-order-logic predicate-logic
edited Feb 18 at 11:57
Mauro ALLEGRANZA
68k449117
asked Feb 3 at 5:03
hanugmhanugm
878621
edited Feb 18 at 11:57
Mauro ALLEGRANZA
68k449117
asked Feb 3 at 5:03
hanugmhanugm
878621
edited Feb 18 at 11:57
Mauro ALLEGRANZA
68k449117
edited Feb 18 at 11:57
Mauro ALLEGRANZA
68k449117
edited Feb 18 at 11:57
Mauro ALLEGRANZA
68k449117
68k449117
asked Feb 3 at 5:03
hanugmhanugm
878621
asked Feb 3 at 5:03
hanugmhanugm
878621
asked Feb 3 at 5:03
hanugmhanugm
878621
878621
1
$begingroup$
See also the post Verum, Falsum, Atoms.
$endgroup$
– Mauro ALLEGRANZA
Feb 3 at 13:30
$begingroup$
Can you give a link to a development of FOL that includes two such constant literals? Note that's FOL, not propositional logic! Also note that an exposition where we see those two symbols doesn't suuffice; they have to be explicitly included as "constant literals" in the language.
$endgroup$
– David C. Ullrich
Feb 3 at 15:46
$begingroup$
@DavidC.Ullrich delivery.acm.org/10.1145/1800000/1795140/… Page no 2 sec 3.1
$endgroup$
– hanugm
Feb 3 at 16:53
$begingroup$
Thanks, but that just gives "An error occurred while processing your request."
$endgroup$
– David C. Ullrich
Feb 3 at 17:59
$begingroup$
@DavidC.Ullrich See the paper titled "First-Order Mixed Integer Linear Programming" by Gordon et al in google scholar
$endgroup$
– hanugm
Feb 3 at 18:03
add a comment |
1
$begingroup$
See also the post Verum, Falsum, Atoms.
$endgroup$
– Mauro ALLEGRANZA
Feb 3 at 13:30
$begingroup$
Can you give a link to a development of FOL that includes two such constant literals? Note that's FOL, not propositional logic! Also note that an exposition where we see those two symbols doesn't suuffice; they have to be explicitly included as "constant literals" in the language.
$endgroup$
– David C. Ullrich
Feb 3 at 15:46
$begingroup$
@DavidC.Ullrich delivery.acm.org/10.1145/1800000/1795140/… Page no 2 sec 3.1
$endgroup$
– hanugm
Feb 3 at 16:53
$begingroup$
Thanks, but that just gives "An error occurred while processing your request."
$endgroup$
– David C. Ullrich
Feb 3 at 17:59
$begingroup$
@DavidC.Ullrich See the paper titled "First-Order Mixed Integer Linear Programming" by Gordon et al in google scholar
$endgroup$
– hanugm
Feb 3 at 18:03
1
1
$begingroup$
See also the post Verum, Falsum, Atoms.
$endgroup$
– Mauro ALLEGRANZA
Feb 3 at 13:30
$begingroup$
See also the post Verum, Falsum, Atoms.
$endgroup$
– Mauro ALLEGRANZA
Feb 3 at 13:30
$begingroup$
Can you give a link to a development of FOL that includes two such constant literals? Note that's FOL, not propositional logic! Also note that an exposition where we see those two symbols doesn't suuffice; they have to be explicitly included as "constant literals" in the language.
$endgroup$
– David C. Ullrich
Feb 3 at 15:46
$begingroup$
Can you give a link to a development of FOL that includes two such constant literals? Note that's FOL, not propositional logic! Also note that an exposition where we see those two symbols doesn't suuffice; they have to be explicitly included as "constant literals" in the language.
$endgroup$
– David C. Ullrich
Feb 3 at 15:46
$begingroup$
@DavidC.Ullrich delivery.acm.org/10.1145/1800000/1795140/… Page no 2 sec 3.1
$endgroup$
– hanugm
Feb 3 at 16:53
$begingroup$
@DavidC.Ullrich delivery.acm.org/10.1145/1800000/1795140/… Page no 2 sec 3.1
$endgroup$
– hanugm
Feb 3 at 16:53
$begingroup$
Thanks, but that just gives "An error occurred while processing your request."
$endgroup$
– David C. Ullrich
Feb 3 at 17:59
$begingroup$
Thanks, but that just gives "An error occurred while processing your request."
$endgroup$
– David C. Ullrich
Feb 3 at 17:59
$begingroup$
@DavidC.Ullrich See the paper titled "First-Order Mixed Integer Linear Programming" by Gordon et al in google scholar
$endgroup$
– hanugm
Feb 3 at 18:03
$begingroup$
@DavidC.Ullrich See the paper titled "First-Order Mixed Integer Linear Programming" by Gordon et al in google scholar
$endgroup$
– hanugm
Feb 3 at 18:03
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
The constant literals $text T$ and $text F$ are symbols of the language (also used : $top$ and $bot$).
The truth-values TRUE and FALSE are "objects" : they are e.g. the only two objects used in the domain of interpretation (the "boolean world" of the classical propositional calculus.
Obviously, the constant literals are constant; i.e. interpretations will always assign to the syntactical objects $text T, text F$ the truth-values TRUE and FALSE respectively.
Usually, the two symbols above are intrduced in propositional calculus.
$bot$ can be used to define negation as : $A to bot$ and obviously $top$ can be defined as $bot to bot$.
But we can develop FOL also with propositional symbols, i.e. $0$-ary predicate symbols, and the propositional constant $bot$.
See e.g. Dirk van Dalen, Logic and Structure, page 57.
In this case (see page 66), an interpretation of the sentences $varphi$ of the language in a structure $mathfrak A$ is a mapping to ${ 0, 1 }$, satisfying (inter alia) the condition $[⊥]^{mathfrak A} = 0$.
answered Feb 3 at 9:07
Mauro ALLEGRANZAMauro ALLEGRANZA
68k449117
$endgroup$
$begingroup$
I believe this is simply wrong. In FOL the interpretation of a constant is an element of the "domain". See my answer...
$endgroup$
– David C. Ullrich
Feb 3 at 15:25
$begingroup$
(In that link you provided they're said to be atomic formmulae, or 0-ary connectives. II think it's clear that they're talking about propositional logic there; in any case an atomic formula in FOL,, if there is such a thing, is certainly not a "constant literal"..)
$endgroup$
– David C. Ullrich
Feb 3 at 15:32
$begingroup$
I see you mentioned propositional logic and didn't mention FOL. My claim that this is simply wrong is referring to the idea that T and F are "constant literals" in FOL.
$endgroup$
– David C. Ullrich
Feb 3 at 15:48
$begingroup$
"But we can develop FOL also with propositional symbols, i.e. 00-ary predicate symbolsy. See van Dalen, Logic and Structure, page 57." And sure enough, the propositional symbols there are not "constant symbols". Two separate categories.
$endgroup$
– David C. Ullrich
Feb 3 at 18:09
add a comment |
$begingroup$
No, there are no such "constant literals" in FOL. There may be such symbols used when we talk about FOL, but they are certainly not part of the language of FOL. (The interpretation of a constant literal in a model of a theory in FOL is an element of the "universe" of the model; that makes no sense for $T$ and $F$.)
In case that's not clear, an example. Consider $mathcal T$, the first-order theory of groups. We can do that without a constant symbol for the identity, or if we wish we can include a constant literal $e$, so we could have an axiom $$forall x(ex=xe=x)$$in place of the constant-free $$exists yforall x(yx=xy=x).$$
Suppose we do include a constant symbol $e$. Now a model of $mathcal T$ is exactly a group, and if $G$ is a group the interpretation of $e$ is just the identity element of $G$. If there is a constant literal $T$, what element of $G$ would be the interpretation of $T$?
Or consider the first-order theory of ordered fields, with, among other things, constant symbols $0$ and $1$ and a binary predicate $ge$. If $c$ is a constant literal the sentence $forall x(xxge c)$ makes sense; in fact it's a theorem if $c$ is $0$ and an anti-theorem if $c$ is $1$. What does that sentence "mean" is $c$ is $T$?
(One could have constant literals T and F in propositional logic...)
answered Feb 3 at 15:24
David C. UllrichDavid C. Ullrich
61.8k44095
$endgroup$
add a comment |
Your Answer
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%2f3098200%2fwhat-is-the-difference-between-value-and-constant-literal-in-first-order-logic-s%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
The constant literals $text T$ and $text F$ are symbols of the language (also used : $top$ and $bot$).
The truth-values TRUE and FALSE are "objects" : they are e.g. the only two objects used in the domain of interpretation (the "boolean world" of the classical propositional calculus.
Obviously, the constant literals are constant; i.e. interpretations will always assign to the syntactical objects $text T, text F$ the truth-values TRUE and FALSE respectively.
Usually, the two symbols above are intrduced in propositional calculus.
$bot$ can be used to define negation as : $A to bot$ and obviously $top$ can be defined as $bot to bot$.
But we can develop FOL also with propositional symbols, i.e. $0$-ary predicate symbols, and the propositional constant $bot$.
See e.g. Dirk van Dalen, Logic and Structure, page 57.
In this case (see page 66), an interpretation of the sentences $varphi$ of the language in a structure $mathfrak A$ is a mapping to ${ 0, 1 }$, satisfying (inter alia) the condition $[⊥]^{mathfrak A} = 0$.
answered Feb 3 at 9:07
Mauro ALLEGRANZAMauro ALLEGRANZA
68k449117
$endgroup$
$begingroup$
I believe this is simply wrong. In FOL the interpretation of a constant is an element of the "domain". See my answer...
$endgroup$
– David C. Ullrich
Feb 3 at 15:25
$begingroup$
(In that link you provided they're said to be atomic formmulae, or 0-ary connectives. II think it's clear that they're talking about propositional logic there; in any case an atomic formula in FOL,, if there is such a thing, is certainly not a "constant literal"..)
$endgroup$
– David C. Ullrich
Feb 3 at 15:32
$begingroup$
I see you mentioned propositional logic and didn't mention FOL. My claim that this is simply wrong is referring to the idea that T and F are "constant literals" in FOL.
$endgroup$
– David C. Ullrich
Feb 3 at 15:48
$begingroup$
"But we can develop FOL also with propositional symbols, i.e. 00-ary predicate symbolsy. See van Dalen, Logic and Structure, page 57." And sure enough, the propositional symbols there are not "constant symbols". Two separate categories.
$endgroup$
– David C. Ullrich
Feb 3 at 18:09
add a comment |
$begingroup$
The constant literals $text T$ and $text F$ are symbols of the language (also used : $top$ and $bot$).
The truth-values TRUE and FALSE are "objects" : they are e.g. the only two objects used in the domain of interpretation (the "boolean world" of the classical propositional calculus.
Obviously, the constant literals are constant; i.e. interpretations will always assign to the syntactical objects $text T, text F$ the truth-values TRUE and FALSE respectively.
Usually, the two symbols above are intrduced in propositional calculus.
$bot$ can be used to define negation as : $A to bot$ and obviously $top$ can be defined as $bot to bot$.
But we can develop FOL also with propositional symbols, i.e. $0$-ary predicate symbols, and the propositional constant $bot$.
See e.g. Dirk van Dalen, Logic and Structure, page 57.
In this case (see page 66), an interpretation of the sentences $varphi$ of the language in a structure $mathfrak A$ is a mapping to ${ 0, 1 }$, satisfying (inter alia) the condition $[⊥]^{mathfrak A} = 0$.
answered Feb 3 at 9:07
Mauro ALLEGRANZAMauro ALLEGRANZA
68k449117
$endgroup$
$begingroup$
I believe this is simply wrong. In FOL the interpretation of a constant is an element of the "domain". See my answer...
$endgroup$
– David C. Ullrich
Feb 3 at 15:25
$begingroup$
(In that link you provided they're said to be atomic formmulae, or 0-ary connectives. II think it's clear that they're talking about propositional logic there; in any case an atomic formula in FOL,, if there is such a thing, is certainly not a "constant literal"..)
$endgroup$
– David C. Ullrich
Feb 3 at 15:32
$begingroup$
I see you mentioned propositional logic and didn't mention FOL. My claim that this is simply wrong is referring to the idea that T and F are "constant literals" in FOL.
$endgroup$
– David C. Ullrich
Feb 3 at 15:48
$begingroup$
"But we can develop FOL also with propositional symbols, i.e. 00-ary predicate symbolsy. See van Dalen, Logic and Structure, page 57." And sure enough, the propositional symbols there are not "constant symbols". Two separate categories.
$endgroup$
– David C. Ullrich
Feb 3 at 18:09
add a comment |
$begingroup$
The constant literals $text T$ and $text F$ are symbols of the language (also used : $top$ and $bot$).
The truth-values TRUE and FALSE are "objects" : they are e.g. the only two objects used in the domain of interpretation (the "boolean world" of the classical propositional calculus.
Obviously, the constant literals are constant; i.e. interpretations will always assign to the syntactical objects $text T, text F$ the truth-values TRUE and FALSE respectively.
Usually, the two symbols above are intrduced in propositional calculus.
$bot$ can be used to define negation as : $A to bot$ and obviously $top$ can be defined as $bot to bot$.
But we can develop FOL also with propositional symbols, i.e. $0$-ary predicate symbols, and the propositional constant $bot$.
See e.g. Dirk van Dalen, Logic and Structure, page 57.
In this case (see page 66), an interpretation of the sentences $varphi$ of the language in a structure $mathfrak A$ is a mapping to ${ 0, 1 }$, satisfying (inter alia) the condition $[⊥]^{mathfrak A} = 0$.
answered Feb 3 at 9:07
Mauro ALLEGRANZAMauro ALLEGRANZA
68k449117
$endgroup$
The constant literals $text T$ and $text F$ are symbols of the language (also used : $top$ and $bot$).
The truth-values TRUE and FALSE are "objects" : they are e.g. the only two objects used in the domain of interpretation (the "boolean world" of the classical propositional calculus.
Obviously, the constant literals are constant; i.e. interpretations will always assign to the syntactical objects $text T, text F$ the truth-values TRUE and FALSE respectively.
Usually, the two symbols above are intrduced in propositional calculus.
$bot$ can be used to define negation as : $A to bot$ and obviously $top$ can be defined as $bot to bot$.
But we can develop FOL also with propositional symbols, i.e. $0$-ary predicate symbols, and the propositional constant $bot$.
See e.g. Dirk van Dalen, Logic and Structure, page 57.
In this case (see page 66), an interpretation of the sentences $varphi$ of the language in a structure $mathfrak A$ is a mapping to ${ 0, 1 }$, satisfying (inter alia) the condition $[⊥]^{mathfrak A} = 0$.
answered Feb 3 at 9:07
Mauro ALLEGRANZAMauro ALLEGRANZA
68k449117
edited Feb 3 at 18:12
answered Feb 3 at 9:07
Mauro ALLEGRANZAMauro ALLEGRANZA
68k449117
answered Feb 3 at 9:07
Mauro ALLEGRANZAMauro ALLEGRANZA
68k449117
answered Feb 3 at 9:07
Mauro ALLEGRANZAMauro ALLEGRANZA
68k449117
68k449117
$begingroup$
I believe this is simply wrong. In FOL the interpretation of a constant is an element of the "domain". See my answer...
$endgroup$
– David C. Ullrich
Feb 3 at 15:25
$begingroup$
(In that link you provided they're said to be atomic formmulae, or 0-ary connectives. II think it's clear that they're talking about propositional logic there; in any case an atomic formula in FOL,, if there is such a thing, is certainly not a "constant literal"..)
$endgroup$
– David C. Ullrich
Feb 3 at 15:32
$begingroup$
I see you mentioned propositional logic and didn't mention FOL. My claim that this is simply wrong is referring to the idea that T and F are "constant literals" in FOL.
$endgroup$
– David C. Ullrich
Feb 3 at 15:48
$begingroup$
"But we can develop FOL also with propositional symbols, i.e. 00-ary predicate symbolsy. See van Dalen, Logic and Structure, page 57." And sure enough, the propositional symbols there are not "constant symbols". Two separate categories.
$endgroup$
– David C. Ullrich
Feb 3 at 18:09
add a comment |
$begingroup$
I believe this is simply wrong. In FOL the interpretation of a constant is an element of the "domain". See my answer...
$endgroup$
– David C. Ullrich
Feb 3 at 15:25
$begingroup$
(In that link you provided they're said to be atomic formmulae, or 0-ary connectives. II think it's clear that they're talking about propositional logic there; in any case an atomic formula in FOL,, if there is such a thing, is certainly not a "constant literal"..)
$endgroup$
– David C. Ullrich
Feb 3 at 15:32
$begingroup$
I see you mentioned propositional logic and didn't mention FOL. My claim that this is simply wrong is referring to the idea that T and F are "constant literals" in FOL.
$endgroup$
– David C. Ullrich
Feb 3 at 15:48
$begingroup$
"But we can develop FOL also with propositional symbols, i.e. 00-ary predicate symbolsy. See van Dalen, Logic and Structure, page 57." And sure enough, the propositional symbols there are not "constant symbols". Two separate categories.
$endgroup$
– David C. Ullrich
Feb 3 at 18:09
$begingroup$
I believe this is simply wrong. In FOL the interpretation of a constant is an element of the "domain". See my answer...
$endgroup$
– David C. Ullrich
Feb 3 at 15:25
$begingroup$
I believe this is simply wrong. In FOL the interpretation of a constant is an element of the "domain". See my answer...
$endgroup$
– David C. Ullrich
Feb 3 at 15:25
$begingroup$
(In that link you provided they're said to be atomic formmulae, or 0-ary connectives. II think it's clear that they're talking about propositional logic there; in any case an atomic formula in FOL,, if there is such a thing, is certainly not a "constant literal"..)
$endgroup$
– David C. Ullrich
Feb 3 at 15:32
$begingroup$
(In that link you provided they're said to be atomic formmulae, or 0-ary connectives. II think it's clear that they're talking about propositional logic there; in any case an atomic formula in FOL,, if there is such a thing, is certainly not a "constant literal"..)
$endgroup$
– David C. Ullrich
Feb 3 at 15:32
$begingroup$
I see you mentioned propositional logic and didn't mention FOL. My claim that this is simply wrong is referring to the idea that T and F are "constant literals" in FOL.
$endgroup$
– David C. Ullrich
Feb 3 at 15:48
$begingroup$
I see you mentioned propositional logic and didn't mention FOL. My claim that this is simply wrong is referring to the idea that T and F are "constant literals" in FOL.
$endgroup$
– David C. Ullrich
Feb 3 at 15:48
$begingroup$
"But we can develop FOL also with propositional symbols, i.e. 00-ary predicate symbolsy. See van Dalen, Logic and Structure, page 57." And sure enough, the propositional symbols there are not "constant symbols". Two separate categories.
$endgroup$
– David C. Ullrich
Feb 3 at 18:09
$begingroup$
"But we can develop FOL also with propositional symbols, i.e. 00-ary predicate symbolsy. See van Dalen, Logic and Structure, page 57." And sure enough, the propositional symbols there are not "constant symbols". Two separate categories.
$endgroup$
– David C. Ullrich
Feb 3 at 18:09
add a comment |
$begingroup$
No, there are no such "constant literals" in FOL. There may be such symbols used when we talk about FOL, but they are certainly not part of the language of FOL. (The interpretation of a constant literal in a model of a theory in FOL is an element of the "universe" of the model; that makes no sense for $T$ and $F$.)
In case that's not clear, an example. Consider $mathcal T$, the first-order theory of groups. We can do that without a constant symbol for the identity, or if we wish we can include a constant literal $e$, so we could have an axiom $$forall x(ex=xe=x)$$in place of the constant-free $$exists yforall x(yx=xy=x).$$
Suppose we do include a constant symbol $e$. Now a model of $mathcal T$ is exactly a group, and if $G$ is a group the interpretation of $e$ is just the identity element of $G$. If there is a constant literal $T$, what element of $G$ would be the interpretation of $T$?
Or consider the first-order theory of ordered fields, with, among other things, constant symbols $0$ and $1$ and a binary predicate $ge$. If $c$ is a constant literal the sentence $forall x(xxge c)$ makes sense; in fact it's a theorem if $c$ is $0$ and an anti-theorem if $c$ is $1$. What does that sentence "mean" is $c$ is $T$?
(One could have constant literals T and F in propositional logic...)
answered Feb 3 at 15:24
David C. UllrichDavid C. Ullrich
61.8k44095
$endgroup$
add a comment |
$begingroup$
No, there are no such "constant literals" in FOL. There may be such symbols used when we talk about FOL, but they are certainly not part of the language of FOL. (The interpretation of a constant literal in a model of a theory in FOL is an element of the "universe" of the model; that makes no sense for $T$ and $F$.)
In case that's not clear, an example. Consider $mathcal T$, the first-order theory of groups. We can do that without a constant symbol for the identity, or if we wish we can include a constant literal $e$, so we could have an axiom $$forall x(ex=xe=x)$$in place of the constant-free $$exists yforall x(yx=xy=x).$$
Suppose we do include a constant symbol $e$. Now a model of $mathcal T$ is exactly a group, and if $G$ is a group the interpretation of $e$ is just the identity element of $G$. If there is a constant literal $T$, what element of $G$ would be the interpretation of $T$?
Or consider the first-order theory of ordered fields, with, among other things, constant symbols $0$ and $1$ and a binary predicate $ge$. If $c$ is a constant literal the sentence $forall x(xxge c)$ makes sense; in fact it's a theorem if $c$ is $0$ and an anti-theorem if $c$ is $1$. What does that sentence "mean" is $c$ is $T$?
(One could have constant literals T and F in propositional logic...)
answered Feb 3 at 15:24
David C. UllrichDavid C. Ullrich
61.8k44095
$endgroup$
add a comment |
$begingroup$
No, there are no such "constant literals" in FOL. There may be such symbols used when we talk about FOL, but they are certainly not part of the language of FOL. (The interpretation of a constant literal in a model of a theory in FOL is an element of the "universe" of the model; that makes no sense for $T$ and $F$.)
In case that's not clear, an example. Consider $mathcal T$, the first-order theory of groups. We can do that without a constant symbol for the identity, or if we wish we can include a constant literal $e$, so we could have an axiom $$forall x(ex=xe=x)$$in place of the constant-free $$exists yforall x(yx=xy=x).$$
Suppose we do include a constant symbol $e$. Now a model of $mathcal T$ is exactly a group, and if $G$ is a group the interpretation of $e$ is just the identity element of $G$. If there is a constant literal $T$, what element of $G$ would be the interpretation of $T$?
Or consider the first-order theory of ordered fields, with, among other things, constant symbols $0$ and $1$ and a binary predicate $ge$. If $c$ is a constant literal the sentence $forall x(xxge c)$ makes sense; in fact it's a theorem if $c$ is $0$ and an anti-theorem if $c$ is $1$. What does that sentence "mean" is $c$ is $T$?
(One could have constant literals T and F in propositional logic...)
answered Feb 3 at 15:24
David C. UllrichDavid C. Ullrich
61.8k44095
$endgroup$
No, there are no such "constant literals" in FOL. There may be such symbols used when we talk about FOL, but they are certainly not part of the language of FOL. (The interpretation of a constant literal in a model of a theory in FOL is an element of the "universe" of the model; that makes no sense for $T$ and $F$.)
In case that's not clear, an example. Consider $mathcal T$, the first-order theory of groups. We can do that without a constant symbol for the identity, or if we wish we can include a constant literal $e$, so we could have an axiom $$forall x(ex=xe=x)$$in place of the constant-free $$exists yforall x(yx=xy=x).$$
Suppose we do include a constant symbol $e$. Now a model of $mathcal T$ is exactly a group, and if $G$ is a group the interpretation of $e$ is just the identity element of $G$. If there is a constant literal $T$, what element of $G$ would be the interpretation of $T$?
Or consider the first-order theory of ordered fields, with, among other things, constant symbols $0$ and $1$ and a binary predicate $ge$. If $c$ is a constant literal the sentence $forall x(xxge c)$ makes sense; in fact it's a theorem if $c$ is $0$ and an anti-theorem if $c$ is $1$. What does that sentence "mean" is $c$ is $T$?
(One could have constant literals T and F in propositional logic...)
answered Feb 3 at 15:24
David C. UllrichDavid C. Ullrich
61.8k44095
edited Feb 3 at 16:30
answered Feb 3 at 15:24
David C. UllrichDavid C. Ullrich
61.8k44095
answered Feb 3 at 15:24
David C. UllrichDavid C. Ullrich
61.8k44095
answered Feb 3 at 15:24
David C. UllrichDavid C. Ullrich
61.8k44095
61.8k44095
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%2f3098200%2fwhat-is-the-difference-between-value-and-constant-literal-in-first-order-logic-s%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
1
$begingroup$
See also the post Verum, Falsum, Atoms.
$endgroup$
– Mauro ALLEGRANZA
Feb 3 at 13:30
$begingroup$
Can you give a link to a development of FOL that includes two such constant literals? Note that's FOL, not propositional logic! Also note that an exposition where we see those two symbols doesn't suuffice; they have to be explicitly included as "constant literals" in the language.
$endgroup$
– David C. Ullrich
Feb 3 at 15:46
$begingroup$
@DavidC.Ullrich delivery.acm.org/10.1145/1800000/1795140/… Page no 2 sec 3.1
$endgroup$
– hanugm
Feb 3 at 16:53
$begingroup$
Thanks, but that just gives "An error occurred while processing your request."
$endgroup$
– David C. Ullrich
Feb 3 at 17:59
$begingroup$
@DavidC.Ullrich See the paper titled "First-Order Mixed Integer Linear Programming" by Gordon et al in google scholar
$endgroup$
– hanugm
Feb 3 at 18:03