If $Sigma vdash varphi$ then $Sigma vdash forall x varphi$. Why when $(varphi implies forall x varphi)$ is...
$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
first-order-logic
asked Dec 30 '18 at 15:12
Ruben aRuben a
153
$endgroup$
|
show 3 more comments
$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
first-order-logic
asked Dec 30 '18 at 15:12
Ruben aRuben a
153
$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
|
show 3 more comments
$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
first-order-logic
asked Dec 30 '18 at 15:12
Ruben aRuben a
153
$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
first-order-logic
asked Dec 30 '18 at 15:12
Ruben aRuben a
153
asked Dec 30 '18 at 15:12
Ruben aRuben a
153
edited Dec 30 '18 at 16:23
Ruben a
asked Dec 30 '18 at 15:12
Ruben aRuben a
153
asked Dec 30 '18 at 15:12
Ruben aRuben a
153
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
|
show 3 more comments
$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
|
show 3 more comments
2 Answers
2
active
oldest
votes
$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.
answered Dec 30 '18 at 16:50
David C. UllrichDavid C. Ullrich
61k43994
$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
add a comment |
$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.
edited Dec 30 '18 at 17:40
David C. Ullrich
61k43994
answered Dec 30 '18 at 15:18
Clive NewsteadClive Newstead
51.8k474136
$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
|
show 2 more comments
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%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
$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.
answered Dec 30 '18 at 16:50
David C. UllrichDavid C. Ullrich
61k43994
$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
add a comment |
$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.
answered Dec 30 '18 at 16:50
David C. UllrichDavid C. Ullrich
61k43994
$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
add a comment |
$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.
answered Dec 30 '18 at 16:50
David C. UllrichDavid C. Ullrich
61k43994
$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.
answered Dec 30 '18 at 16:50
David C. UllrichDavid C. Ullrich
61k43994
edited Dec 30 '18 at 19:00
answered Dec 30 '18 at 16:50
David C. UllrichDavid C. Ullrich
61k43994
answered Dec 30 '18 at 16:50
David C. UllrichDavid C. Ullrich
61k43994
answered Dec 30 '18 at 16:50
David C. UllrichDavid C. Ullrich
61k43994
61k43994
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
add a comment |
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
add a comment |
$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.
edited Dec 30 '18 at 17:40
David C. Ullrich
61k43994
answered Dec 30 '18 at 15:18
Clive NewsteadClive Newstead
51.8k474136
$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
|
show 2 more comments
$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.
edited Dec 30 '18 at 17:40
David C. Ullrich
61k43994
answered Dec 30 '18 at 15:18
Clive NewsteadClive Newstead
51.8k474136
$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
|
show 2 more comments
$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.
edited Dec 30 '18 at 17:40
David C. Ullrich
61k43994
answered Dec 30 '18 at 15:18
Clive NewsteadClive Newstead
51.8k474136
$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.
edited Dec 30 '18 at 17:40
David C. Ullrich
61k43994
answered Dec 30 '18 at 15:18
Clive NewsteadClive Newstead
51.8k474136
edited Dec 30 '18 at 17:40
David C. Ullrich
61k43994
edited Dec 30 '18 at 17:40
David C. Ullrich
61k43994
edited Dec 30 '18 at 17:40
David C. Ullrich
61k43994
61k43994
answered Dec 30 '18 at 15:18
Clive NewsteadClive Newstead
51.8k474136
answered Dec 30 '18 at 15:18
Clive NewsteadClive Newstead
51.8k474136
answered Dec 30 '18 at 15:18
Clive NewsteadClive Newstead
51.8k474136
51.8k474136
$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
|
show 2 more comments
$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
|
show 2 more comments
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%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
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$
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