Dtjytyk

Processor speed limited at 0.4 Ghz

Can someone clarify Hamming's notion of important problems in relation to modern academia?

Can compressed videos be decoded back to their uncompresed original format?

What is the most common color to indicate the input-field is disabled?

Does int main() need a declaration on C++?

How dangerous is XSS

How to travel to Japan while expressing milk?

Can a virus destroy the BIOS of a modern computer?

Does the Idaho Potato Commission associate potato skins with healthy eating?

Is "/bin/[.exe" a legitimate file? [Cygwin, Windows 10]

How to show a landlord what we have in savings?

How obscure is the use of 令 in 令和?

What is required to make GPS signals available indoors?

How can a day be of 24 hours?

Finding the reason behind the value of the integral.

Is this draw by repetition?

How to compactly explain secondary and tertiary characters without resorting to stereotypes?

How can saying a song's name be a copyright violation?

How to stretch the corners of this image so that it looks like a perfect rectangle?

Finitely generated matrix groups whose eigenvalues are all algebraic

Why do I get negative height?

Are British MPs missing the point, with these 'Indicative Votes'?

Send out email when Apex Queueable fails and test it

What do you call someone who asks many questions?

Deriving symmetry of equality in FOL

Not 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.

1

$begingroup$

In FOL with equality, the axioms of equality are:

1. $forall x(x=x).$


2. 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

share|cite|improve this question

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 | 

1

$begingroup$

In FOL with equality, the axioms of equality are:

1. $forall x(x=x).$


2. 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

share|cite|improve this question

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:

1. $forall x(x=x).$


2. 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

share|cite|improve this question

asked Mar 18 at 13:03

mjtsquaredmjtsquared

12715

$endgroup$

share|cite|improve this question

asked Mar 18 at 13:03

mjtsquaredmjtsquared

12715

share|cite|improve this question

asked Mar 18 at 13:03

mjtsquaredmjtsquared

12715

asked Mar 18 at 13:03

mjtsquaredmjtsquared

12715

asked Mar 18 at 13:03

mjtsquaredmjtsquared

12715

1 Answer
1

active

oldest

votes

1

$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.

share|cite|improve this answer

edited Mar 25 at 11:34

answered Mar 18 at 13:26

Mauro ALLEGRANZAMauro ALLEGRANZA

67.6k449117

$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
});


}
});

draft saved

draft discarded

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

Name

Email

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

Name

Email

Required, but never shown

1

$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.

share|cite|improve this answer

edited Mar 25 at 11:34

answered Mar 18 at 13:26

Mauro ALLEGRANZAMauro ALLEGRANZA

67.6k449117

$endgroup$

add a comment | 

1

$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.

share|cite|improve this answer

edited Mar 25 at 11:34

answered Mar 18 at 13:26

Mauro ALLEGRANZAMauro ALLEGRANZA

67.6k449117

$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.

share|cite|improve this answer

edited Mar 25 at 11:34

answered Mar 18 at 13:26

Mauro ALLEGRANZAMauro ALLEGRANZA

67.6k449117

$endgroup$

share|cite|improve this answer

edited Mar 25 at 11:34

answered Mar 18 at 13:26

Mauro ALLEGRANZAMauro ALLEGRANZA

67.6k449117

answered Mar 18 at 13:26

Mauro ALLEGRANZAMauro ALLEGRANZA

67.6k449117

answered Mar 18 at 13:26

Mauro ALLEGRANZAMauro ALLEGRANZA

67.6k449117