If $Sigma vdash varphi$ then $Sigma vdash forall x varphi$. Why when $(varphi implies forall x varphi)$ is...












0












$begingroup$


In the book of first order logic I'm reading they say that if $(varphi_1,...,varphi_n)$ is a proof from a set of formulae $Sigma$, then so is $(varphi_1,...,varphi_n,forall x varphi_j)$ for all $1leq j leq n$. They assume that as an axiom but it doesn't make sense to me. Why if $varphi$ is true then so is $forall x varphi$? For example if $varphi$ is $x=1$ that wouldn't mean that $forall x : x=1$ , or would it?



Maybe what I don't understand is: why $(Sigma vdash varphi implies Sigma vdash forall x varphi)$ is true but $(varphi implies forall x varphi)$ is not true?



The book is this: https://www.springer.com/cda/content/document/cda_downloaddocument/9781447121756-c2.pdf?SGWID=0-0-45-1192238-p174141200










share|cite|improve this question











$endgroup$












  • $begingroup$
    Which book are you referring to? Please edit the question to include the details.
    $endgroup$
    – Shaun
    Dec 30 '18 at 15:45






  • 1




    $begingroup$
    NO; the rule of Universal generalization holds provided that $x$ is not free in $Σ$.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 15:51










  • $begingroup$
    "For example if φ is $x=1$ that wouldn't mean that $∀x (x=1)$, or would it?" Correct; the issue is that $x=1$ is not provable from e.g. arithmetical axioms.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 15:53












  • $begingroup$
    @MauroALLEGRANZA but $Sigma cup varphi$ is a set of formulae and $varphi$ is provable from it so.. Maybe my doubt is: What does $x=1$ even mean?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:14












  • $begingroup$
    As already commented,, you need to add the assumption that $x$ does not occur free in $sum$. Also it's a bad title - sounds like you're saying $phitoforall xphi$ is a theorem, which is certainly not so. You meant to say that if $sumvdashphi$ then $sumvdashforall xphi$.
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 16:21


















0












$begingroup$


In the book of first order logic I'm reading they say that if $(varphi_1,...,varphi_n)$ is a proof from a set of formulae $Sigma$, then so is $(varphi_1,...,varphi_n,forall x varphi_j)$ for all $1leq j leq n$. They assume that as an axiom but it doesn't make sense to me. Why if $varphi$ is true then so is $forall x varphi$? For example if $varphi$ is $x=1$ that wouldn't mean that $forall x : x=1$ , or would it?



Maybe what I don't understand is: why $(Sigma vdash varphi implies Sigma vdash forall x varphi)$ is true but $(varphi implies forall x varphi)$ is not true?



The book is this: https://www.springer.com/cda/content/document/cda_downloaddocument/9781447121756-c2.pdf?SGWID=0-0-45-1192238-p174141200










share|cite|improve this question











$endgroup$












  • $begingroup$
    Which book are you referring to? Please edit the question to include the details.
    $endgroup$
    – Shaun
    Dec 30 '18 at 15:45






  • 1




    $begingroup$
    NO; the rule of Universal generalization holds provided that $x$ is not free in $Σ$.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 15:51










  • $begingroup$
    "For example if φ is $x=1$ that wouldn't mean that $∀x (x=1)$, or would it?" Correct; the issue is that $x=1$ is not provable from e.g. arithmetical axioms.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 15:53












  • $begingroup$
    @MauroALLEGRANZA but $Sigma cup varphi$ is a set of formulae and $varphi$ is provable from it so.. Maybe my doubt is: What does $x=1$ even mean?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:14












  • $begingroup$
    As already commented,, you need to add the assumption that $x$ does not occur free in $sum$. Also it's a bad title - sounds like you're saying $phitoforall xphi$ is a theorem, which is certainly not so. You meant to say that if $sumvdashphi$ then $sumvdashforall xphi$.
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 16:21
















0












0








0





$begingroup$


In the book of first order logic I'm reading they say that if $(varphi_1,...,varphi_n)$ is a proof from a set of formulae $Sigma$, then so is $(varphi_1,...,varphi_n,forall x varphi_j)$ for all $1leq j leq n$. They assume that as an axiom but it doesn't make sense to me. Why if $varphi$ is true then so is $forall x varphi$? For example if $varphi$ is $x=1$ that wouldn't mean that $forall x : x=1$ , or would it?



Maybe what I don't understand is: why $(Sigma vdash varphi implies Sigma vdash forall x varphi)$ is true but $(varphi implies forall x varphi)$ is not true?



The book is this: https://www.springer.com/cda/content/document/cda_downloaddocument/9781447121756-c2.pdf?SGWID=0-0-45-1192238-p174141200










share|cite|improve this question











$endgroup$




In the book of first order logic I'm reading they say that if $(varphi_1,...,varphi_n)$ is a proof from a set of formulae $Sigma$, then so is $(varphi_1,...,varphi_n,forall x varphi_j)$ for all $1leq j leq n$. They assume that as an axiom but it doesn't make sense to me. Why if $varphi$ is true then so is $forall x varphi$? For example if $varphi$ is $x=1$ that wouldn't mean that $forall x : x=1$ , or would it?



Maybe what I don't understand is: why $(Sigma vdash varphi implies Sigma vdash forall x varphi)$ is true but $(varphi implies forall x varphi)$ is not true?



The book is this: https://www.springer.com/cda/content/document/cda_downloaddocument/9781447121756-c2.pdf?SGWID=0-0-45-1192238-p174141200







first-order-logic






share|cite|improve this question















share|cite|improve this question













share|cite|improve this question




share|cite|improve this question








edited Dec 30 '18 at 16:23







Ruben a

















asked Dec 30 '18 at 15:12









Ruben aRuben a

153




