Deriving symmetry of equality in FOL The Next CEO of Stack OverflowNot understanding universal generalisation, and proof that uses itHints and/or help needed for axiomatic deductionHow can universal quantifier manipulation rules be made redundant by the generalization rule (metatheorem)?completeness theorem in Enderton's bookLogical equivalence of a given formulaEquality and its axiomsIs there a finite axiomatization of Tarski's geometry axioms?Why is the rule of substitution of functions an axiom?FOL-Proof that “There is no set of all sets.”A $L$-sentence Deduction using only $L$-sentences.
Why do professional authors make "consistency" mistakes? And how to avoid them?
How long to clear the 'suck zone' of a turbofan after start is initiated?
How to write papers efficiently when English isn't my first language?
How do I go from 300 unfinished/half written blog posts, to published posts?
Robert Sheckley short story about vacation spots being overwhelmed
Why does C# sound extremely flat when saxophone is tuned to G?
What's the point of interval inversion?
Is it okay to store user locations?
How to Reset Passwords on Multiple Websites Easily?
Where to find order of arguments for default functions
Why do remote companies require working in the US?
What do "high sea" and "carry" mean in this sentence?
Whats the best way to handle refactoring a big file?
How do spells that require an ability check vs. the caster's spell save DC work?
How to get regions to plot as graphics
If the heap is initialized for security, then why is the stack uninitialized?
Shade part of a Venn diagram
What makes a siege story/plot interesting?
What can we do to stop prior company from asking us questions?
India just shot down a satellite from the ground. At what altitude range is the resulting debris field?
How do I construct this japanese bowl?
Natural language into sentence logic
What does "Its cash flow is deeply negative" mean?
Describing a person. What needs to be mentioned?
Deriving symmetry of equality in FOL
The Next CEO of Stack OverflowNot understanding universal generalisation, and proof that uses itHints and/or help needed for axiomatic deductionHow can universal quantifier manipulation rules be made redundant by the generalization rule (metatheorem)?completeness theorem in Enderton's bookLogical equivalence of a given formulaEquality and its axiomsIs there a finite axiomatization of Tarski's geometry axioms?Why is the rule of substitution of functions an axiom?FOL-Proof that “There is no set of all sets.”A $L$-sentence Deduction using only $L$-sentences.
$begingroup$
In FOL with equality, the axioms of equality are:
- $forall x(x=x).$
- Let $varphi$ be a formula with free occurences of $x$, and define $varphi'$ by replacing some or all of the free occurences of $x$ in $varphi$ with $y$, then $forall xforall y(x=yrightarrow(varphirightarrowvarphi')).$
The symmetric property of equality becomes a theorem that follows from these, and I've tried the following:
Let $varphiequiv x=x$ and $varphi'equiv y=x$, then by the second schema:
$$forall xforall y(x=yrightarrow(x=xrightarrow y=x)).$$
It's pretty tempting to proceed as follows:
$$forall xforall y(x=yrightarrow(toprightarrow y=x))$$
$$forall xforall y(x=yrightarrow y=x).$$
My doubt however is, is it wrong to assume that the formula $x=x$ is always true, even when all occurences of $x$ are unbound? Does the universal quantification shown in the first axiom make a difference?
first-order-logic predicate-logic
asked Mar 18 at 13:03
mjtsquaredmjtsquared
12715
$endgroup$
add a comment |
$begingroup$
In FOL with equality, the axioms of equality are:
- $forall x(x=x).$
- Let $varphi$ be a formula with free occurences of $x$, and define $varphi'$ by replacing some or all of the free occurences of $x$ in $varphi$ with $y$, then $forall xforall y(x=yrightarrow(varphirightarrowvarphi')).$
The symmetric property of equality becomes a theorem that follows from these, and I've tried the following:
Let $varphiequiv x=x$ and $varphi'equiv y=x$, then by the second schema:
$$forall xforall y(x=yrightarrow(x=xrightarrow y=x)).$$
It's pretty tempting to proceed as follows:
$$forall xforall y(x=yrightarrow(toprightarrow y=x))$$
$$forall xforall y(x=yrightarrow y=x).$$
My doubt however is, is it wrong to assume that the formula $x=x$ is always true, even when all occurences of $x$ are unbound? Does the universal quantification shown in the first axiom make a difference?
first-order-logic predicate-logic
asked Mar 18 at 13:03
mjtsquaredmjtsquared
12715
$endgroup$
$begingroup$
Your approach shows only that equality is symmetric over variables. What you want to show is that if $phi = phi'$ then $phi' = phi$. For that, you have to use part (2) of the definition.
$endgroup$
– frabala
Mar 18 at 13:25
add a comment |
$begingroup$
In FOL with equality, the axioms of equality are:
- $forall x(x=x).$
- Let $varphi$ be a formula with free occurences of $x$, and define $varphi'$ by replacing some or all of the free occurences of $x$ in $varphi$ with $y$, then $forall xforall y(x=yrightarrow(varphirightarrowvarphi')).$
The symmetric property of equality becomes a theorem that follows from these, and I've tried the following:
Let $varphiequiv x=x$ and $varphi'equiv y=x$, then by the second schema:
$$forall xforall y(x=yrightarrow(x=xrightarrow y=x)).$$
It's pretty tempting to proceed as follows:
$$forall xforall y(x=yrightarrow(toprightarrow y=x))$$
$$forall xforall y(x=yrightarrow y=x).$$
My doubt however is, is it wrong to assume that the formula $x=x$ is always true, even when all occurences of $x$ are unbound? Does the universal quantification shown in the first axiom make a difference?
first-order-logic predicate-logic
asked Mar 18 at 13:03
mjtsquaredmjtsquared
12715
$endgroup$
In FOL with equality, the axioms of equality are:
- $forall x(x=x).$
- Let $varphi$ be a formula with free occurences of $x$, and define $varphi'$ by replacing some or all of the free occurences of $x$ in $varphi$ with $y$, then $forall xforall y(x=yrightarrow(varphirightarrowvarphi')).$
The symmetric property of equality becomes a theorem that follows from these, and I've tried the following:
Let $varphiequiv x=x$ and $varphi'equiv y=x$, then by the second schema:
$$forall xforall y(x=yrightarrow(x=xrightarrow y=x)).$$
It's pretty tempting to proceed as follows:
$$forall xforall y(x=yrightarrow(toprightarrow y=x))$$
$$forall xforall y(x=yrightarrow y=x).$$
My doubt however is, is it wrong to assume that the formula $x=x$ is always true, even when all occurences of $x$ are unbound? Does the universal quantification shown in the first axiom make a difference?
first-order-logic predicate-logic
first-order-logic predicate-logic
asked Mar 18 at 13:03
mjtsquaredmjtsquared
12715
asked Mar 18 at 13:03
mjtsquaredmjtsquared
12715
asked Mar 18 at 13:03
mjtsquaredmjtsquared
12715
asked Mar 18 at 13:03
mjtsquaredmjtsquared
12715
asked Mar 18 at 13:03
mjtsquaredmjtsquared
12715
12715
$begingroup$
Your approach shows only that equality is symmetric over variables. What you want to show is that if $phi = phi'$ then $phi' = phi$. For that, you have to use part (2) of the definition.
$endgroup$
– frabala
Mar 18 at 13:25
add a comment |
$begingroup$
Your approach shows only that equality is symmetric over variables. What you want to show is that if $phi = phi'$ then $phi' = phi$. For that, you have to use part (2) of the definition.
$endgroup$
– frabala
Mar 18 at 13:25
$begingroup$
Your approach shows only that equality is symmetric over variables. What you want to show is that if $phi = phi'$ then $phi' = phi$. For that, you have to use part (2) of the definition.
$endgroup$
– frabala
Mar 18 at 13:25
$begingroup$
Your approach shows only that equality is symmetric over variables. What you want to show is that if $phi = phi'$ then $phi' = phi$. For that, you have to use part (2) of the definition.
$endgroup$
– frabala
Mar 18 at 13:25
add a comment |
1 Answer
1
active
oldest
votes
$begingroup$
is it wrong to assume [in the proof of simmetry of equality] that the formula $x=x$ is always true?
No, it works.
More detailed proof :
1) $vdash forall x (x=x)$ --- axiom 1
2) $vdash ∀x∀y(x=y → (x=x → y=x))$ --- from axiom-schema 2 : $∀x∀y(x=y → (phi[z/x] → phi[z/y]))$, where $phi(z) := (z=x)$
3) $x=y$ --- assumed [a]
4) $x=x$ --- from 1) by $forall$-elim (i.e. Universal Instantiation)
5) $x=y → (x=x → y=x)$ --- from 2) by $forall$-elim
6) $(x=x → y=x)$ --- from 3) and 5) by $to$-elim (aka Modus Ponens)
7) $y=x$ --- from 4) and 6)
8) $(x=y to y=x)$ --- from 3) and 7) by $to$-intro (aka Conditional Proof), discharging [a]
$vdash ∀x∀y(x=y to y=x)$ --- from 8) by $forall$-intro (i.e. Universal generalization) twice.
answered Mar 18 at 13:26
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
$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%2f3152758%2fderiving-symmetry-of-equality-in-fol%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$
is it wrong to assume [in the proof of simmetry of equality] that the formula $x=x$ is always true?
No, it works.
More detailed proof :
1) $vdash forall x (x=x)$ --- axiom 1
2) $vdash ∀x∀y(x=y → (x=x → y=x))$ --- from axiom-schema 2 : $∀x∀y(x=y → (phi[z/x] → phi[z/y]))$, where $phi(z) := (z=x)$
3) $x=y$ --- assumed [a]
4) $x=x$ --- from 1) by $forall$-elim (i.e. Universal Instantiation)
5) $x=y → (x=x → y=x)$ --- from 2) by $forall$-elim
6) $(x=x → y=x)$ --- from 3) and 5) by $to$-elim (aka Modus Ponens)
7) $y=x$ --- from 4) and 6)
8) $(x=y to y=x)$ --- from 3) and 7) by $to$-intro (aka Conditional Proof), discharging [a]
$vdash ∀x∀y(x=y to y=x)$ --- from 8) by $forall$-intro (i.e. Universal generalization) twice.
answered Mar 18 at 13:26
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
$endgroup$
add a comment |
$begingroup$
is it wrong to assume [in the proof of simmetry of equality] that the formula $x=x$ is always true?
No, it works.
More detailed proof :
1) $vdash forall x (x=x)$ --- axiom 1
2) $vdash ∀x∀y(x=y → (x=x → y=x))$ --- from axiom-schema 2 : $∀x∀y(x=y → (phi[z/x] → phi[z/y]))$, where $phi(z) := (z=x)$
3) $x=y$ --- assumed [a]
4) $x=x$ --- from 1) by $forall$-elim (i.e. Universal Instantiation)
5) $x=y → (x=x → y=x)$ --- from 2) by $forall$-elim
6) $(x=x → y=x)$ --- from 3) and 5) by $to$-elim (aka Modus Ponens)
7) $y=x$ --- from 4) and 6)
8) $(x=y to y=x)$ --- from 3) and 7) by $to$-intro (aka Conditional Proof), discharging [a]
$vdash ∀x∀y(x=y to y=x)$ --- from 8) by $forall$-intro (i.e. Universal generalization) twice.
answered Mar 18 at 13:26
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
$endgroup$
add a comment |
$begingroup$
is it wrong to assume [in the proof of simmetry of equality] that the formula $x=x$ is always true?
No, it works.
More detailed proof :
1) $vdash forall x (x=x)$ --- axiom 1
2) $vdash ∀x∀y(x=y → (x=x → y=x))$ --- from axiom-schema 2 : $∀x∀y(x=y → (phi[z/x] → phi[z/y]))$, where $phi(z) := (z=x)$
3) $x=y$ --- assumed [a]
4) $x=x$ --- from 1) by $forall$-elim (i.e. Universal Instantiation)
5) $x=y → (x=x → y=x)$ --- from 2) by $forall$-elim
6) $(x=x → y=x)$ --- from 3) and 5) by $to$-elim (aka Modus Ponens)
7) $y=x$ --- from 4) and 6)
8) $(x=y to y=x)$ --- from 3) and 7) by $to$-intro (aka Conditional Proof), discharging [a]
$vdash ∀x∀y(x=y to y=x)$ --- from 8) by $forall$-intro (i.e. Universal generalization) twice.
answered Mar 18 at 13:26
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
$endgroup$
is it wrong to assume [in the proof of simmetry of equality] that the formula $x=x$ is always true?
No, it works.
More detailed proof :
1) $vdash forall x (x=x)$ --- axiom 1
2) $vdash ∀x∀y(x=y → (x=x → y=x))$ --- from axiom-schema 2 : $∀x∀y(x=y → (phi[z/x] → phi[z/y]))$, where $phi(z) := (z=x)$
3) $x=y$ --- assumed [a]
4) $x=x$ --- from 1) by $forall$-elim (i.e. Universal Instantiation)
5) $x=y → (x=x → y=x)$ --- from 2) by $forall$-elim
6) $(x=x → y=x)$ --- from 3) and 5) by $to$-elim (aka Modus Ponens)
7) $y=x$ --- from 4) and 6)
8) $(x=y to y=x)$ --- from 3) and 7) by $to$-intro (aka Conditional Proof), discharging [a]
$vdash ∀x∀y(x=y to y=x)$ --- from 8) by $forall$-intro (i.e. Universal generalization) twice.
answered Mar 18 at 13:26
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
edited Mar 25 at 11:34
answered Mar 18 at 13:26
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
answered Mar 18 at 13:26
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
answered Mar 18 at 13:26
Mauro ALLEGRANZAMauro ALLEGRANZA
67.5k449117
67.5k449117
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%2f3152758%2fderiving-symmetry-of-equality-in-fol%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$
Your approach shows only that equality is symmetric over variables. What you want to show is that if $phi = phi'$ then $phi' = phi$. For that, you have to use part (2) of the definition.
$endgroup$
– frabala
Mar 18 at 13:25