Mixing
Logical equivalence versus definitional equality
$begingroup$
From a previous question it was confirmed that the equivalence:
$forall x forall y bullet Overlap(x,y) equiv (exists z Part(z,y) land Part(z,x))$ (1)
could be transformed into the pair of implications:
$forall x forall y : (overlap(x,y) Rightarrow (exists z : (part(z,x) land part(z,y)))) $ (1a)
$forall x forall y : ((exists z : part(z,x) land part(z,y)) Rightarrow overlap(x,y)) $ (1b)
Is this transformation still valid if the sentence is definitional using definitional equality?
$forall x forall y bullet Overlap(x,y) stackrel{mathrm{def}}{=} (exists z Part(z,y) land Part(z,x))$ (2)
first-order-logic
asked Jan 8 at 12:47
Patrick BrownePatrick Browne
528
$endgroup$
add a comment |
$begingroup$
From a previous question it was confirmed that the equivalence:
$forall x forall y bullet Overlap(x,y) equiv (exists z Part(z,y) land Part(z,x))$ (1)
could be transformed into the pair of implications:
$forall x forall y : (overlap(x,y) Rightarrow (exists z : (part(z,x) land part(z,y)))) $ (1a)
$forall x forall y : ((exists z : part(z,x) land part(z,y)) Rightarrow overlap(x,y)) $ (1b)
Is this transformation still valid if the sentence is definitional using definitional equality?
$forall x forall y bullet Overlap(x,y) stackrel{mathrm{def}}{=} (exists z Part(z,y) land Part(z,x))$ (2)
first-order-logic
asked Jan 8 at 12:47
Patrick BrownePatrick Browne
528
$endgroup$
1
$begingroup$
YES. In FOL the "expansion" of a language through the definition of e.g. a new predicate $phi$ can be managed adding as an axiom, the universal closure of the bi-conditional $ϕ(x_1,…,x_n) ↔ mathcal A(x_1,…,x_n)$.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:06
1
$begingroup$
There are two "equivalent" approaches in place : (i) expanding the object language adding the axiom (with bi-conditional); (ii) introduce the definitional equality in the meta-language.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:19
add a comment |
$begingroup$
From a previous question it was confirmed that the equivalence:
$forall x forall y bullet Overlap(x,y) equiv (exists z Part(z,y) land Part(z,x))$ (1)
could be transformed into the pair of implications:
$forall x forall y : (overlap(x,y) Rightarrow (exists z : (part(z,x) land part(z,y)))) $ (1a)
$forall x forall y : ((exists z : part(z,x) land part(z,y)) Rightarrow overlap(x,y)) $ (1b)
Is this transformation still valid if the sentence is definitional using definitional equality?
$forall x forall y bullet Overlap(x,y) stackrel{mathrm{def}}{=} (exists z Part(z,y) land Part(z,x))$ (2)
first-order-logic
asked Jan 8 at 12:47
Patrick BrownePatrick Browne
528
$endgroup$
From a previous question it was confirmed that the equivalence:
$forall x forall y bullet Overlap(x,y) equiv (exists z Part(z,y) land Part(z,x))$ (1)
could be transformed into the pair of implications:
$forall x forall y : (overlap(x,y) Rightarrow (exists z : (part(z,x) land part(z,y)))) $ (1a)
$forall x forall y : ((exists z : part(z,x) land part(z,y)) Rightarrow overlap(x,y)) $ (1b)
Is this transformation still valid if the sentence is definitional using definitional equality?
$forall x forall y bullet Overlap(x,y) stackrel{mathrm{def}}{=} (exists z Part(z,y) land Part(z,x))$ (2)
first-order-logic
first-order-logic
asked Jan 8 at 12:47
Patrick BrownePatrick Browne
528
asked Jan 8 at 12:47
Patrick BrownePatrick Browne
528
edited Jan 8 at 13:47
Patrick Browne
asked Jan 8 at 12:47
Patrick BrownePatrick Browne
528
asked Jan 8 at 12:47
Patrick BrownePatrick Browne
528
asked Jan 8 at 12:47
Patrick BrownePatrick Browne
528
528
1
$begingroup$
YES. In FOL the "expansion" of a language through the definition of e.g. a new predicate $phi$ can be managed adding as an axiom, the universal closure of the bi-conditional $ϕ(x_1,…,x_n) ↔ mathcal A(x_1,…,x_n)$.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:06
1
$begingroup$
There are two "equivalent" approaches in place : (i) expanding the object language adding the axiom (with bi-conditional); (ii) introduce the definitional equality in the meta-language.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:19
add a comment |
1
$begingroup$
YES. In FOL the "expansion" of a language through the definition of e.g. a new predicate $phi$ can be managed adding as an axiom, the universal closure of the bi-conditional $ϕ(x_1,…,x_n) ↔ mathcal A(x_1,…,x_n)$.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:06
1
$begingroup$
There are two "equivalent" approaches in place : (i) expanding the object language adding the axiom (with bi-conditional); (ii) introduce the definitional equality in the meta-language.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:19
1
1
$begingroup$
YES. In FOL the "expansion" of a language through the definition of e.g. a new predicate $phi$ can be managed adding as an axiom, the universal closure of the bi-conditional $ϕ(x_1,…,x_n) ↔ mathcal A(x_1,…,x_n)$.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:06
$begingroup$
YES. In FOL the "expansion" of a language through the definition of e.g. a new predicate $phi$ can be managed adding as an axiom, the universal closure of the bi-conditional $ϕ(x_1,…,x_n) ↔ mathcal A(x_1,…,x_n)$.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:06
1
1
$begingroup$
There are two "equivalent" approaches in place : (i) expanding the object language adding the axiom (with bi-conditional); (ii) introduce the definitional equality in the meta-language.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:19
$begingroup$
There are two "equivalent" approaches in place : (i) expanding the object language adding the axiom (with bi-conditional); (ii) introduce the definitional equality in the meta-language.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:19
add a comment |
0
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',
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%2f3066124%2flogical-equivalence-versus-definitional-equality%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
0
active
oldest
votes
0
active
oldest
votes
active
oldest
votes
active
oldest
votes
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%2f3066124%2flogical-equivalence-versus-definitional-equality%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$
YES. In FOL the "expansion" of a language through the definition of e.g. a new predicate $phi$ can be managed adding as an axiom, the universal closure of the bi-conditional $ϕ(x_1,…,x_n) ↔ mathcal A(x_1,…,x_n)$.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:06
1
$begingroup$
There are two "equivalent" approaches in place : (i) expanding the object language adding the axiom (with bi-conditional); (ii) introduce the definitional equality in the meta-language.
$endgroup$
– Mauro ALLEGRANZA
Jan 8 at 13:19