Mixing
How to prove (4|n)→(2|n) in P
$begingroup$
Let 4|n means n is divisible by 4. How to prove (4|n)→(2|n) in P?
Knowing that we have ¬(4|5), so we have ¬∀n(4|n). That is, we can not suppose 4|n because otherwise we would have ∀n(4|n) by generalization, but the hypothesis is in contradiction with ¬∀n(4|n). This shows that the hypothetical proof: if B ├ C then ├ B→C of propositional logic cannot be applied to predicate logic.
We prove (4|n)→(2|n) intuitively by suppose 4|n. If we cannot suppose it, how to prove it?
logic predicate-logic
asked Jan 17 at 16:20
user49413user49413
294
$endgroup$
add a comment |
$begingroup$
Let 4|n means n is divisible by 4. How to prove (4|n)→(2|n) in P?
Knowing that we have ¬(4|5), so we have ¬∀n(4|n). That is, we can not suppose 4|n because otherwise we would have ∀n(4|n) by generalization, but the hypothesis is in contradiction with ¬∀n(4|n). This shows that the hypothetical proof: if B ├ C then ├ B→C of propositional logic cannot be applied to predicate logic.
We prove (4|n)→(2|n) intuitively by suppose 4|n. If we cannot suppose it, how to prove it?
logic predicate-logic
asked Jan 17 at 16:20
user49413user49413
294
$endgroup$
$begingroup$
Please try to use mathjax. Thank you.
$endgroup$
– Jakobian
Jan 17 at 16:28
$begingroup$
@user49413 I think you have misunderstood. $(4|n) rightarrow (2|n)$. It is not equivalent to $(4|n) forall n$. However, it is equivalent $lnot (4|n) lor (2|n) forall n$.
$endgroup$
– gandalf61
Jan 17 at 16:58
$begingroup$
(4|n)→(2|n) means ∀n((4|n)→(2|n)) by generalization or ∀n(¬(4|n)∨(2|n)) if you prefer. It doesn't mean (∀n(4|n))→(∀n(2|n)).
$endgroup$
– user49413
Jan 17 at 17:14
$begingroup$
If we suppose 4|n, then we would have ∀n(4|n) and would prove (∀n(4|n))→(∀n(2|n)) which is evidently wrong. This is from another point of view why we cannot suppose 4|n.
$endgroup$
– user49413
Jan 17 at 17:23
add a comment |
$begingroup$
Let 4|n means n is divisible by 4. How to prove (4|n)→(2|n) in P?
Knowing that we have ¬(4|5), so we have ¬∀n(4|n). That is, we can not suppose 4|n because otherwise we would have ∀n(4|n) by generalization, but the hypothesis is in contradiction with ¬∀n(4|n). This shows that the hypothetical proof: if B ├ C then ├ B→C of propositional logic cannot be applied to predicate logic.
We prove (4|n)→(2|n) intuitively by suppose 4|n. If we cannot suppose it, how to prove it?
logic predicate-logic
asked Jan 17 at 16:20
user49413user49413
294
$endgroup$
Let 4|n means n is divisible by 4. How to prove (4|n)→(2|n) in P?
Knowing that we have ¬(4|5), so we have ¬∀n(4|n). That is, we can not suppose 4|n because otherwise we would have ∀n(4|n) by generalization, but the hypothesis is in contradiction with ¬∀n(4|n). This shows that the hypothetical proof: if B ├ C then ├ B→C of propositional logic cannot be applied to predicate logic.
We prove (4|n)→(2|n) intuitively by suppose 4|n. If we cannot suppose it, how to prove it?
logic predicate-logic
logic predicate-logic
asked Jan 17 at 16:20
user49413user49413
294
asked Jan 17 at 16:20
user49413user49413
294
asked Jan 17 at 16:20
user49413user49413
294
asked Jan 17 at 16:20
user49413user49413
294
asked Jan 17 at 16:20
user49413user49413
294
294
$begingroup$
Please try to use mathjax. Thank you.
$endgroup$
– Jakobian
Jan 17 at 16:28
$begingroup$
@user49413 I think you have misunderstood. $(4|n) rightarrow (2|n)$. It is not equivalent to $(4|n) forall n$. However, it is equivalent $lnot (4|n) lor (2|n) forall n$.
$endgroup$
– gandalf61
Jan 17 at 16:58
$begingroup$
(4|n)→(2|n) means ∀n((4|n)→(2|n)) by generalization or ∀n(¬(4|n)∨(2|n)) if you prefer. It doesn't mean (∀n(4|n))→(∀n(2|n)).
$endgroup$
– user49413
Jan 17 at 17:14
$begingroup$
If we suppose 4|n, then we would have ∀n(4|n) and would prove (∀n(4|n))→(∀n(2|n)) which is evidently wrong. This is from another point of view why we cannot suppose 4|n.
$endgroup$
– user49413
Jan 17 at 17:23
add a comment |
$begingroup$
Please try to use mathjax. Thank you.
$endgroup$
– Jakobian
Jan 17 at 16:28
$begingroup$
@user49413 I think you have misunderstood. $(4|n) rightarrow (2|n)$. It is not equivalent to $(4|n) forall n$. However, it is equivalent $lnot (4|n) lor (2|n) forall n$.
$endgroup$
– gandalf61
Jan 17 at 16:58
$begingroup$
(4|n)→(2|n) means ∀n((4|n)→(2|n)) by generalization or ∀n(¬(4|n)∨(2|n)) if you prefer. It doesn't mean (∀n(4|n))→(∀n(2|n)).
$endgroup$
– user49413
Jan 17 at 17:14
$begingroup$
If we suppose 4|n, then we would have ∀n(4|n) and would prove (∀n(4|n))→(∀n(2|n)) which is evidently wrong. This is from another point of view why we cannot suppose 4|n.
$endgroup$
– user49413
Jan 17 at 17:23
$begingroup$
Please try to use mathjax. Thank you.
$endgroup$
– Jakobian
Jan 17 at 16:28
$begingroup$
Please try to use mathjax. Thank you.
$endgroup$
– Jakobian
Jan 17 at 16:28
$begingroup$
@user49413 I think you have misunderstood. $(4|n) rightarrow (2|n)$. It is not equivalent to $(4|n) forall n$. However, it is equivalent $lnot (4|n) lor (2|n) forall n$.
$endgroup$
– gandalf61
Jan 17 at 16:58
$begingroup$
@user49413 I think you have misunderstood. $(4|n) rightarrow (2|n)$. It is not equivalent to $(4|n) forall n$. However, it is equivalent $lnot (4|n) lor (2|n) forall n$.
$endgroup$
– gandalf61
Jan 17 at 16:58
$begingroup$
(4|n)→(2|n) means ∀n((4|n)→(2|n)) by generalization or ∀n(¬(4|n)∨(2|n)) if you prefer. It doesn't mean (∀n(4|n))→(∀n(2|n)).
$endgroup$
– user49413
Jan 17 at 17:14
$begingroup$
(4|n)→(2|n) means ∀n((4|n)→(2|n)) by generalization or ∀n(¬(4|n)∨(2|n)) if you prefer. It doesn't mean (∀n(4|n))→(∀n(2|n)).
$endgroup$
– user49413
Jan 17 at 17:14
$begingroup$
If we suppose 4|n, then we would have ∀n(4|n) and would prove (∀n(4|n))→(∀n(2|n)) which is evidently wrong. This is from another point of view why we cannot suppose 4|n.
$endgroup$
– user49413
Jan 17 at 17:23
$begingroup$
If we suppose 4|n, then we would have ∀n(4|n) and would prove (∀n(4|n))→(∀n(2|n)) which is evidently wrong. This is from another point of view why we cannot suppose 4|n.
$endgroup$
– user49413
Jan 17 at 17:23
add a comment |
3 Answers
3
active
oldest
votes
$begingroup$
Let me assume what you want to prove is $(forall nin mathbb{Z})[4|nimplies 2|n]$ (I'm not sure what your $P$ stands for, positive integers?)
Proof: For any integer $n$, if $4|n$, we can find an integer $p$ such that $4p=n$ (This follows by the Division Theorem). Then, by arithmetic we have $4p=2(2p)=n$. Since $p$ is an integer, $2p$ is also an integer. Thus, let $q=2p$, and we have found the integer $q$ that satisfies $2q=n$. By the definition of divisibility, $2|n$. That completes the proof.
Clarification: To prove the implication, we do not suppose $4|n$ for all $n$, we suppose that for each possible $n$.
answered Jan 18 at 10:58
MacrophageMacrophage
1,181115
$endgroup$
$begingroup$
In your proof, you say "if 4|n", so you suppose 4|n. I know that what you mean for "if 4|n" is not ∀n(4|n) but "for the n so that 4|n". But in P, that is, in your n∈Z, to suppose 4|n does mean ∀n(4|n). That is THE PROBLEM. So, my question is in reality could we prove the formula without supposing 4|n?
$endgroup$
– user49413
Jan 19 at 10:16
$begingroup$
@user49413 I see what you mean now. Of course, prove the contrapositive, so you assume not (2|n) and prove not (4|n)
$endgroup$
– Macrophage
Jan 19 at 10:44
$begingroup$
We meet the same problem: we cannot assume 2|n because we have ¬(2|3) so ¬∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:15
$begingroup$
@user49413 I think your logic is not quite right. We test for each n, what will happen if we assume 2|n, not 2|n for all n.
$endgroup$
– Macrophage
Jan 19 at 11:18
$begingroup$
I know that by supposing 2|n, what we would like to mean is "for the n so that 2|n", but not "∀n(2|n)". But at the actual status, in theory, to assume 2|n means to add 2|n, temporally, to the theory system so we can use it as a TRUE formula, so means ∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:27
add a comment |
$begingroup$
Sketch of a proof (Natural Deduction-like).
The proof obviously needs Peano axioms; thus, what we will prove is :
$mathsf {PA} vdash forall n [exists k (n = 4 times k) to exists l (n = 2 times l)]$.
1) $exists k (n = 4 times k)$ --- assumed [a] (this is : $4 | n$)
2) $n = 4 times k_1$ --- assumed [b] from 1) for $exists$-elim
3) $mathsf {PA} vdash (4= 2 times 2)$ --- from axioms for $times$
4) $n = (2 times 2) times k_1$ --- from 2) and 3) by properties of equality
Now we need the commutative law for $times$, i.e. :
$mathsf {PA} vdash forall a,b,c [(a times b) times c = a times (b times c)]$
and we have, by transitivity of equality :
5) $n=2 times (2 times k_1)$
6) $exists l (n = 2 times l)$ --- from 5) by $exists$-intro (this is : $2 | n$)
7) $exists l (n = 2 times l)$ --- from 1) and 2)-6) by $exists$-elim, discharging [b]
8) $exists k (n = 4 times k) to exists l (n = 2 times l)$ --- from 1) and 7) by $to$-intro, discharging [a]
9) $mathsf {PA} vdash forall n [exists k (n = 4 times k) to exists l (n = 2 times l)]$ --- from 8) by $forall$-intro.
Note : you concern about Deduction Theorem is right for Hilbert-styple proof systems with "unrestricted" Generalization rule (see Mendelson's textbook).
The restriction on Universal generalization rule typical of Natural Deduction gives us the benefit of using $to$-introduction rule (aka : Deduction Theorem) without restrictions also in predicate calculus.
In any case, the above proof is sound also for Mendelson's system, because the only use of Generalization in performed after the Deduction Th step to a variable $n$ that is not free in any assumption.
answered Jan 17 at 16:37
Mauro ALLEGRANZAMauro ALLEGRANZA
66.5k449115
$endgroup$
$begingroup$
By 1), you suppose 4|n. But you introduce contradiction already by this step!
$endgroup$
– user49413
Jan 17 at 16:41
$begingroup$
@user49413 Your question seems to be asking how to use $4mid n$ to show that $2mid n$ for some $n$. Why would supposing $4mid n$ introduce contradiction?
$endgroup$
– Cardioid_Ass_22
Jan 17 at 16:54
$begingroup$
It's in the question itself. If we suppose 4|n, then we have ∀n(4|n) by generalization. But we have already ¬∀n(4|n) by ¬(4|5). So to suppose 4|n leads to contradiction.
$endgroup$
– user49413
Jan 17 at 16:58
$begingroup$
@user49413 - Universal generalization does not work that way. I've assumed $∃k (n=4×k)$ and derived $∃l (n=2×l)$, then use Deduction Theorem to get $∃k (n=4×k) to ∃l (n=2×l)$ and finally Gen to get : $forall n [∃k (n=4×k) to ∃l (n=2×l)]$.
$endgroup$
– Mauro ALLEGRANZA
Jan 17 at 19:56
$begingroup$
The step "1) ∃k (n=4×k) --- 4|n" means "if 4|n, then ∃k (n=4×k)". Otherwise, what is the reason for "∃k (n=4×k)"? So, you suppose 4|n.
$endgroup$
– user49413
Jan 19 at 10:24
|
show 5 more comments
$begingroup$
I doubt that (4|n)→(2|n) can be proven in P. I think that it could be necessary to add a new rule of deduction for that. Let's call it the rule of conditional deduction and denote it by CDt here.
With CDt, we deduct in a restricted domain of discourse. The domain of discourse of P is natural number N. For any non empty class C⊂N, CDt works as a theory system P' that is the same as P except that its domain of discourse is C. Then, all TRUE formulas in P free of the quantifier ∃ are TRUE formula in P'. A TRUE formula in P containing ∃ cannot be translated to P'. Knowing that ¬∀x(f(x)) should be considered as ∃x(¬f(x)), and ¬∃x(f(x)) should be considered as ∀x(¬f(x)). So, we have less TRUE formulas in P' than in P at beginning of CDt. A TRUE formula in P' containing neither free variable nor quantifier ∀ is also a TRUE formula in P. A TRUE formula containing free variable x denoted by f(x) can be translated to a TRUE formula in P by (x∈C)→f(x), similarly, ∀x(f(x)) to ∀x((x∈C)→f(x)).
With CDt for proving (4|n)→(2|n), we use the C relative to the formula 4|n according to the axiom IV.1 which is similar to the axiom of comprehension. So, we have ∀n((n∈C)↔(4|n)) in P so also in P'.
We can add 4|n to P', or in other words assume 4|n in P', under CDt because the ¬(4|5) in P cannot lead to contradiction in P' for the reason that 5 is not in C. Then we can obtain 2|n by deduction in P', and translate 2|n in P' to (4|n)→(2|n) in P.
This process is the same as what we do usually by intuition. So, CDt just formalize what we do usually by introducing restricted domain of discourse. We get (4|n)→(2|n) by extension of domain of discourse, but not by reason that it's part of some TRUE formula or it's defined recursively.
In general, the restricted domain of discourse can be extended to variable domain of discourse that can further be used to extend P to a bigger domain of discourse. For example, (4|n)→(2|n) would become isN(n)→((4|n)→(2|n)) where isN(x) is TRUE if and only if x is a natural number. This would permit a unified formal theory system by mixing all theory systems in a unified domain of discourse: the universe.
answered Jan 22 at 11:57
user49413user49413
294
$endgroup$
add a comment |
Your Answer
StackExchange.ifUsing("editor", function () {
return StackExchange.using("mathjaxEditing", function () {
StackExchange.MarkdownEditor.creationCallbacks.add(function (editor, postfix) {
StackExchange.mathjaxEditing.prepareWmdForMathJax(editor, postfix, [["$", "$"], ["\\(","\\)"]]);
});
});
}, "mathjax-editing");
StackExchange.ready(function() {
var channelOptions = {
tags: "".split(" "),
id: "69"
};
initTagRenderer("".split(" "), "".split(" "), channelOptions);
StackExchange.using("externalEditor", function() {
// Have to fire editor after snippets, if snippets enabled
if (StackExchange.settings.snippets.snippetsEnabled) {
StackExchange.using("snippets", function() {
createEditor();
});
}
else {
createEditor();
}
});
function createEditor() {
StackExchange.prepareEditor({
heartbeatType: 'answer',
autoActivateHeartbeat: false,
convertImagesToLinks: true,
noModals: true,
showLowRepImageUploadWarning: true,
reputationToPostImages: 10,
bindNavPrevention: true,
postfix: "",
imageUploader: {
brandingHtml: "Powered by u003ca class="icon-imgur-white" href="https://imgur.com/"u003eu003c/au003e",
contentPolicyHtml: "User contributions licensed under u003ca href="https://creativecommons.org/licenses/by-sa/3.0/"u003ecc by-sa 3.0 with attribution requiredu003c/au003e u003ca href="https://stackoverflow.com/legal/content-policy"u003e(content policy)u003c/au003e",
allowUrls: true
},
noCode: true, onDemand: true,
discardSelector: ".discard-answer"
,immediatelyShowMarkdownHelp:true
});
}
});
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3077187%2fhow-to-prove-4n%25e2%2586%25922n-in-p%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
3 Answers
3
active
oldest
votes
3 Answers
3
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
Let me assume what you want to prove is $(forall nin mathbb{Z})[4|nimplies 2|n]$ (I'm not sure what your $P$ stands for, positive integers?)
Proof: For any integer $n$, if $4|n$, we can find an integer $p$ such that $4p=n$ (This follows by the Division Theorem). Then, by arithmetic we have $4p=2(2p)=n$. Since $p$ is an integer, $2p$ is also an integer. Thus, let $q=2p$, and we have found the integer $q$ that satisfies $2q=n$. By the definition of divisibility, $2|n$. That completes the proof.
Clarification: To prove the implication, we do not suppose $4|n$ for all $n$, we suppose that for each possible $n$.
answered Jan 18 at 10:58
MacrophageMacrophage
1,181115
$endgroup$
$begingroup$
In your proof, you say "if 4|n", so you suppose 4|n. I know that what you mean for "if 4|n" is not ∀n(4|n) but "for the n so that 4|n". But in P, that is, in your n∈Z, to suppose 4|n does mean ∀n(4|n). That is THE PROBLEM. So, my question is in reality could we prove the formula without supposing 4|n?
$endgroup$
– user49413
Jan 19 at 10:16
$begingroup$
@user49413 I see what you mean now. Of course, prove the contrapositive, so you assume not (2|n) and prove not (4|n)
$endgroup$
– Macrophage
Jan 19 at 10:44
$begingroup$
We meet the same problem: we cannot assume 2|n because we have ¬(2|3) so ¬∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:15
$begingroup$
@user49413 I think your logic is not quite right. We test for each n, what will happen if we assume 2|n, not 2|n for all n.
$endgroup$
– Macrophage
Jan 19 at 11:18
$begingroup$
I know that by supposing 2|n, what we would like to mean is "for the n so that 2|n", but not "∀n(2|n)". But at the actual status, in theory, to assume 2|n means to add 2|n, temporally, to the theory system so we can use it as a TRUE formula, so means ∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:27
add a comment |
$begingroup$
Let me assume what you want to prove is $(forall nin mathbb{Z})[4|nimplies 2|n]$ (I'm not sure what your $P$ stands for, positive integers?)
Proof: For any integer $n$, if $4|n$, we can find an integer $p$ such that $4p=n$ (This follows by the Division Theorem). Then, by arithmetic we have $4p=2(2p)=n$. Since $p$ is an integer, $2p$ is also an integer. Thus, let $q=2p$, and we have found the integer $q$ that satisfies $2q=n$. By the definition of divisibility, $2|n$. That completes the proof.
Clarification: To prove the implication, we do not suppose $4|n$ for all $n$, we suppose that for each possible $n$.
answered Jan 18 at 10:58
MacrophageMacrophage
1,181115
$endgroup$
$begingroup$
In your proof, you say "if 4|n", so you suppose 4|n. I know that what you mean for "if 4|n" is not ∀n(4|n) but "for the n so that 4|n". But in P, that is, in your n∈Z, to suppose 4|n does mean ∀n(4|n). That is THE PROBLEM. So, my question is in reality could we prove the formula without supposing 4|n?
$endgroup$
– user49413
Jan 19 at 10:16
$begingroup$
@user49413 I see what you mean now. Of course, prove the contrapositive, so you assume not (2|n) and prove not (4|n)
$endgroup$
– Macrophage
Jan 19 at 10:44
$begingroup$
We meet the same problem: we cannot assume 2|n because we have ¬(2|3) so ¬∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:15
$begingroup$
@user49413 I think your logic is not quite right. We test for each n, what will happen if we assume 2|n, not 2|n for all n.
$endgroup$
– Macrophage
Jan 19 at 11:18
$begingroup$
I know that by supposing 2|n, what we would like to mean is "for the n so that 2|n", but not "∀n(2|n)". But at the actual status, in theory, to assume 2|n means to add 2|n, temporally, to the theory system so we can use it as a TRUE formula, so means ∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:27
add a comment |
$begingroup$
Let me assume what you want to prove is $(forall nin mathbb{Z})[4|nimplies 2|n]$ (I'm not sure what your $P$ stands for, positive integers?)
Proof: For any integer $n$, if $4|n$, we can find an integer $p$ such that $4p=n$ (This follows by the Division Theorem). Then, by arithmetic we have $4p=2(2p)=n$. Since $p$ is an integer, $2p$ is also an integer. Thus, let $q=2p$, and we have found the integer $q$ that satisfies $2q=n$. By the definition of divisibility, $2|n$. That completes the proof.
Clarification: To prove the implication, we do not suppose $4|n$ for all $n$, we suppose that for each possible $n$.
answered Jan 18 at 10:58
MacrophageMacrophage
1,181115
$endgroup$
Let me assume what you want to prove is $(forall nin mathbb{Z})[4|nimplies 2|n]$ (I'm not sure what your $P$ stands for, positive integers?)
Proof: For any integer $n$, if $4|n$, we can find an integer $p$ such that $4p=n$ (This follows by the Division Theorem). Then, by arithmetic we have $4p=2(2p)=n$. Since $p$ is an integer, $2p$ is also an integer. Thus, let $q=2p$, and we have found the integer $q$ that satisfies $2q=n$. By the definition of divisibility, $2|n$. That completes the proof.
Clarification: To prove the implication, we do not suppose $4|n$ for all $n$, we suppose that for each possible $n$.
answered Jan 18 at 10:58
MacrophageMacrophage
1,181115
answered Jan 18 at 10:58
MacrophageMacrophage
1,181115
answered Jan 18 at 10:58
MacrophageMacrophage
1,181115
answered Jan 18 at 10:58
MacrophageMacrophage
1,181115
1,181115
$begingroup$
In your proof, you say "if 4|n", so you suppose 4|n. I know that what you mean for "if 4|n" is not ∀n(4|n) but "for the n so that 4|n". But in P, that is, in your n∈Z, to suppose 4|n does mean ∀n(4|n). That is THE PROBLEM. So, my question is in reality could we prove the formula without supposing 4|n?
$endgroup$
– user49413
Jan 19 at 10:16
$begingroup$
@user49413 I see what you mean now. Of course, prove the contrapositive, so you assume not (2|n) and prove not (4|n)
$endgroup$
– Macrophage
Jan 19 at 10:44
$begingroup$
We meet the same problem: we cannot assume 2|n because we have ¬(2|3) so ¬∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:15
$begingroup$
@user49413 I think your logic is not quite right. We test for each n, what will happen if we assume 2|n, not 2|n for all n.
$endgroup$
– Macrophage
Jan 19 at 11:18
$begingroup$
I know that by supposing 2|n, what we would like to mean is "for the n so that 2|n", but not "∀n(2|n)". But at the actual status, in theory, to assume 2|n means to add 2|n, temporally, to the theory system so we can use it as a TRUE formula, so means ∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:27
add a comment |
$begingroup$
In your proof, you say "if 4|n", so you suppose 4|n. I know that what you mean for "if 4|n" is not ∀n(4|n) but "for the n so that 4|n". But in P, that is, in your n∈Z, to suppose 4|n does mean ∀n(4|n). That is THE PROBLEM. So, my question is in reality could we prove the formula without supposing 4|n?
$endgroup$
– user49413
Jan 19 at 10:16
$begingroup$
@user49413 I see what you mean now. Of course, prove the contrapositive, so you assume not (2|n) and prove not (4|n)
$endgroup$
– Macrophage
Jan 19 at 10:44
$begingroup$
We meet the same problem: we cannot assume 2|n because we have ¬(2|3) so ¬∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:15
$begingroup$
@user49413 I think your logic is not quite right. We test for each n, what will happen if we assume 2|n, not 2|n for all n.
$endgroup$
– Macrophage
Jan 19 at 11:18
$begingroup$
I know that by supposing 2|n, what we would like to mean is "for the n so that 2|n", but not "∀n(2|n)". But at the actual status, in theory, to assume 2|n means to add 2|n, temporally, to the theory system so we can use it as a TRUE formula, so means ∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:27
$begingroup$
In your proof, you say "if 4|n", so you suppose 4|n. I know that what you mean for "if 4|n" is not ∀n(4|n) but "for the n so that 4|n". But in P, that is, in your n∈Z, to suppose 4|n does mean ∀n(4|n). That is THE PROBLEM. So, my question is in reality could we prove the formula without supposing 4|n?
$endgroup$
– user49413
Jan 19 at 10:16
$begingroup$
In your proof, you say "if 4|n", so you suppose 4|n. I know that what you mean for "if 4|n" is not ∀n(4|n) but "for the n so that 4|n". But in P, that is, in your n∈Z, to suppose 4|n does mean ∀n(4|n). That is THE PROBLEM. So, my question is in reality could we prove the formula without supposing 4|n?
$endgroup$
– user49413
Jan 19 at 10:16
$begingroup$
@user49413 I see what you mean now. Of course, prove the contrapositive, so you assume not (2|n) and prove not (4|n)
$endgroup$
– Macrophage
Jan 19 at 10:44
$begingroup$
@user49413 I see what you mean now. Of course, prove the contrapositive, so you assume not (2|n) and prove not (4|n)
$endgroup$
– Macrophage
Jan 19 at 10:44
$begingroup$
We meet the same problem: we cannot assume 2|n because we have ¬(2|3) so ¬∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:15
$begingroup$
We meet the same problem: we cannot assume 2|n because we have ¬(2|3) so ¬∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:15
$begingroup$
@user49413 I think your logic is not quite right. We test for each n, what will happen if we assume 2|n, not 2|n for all n.
$endgroup$
– Macrophage
Jan 19 at 11:18
$begingroup$
@user49413 I think your logic is not quite right. We test for each n, what will happen if we assume 2|n, not 2|n for all n.
$endgroup$
– Macrophage
Jan 19 at 11:18
$begingroup$
I know that by supposing 2|n, what we would like to mean is "for the n so that 2|n", but not "∀n(2|n)". But at the actual status, in theory, to assume 2|n means to add 2|n, temporally, to the theory system so we can use it as a TRUE formula, so means ∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:27
$begingroup$
I know that by supposing 2|n, what we would like to mean is "for the n so that 2|n", but not "∀n(2|n)". But at the actual status, in theory, to assume 2|n means to add 2|n, temporally, to the theory system so we can use it as a TRUE formula, so means ∀n(2|n).
$endgroup$
– user49413
Jan 19 at 11:27
add a comment |
$begingroup$
Sketch of a proof (Natural Deduction-like).
The proof obviously needs Peano axioms; thus, what we will prove is :
$mathsf {PA} vdash forall n [exists k (n = 4 times k) to exists l (n = 2 times l)]$.
1) $exists k (n = 4 times k)$ --- assumed [a] (this is : $4 | n$)
2) $n = 4 times k_1$ --- assumed [b] from 1) for $exists$-elim
3) $mathsf {PA} vdash (4= 2 times 2)$ --- from axioms for $times$
4) $n = (2 times 2) times k_1$ --- from 2) and 3) by properties of equality
Now we need the commutative law for $times$, i.e. :
$mathsf {PA} vdash forall a,b,c [(a times b) times c = a times (b times c)]$
and we have, by transitivity of equality :
5) $n=2 times (2 times k_1)$
6) $exists l (n = 2 times l)$ --- from 5) by $exists$-intro (this is : $2 | n$)
7) $exists l (n = 2 times l)$ --- from 1) and 2)-6) by $exists$-elim, discharging [b]
8) $exists k (n = 4 times k) to exists l (n = 2 times l)$ --- from 1) and 7) by $to$-intro, discharging [a]
9) $mathsf {PA} vdash forall n [exists k (n = 4 times k) to exists l (n = 2 times l)]$ --- from 8) by $forall$-intro.
Note : you concern about Deduction Theorem is right for Hilbert-styple proof systems with "unrestricted" Generalization rule (see Mendelson's textbook).
The restriction on Universal generalization rule typical of Natural Deduction gives us the benefit of using $to$-introduction rule (aka : Deduction Theorem) without restrictions also in predicate calculus.
In any case, the above proof is sound also for Mendelson's system, because the only use of Generalization in performed after the Deduction Th step to a variable $n$ that is not free in any assumption.
answered Jan 17 at 16:37
Mauro ALLEGRANZAMauro ALLEGRANZA
66.5k449115
$endgroup$
$begingroup$
By 1), you suppose 4|n. But you introduce contradiction already by this step!
$endgroup$
– user49413
Jan 17 at 16:41
$begingroup$
@user49413 Your question seems to be asking how to use $4mid n$ to show that $2mid n$ for some $n$. Why would supposing $4mid n$ introduce contradiction?
$endgroup$
– Cardioid_Ass_22
Jan 17 at 16:54
$begingroup$
It's in the question itself. If we suppose 4|n, then we have ∀n(4|n) by generalization. But we have already ¬∀n(4|n) by ¬(4|5). So to suppose 4|n leads to contradiction.
$endgroup$
– user49413
Jan 17 at 16:58
$begingroup$
@user49413 - Universal generalization does not work that way. I've assumed $∃k (n=4×k)$ and derived $∃l (n=2×l)$, then use Deduction Theorem to get $∃k (n=4×k) to ∃l (n=2×l)$ and finally Gen to get : $forall n [∃k (n=4×k) to ∃l (n=2×l)]$.
$endgroup$
– Mauro ALLEGRANZA
Jan 17 at 19:56
$begingroup$
The step "1) ∃k (n=4×k) --- 4|n" means "if 4|n, then ∃k (n=4×k)". Otherwise, what is the reason for "∃k (n=4×k)"? So, you suppose 4|n.
$endgroup$
– user49413
Jan 19 at 10:24
|
show 5 more comments
$begingroup$
Sketch of a proof (Natural Deduction-like).
The proof obviously needs Peano axioms; thus, what we will prove is :
$mathsf {PA} vdash forall n [exists k (n = 4 times k) to exists l (n = 2 times l)]$.
1) $exists k (n = 4 times k)$ --- assumed [a] (this is : $4 | n$)
2) $n = 4 times k_1$ --- assumed [b] from 1) for $exists$-elim
3) $mathsf {PA} vdash (4= 2 times 2)$ --- from axioms for $times$
4) $n = (2 times 2) times k_1$ --- from 2) and 3) by properties of equality
Now we need the commutative law for $times$, i.e. :
$mathsf {PA} vdash forall a,b,c [(a times b) times c = a times (b times c)]$
and we have, by transitivity of equality :
5) $n=2 times (2 times k_1)$
6) $exists l (n = 2 times l)$ --- from 5) by $exists$-intro (this is : $2 | n$)
7) $exists l (n = 2 times l)$ --- from 1) and 2)-6) by $exists$-elim, discharging [b]
8) $exists k (n = 4 times k) to exists l (n = 2 times l)$ --- from 1) and 7) by $to$-intro, discharging [a]
9) $mathsf {PA} vdash forall n [exists k (n = 4 times k) to exists l (n = 2 times l)]$ --- from 8) by $forall$-intro.
Note : you concern about Deduction Theorem is right for Hilbert-styple proof systems with "unrestricted" Generalization rule (see Mendelson's textbook).
The restriction on Universal generalization rule typical of Natural Deduction gives us the benefit of using $to$-introduction rule (aka : Deduction Theorem) without restrictions also in predicate calculus.
In any case, the above proof is sound also for Mendelson's system, because the only use of Generalization in performed after the Deduction Th step to a variable $n$ that is not free in any assumption.
answered Jan 17 at 16:37
Mauro ALLEGRANZAMauro ALLEGRANZA
66.5k449115
$endgroup$
$begingroup$
By 1), you suppose 4|n. But you introduce contradiction already by this step!
$endgroup$
– user49413
Jan 17 at 16:41
$begingroup$
@user49413 Your question seems to be asking how to use $4mid n$ to show that $2mid n$ for some $n$. Why would supposing $4mid n$ introduce contradiction?
$endgroup$
– Cardioid_Ass_22
Jan 17 at 16:54
$begingroup$
It's in the question itself. If we suppose 4|n, then we have ∀n(4|n) by generalization. But we have already ¬∀n(4|n) by ¬(4|5). So to suppose 4|n leads to contradiction.
$endgroup$
– user49413
Jan 17 at 16:58
$begingroup$
@user49413 - Universal generalization does not work that way. I've assumed $∃k (n=4×k)$ and derived $∃l (n=2×l)$, then use Deduction Theorem to get $∃k (n=4×k) to ∃l (n=2×l)$ and finally Gen to get : $forall n [∃k (n=4×k) to ∃l (n=2×l)]$.
$endgroup$
– Mauro ALLEGRANZA
Jan 17 at 19:56
$begingroup$
The step "1) ∃k (n=4×k) --- 4|n" means "if 4|n, then ∃k (n=4×k)". Otherwise, what is the reason for "∃k (n=4×k)"? So, you suppose 4|n.
$endgroup$
– user49413
Jan 19 at 10:24
|
show 5 more comments
$begingroup$
Sketch of a proof (Natural Deduction-like).
The proof obviously needs Peano axioms; thus, what we will prove is :
$mathsf {PA} vdash forall n [exists k (n = 4 times k) to exists l (n = 2 times l)]$.
1) $exists k (n = 4 times k)$ --- assumed [a] (this is : $4 | n$)
2) $n = 4 times k_1$ --- assumed [b] from 1) for $exists$-elim
3) $mathsf {PA} vdash (4= 2 times 2)$ --- from axioms for $times$
4) $n = (2 times 2) times k_1$ --- from 2) and 3) by properties of equality
Now we need the commutative law for $times$, i.e. :
$mathsf {PA} vdash forall a,b,c [(a times b) times c = a times (b times c)]$
and we have, by transitivity of equality :
5) $n=2 times (2 times k_1)$
6) $exists l (n = 2 times l)$ --- from 5) by $exists$-intro (this is : $2 | n$)
7) $exists l (n = 2 times l)$ --- from 1) and 2)-6) by $exists$-elim, discharging [b]
8) $exists k (n = 4 times k) to exists l (n = 2 times l)$ --- from 1) and 7) by $to$-intro, discharging [a]
9) $mathsf {PA} vdash forall n [exists k (n = 4 times k) to exists l (n = 2 times l)]$ --- from 8) by $forall$-intro.
Note : you concern about Deduction Theorem is right for Hilbert-styple proof systems with "unrestricted" Generalization rule (see Mendelson's textbook).
The restriction on Universal generalization rule typical of Natural Deduction gives us the benefit of using $to$-introduction rule (aka : Deduction Theorem) without restrictions also in predicate calculus.
In any case, the above proof is sound also for Mendelson's system, because the only use of Generalization in performed after the Deduction Th step to a variable $n$ that is not free in any assumption.
answered Jan 17 at 16:37
Mauro ALLEGRANZAMauro ALLEGRANZA
66.5k449115
$endgroup$
Sketch of a proof (Natural Deduction-like).
The proof obviously needs Peano axioms; thus, what we will prove is :
$mathsf {PA} vdash forall n [exists k (n = 4 times k) to exists l (n = 2 times l)]$.
1) $exists k (n = 4 times k)$ --- assumed [a] (this is : $4 | n$)
2) $n = 4 times k_1$ --- assumed [b] from 1) for $exists$-elim
3) $mathsf {PA} vdash (4= 2 times 2)$ --- from axioms for $times$
4) $n = (2 times 2) times k_1$ --- from 2) and 3) by properties of equality
Now we need the commutative law for $times$, i.e. :
$mathsf {PA} vdash forall a,b,c [(a times b) times c = a times (b times c)]$
and we have, by transitivity of equality :
5) $n=2 times (2 times k_1)$
6) $exists l (n = 2 times l)$ --- from 5) by $exists$-intro (this is : $2 | n$)
7) $exists l (n = 2 times l)$ --- from 1) and 2)-6) by $exists$-elim, discharging [b]
8) $exists k (n = 4 times k) to exists l (n = 2 times l)$ --- from 1) and 7) by $to$-intro, discharging [a]
9) $mathsf {PA} vdash forall n [exists k (n = 4 times k) to exists l (n = 2 times l)]$ --- from 8) by $forall$-intro.
Note : you concern about Deduction Theorem is right for Hilbert-styple proof systems with "unrestricted" Generalization rule (see Mendelson's textbook).
The restriction on Universal generalization rule typical of Natural Deduction gives us the benefit of using $to$-introduction rule (aka : Deduction Theorem) without restrictions also in predicate calculus.
In any case, the above proof is sound also for Mendelson's system, because the only use of Generalization in performed after the Deduction Th step to a variable $n$ that is not free in any assumption.
answered Jan 17 at 16:37
Mauro ALLEGRANZAMauro ALLEGRANZA
66.5k449115
edited Jan 19 at 19:53
answered Jan 17 at 16:37
Mauro ALLEGRANZAMauro ALLEGRANZA
66.5k449115
answered Jan 17 at 16:37
Mauro ALLEGRANZAMauro ALLEGRANZA
66.5k449115
answered Jan 17 at 16:37
Mauro ALLEGRANZAMauro ALLEGRANZA
66.5k449115
66.5k449115
$begingroup$
By 1), you suppose 4|n. But you introduce contradiction already by this step!
$endgroup$
– user49413
Jan 17 at 16:41
$begingroup$
@user49413 Your question seems to be asking how to use $4mid n$ to show that $2mid n$ for some $n$. Why would supposing $4mid n$ introduce contradiction?
$endgroup$
– Cardioid_Ass_22
Jan 17 at 16:54
$begingroup$
It's in the question itself. If we suppose 4|n, then we have ∀n(4|n) by generalization. But we have already ¬∀n(4|n) by ¬(4|5). So to suppose 4|n leads to contradiction.
$endgroup$
– user49413
Jan 17 at 16:58
$begingroup$
@user49413 - Universal generalization does not work that way. I've assumed $∃k (n=4×k)$ and derived $∃l (n=2×l)$, then use Deduction Theorem to get $∃k (n=4×k) to ∃l (n=2×l)$ and finally Gen to get : $forall n [∃k (n=4×k) to ∃l (n=2×l)]$.
$endgroup$
– Mauro ALLEGRANZA
Jan 17 at 19:56
$begingroup$
The step "1) ∃k (n=4×k) --- 4|n" means "if 4|n, then ∃k (n=4×k)". Otherwise, what is the reason for "∃k (n=4×k)"? So, you suppose 4|n.
$endgroup$
– user49413
Jan 19 at 10:24
|
show 5 more comments
$begingroup$
By 1), you suppose 4|n. But you introduce contradiction already by this step!
$endgroup$
– user49413
Jan 17 at 16:41
$begingroup$
@user49413 Your question seems to be asking how to use $4mid n$ to show that $2mid n$ for some $n$. Why would supposing $4mid n$ introduce contradiction?
$endgroup$
– Cardioid_Ass_22
Jan 17 at 16:54
$begingroup$
It's in the question itself. If we suppose 4|n, then we have ∀n(4|n) by generalization. But we have already ¬∀n(4|n) by ¬(4|5). So to suppose 4|n leads to contradiction.
$endgroup$
– user49413
Jan 17 at 16:58
$begingroup$
@user49413 - Universal generalization does not work that way. I've assumed $∃k (n=4×k)$ and derived $∃l (n=2×l)$, then use Deduction Theorem to get $∃k (n=4×k) to ∃l (n=2×l)$ and finally Gen to get : $forall n [∃k (n=4×k) to ∃l (n=2×l)]$.
$endgroup$
– Mauro ALLEGRANZA
Jan 17 at 19:56
$begingroup$
The step "1) ∃k (n=4×k) --- 4|n" means "if 4|n, then ∃k (n=4×k)". Otherwise, what is the reason for "∃k (n=4×k)"? So, you suppose 4|n.
$endgroup$
– user49413
Jan 19 at 10:24
$begingroup$
By 1), you suppose 4|n. But you introduce contradiction already by this step!
$endgroup$
– user49413
Jan 17 at 16:41
$begingroup$
By 1), you suppose 4|n. But you introduce contradiction already by this step!
$endgroup$
– user49413
Jan 17 at 16:41
$begingroup$
@user49413 Your question seems to be asking how to use $4mid n$ to show that $2mid n$ for some $n$. Why would supposing $4mid n$ introduce contradiction?
$endgroup$
– Cardioid_Ass_22
Jan 17 at 16:54
$begingroup$
@user49413 Your question seems to be asking how to use $4mid n$ to show that $2mid n$ for some $n$. Why would supposing $4mid n$ introduce contradiction?
$endgroup$
– Cardioid_Ass_22
Jan 17 at 16:54
$begingroup$
It's in the question itself. If we suppose 4|n, then we have ∀n(4|n) by generalization. But we have already ¬∀n(4|n) by ¬(4|5). So to suppose 4|n leads to contradiction.
$endgroup$
– user49413
Jan 17 at 16:58
$begingroup$
It's in the question itself. If we suppose 4|n, then we have ∀n(4|n) by generalization. But we have already ¬∀n(4|n) by ¬(4|5). So to suppose 4|n leads to contradiction.
$endgroup$
– user49413
Jan 17 at 16:58
$begingroup$
@user49413 - Universal generalization does not work that way. I've assumed $∃k (n=4×k)$ and derived $∃l (n=2×l)$, then use Deduction Theorem to get $∃k (n=4×k) to ∃l (n=2×l)$ and finally Gen to get : $forall n [∃k (n=4×k) to ∃l (n=2×l)]$.
$endgroup$
– Mauro ALLEGRANZA
Jan 17 at 19:56
$begingroup$
@user49413 - Universal generalization does not work that way. I've assumed $∃k (n=4×k)$ and derived $∃l (n=2×l)$, then use Deduction Theorem to get $∃k (n=4×k) to ∃l (n=2×l)$ and finally Gen to get : $forall n [∃k (n=4×k) to ∃l (n=2×l)]$.
$endgroup$
– Mauro ALLEGRANZA
Jan 17 at 19:56
$begingroup$
The step "1) ∃k (n=4×k) --- 4|n" means "if 4|n, then ∃k (n=4×k)". Otherwise, what is the reason for "∃k (n=4×k)"? So, you suppose 4|n.
$endgroup$
– user49413
Jan 19 at 10:24
$begingroup$
The step "1) ∃k (n=4×k) --- 4|n" means "if 4|n, then ∃k (n=4×k)". Otherwise, what is the reason for "∃k (n=4×k)"? So, you suppose 4|n.
$endgroup$
– user49413
Jan 19 at 10:24
|
show 5 more comments
$begingroup$
I doubt that (4|n)→(2|n) can be proven in P. I think that it could be necessary to add a new rule of deduction for that. Let's call it the rule of conditional deduction and denote it by CDt here.
With CDt, we deduct in a restricted domain of discourse. The domain of discourse of P is natural number N. For any non empty class C⊂N, CDt works as a theory system P' that is the same as P except that its domain of discourse is C. Then, all TRUE formulas in P free of the quantifier ∃ are TRUE formula in P'. A TRUE formula in P containing ∃ cannot be translated to P'. Knowing that ¬∀x(f(x)) should be considered as ∃x(¬f(x)), and ¬∃x(f(x)) should be considered as ∀x(¬f(x)). So, we have less TRUE formulas in P' than in P at beginning of CDt. A TRUE formula in P' containing neither free variable nor quantifier ∀ is also a TRUE formula in P. A TRUE formula containing free variable x denoted by f(x) can be translated to a TRUE formula in P by (x∈C)→f(x), similarly, ∀x(f(x)) to ∀x((x∈C)→f(x)).
With CDt for proving (4|n)→(2|n), we use the C relative to the formula 4|n according to the axiom IV.1 which is similar to the axiom of comprehension. So, we have ∀n((n∈C)↔(4|n)) in P so also in P'.
We can add 4|n to P', or in other words assume 4|n in P', under CDt because the ¬(4|5) in P cannot lead to contradiction in P' for the reason that 5 is not in C. Then we can obtain 2|n by deduction in P', and translate 2|n in P' to (4|n)→(2|n) in P.
This process is the same as what we do usually by intuition. So, CDt just formalize what we do usually by introducing restricted domain of discourse. We get (4|n)→(2|n) by extension of domain of discourse, but not by reason that it's part of some TRUE formula or it's defined recursively.
In general, the restricted domain of discourse can be extended to variable domain of discourse that can further be used to extend P to a bigger domain of discourse. For example, (4|n)→(2|n) would become isN(n)→((4|n)→(2|n)) where isN(x) is TRUE if and only if x is a natural number. This would permit a unified formal theory system by mixing all theory systems in a unified domain of discourse: the universe.
answered Jan 22 at 11:57
user49413user49413
294
$endgroup$
add a comment |
$begingroup$
I doubt that (4|n)→(2|n) can be proven in P. I think that it could be necessary to add a new rule of deduction for that. Let's call it the rule of conditional deduction and denote it by CDt here.
With CDt, we deduct in a restricted domain of discourse. The domain of discourse of P is natural number N. For any non empty class C⊂N, CDt works as a theory system P' that is the same as P except that its domain of discourse is C. Then, all TRUE formulas in P free of the quantifier ∃ are TRUE formula in P'. A TRUE formula in P containing ∃ cannot be translated to P'. Knowing that ¬∀x(f(x)) should be considered as ∃x(¬f(x)), and ¬∃x(f(x)) should be considered as ∀x(¬f(x)). So, we have less TRUE formulas in P' than in P at beginning of CDt. A TRUE formula in P' containing neither free variable nor quantifier ∀ is also a TRUE formula in P. A TRUE formula containing free variable x denoted by f(x) can be translated to a TRUE formula in P by (x∈C)→f(x), similarly, ∀x(f(x)) to ∀x((x∈C)→f(x)).
With CDt for proving (4|n)→(2|n), we use the C relative to the formula 4|n according to the axiom IV.1 which is similar to the axiom of comprehension. So, we have ∀n((n∈C)↔(4|n)) in P so also in P'.
We can add 4|n to P', or in other words assume 4|n in P', under CDt because the ¬(4|5) in P cannot lead to contradiction in P' for the reason that 5 is not in C. Then we can obtain 2|n by deduction in P', and translate 2|n in P' to (4|n)→(2|n) in P.
This process is the same as what we do usually by intuition. So, CDt just formalize what we do usually by introducing restricted domain of discourse. We get (4|n)→(2|n) by extension of domain of discourse, but not by reason that it's part of some TRUE formula or it's defined recursively.
In general, the restricted domain of discourse can be extended to variable domain of discourse that can further be used to extend P to a bigger domain of discourse. For example, (4|n)→(2|n) would become isN(n)→((4|n)→(2|n)) where isN(x) is TRUE if and only if x is a natural number. This would permit a unified formal theory system by mixing all theory systems in a unified domain of discourse: the universe.
answered Jan 22 at 11:57
user49413user49413
294
$endgroup$
add a comment |
$begingroup$
I doubt that (4|n)→(2|n) can be proven in P. I think that it could be necessary to add a new rule of deduction for that. Let's call it the rule of conditional deduction and denote it by CDt here.
With CDt, we deduct in a restricted domain of discourse. The domain of discourse of P is natural number N. For any non empty class C⊂N, CDt works as a theory system P' that is the same as P except that its domain of discourse is C. Then, all TRUE formulas in P free of the quantifier ∃ are TRUE formula in P'. A TRUE formula in P containing ∃ cannot be translated to P'. Knowing that ¬∀x(f(x)) should be considered as ∃x(¬f(x)), and ¬∃x(f(x)) should be considered as ∀x(¬f(x)). So, we have less TRUE formulas in P' than in P at beginning of CDt. A TRUE formula in P' containing neither free variable nor quantifier ∀ is also a TRUE formula in P. A TRUE formula containing free variable x denoted by f(x) can be translated to a TRUE formula in P by (x∈C)→f(x), similarly, ∀x(f(x)) to ∀x((x∈C)→f(x)).
With CDt for proving (4|n)→(2|n), we use the C relative to the formula 4|n according to the axiom IV.1 which is similar to the axiom of comprehension. So, we have ∀n((n∈C)↔(4|n)) in P so also in P'.
We can add 4|n to P', or in other words assume 4|n in P', under CDt because the ¬(4|5) in P cannot lead to contradiction in P' for the reason that 5 is not in C. Then we can obtain 2|n by deduction in P', and translate 2|n in P' to (4|n)→(2|n) in P.
This process is the same as what we do usually by intuition. So, CDt just formalize what we do usually by introducing restricted domain of discourse. We get (4|n)→(2|n) by extension of domain of discourse, but not by reason that it's part of some TRUE formula or it's defined recursively.
In general, the restricted domain of discourse can be extended to variable domain of discourse that can further be used to extend P to a bigger domain of discourse. For example, (4|n)→(2|n) would become isN(n)→((4|n)→(2|n)) where isN(x) is TRUE if and only if x is a natural number. This would permit a unified formal theory system by mixing all theory systems in a unified domain of discourse: the universe.
answered Jan 22 at 11:57
user49413user49413
294
$endgroup$
I doubt that (4|n)→(2|n) can be proven in P. I think that it could be necessary to add a new rule of deduction for that. Let's call it the rule of conditional deduction and denote it by CDt here.
With CDt, we deduct in a restricted domain of discourse. The domain of discourse of P is natural number N. For any non empty class C⊂N, CDt works as a theory system P' that is the same as P except that its domain of discourse is C. Then, all TRUE formulas in P free of the quantifier ∃ are TRUE formula in P'. A TRUE formula in P containing ∃ cannot be translated to P'. Knowing that ¬∀x(f(x)) should be considered as ∃x(¬f(x)), and ¬∃x(f(x)) should be considered as ∀x(¬f(x)). So, we have less TRUE formulas in P' than in P at beginning of CDt. A TRUE formula in P' containing neither free variable nor quantifier ∀ is also a TRUE formula in P. A TRUE formula containing free variable x denoted by f(x) can be translated to a TRUE formula in P by (x∈C)→f(x), similarly, ∀x(f(x)) to ∀x((x∈C)→f(x)).
With CDt for proving (4|n)→(2|n), we use the C relative to the formula 4|n according to the axiom IV.1 which is similar to the axiom of comprehension. So, we have ∀n((n∈C)↔(4|n)) in P so also in P'.
We can add 4|n to P', or in other words assume 4|n in P', under CDt because the ¬(4|5) in P cannot lead to contradiction in P' for the reason that 5 is not in C. Then we can obtain 2|n by deduction in P', and translate 2|n in P' to (4|n)→(2|n) in P.
This process is the same as what we do usually by intuition. So, CDt just formalize what we do usually by introducing restricted domain of discourse. We get (4|n)→(2|n) by extension of domain of discourse, but not by reason that it's part of some TRUE formula or it's defined recursively.
In general, the restricted domain of discourse can be extended to variable domain of discourse that can further be used to extend P to a bigger domain of discourse. For example, (4|n)→(2|n) would become isN(n)→((4|n)→(2|n)) where isN(x) is TRUE if and only if x is a natural number. This would permit a unified formal theory system by mixing all theory systems in a unified domain of discourse: the universe.
answered Jan 22 at 11:57
user49413user49413
294
edited Jan 23 at 17:44
answered Jan 22 at 11:57
user49413user49413
294
answered Jan 22 at 11:57
user49413user49413
294
answered Jan 22 at 11:57
user49413user49413
294
294
add a comment |
add a comment |
Thanks for contributing an answer to Mathematics Stack Exchange!
- Please be sure to answer the question. Provide details and share your research!
But avoid …
- Asking for help, clarification, or responding to other answers.
- Making statements based on opinion; back them up with references or personal experience.
Use MathJax to format equations. MathJax reference.
To learn more, see our tips on writing great answers.
Sign up or log in
StackExchange.ready(function () {
StackExchange.helpers.onClickDraftSave('#login-link');
});
Sign up using Google
Sign up using Facebook
Sign up using Email and Password
Post as a guest
Required, but never shown
StackExchange.ready(
function () {
StackExchange.openid.initPostLogin('.new-post-login', 'https%3a%2f%2fmath.stackexchange.com%2fquestions%2f3077187%2fhow-to-prove-4n%25e2%2586%25922n-in-p%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$
Please try to use mathjax. Thank you.
$endgroup$
– Jakobian
Jan 17 at 16:28
$begingroup$
@user49413 I think you have misunderstood. $(4|n) rightarrow (2|n)$. It is not equivalent to $(4|n) forall n$. However, it is equivalent $lnot (4|n) lor (2|n) forall n$.
$endgroup$
– gandalf61
Jan 17 at 16:58
$begingroup$
(4|n)→(2|n) means ∀n((4|n)→(2|n)) by generalization or ∀n(¬(4|n)∨(2|n)) if you prefer. It doesn't mean (∀n(4|n))→(∀n(2|n)).
$endgroup$
– user49413
Jan 17 at 17:14
$begingroup$
If we suppose 4|n, then we would have ∀n(4|n) and would prove (∀n(4|n))→(∀n(2|n)) which is evidently wrong. This is from another point of view why we cannot suppose 4|n.
$endgroup$
– user49413
Jan 17 at 17:23