153












  • $begingroup$
    Which book are you referring to? Please edit the question to include the details.
    $endgroup$
    – Shaun
    Dec 30 '18 at 15:45






  • 1




    $begingroup$
    NO; the rule of Universal generalization holds provided that $x$ is not free in $Σ$.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 15:51










  • $begingroup$
    "For example if φ is $x=1$ that wouldn't mean that $∀x (x=1)$, or would it?" Correct; the issue is that $x=1$ is not provable from e.g. arithmetical axioms.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 15:53












  • $begingroup$
    @MauroALLEGRANZA but $Sigma cup varphi$ is a set of formulae and $varphi$ is provable from it so.. Maybe my doubt is: What does $x=1$ even mean?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:14












  • $begingroup$
    As already commented,, you need to add the assumption that $x$ does not occur free in $sum$. Also it's a bad title - sounds like you're saying $phitoforall xphi$ is a theorem, which is certainly not so. You meant to say that if $sumvdashphi$ then $sumvdashforall xphi$.
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 16:21




















  • $begingroup$
    Which book are you referring to? Please edit the question to include the details.
    $endgroup$
    – Shaun
    Dec 30 '18 at 15:45






  • 1




    $begingroup$
    NO; the rule of Universal generalization holds provided that $x$ is not free in $Σ$.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 15:51










  • $begingroup$
    "For example if φ is $x=1$ that wouldn't mean that $∀x (x=1)$, or would it?" Correct; the issue is that $x=1$ is not provable from e.g. arithmetical axioms.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 15:53












  • $begingroup$
    @MauroALLEGRANZA but $Sigma cup varphi$ is a set of formulae and $varphi$ is provable from it so.. Maybe my doubt is: What does $x=1$ even mean?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:14












  • $begingroup$
    As already commented,, you need to add the assumption that $x$ does not occur free in $sum$. Also it's a bad title - sounds like you're saying $phitoforall xphi$ is a theorem, which is certainly not so. You meant to say that if $sumvdashphi$ then $sumvdashforall xphi$.
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 16:21


















$begingroup$
Which book are you referring to? Please edit the question to include the details.
$endgroup$
– Shaun
Dec 30 '18 at 15:45




$begingroup$
Which book are you referring to? Please edit the question to include the details.
$endgroup$
– Shaun
Dec 30 '18 at 15:45




1




1




$begingroup$
NO; the rule of Universal generalization holds provided that $x$ is not free in $Σ$.
$endgroup$
– Mauro ALLEGRANZA
Dec 30 '18 at 15:51




$begingroup$
NO; the rule of Universal generalization holds provided that $x$ is not free in $Σ$.
$endgroup$
– Mauro ALLEGRANZA
Dec 30 '18 at 15:51












$begingroup$
"For example if φ is $x=1$ that wouldn't mean that $∀x (x=1)$, or would it?" Correct; the issue is that $x=1$ is not provable from e.g. arithmetical axioms.
$endgroup$
– Mauro ALLEGRANZA
Dec 30 '18 at 15:53






$begingroup$
"For example if φ is $x=1$ that wouldn't mean that $∀x (x=1)$, or would it?" Correct; the issue is that $x=1$ is not provable from e.g. arithmetical axioms.
$endgroup$
– Mauro ALLEGRANZA
Dec 30 '18 at 15:53














$begingroup$
@MauroALLEGRANZA but $Sigma cup varphi$ is a set of formulae and $varphi$ is provable from it so.. Maybe my doubt is: What does $x=1$ even mean?
$endgroup$
– Ruben a
Dec 30 '18 at 16:14






$begingroup$
@MauroALLEGRANZA but $Sigma cup varphi$ is a set of formulae and $varphi$ is provable from it so.. Maybe my doubt is: What does $x=1$ even mean?
$endgroup$
– Ruben a
Dec 30 '18 at 16:14














$begingroup$
As already commented,, you need to add the assumption that $x$ does not occur free in $sum$. Also it's a bad title - sounds like you're saying $phitoforall xphi$ is a theorem, which is certainly not so. You meant to say that if $sumvdashphi$ then $sumvdashforall xphi$.
$endgroup$
– David C. Ullrich
Dec 30 '18 at 16:21






$begingroup$
As already commented,, you need to add the assumption that $x$ does not occur free in $sum$. Also it's a bad title - sounds like you're saying $phitoforall xphi$ is a theorem, which is certainly not so. You meant to say that if $sumvdashphi$ then $sumvdashforall xphi$.
$endgroup$
– David C. Ullrich
Dec 30 '18 at 16:21












2 Answers
2






active

oldest

votes


















0












$begingroup$

Edit: It turns out that the system you're dealing with is very different from the systems I'm familiar with. Hence more or less everything below is wrong, with regard to that system. I'd simply delete the whole thing but I can't since it's "accepted"...



The reason your version makes no sense is it's false. You're leaving out a crucial hypothesis; what's true, and what it had better say in the book, is this:






If $Sigmavdashphi$, where $x$ does not occur free in $Sigma$, then $Sigmavdashforall xphi$.






That makes much more sense. Informally, saying $x$ does not occur free in $Sigma$ means that the formulas in $Sigma$ do not say anything about $x$. So saying $Sigmavdash phi$ where $x$ does not occur free in $Sigma$ means "you can prove $phi$ without assuming anything about $x$".



Now it makes sense. If you can prove $phi$ from a set of assumptions that don't mention $x$, then $phi$ follows from your assumptions regardless of what $x$ is, so $forall xphi$ "should" also follow from the same assumptions.



Taking $phi$ to be $x=1$ is a bad example, because it's hard to imagine a system where you can prove $x=1$ without assuming anything about $x$. Instead imagine you have some axioms describing how the real numbers work, and you want to prove $forall x(x>1to x^2>1)$. If you can prove $x>1to x^2>1$ without assuming anything special about $x$ then $forall x(x>1to x^2>1)$ follows. (That is how people prove $forall xphi$ in actual math: prove $phi$ without assuming anything about $x$.)



Hmm. An example of a $Sigma$ where $Sigmavdash x=1$ but $x$ is not free in $Sigma$ would be $Sigma={forall y (y=1)}$. Yes, $forall y (y=1)$ implies $x=1$, and it also implies $forall x (x=1)$.



Another example, illustrating how if $x$ does occur free in $Sigma$ then all bets are off: It's true that $x=1vdash x=1$. But $x=1notvdash forall x(x=1)$. If you leave out that "where $x$ does not occur free in $Sigma$" then you're going to conclude that in fact $x=1vdashforall x(x=1)$, which is nonsense; luckily $x=1vdashforall x(x=1)$ does not follow from the correct version of the result we're talking about.






