Mixing
Is it possible to have equality in the body or head of the implication of the first order logic?
Clash Royale CLAN TAG#URR8PPP
up vote
1
down vote
favorite
I am confused a bit, is the following formul a syntactically valid formula of first order logic?
is_VAT_taxable_good(milk) ->
price_with_VAT(good)=price(good)+apply_highest_VAT_rate(price(good))
where
is_VAT_taxable_good(...) - predicate
pricate_with_VAT, price, apply_highest_VAT_rate, ...+... - functions
good - constant
(the language of first order logic, of course, allows to use funnctions inside terms). So - is my initial implication a syntactically valid first order formula (wrt the language with the mentioned functions, variables and constants). If it is not syntactically valid formula, then what is wrong with it and how differently and in right manner I can express the same implication?
Or maybe I should make distinction between logical equality of first order logic and my own custom equality that I can define on two terms as custom 2-ary function e.g. =(..., ...). If that is the case the in which situations should I define such custom equality function and in which situations I can use the build in FOL equality? Is there theory of such custom equality in FOL?
logic first-order-logic formal-languages
asked Jul 30 at 21:33
TomR
256312
add a comment |Â
up vote
1
down vote
favorite
I am confused a bit, is the following formul a syntactically valid formula of first order logic?
is_VAT_taxable_good(milk) ->
price_with_VAT(good)=price(good)+apply_highest_VAT_rate(price(good))
where
is_VAT_taxable_good(...) - predicate
pricate_with_VAT, price, apply_highest_VAT_rate, ...+... - functions
good - constant
(the language of first order logic, of course, allows to use funnctions inside terms). So - is my initial implication a syntactically valid first order formula (wrt the language with the mentioned functions, variables and constants). If it is not syntactically valid formula, then what is wrong with it and how differently and in right manner I can express the same implication?
Or maybe I should make distinction between logical equality of first order logic and my own custom equality that I can define on two terms as custom 2-ary function e.g. =(..., ...). If that is the case the in which situations should I define such custom equality function and in which situations I can use the build in FOL equality? Is there theory of such custom equality in FOL?
logic first-order-logic formal-languages
asked Jul 30 at 21:33
TomR
256312
6
Equality is a binary predicate. Any predicate, fully applied, is a formula. Implication is a connective that combines two formulas. There is no restriction on what formulas implication combines in FOL.
– Derek Elkins
Jul 30 at 21:47
add a comment |Â
up vote
1
down vote
favorite
up vote
1
down vote
favorite
I am confused a bit, is the following formul a syntactically valid formula of first order logic?
is_VAT_taxable_good(milk) ->
price_with_VAT(good)=price(good)+apply_highest_VAT_rate(price(good))
where
is_VAT_taxable_good(...) - predicate
pricate_with_VAT, price, apply_highest_VAT_rate, ...+... - functions
good - constant
(the language of first order logic, of course, allows to use funnctions inside terms). So - is my initial implication a syntactically valid first order formula (wrt the language with the mentioned functions, variables and constants). If it is not syntactically valid formula, then what is wrong with it and how differently and in right manner I can express the same implication?
Or maybe I should make distinction between logical equality of first order logic and my own custom equality that I can define on two terms as custom 2-ary function e.g. =(..., ...). If that is the case the in which situations should I define such custom equality function and in which situations I can use the build in FOL equality? Is there theory of such custom equality in FOL?
logic first-order-logic formal-languages
asked Jul 30 at 21:33
TomR
256312
I am confused a bit, is the following formul a syntactically valid formula of first order logic?
is_VAT_taxable_good(milk) ->
price_with_VAT(good)=price(good)+apply_highest_VAT_rate(price(good))
where
is_VAT_taxable_good(...) - predicate
pricate_with_VAT, price, apply_highest_VAT_rate, ...+... - functions
good - constant
(the language of first order logic, of course, allows to use funnctions inside terms). So - is my initial implication a syntactically valid first order formula (wrt the language with the mentioned functions, variables and constants). If it is not syntactically valid formula, then what is wrong with it and how differently and in right manner I can express the same implication?
Or maybe I should make distinction between logical equality of first order logic and my own custom equality that I can define on two terms as custom 2-ary function e.g. =(..., ...). If that is the case the in which situations should I define such custom equality function and in which situations I can use the build in FOL equality? Is there theory of such custom equality in FOL?
logic first-order-logic formal-languages
asked Jul 30 at 21:33
TomR
256312
edited Jul 30 at 21:38
asked Jul 30 at 21:33
TomR
256312
asked Jul 30 at 21:33
TomR
256312
asked Jul 30 at 21:33
TomR
256312
256312
6
Equality is a binary predicate. Any predicate, fully applied, is a formula. Implication is a connective that combines two formulas. There is no restriction on what formulas implication combines in FOL.
– Derek Elkins
Jul 30 at 21:47
add a comment |Â
6
Equality is a binary predicate. Any predicate, fully applied, is a formula. Implication is a connective that combines two formulas. There is no restriction on what formulas implication combines in FOL.
– Derek Elkins
Jul 30 at 21:47
6
6
Equality is a binary predicate. Any predicate, fully applied, is a formula. Implication is a connective that combines two formulas. There is no restriction on what formulas implication combines in FOL.
– Derek Elkins
Jul 30 at 21:47
Equality is a binary predicate. Any predicate, fully applied, is a formula. Implication is a connective that combines two formulas. There is no restriction on what formulas implication combines in FOL.
– Derek Elkins
Jul 30 at 21:47
add a comment |Â
1 Answer
1
active
oldest
votes
up vote
1
down vote
accepted
Your formula looks fine, as your implication, as @Derek Elkins said, combines validly built atomic formulas together, while these are in turn formed using the equality relation and a function applied to good, whatever this represents in your underlying language.
In think the second concern/question about equality or the equality symbol $=$ is a little more engaging. First, you should note that on a syntactical level, that is on the formal language level of first order logic, $=$ is just a symbol, initially with no attached meaning. The meaning is supplied via semantics. In first order logic, one often differentiates between first order logic with equality and first order logic without equality.
FO with equality incorporates $=$ as a prime symbol into the signature/language and forces its interpretation in a model $mathfrakM=langle M,dotsrangle$ to be an object equality, i.e. (without getting into too much formalism) the syntactical structure $a=b$ with variables(or constants, terms) $a,b$ is true under an interpretation if the objects of $M$ assigned to $a$ and $b$ are the same, i.e. are equal on the meta-level.
FO without equality essentially omits this concept as a primitve. The reasons for distinction is largely historic and I omit any further details now.
What I think is more important, is that of course you can add a relation symbol to the signature/language as a custom equality symbol and enforce some kind of behaviour by restricting the desired models to those having the corresponding properties, e.g. through a corresponding axiomatization of a desired model class, that is you may specify the class of models you want to consider as the models of some set of first order sentences:
Say you might want to create another type of equality in some context, written syntactically in the formal language as $equiv$ for which you may ask different properties from, e.g. transitive behaviour
$$forall xforall yforall z:xequiv yrightarrow(yequiv zrightarrow xequiv z)$$
Classical equality as perceived e.g. in mathematics of course has other properties as well like symmetry etc., which you may omit or add depending on whatever you try to model(where model is a great descriptor, as you restrict the class of models to those already satisfying your required properties).
Since it seems that your question comes from a more applied background, let me end with that it depends largely on what you try to model and how you want to model it, but you may always, and this is the great strength and diversity of FO compared to e.g. (in a drastic way) classical propositional logic, specify a signature of symbols representing functions and relations for some scenario for which you then can specify semantic properties syntactically through corresponding formulas.
EDIT: I'm sorry if I drove off a little bit, concerning your question I was not sure if you asked for soft discussion, elaboration of a concept or a more formal treatment of these questions.
answered Jul 30 at 23:45
zzuussee
1,172419
add a comment |Â
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
1
down vote
accepted
Your formula looks fine, as your implication, as @Derek Elkins said, combines validly built atomic formulas together, while these are in turn formed using the equality relation and a function applied to good, whatever this represents in your underlying language.
In think the second concern/question about equality or the equality symbol $=$ is a little more engaging. First, you should note that on a syntactical level, that is on the formal language level of first order logic, $=$ is just a symbol, initially with no attached meaning. The meaning is supplied via semantics. In first order logic, one often differentiates between first order logic with equality and first order logic without equality.
FO with equality incorporates $=$ as a prime symbol into the signature/language and forces its interpretation in a model $mathfrakM=langle M,dotsrangle$ to be an object equality, i.e. (without getting into too much formalism) the syntactical structure $a=b$ with variables(or constants, terms) $a,b$ is true under an interpretation if the objects of $M$ assigned to $a$ and $b$ are the same, i.e. are equal on the meta-level.
FO without equality essentially omits this concept as a primitve. The reasons for distinction is largely historic and I omit any further details now.
What I think is more important, is that of course you can add a relation symbol to the signature/language as a custom equality symbol and enforce some kind of behaviour by restricting the desired models to those having the corresponding properties, e.g. through a corresponding axiomatization of a desired model class, that is you may specify the class of models you want to consider as the models of some set of first order sentences:
Say you might want to create another type of equality in some context, written syntactically in the formal language as $equiv$ for which you may ask different properties from, e.g. transitive behaviour
$$forall xforall yforall z:xequiv yrightarrow(yequiv zrightarrow xequiv z)$$
Classical equality as perceived e.g. in mathematics of course has other properties as well like symmetry etc., which you may omit or add depending on whatever you try to model(where model is a great descriptor, as you restrict the class of models to those already satisfying your required properties).
Since it seems that your question comes from a more applied background, let me end with that it depends largely on what you try to model and how you want to model it, but you may always, and this is the great strength and diversity of FO compared to e.g. (in a drastic way) classical propositional logic, specify a signature of symbols representing functions and relations for some scenario for which you then can specify semantic properties syntactically through corresponding formulas.
EDIT: I'm sorry if I drove off a little bit, concerning your question I was not sure if you asked for soft discussion, elaboration of a concept or a more formal treatment of these questions.
answered Jul 30 at 23:45
zzuussee
1,172419
add a comment |Â
up vote
1
down vote
accepted
Your formula looks fine, as your implication, as @Derek Elkins said, combines validly built atomic formulas together, while these are in turn formed using the equality relation and a function applied to good, whatever this represents in your underlying language.
In think the second concern/question about equality or the equality symbol $=$ is a little more engaging. First, you should note that on a syntactical level, that is on the formal language level of first order logic, $=$ is just a symbol, initially with no attached meaning. The meaning is supplied via semantics. In first order logic, one often differentiates between first order logic with equality and first order logic without equality.
FO with equality incorporates $=$ as a prime symbol into the signature/language and forces its interpretation in a model $mathfrakM=langle M,dotsrangle$ to be an object equality, i.e. (without getting into too much formalism) the syntactical structure $a=b$ with variables(or constants, terms) $a,b$ is true under an interpretation if the objects of $M$ assigned to $a$ and $b$ are the same, i.e. are equal on the meta-level.
FO without equality essentially omits this concept as a primitve. The reasons for distinction is largely historic and I omit any further details now.
What I think is more important, is that of course you can add a relation symbol to the signature/language as a custom equality symbol and enforce some kind of behaviour by restricting the desired models to those having the corresponding properties, e.g. through a corresponding axiomatization of a desired model class, that is you may specify the class of models you want to consider as the models of some set of first order sentences:
Say you might want to create another type of equality in some context, written syntactically in the formal language as $equiv$ for which you may ask different properties from, e.g. transitive behaviour
$$forall xforall yforall z:xequiv yrightarrow(yequiv zrightarrow xequiv z)$$
Classical equality as perceived e.g. in mathematics of course has other properties as well like symmetry etc., which you may omit or add depending on whatever you try to model(where model is a great descriptor, as you restrict the class of models to those already satisfying your required properties).
Since it seems that your question comes from a more applied background, let me end with that it depends largely on what you try to model and how you want to model it, but you may always, and this is the great strength and diversity of FO compared to e.g. (in a drastic way) classical propositional logic, specify a signature of symbols representing functions and relations for some scenario for which you then can specify semantic properties syntactically through corresponding formulas.
EDIT: I'm sorry if I drove off a little bit, concerning your question I was not sure if you asked for soft discussion, elaboration of a concept or a more formal treatment of these questions.
answered Jul 30 at 23:45
zzuussee
1,172419
add a comment |Â
up vote
1
down vote
accepted
up vote
1
down vote
accepted
Your formula looks fine, as your implication, as @Derek Elkins said, combines validly built atomic formulas together, while these are in turn formed using the equality relation and a function applied to good, whatever this represents in your underlying language.
In think the second concern/question about equality or the equality symbol $=$ is a little more engaging. First, you should note that on a syntactical level, that is on the formal language level of first order logic, $=$ is just a symbol, initially with no attached meaning. The meaning is supplied via semantics. In first order logic, one often differentiates between first order logic with equality and first order logic without equality.
FO with equality incorporates $=$ as a prime symbol into the signature/language and forces its interpretation in a model $mathfrakM=langle M,dotsrangle$ to be an object equality, i.e. (without getting into too much formalism) the syntactical structure $a=b$ with variables(or constants, terms) $a,b$ is true under an interpretation if the objects of $M$ assigned to $a$ and $b$ are the same, i.e. are equal on the meta-level.
FO without equality essentially omits this concept as a primitve. The reasons for distinction is largely historic and I omit any further details now.
What I think is more important, is that of course you can add a relation symbol to the signature/language as a custom equality symbol and enforce some kind of behaviour by restricting the desired models to those having the corresponding properties, e.g. through a corresponding axiomatization of a desired model class, that is you may specify the class of models you want to consider as the models of some set of first order sentences:
Say you might want to create another type of equality in some context, written syntactically in the formal language as $equiv$ for which you may ask different properties from, e.g. transitive behaviour
$$forall xforall yforall z:xequiv yrightarrow(yequiv zrightarrow xequiv z)$$
Classical equality as perceived e.g. in mathematics of course has other properties as well like symmetry etc., which you may omit or add depending on whatever you try to model(where model is a great descriptor, as you restrict the class of models to those already satisfying your required properties).
Since it seems that your question comes from a more applied background, let me end with that it depends largely on what you try to model and how you want to model it, but you may always, and this is the great strength and diversity of FO compared to e.g. (in a drastic way) classical propositional logic, specify a signature of symbols representing functions and relations for some scenario for which you then can specify semantic properties syntactically through corresponding formulas.
EDIT: I'm sorry if I drove off a little bit, concerning your question I was not sure if you asked for soft discussion, elaboration of a concept or a more formal treatment of these questions.
answered Jul 30 at 23:45
zzuussee
1,172419
Your formula looks fine, as your implication, as @Derek Elkins said, combines validly built atomic formulas together, while these are in turn formed using the equality relation and a function applied to good, whatever this represents in your underlying language.
In think the second concern/question about equality or the equality symbol $=$ is a little more engaging. First, you should note that on a syntactical level, that is on the formal language level of first order logic, $=$ is just a symbol, initially with no attached meaning. The meaning is supplied via semantics. In first order logic, one often differentiates between first order logic with equality and first order logic without equality.
FO with equality incorporates $=$ as a prime symbol into the signature/language and forces its interpretation in a model $mathfrakM=langle M,dotsrangle$ to be an object equality, i.e. (without getting into too much formalism) the syntactical structure $a=b$ with variables(or constants, terms) $a,b$ is true under an interpretation if the objects of $M$ assigned to $a$ and $b$ are the same, i.e. are equal on the meta-level.
FO without equality essentially omits this concept as a primitve. The reasons for distinction is largely historic and I omit any further details now.
What I think is more important, is that of course you can add a relation symbol to the signature/language as a custom equality symbol and enforce some kind of behaviour by restricting the desired models to those having the corresponding properties, e.g. through a corresponding axiomatization of a desired model class, that is you may specify the class of models you want to consider as the models of some set of first order sentences:
Say you might want to create another type of equality in some context, written syntactically in the formal language as $equiv$ for which you may ask different properties from, e.g. transitive behaviour
$$forall xforall yforall z:xequiv yrightarrow(yequiv zrightarrow xequiv z)$$
Classical equality as perceived e.g. in mathematics of course has other properties as well like symmetry etc., which you may omit or add depending on whatever you try to model(where model is a great descriptor, as you restrict the class of models to those already satisfying your required properties).
Since it seems that your question comes from a more applied background, let me end with that it depends largely on what you try to model and how you want to model it, but you may always, and this is the great strength and diversity of FO compared to e.g. (in a drastic way) classical propositional logic, specify a signature of symbols representing functions and relations for some scenario for which you then can specify semantic properties syntactically through corresponding formulas.
EDIT: I'm sorry if I drove off a little bit, concerning your question I was not sure if you asked for soft discussion, elaboration of a concept or a more formal treatment of these questions.
answered Jul 30 at 23:45
zzuussee
1,172419
edited Aug 1 at 21:48
answered Jul 30 at 23:45
zzuussee
1,172419
answered Jul 30 at 23:45
zzuussee
1,172419
answered Jul 30 at 23:45
zzuussee
1,172419
1,172419
add a comment |Â
add a comment |Â
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
StackExchange.ready(
function ()
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f2867441%2fis-it-possible-to-have-equality-in-the-body-or-head-of-the-implication-of-the-fi%23new-answer', 'question_page');
);
Post as a guest
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
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
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
6
Equality is a binary predicate. Any predicate, fully applied, is a formula. Implication is a connective that combines two formulas. There is no restriction on what formulas implication combines in FOL.
– Derek Elkins
Jul 30 at 21:47