share|cite|improve this answer











$endgroup$









  • 1




    $begingroup$
    But the exposition of FOL used by the OP is "Mendelson-like" : no restriction on Gen rule. The restriction is on the Deduction Th. So $(x=1) vdash forall x (x=1)$ is formally correct in the system; what is not is to apply DT to it to get : $vdash (x=1) to forall x (x=1)$.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 18:13












  • $begingroup$
    Oh. All I know about logic is what I read in Enderton years ago; the notion of a system were $x=1vdashforall x(x=1)$ makes no sense to me. As sort of a check on whether it's "$x=1$" or $"vdash$" that's totally different: what about $x=1modelsforall x(x=1)$?
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 18:30










  • $begingroup$
    Only browsed the text... it seems to me that is not defined. But $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash varphi(x) [h]$ for every evaluation $h$ and thus $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash forall x varphi(x)$. So, no problem...
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 18:55










  • $begingroup$
    @MauroALLEGRANZA but then in "Mendelson-like logic" what is the difference between $(x=1)$ and $forall x (x=1)$ ? What do those formulas mean?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 19:18










  • $begingroup$
    @Rubena - consider $mathbb N$ as domain of the interpretation. $mathbb N nvDash forall x (x=1)$, obviously, while for $(x=1)$ we need a variable assignment $h$. If $h(x)=1$ then $mathbb N vDash (x=1)[h]$, while for $h'$ such that e.g. $h'(x)=0$ we have that $mathbb N nvDash (x=1)[h']$. So the semantics is Ok: we are licensed to asserts $mathfrak A vDash varphi(x)$ only if every variable assignment $h$ gives the same truth value.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 19:37





















1












$begingroup$

A proof of $varphi$, with $x$ as a free variable, treats $x$ as an arbitrary element of its domain of discourse. This is exactly how we obtain a proof of $forall x ~ varphi$—introduce a variable $x$ and, knowing only those properties of $x$ that hold of all elements in its domain of discourse, prove $varphi$. This is essentially the content of the $forall$-introduction rule (a.k.a. universal generalisation).



If you could prove $x=1$ knowing nothing about $x$ than that it is an element of its domain of discourse, then it would indeed be true that $forall x (x = 1)$ is true. But of course this is only going to be true if the domain of discourse of $x$ is ${ 1 }$. (Or $varnothing$, I suppose.)



Now if you're doing first-order logic, it's likely that your domain of discourse is some ambient set theoretic universe, in which case $x=1$ will almost certainly not be provable, but formulae like $varnothing subseteq x$ and $x in { x }$ are provable.






share|cite|improve this answer











$endgroup$













  • $begingroup$
    The book I'm using doesn't seem to mention anything about a domain of discourse though.. And isn't set theory an extension of first order logic?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:11










  • $begingroup$
    @Rubena: Regarding your second question, a model of a first-order theory is a set together with certain structure (constants, functions, etc.). This means that a model $V$ of (say) ZFC set theory is externally a set, even though internally it is a proper class. But then if you're doing first-order logic, you must be working within some meta-theory, which in all likelihood is itself a model of the theory of sets.
    $endgroup$
    – Clive Newstead
    Dec 30 '18 at 16:36










  • $begingroup$
    Regarding your first question, first-order logic is just a formal system for manipulating symbols, so the variable $x$ doesn't necessarily refer to an element of any set—it's just a symbol. But semantically the variable $x$ must refer to an element of a set, and it is this set that is the domain of discourse of $x$.
    $endgroup$
    – Clive Newstead
    Dec 30 '18 at 16:38










  • $begingroup$
    But then what's the difference between $x=1$ and $forall x (x=1)$ ? If $x=1$ then all elements in the domain of discourse of $x$ are equal to 1? Then how does it differ from $forall x(x=1)$ ?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:48








  • 1




    $begingroup$
    @Rubena No! It's not true that if $x=1$ then all elements in the domain must equal $1$. Nobody has said that. You keep on leaving out that crucial hypothesis. What's true is that if it's possible to prove $x=1$ without assuming anything about $x$ then all elements in the domain must equal $1$.
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 16:53











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


















StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3056916%2fif-sigma-vdash-varphi-then-sigma-vdash-forall-x-varphi-why-when-v%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









0












$begingroup$

Edit: It turns out that the system you're dealing with is very different from the systems I'm familiar with. Hence more or less everything below is wrong, with regard to that system. I'd simply delete the whole thing but I can't since it's "accepted"...



The reason your version makes no sense is it's false. You're leaving out a crucial hypothesis; what's true, and what it had better say in the book, is this:






If $Sigmavdashphi$, where $x$ does not occur free in $Sigma$, then $Sigmavdashforall xphi$.






That makes much more sense. Informally, saying $x$ does not occur free in $Sigma$ means that the formulas in $Sigma$ do not say anything about $x$. So saying $Sigmavdash phi$ where $x$ does not occur free in $Sigma$ means "you can prove $phi$ without assuming anything about $x$".



Now it makes sense. If you can prove $phi$ from a set of assumptions that don't mention $x$, then $phi$ follows from your assumptions regardless of what $x$ is, so $forall xphi$ "should" also follow from the same assumptions.



Taking $phi$ to be $x=1$ is a bad example, because it's hard to imagine a system where you can prove $x=1$ without assuming anything about $x$. Instead imagine you have some axioms describing how the real numbers work, and you want to prove $forall x(x>1to x^2>1)$. If you can prove $x>1to x^2>1$ without assuming anything special about $x$ then $forall x(x>1to x^2>1)$ follows. (That is how people prove $forall xphi$ in actual math: prove $phi$ without assuming anything about $x$.)



Hmm. An example of a $Sigma$ where $Sigmavdash x=1$ but $x$ is not free in $Sigma$ would be $Sigma={forall y (y=1)}$. Yes, $forall y (y=1)$ implies $x=1$, and it also implies $forall x (x=1)$.



Another example, illustrating how if $x$ does occur free in $Sigma$ then all bets are off: It's true that $x=1vdash x=1$. But $x=1notvdash forall x(x=1)$. If you leave out that "where $x$ does not occur free in $Sigma$" then you're going to conclude that in fact $x=1vdashforall x(x=1)$, which is nonsense; luckily $x=1vdashforall x(x=1)$ does not follow from the correct version of the result we're talking about.






share|cite|improve this answer











$endgroup$









  • 1




    $begingroup$
    But the exposition of FOL used by the OP is "Mendelson-like" : no restriction on Gen rule. The restriction is on the Deduction Th. So $(x=1) vdash forall x (x=1)$ is formally correct in the system; what is not is to apply DT to it to get : $vdash (x=1) to forall x (x=1)$.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 18:13












  • $begingroup$
    Oh. All I know about logic is what I read in Enderton years ago; the notion of a system were $x=1vdashforall x(x=1)$ makes no sense to me. As sort of a check on whether it's "$x=1$" or $"vdash$" that's totally different: what about $x=1modelsforall x(x=1)$?
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 18:30










  • $begingroup$
    Only browsed the text... it seems to me that is not defined. But $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash varphi(x) [h]$ for every evaluation $h$ and thus $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash forall x varphi(x)$. So, no problem...
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 18:55










  • $begingroup$
    @MauroALLEGRANZA but then in "Mendelson-like logic" what is the difference between $(x=1)$ and $forall x (x=1)$ ? What do those formulas mean?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 19:18










  • $begingroup$
    @Rubena - consider $mathbb N$ as domain of the interpretation. $mathbb N nvDash forall x (x=1)$, obviously, while for $(x=1)$ we need a variable assignment $h$. If $h(x)=1$ then $mathbb N vDash (x=1)[h]$, while for $h'$ such that e.g. $h'(x)=0$ we have that $mathbb N nvDash (x=1)[h']$. So the semantics is Ok: we are licensed to asserts $mathfrak A vDash varphi(x)$ only if every variable assignment $h$ gives the same truth value.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 19:37


















0












$begingroup$

Edit: It turns out that the system you're dealing with is very different from the systems I'm familiar with. Hence more or less everything below is wrong, with regard to that system. I'd simply delete the whole thing but I can't since it's "accepted"...



The reason your version makes no sense is it's false. You're leaving out a crucial hypothesis; what's true, and what it had better say in the book, is this:






If $Sigmavdashphi$, where $x$ does not occur free in $Sigma$, then $Sigmavdashforall xphi$.






That makes much more sense. Informally, saying $x$ does not occur free in $Sigma$ means that the formulas in $Sigma$ do not say anything about $x$. So saying $Sigmavdash phi$ where $x$ does not occur free in $Sigma$ means "you can prove $phi$ without assuming anything about $x$".



Now it makes sense. If you can prove $phi$ from a set of assumptions that don't mention $x$, then $phi$ follows from your assumptions regardless of what $x$ is, so $forall xphi$ "should" also follow from the same assumptions.



Taking $phi$ to be $x=1$ is a bad example, because it's hard to imagine a system where you can prove $x=1$ without assuming anything about $x$. Instead imagine you have some axioms describing how the real numbers work, and you want to prove $forall x(x>1to x^2>1)$. If you can prove $x>1to x^2>1$ without assuming anything special about $x$ then $forall x(x>1to x^2>1)$ follows. (That is how people prove $forall xphi$ in actual math: prove $phi$ without assuming anything about $x$.)



Hmm. An example of a $Sigma$ where $Sigmavdash x=1$ but $x$ is not free in $Sigma$ would be $Sigma={forall y (y=1)}$. Yes, $forall y (y=1)$ implies $x=1$, and it also implies $forall x (x=1)$.



Another example, illustrating how if $x$ does occur free in $Sigma$ then all bets are off: It's true that $x=1vdash x=1$. But $x=1notvdash forall x(x=1)$. If you leave out that "where $x$ does not occur free in $Sigma$" then you're going to conclude that in fact $x=1vdashforall x(x=1)$, which is nonsense; luckily $x=1vdashforall x(x=1)$ does not follow from the correct version of the result we're talking about.






share|cite|improve this answer











$endgroup$









  • 1




    $begingroup$
    But the exposition of FOL used by the OP is "Mendelson-like" : no restriction on Gen rule. The restriction is on the Deduction Th. So $(x=1) vdash forall x (x=1)$ is formally correct in the system; what is not is to apply DT to it to get : $vdash (x=1) to forall x (x=1)$.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 18:13












  • $begingroup$
    Oh. All I know about logic is what I read in Enderton years ago; the notion of a system were $x=1vdashforall x(x=1)$ makes no sense to me. As sort of a check on whether it's "$x=1$" or $"vdash$" that's totally different: what about $x=1modelsforall x(x=1)$?
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 18:30










  • $begingroup$
    Only browsed the text... it seems to me that is not defined. But $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash varphi(x) [h]$ for every evaluation $h$ and thus $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash forall x varphi(x)$. So, no problem...
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 18:55










  • $begingroup$
    @MauroALLEGRANZA but then in "Mendelson-like logic" what is the difference between $(x=1)$ and $forall x (x=1)$ ? What do those formulas mean?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 19:18










  • $begingroup$
    @Rubena - consider $mathbb N$ as domain of the interpretation. $mathbb N nvDash forall x (x=1)$, obviously, while for $(x=1)$ we need a variable assignment $h$. If $h(x)=1$ then $mathbb N vDash (x=1)[h]$, while for $h'$ such that e.g. $h'(x)=0$ we have that $mathbb N nvDash (x=1)[h']$. So the semantics is Ok: we are licensed to asserts $mathfrak A vDash varphi(x)$ only if every variable assignment $h$ gives the same truth value.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 19:37
















0












0








0





$begingroup$

Edit: It turns out that the system you're dealing with is very different from the systems I'm familiar with. Hence more or less everything below is wrong, with regard to that system. I'd simply delete the whole thing but I can't since it's "accepted"...



The reason your version makes no sense is it's false. You're leaving out a crucial hypothesis; what's true, and what it had better say in the book, is this:






If $Sigmavdashphi$, where $x$ does not occur free in $Sigma$, then $Sigmavdashforall xphi$.






That makes much more sense. Informally, saying $x$ does not occur free in $Sigma$ means that the formulas in $Sigma$ do not say anything about $x$. So saying $Sigmavdash phi$ where $x$ does not occur free in $Sigma$ means "you can prove $phi$ without assuming anything about $x$".



Now it makes sense. If you can prove $phi$ from a set of assumptions that don't mention $x$, then $phi$ follows from your assumptions regardless of what $x$ is, so $forall xphi$ "should" also follow from the same assumptions.



Taking $phi$ to be $x=1$ is a bad example, because it's hard to imagine a system where you can prove $x=1$ without assuming anything about $x$. Instead imagine you have some axioms describing how the real numbers work, and you want to prove $forall x(x>1to x^2>1)$. If you can prove $x>1to x^2>1$ without assuming anything special about $x$ then $forall x(x>1to x^2>1)$ follows. (That is how people prove $forall xphi$ in actual math: prove $phi$ without assuming anything about $x$.)



Hmm. An example of a $Sigma$ where $Sigmavdash x=1$ but $x$ is not free in $Sigma$ would be $Sigma={forall y (y=1)}$. Yes, $forall y (y=1)$ implies $x=1$, and it also implies $forall x (x=1)$.



Another example, illustrating how if $x$ does occur free in $Sigma$ then all bets are off: It's true that $x=1vdash x=1$. But $x=1notvdash forall x(x=1)$. If you leave out that "where $x$ does not occur free in $Sigma$" then you're going to conclude that in fact $x=1vdashforall x(x=1)$, which is nonsense; luckily $x=1vdashforall x(x=1)$ does not follow from the correct version of the result we're talking about.






share|cite|improve this answer











$endgroup$



Edit: It turns out that the system you're dealing with is very different from the systems I'm familiar with. Hence more or less everything below is wrong, with regard to that system. I'd simply delete the whole thing but I can't since it's "accepted"...



The reason your version makes no sense is it's false. You're leaving out a crucial hypothesis; what's true, and what it had better say in the book, is this:






If $Sigmavdashphi$, where $x$ does not occur free in $Sigma$, then $Sigmavdashforall xphi$.






That makes much more sense. Informally, saying $x$ does not occur free in $Sigma$ means that the formulas in $Sigma$ do not say anything about $x$. So saying $Sigmavdash phi$ where $x$ does not occur free in $Sigma$ means "you can prove $phi$ without assuming anything about $x$".



Now it makes sense. If you can prove $phi$ from a set of assumptions that don't mention $x$, then $phi$ follows from your assumptions regardless of what $x$ is, so $forall xphi$ "should" also follow from the same assumptions.



Taking $phi$ to be $x=1$ is a bad example, because it's hard to imagine a system where you can prove $x=1$ without assuming anything about $x$. Instead imagine you have some axioms describing how the real numbers work, and you want to prove $forall x(x>1to x^2>1)$. If you can prove $x>1to x^2>1$ without assuming anything special about $x$ then $forall x(x>1to x^2>1)$ follows. (That is how people prove $forall xphi$ in actual math: prove $phi$ without assuming anything about $x$.)



Hmm. An example of a $Sigma$ where $Sigmavdash x=1$ but $x$ is not free in $Sigma$ would be $Sigma={forall y (y=1)}$. Yes, $forall y (y=1)$ implies $x=1$, and it also implies $forall x (x=1)$.



Another example, illustrating how if $x$ does occur free in $Sigma$ then all bets are off: It's true that $x=1vdash x=1$. But $x=1notvdash forall x(x=1)$. If you leave out that "where $x$ does not occur free in $Sigma$" then you're going to conclude that in fact $x=1vdashforall x(x=1)$, which is nonsense; luckily $x=1vdashforall x(x=1)$ does not follow from the correct version of the result we're talking about.







share|cite|improve this answer














share|cite|improve this answer



share|cite|improve this answer








edited Dec 30 '18 at 19:00

























answered Dec 30 '18 at 16:50









David C. UllrichDavid C. Ullrich

61.6k43995




61.6k43995








  • 1




    $begingroup$
    But the exposition of FOL used by the OP is "Mendelson-like" : no restriction on Gen rule. The restriction is on the Deduction Th. So $(x=1) vdash forall x (x=1)$ is formally correct in the system; what is not is to apply DT to it to get : $vdash (x=1) to forall x (x=1)$.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 18:13












  • $begingroup$
    Oh. All I know about logic is what I read in Enderton years ago; the notion of a system were $x=1vdashforall x(x=1)$ makes no sense to me. As sort of a check on whether it's "$x=1$" or $"vdash$" that's totally different: what about $x=1modelsforall x(x=1)$?
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 18:30










  • $begingroup$
    Only browsed the text... it seems to me that is not defined. But $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash varphi(x) [h]$ for every evaluation $h$ and thus $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash forall x varphi(x)$. So, no problem...
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 18:55










  • $begingroup$
    @MauroALLEGRANZA but then in "Mendelson-like logic" what is the difference between $(x=1)$ and $forall x (x=1)$ ? What do those formulas mean?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 19:18










  • $begingroup$
    @Rubena - consider $mathbb N$ as domain of the interpretation. $mathbb N nvDash forall x (x=1)$, obviously, while for $(x=1)$ we need a variable assignment $h$. If $h(x)=1$ then $mathbb N vDash (x=1)[h]$, while for $h'$ such that e.g. $h'(x)=0$ we have that $mathbb N nvDash (x=1)[h']$. So the semantics is Ok: we are licensed to asserts $mathfrak A vDash varphi(x)$ only if every variable assignment $h$ gives the same truth value.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 19:37
















  • 1




    $begingroup$
    But the exposition of FOL used by the OP is "Mendelson-like" : no restriction on Gen rule. The restriction is on the Deduction Th. So $(x=1) vdash forall x (x=1)$ is formally correct in the system; what is not is to apply DT to it to get : $vdash (x=1) to forall x (x=1)$.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 18:13












  • $begingroup$
    Oh. All I know about logic is what I read in Enderton years ago; the notion of a system were $x=1vdashforall x(x=1)$ makes no sense to me. As sort of a check on whether it's "$x=1$" or $"vdash$" that's totally different: what about $x=1modelsforall x(x=1)$?
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 18:30










  • $begingroup$
    Only browsed the text... it seems to me that is not defined. But $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash varphi(x) [h]$ for every evaluation $h$ and thus $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash forall x varphi(x)$. So, no problem...
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 18:55










  • $begingroup$
    @MauroALLEGRANZA but then in "Mendelson-like logic" what is the difference between $(x=1)$ and $forall x (x=1)$ ? What do those formulas mean?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 19:18










  • $begingroup$
    @Rubena - consider $mathbb N$ as domain of the interpretation. $mathbb N nvDash forall x (x=1)$, obviously, while for $(x=1)$ we need a variable assignment $h$. If $h(x)=1$ then $mathbb N vDash (x=1)[h]$, while for $h'$ such that e.g. $h'(x)=0$ we have that $mathbb N nvDash (x=1)[h']$. So the semantics is Ok: we are licensed to asserts $mathfrak A vDash varphi(x)$ only if every variable assignment $h$ gives the same truth value.
    $endgroup$
    – Mauro ALLEGRANZA
    Dec 30 '18 at 19:37










1




1




$begingroup$
But the exposition of FOL used by the OP is "Mendelson-like" : no restriction on Gen rule. The restriction is on the Deduction Th. So $(x=1) vdash forall x (x=1)$ is formally correct in the system; what is not is to apply DT to it to get : $vdash (x=1) to forall x (x=1)$.
$endgroup$
– Mauro ALLEGRANZA
Dec 30 '18 at 18:13






$begingroup$
But the exposition of FOL used by the OP is "Mendelson-like" : no restriction on Gen rule. The restriction is on the Deduction Th. So $(x=1) vdash forall x (x=1)$ is formally correct in the system; what is not is to apply DT to it to get : $vdash (x=1) to forall x (x=1)$.
$endgroup$
– Mauro ALLEGRANZA
Dec 30 '18 at 18:13














$begingroup$
Oh. All I know about logic is what I read in Enderton years ago; the notion of a system were $x=1vdashforall x(x=1)$ makes no sense to me. As sort of a check on whether it's "$x=1$" or $"vdash$" that's totally different: what about $x=1modelsforall x(x=1)$?
$endgroup$
– David C. Ullrich
Dec 30 '18 at 18:30




$begingroup$
Oh. All I know about logic is what I read in Enderton years ago; the notion of a system were $x=1vdashforall x(x=1)$ makes no sense to me. As sort of a check on whether it's "$x=1$" or $"vdash$" that's totally different: what about $x=1modelsforall x(x=1)$?
$endgroup$
– David C. Ullrich
Dec 30 '18 at 18:30












$begingroup$
Only browsed the text... it seems to me that is not defined. But $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash varphi(x) [h]$ for every evaluation $h$ and thus $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash forall x varphi(x)$. So, no problem...
$endgroup$
– Mauro ALLEGRANZA
Dec 30 '18 at 18:55




$begingroup$
Only browsed the text... it seems to me that is not defined. But $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash varphi(x) [h]$ for every evaluation $h$ and thus $mathfrak A vDash varphi(x)$ iff $mathfrak A vDash forall x varphi(x)$. So, no problem...
$endgroup$
– Mauro ALLEGRANZA
Dec 30 '18 at 18:55












$begingroup$
@MauroALLEGRANZA but then in "Mendelson-like logic" what is the difference between $(x=1)$ and $forall x (x=1)$ ? What do those formulas mean?
$endgroup$
– Ruben a
Dec 30 '18 at 19:18




$begingroup$
@MauroALLEGRANZA but then in "Mendelson-like logic" what is the difference between $(x=1)$ and $forall x (x=1)$ ? What do those formulas mean?
$endgroup$
– Ruben a
Dec 30 '18 at 19:18












$begingroup$
@Rubena - consider $mathbb N$ as domain of the interpretation. $mathbb N nvDash forall x (x=1)$, obviously, while for $(x=1)$ we need a variable assignment $h$. If $h(x)=1$ then $mathbb N vDash (x=1)[h]$, while for $h'$ such that e.g. $h'(x)=0$ we have that $mathbb N nvDash (x=1)[h']$. So the semantics is Ok: we are licensed to asserts $mathfrak A vDash varphi(x)$ only if every variable assignment $h$ gives the same truth value.
$endgroup$
– Mauro ALLEGRANZA
Dec 30 '18 at 19:37






$begingroup$
@Rubena - consider $mathbb N$ as domain of the interpretation. $mathbb N nvDash forall x (x=1)$, obviously, while for $(x=1)$ we need a variable assignment $h$. If $h(x)=1$ then $mathbb N vDash (x=1)[h]$, while for $h'$ such that e.g. $h'(x)=0$ we have that $mathbb N nvDash (x=1)[h']$. So the semantics is Ok: we are licensed to asserts $mathfrak A vDash varphi(x)$ only if every variable assignment $h$ gives the same truth value.
$endgroup$
– Mauro ALLEGRANZA
Dec 30 '18 at 19:37













1












$begingroup$

A proof of $varphi$, with $x$ as a free variable, treats $x$ as an arbitrary element of its domain of discourse. This is exactly how we obtain a proof of $forall x ~ varphi$—introduce a variable $x$ and, knowing only those properties of $x$ that hold of all elements in its domain of discourse, prove $varphi$. This is essentially the content of the $forall$-introduction rule (a.k.a. universal generalisation).



If you could prove $x=1$ knowing nothing about $x$ than that it is an element of its domain of discourse, then it would indeed be true that $forall x (x = 1)$ is true. But of course this is only going to be true if the domain of discourse of $x$ is ${ 1 }$. (Or $varnothing$, I suppose.)



Now if you're doing first-order logic, it's likely that your domain of discourse is some ambient set theoretic universe, in which case $x=1$ will almost certainly not be provable, but formulae like $varnothing subseteq x$ and $x in { x }$ are provable.






share|cite|improve this answer











$endgroup$













  • $begingroup$
    The book I'm using doesn't seem to mention anything about a domain of discourse though.. And isn't set theory an extension of first order logic?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:11










  • $begingroup$
    @Rubena: Regarding your second question, a model of a first-order theory is a set together with certain structure (constants, functions, etc.). This means that a model $V$ of (say) ZFC set theory is externally a set, even though internally it is a proper class. But then if you're doing first-order logic, you must be working within some meta-theory, which in all likelihood is itself a model of the theory of sets.
    $endgroup$
    – Clive Newstead
    Dec 30 '18 at 16:36










  • $begingroup$
    Regarding your first question, first-order logic is just a formal system for manipulating symbols, so the variable $x$ doesn't necessarily refer to an element of any set—it's just a symbol. But semantically the variable $x$ must refer to an element of a set, and it is this set that is the domain of discourse of $x$.
    $endgroup$
    – Clive Newstead
    Dec 30 '18 at 16:38










  • $begingroup$
    But then what's the difference between $x=1$ and $forall x (x=1)$ ? If $x=1$ then all elements in the domain of discourse of $x$ are equal to 1? Then how does it differ from $forall x(x=1)$ ?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:48








  • 1




    $begingroup$
    @Rubena No! It's not true that if $x=1$ then all elements in the domain must equal $1$. Nobody has said that. You keep on leaving out that crucial hypothesis. What's true is that if it's possible to prove $x=1$ without assuming anything about $x$ then all elements in the domain must equal $1$.
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 16:53
















1












$begingroup$

A proof of $varphi$, with $x$ as a free variable, treats $x$ as an arbitrary element of its domain of discourse. This is exactly how we obtain a proof of $forall x ~ varphi$—introduce a variable $x$ and, knowing only those properties of $x$ that hold of all elements in its domain of discourse, prove $varphi$. This is essentially the content of the $forall$-introduction rule (a.k.a. universal generalisation).



If you could prove $x=1$ knowing nothing about $x$ than that it is an element of its domain of discourse, then it would indeed be true that $forall x (x = 1)$ is true. But of course this is only going to be true if the domain of discourse of $x$ is ${ 1 }$. (Or $varnothing$, I suppose.)



Now if you're doing first-order logic, it's likely that your domain of discourse is some ambient set theoretic universe, in which case $x=1$ will almost certainly not be provable, but formulae like $varnothing subseteq x$ and $x in { x }$ are provable.






share|cite|improve this answer











$endgroup$













  • $begingroup$
    The book I'm using doesn't seem to mention anything about a domain of discourse though.. And isn't set theory an extension of first order logic?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:11










  • $begingroup$
    @Rubena: Regarding your second question, a model of a first-order theory is a set together with certain structure (constants, functions, etc.). This means that a model $V$ of (say) ZFC set theory is externally a set, even though internally it is a proper class. But then if you're doing first-order logic, you must be working within some meta-theory, which in all likelihood is itself a model of the theory of sets.
    $endgroup$
    – Clive Newstead
    Dec 30 '18 at 16:36










  • $begingroup$
    Regarding your first question, first-order logic is just a formal system for manipulating symbols, so the variable $x$ doesn't necessarily refer to an element of any set—it's just a symbol. But semantically the variable $x$ must refer to an element of a set, and it is this set that is the domain of discourse of $x$.
    $endgroup$
    – Clive Newstead
    Dec 30 '18 at 16:38










  • $begingroup$
    But then what's the difference between $x=1$ and $forall x (x=1)$ ? If $x=1$ then all elements in the domain of discourse of $x$ are equal to 1? Then how does it differ from $forall x(x=1)$ ?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:48








  • 1




    $begingroup$
    @Rubena No! It's not true that if $x=1$ then all elements in the domain must equal $1$. Nobody has said that. You keep on leaving out that crucial hypothesis. What's true is that if it's possible to prove $x=1$ without assuming anything about $x$ then all elements in the domain must equal $1$.
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 16:53














1












1








1





$begingroup$

A proof of $varphi$, with $x$ as a free variable, treats $x$ as an arbitrary element of its domain of discourse. This is exactly how we obtain a proof of $forall x ~ varphi$—introduce a variable $x$ and, knowing only those properties of $x$ that hold of all elements in its domain of discourse, prove $varphi$. This is essentially the content of the $forall$-introduction rule (a.k.a. universal generalisation).



If you could prove $x=1$ knowing nothing about $x$ than that it is an element of its domain of discourse, then it would indeed be true that $forall x (x = 1)$ is true. But of course this is only going to be true if the domain of discourse of $x$ is ${ 1 }$. (Or $varnothing$, I suppose.)



Now if you're doing first-order logic, it's likely that your domain of discourse is some ambient set theoretic universe, in which case $x=1$ will almost certainly not be provable, but formulae like $varnothing subseteq x$ and $x in { x }$ are provable.






share|cite|improve this answer











$endgroup$



A proof of $varphi$, with $x$ as a free variable, treats $x$ as an arbitrary element of its domain of discourse. This is exactly how we obtain a proof of $forall x ~ varphi$—introduce a variable $x$ and, knowing only those properties of $x$ that hold of all elements in its domain of discourse, prove $varphi$. This is essentially the content of the $forall$-introduction rule (a.k.a. universal generalisation).



If you could prove $x=1$ knowing nothing about $x$ than that it is an element of its domain of discourse, then it would indeed be true that $forall x (x = 1)$ is true. But of course this is only going to be true if the domain of discourse of $x$ is ${ 1 }$. (Or $varnothing$, I suppose.)



Now if you're doing first-order logic, it's likely that your domain of discourse is some ambient set theoretic universe, in which case $x=1$ will almost certainly not be provable, but formulae like $varnothing subseteq x$ and $x in { x }$ are provable.







share|cite|improve this answer














share|cite|improve this answer



share|cite|improve this answer








edited Dec 30 '18 at 17:40









David C. Ullrich

61.6k43995




61.6k43995










answered Dec 30 '18 at 15:18









Clive NewsteadClive Newstead

51.9k474136




51.9k474136












  • $begingroup$
    The book I'm using doesn't seem to mention anything about a domain of discourse though.. And isn't set theory an extension of first order logic?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:11










  • $begingroup$
    @Rubena: Regarding your second question, a model of a first-order theory is a set together with certain structure (constants, functions, etc.). This means that a model $V$ of (say) ZFC set theory is externally a set, even though internally it is a proper class. But then if you're doing first-order logic, you must be working within some meta-theory, which in all likelihood is itself a model of the theory of sets.
    $endgroup$
    – Clive Newstead
    Dec 30 '18 at 16:36










  • $begingroup$
    Regarding your first question, first-order logic is just a formal system for manipulating symbols, so the variable $x$ doesn't necessarily refer to an element of any set—it's just a symbol. But semantically the variable $x$ must refer to an element of a set, and it is this set that is the domain of discourse of $x$.
    $endgroup$
    – Clive Newstead
    Dec 30 '18 at 16:38










  • $begingroup$
    But then what's the difference between $x=1$ and $forall x (x=1)$ ? If $x=1$ then all elements in the domain of discourse of $x$ are equal to 1? Then how does it differ from $forall x(x=1)$ ?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:48








  • 1




    $begingroup$
    @Rubena No! It's not true that if $x=1$ then all elements in the domain must equal $1$. Nobody has said that. You keep on leaving out that crucial hypothesis. What's true is that if it's possible to prove $x=1$ without assuming anything about $x$ then all elements in the domain must equal $1$.
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 16:53


















  • $begingroup$
    The book I'm using doesn't seem to mention anything about a domain of discourse though.. And isn't set theory an extension of first order logic?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:11










  • $begingroup$
    @Rubena: Regarding your second question, a model of a first-order theory is a set together with certain structure (constants, functions, etc.). This means that a model $V$ of (say) ZFC set theory is externally a set, even though internally it is a proper class. But then if you're doing first-order logic, you must be working within some meta-theory, which in all likelihood is itself a model of the theory of sets.
    $endgroup$
    – Clive Newstead
    Dec 30 '18 at 16:36










  • $begingroup$
    Regarding your first question, first-order logic is just a formal system for manipulating symbols, so the variable $x$ doesn't necessarily refer to an element of any set—it's just a symbol. But semantically the variable $x$ must refer to an element of a set, and it is this set that is the domain of discourse of $x$.
    $endgroup$
    – Clive Newstead
    Dec 30 '18 at 16:38










  • $begingroup$
    But then what's the difference between $x=1$ and $forall x (x=1)$ ? If $x=1$ then all elements in the domain of discourse of $x$ are equal to 1? Then how does it differ from $forall x(x=1)$ ?
    $endgroup$
    – Ruben a
    Dec 30 '18 at 16:48








  • 1




    $begingroup$
    @Rubena No! It's not true that if $x=1$ then all elements in the domain must equal $1$. Nobody has said that. You keep on leaving out that crucial hypothesis. What's true is that if it's possible to prove $x=1$ without assuming anything about $x$ then all elements in the domain must equal $1$.
    $endgroup$
    – David C. Ullrich
    Dec 30 '18 at 16:53
















$begingroup$
The book I'm using doesn't seem to mention anything about a domain of discourse though.. And isn't set theory an extension of first order logic?
$endgroup$
– Ruben a
Dec 30 '18 at 16:11




$begingroup$
The book I'm using doesn't seem to mention anything about a domain of discourse though.. And isn't set theory an extension of first order logic?
$endgroup$
– Ruben a
Dec 30 '18 at 16:11












$begingroup$
@Rubena: Regarding your second question, a model of a first-order theory is a set together with certain structure (constants, functions, etc.). This means that a model $V$ of (say) ZFC set theory is externally a set, even though internally it is a proper class. But then if you're doing first-order logic, you must be working within some meta-theory, which in all likelihood is itself a model of the theory of sets.
$endgroup$
– Clive Newstead
Dec 30 '18 at 16:36




$begingroup$
@Rubena: Regarding your second question, a model of a first-order theory is a set together with certain structure (constants, functions, etc.). This means that a model $V$ of (say) ZFC set theory is externally a set, even though internally it is a proper class. But then if you're doing first-order logic, you must be working within some meta-theory, which in all likelihood is itself a model of the theory of sets.
$endgroup$
– Clive Newstead
Dec 30 '18 at 16:36












$begingroup$
Regarding your first question, first-order logic is just a formal system for manipulating symbols, so the variable $x$ doesn't necessarily refer to an element of any set—it's just a symbol. But semantically the variable $x$ must refer to an element of a set, and it is this set that is the domain of discourse of $x$.
$endgroup$
– Clive Newstead
Dec 30 '18 at 16:38




$begingroup$
Regarding your first question, first-order logic is just a formal system for manipulating symbols, so the variable $x$ doesn't necessarily refer to an element of any set—it's just a symbol. But semantically the variable $x$ must refer to an element of a set, and it is this set that is the domain of discourse of $x$.
$endgroup$
– Clive Newstead
Dec 30 '18 at 16:38












$begingroup$
But then what's the difference between $x=1$ and $forall x (x=1)$ ? If $x=1$ then all elements in the domain of discourse of $x$ are equal to 1? Then how does it differ from $forall x(x=1)$ ?
$endgroup$
– Ruben a
Dec 30 '18 at 16:48






$begingroup$
But then what's the difference between $x=1$ and $forall x (x=1)$ ? If $x=1$ then all elements in the domain of discourse of $x$ are equal to 1? Then how does it differ from $forall x(x=1)$ ?
$endgroup$
– Ruben a
Dec 30 '18 at 16:48






1




1




$begingroup$
@Rubena No! It's not true that if $x=1$ then all elements in the domain must equal $1$. Nobody has said that. You keep on leaving out that crucial hypothesis. What's true is that if it's possible to prove $x=1$ without assuming anything about $x$ then all elements in the domain must equal $1$.
$endgroup$
– David C. Ullrich
Dec 30 '18 at 16:53




$begingroup$
@Rubena No! It's not true that if $x=1$ then all elements in the domain must equal $1$. Nobody has said that. You keep on leaving out that crucial hypothesis. What's true is that if it's possible to prove $x=1$ without assuming anything about $x$ then all elements in the domain must equal $1$.
$endgroup$
– David C. Ullrich
Dec 30 '18 at 16:53


















draft saved

draft discarded




















































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.




draft saved


draft discarded














StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3056916%2fif-sigma-vdash-varphi-then-sigma-vdash-forall-x-varphi-why-when-v%23new-answer', 'question_page');
}
);

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







Popular posts from this blog

Probability when a professor distributes a quiz and homework assignment to a class of n students.

Aardman Animations

Are they similar matrix