Mixing
Why is a proposition implying its converse equivalent to its converse?
$begingroup$
In other words,
Why is ((p implies q) implies (q implies p)) equivalent to just (q implies p)?
How to prove it without the help of a truth value table?
logic propositional-calculus
asked Feb 2 at 16:38
Jean-Guy PistacheJean-Guy Pistache
161
$endgroup$
add a comment |
$begingroup$
In other words,
Why is ((p implies q) implies (q implies p)) equivalent to just (q implies p)?
How to prove it without the help of a truth value table?
logic propositional-calculus
asked Feb 2 at 16:38
Jean-Guy PistacheJean-Guy Pistache
161
$endgroup$
$begingroup$
Because we can prove it.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:05
$begingroup$
Two parts proof : (i) $(q to p) vdash [(p to q) to (q to p)]$. Obvious using the tautology : $A to (B to A)$.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
$begingroup$
(ii) $[(p→q) → (q→p)] vdash (q to p)$. Less obvious...
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
add a comment |
$begingroup$
In other words,
Why is ((p implies q) implies (q implies p)) equivalent to just (q implies p)?
How to prove it without the help of a truth value table?
logic propositional-calculus
asked Feb 2 at 16:38
Jean-Guy PistacheJean-Guy Pistache
161
$endgroup$
In other words,
Why is ((p implies q) implies (q implies p)) equivalent to just (q implies p)?
How to prove it without the help of a truth value table?
logic propositional-calculus
logic propositional-calculus
asked Feb 2 at 16:38
Jean-Guy PistacheJean-Guy Pistache
161
asked Feb 2 at 16:38
Jean-Guy PistacheJean-Guy Pistache
161
asked Feb 2 at 16:38
Jean-Guy PistacheJean-Guy Pistache
161
asked Feb 2 at 16:38
Jean-Guy PistacheJean-Guy Pistache
161
asked Feb 2 at 16:38
Jean-Guy PistacheJean-Guy Pistache
161
161
$begingroup$
Because we can prove it.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:05
$begingroup$
Two parts proof : (i) $(q to p) vdash [(p to q) to (q to p)]$. Obvious using the tautology : $A to (B to A)$.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
$begingroup$
(ii) $[(p→q) → (q→p)] vdash (q to p)$. Less obvious...
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
add a comment |
$begingroup$
Because we can prove it.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:05
$begingroup$
Two parts proof : (i) $(q to p) vdash [(p to q) to (q to p)]$. Obvious using the tautology : $A to (B to A)$.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
$begingroup$
(ii) $[(p→q) → (q→p)] vdash (q to p)$. Less obvious...
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
$begingroup$
Because we can prove it.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:05
$begingroup$
Because we can prove it.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:05
$begingroup$
Two parts proof : (i) $(q to p) vdash [(p to q) to (q to p)]$. Obvious using the tautology : $A to (B to A)$.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
$begingroup$
Two parts proof : (i) $(q to p) vdash [(p to q) to (q to p)]$. Obvious using the tautology : $A to (B to A)$.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
$begingroup$
(ii) $[(p→q) → (q→p)] vdash (q to p)$. Less obvious...
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
$begingroup$
(ii) $[(p→q) → (q→p)] vdash (q to p)$. Less obvious...
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
add a comment |
4 Answers
4
active
oldest
votes
$begingroup$
You can reason informally like this. $$((pto q)to(qto p))iff(qto p)$$ if (and only if) $(pto q)to(qto p)$ and $qto p$ always have the same truth value. Remember that $ato b$ is true except in the case where $a$ is true and $b$ is false.
First, suppose that $qto p$ is true. Then $(pto q)to(qto p)$ is true also, since the conclusion is true.
Second, suppose $qto p$ is false. Then $p$ is false, so $pto q$ is true. Therefore $(pto q)to(qto p)$ is false.
In all cases, the two statements have the same truth value. I'm not sure this proof is any more intuitive than a truth table. The statement itself is not very intuitive.
answered Feb 2 at 17:08
saulspatzsaulspatz
17.3k31435
$endgroup$
add a comment |
$begingroup$
I think the key point here is the following:
For any propositions $p,q$, at least one of $prightarrow q$ and $qrightarrow p$ is true.
(They could both be true - in fact, they'll both be true exactly when $p$ and $q$ have the same truth value.)
This fact is really weird from the point of view of natural language; it's a feature of the way we define implication ("material implication") in formal logic. Namely, the only way "$arightarrow b$" can be false is if $a$ is true and $b$ is false, so in order for $prightarrow q$ and $qrightarrow p$ to each be false we'd have to have $p$ be true and $q$ be false and $q$ be true and $p$ be false - and this is clearly impossible.
So write $A$ for $prightarrow q$ and $B$ for $qrightarrow p$. The hypothesis you're considering is $Arightarrow B$, and the fact above says that we know $Avee B$ right from the get-go. But it should be clear that from $Arightarrow B$ and $Avee B$ we can conclude $B$.
OK, strictly speaking all this is saying is that $(prightarrow q)rightarrow (qrightarrow p)$ implies $qrightarrow p$. But the other direction should be easy to understand once this one's grasped: if the consequent of an implication is true, then the whole implication is automatically true (remember: an implication is false if and only if its antecedent is true and its consequent is false), so if $qrightarrow p$ is true then so is $Xrightarrow (qrightarrow p)$ for any $X$ - now just take $X$ to be $prightarrow q$.
answered Feb 2 at 18:39
Noah SchweberNoah Schweber
129k10152294
$endgroup$
add a comment |
$begingroup$
It is indeed not intuitive, because the mathematically defined material implication ($to$) does not always line up with our intuitions when reading it is as an English 'if ... then ...' (see Paradoxes of Material Implication)
But, the way the material implication is defined, the following equivalence holds:
Implication
$$p lor q iff neg p lor q$$
With Implication, and some other equivalence principles you can now prove the equivalence you are asking about:
$$(pto q)to(qto p) overset{Implication}{iff}$$
$$neg (p to q) lor (qto p)overset{Implication}{iff} $$
$$neg (neg p lor q) lor (neg q lor p)overset{DeMorgan}{iff} $$
$$(p land neg q) lor neg q lor poverset{Absorption}{iff} $$
$$neg q lor poverset{Implication}{iff} $$
$$qto p$$
answered Feb 2 at 18:16
Bram28Bram28
64.5k44793
$endgroup$
add a comment |
$begingroup$
As a different perspective, we can use a propositions-as-types approach or the BHK interpretation. This approach works most naturally for constructive logic, but I find it enlightening when it is applicable. Luckily, this result is constructively true. In these interpretations, an implication $Pto Q$ is represented as a function from some type of evidence for $P$ to a type of evidence for $Q$. In other words, evidence for $Pto Q$ is a function from evidence for $P$ to evidence for $Q$. What constitutes evidence for an atomic proposition is left abstract. For example, to provide evidence for $Pto P$, we don't actually need to know what evidence for $P$ looks like; we can just provide a function that returns whatever evidence it is given, i.e. the identity function.
Below is a mechanized proof (in Agda) for the harder direction of the equivalence. This uses notation from the (typed) lambda calculus.
thm : {P Q : Set} → ((P → Q) → (Q → P)) → (Q → P)
thm f q = f (λ _ → q) q
What's going on is f represents the evidence for $(Pto Q)to(Qto P)$ which is to say a function that takes a function $Pto Q$ and evidence for $Q$ and produces evidence for $P$. We've also been given some evidence for $Q$, namely q. We then need to produce some evidence for $P$. f produces such evidence as long as we can give it evidence for $Pto Q$ and $Q$. We already have evidence for $Q$, so we just need to construct evidence for $Pto Q$. But if we know $Q$ (i.e. have evidence for it) then $Pto Q$ holds no matter what $P$ is. This is represented by the evidence for $Pto Q$ being the constantly q function which just ignores the evidence for $P$.
One nice thing about this approach is that it is fairly obvious what to do at each step. (In fact, it is so obvious that Agda produces exactly the above proof term itself, completely automatically.) If you have experience with programming (and particularly typed functional programming), many intuitions with respect to data flow and such make it very easy to see how to prove certain statements, or if they are not (constructively) provable.
answered Feb 3 at 1:42
Derek ElkinsDerek Elkins
17.7k11437
$endgroup$
add a comment |
Your Answer
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%2f3097480%2fwhy-is-a-proposition-implying-its-converse-equivalent-to-its-converse%23new-answer', 'question_page');
}
);
Post as a guest
Required, but never shown
4 Answers
4
active
oldest
votes
4 Answers
4
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
You can reason informally like this. $$((pto q)to(qto p))iff(qto p)$$ if (and only if) $(pto q)to(qto p)$ and $qto p$ always have the same truth value. Remember that $ato b$ is true except in the case where $a$ is true and $b$ is false.
First, suppose that $qto p$ is true. Then $(pto q)to(qto p)$ is true also, since the conclusion is true.
Second, suppose $qto p$ is false. Then $p$ is false, so $pto q$ is true. Therefore $(pto q)to(qto p)$ is false.
In all cases, the two statements have the same truth value. I'm not sure this proof is any more intuitive than a truth table. The statement itself is not very intuitive.
answered Feb 2 at 17:08
saulspatzsaulspatz
17.3k31435
$endgroup$
add a comment |
$begingroup$
You can reason informally like this. $$((pto q)to(qto p))iff(qto p)$$ if (and only if) $(pto q)to(qto p)$ and $qto p$ always have the same truth value. Remember that $ato b$ is true except in the case where $a$ is true and $b$ is false.
First, suppose that $qto p$ is true. Then $(pto q)to(qto p)$ is true also, since the conclusion is true.
Second, suppose $qto p$ is false. Then $p$ is false, so $pto q$ is true. Therefore $(pto q)to(qto p)$ is false.
In all cases, the two statements have the same truth value. I'm not sure this proof is any more intuitive than a truth table. The statement itself is not very intuitive.
answered Feb 2 at 17:08
saulspatzsaulspatz
17.3k31435
$endgroup$
add a comment |
$begingroup$
You can reason informally like this. $$((pto q)to(qto p))iff(qto p)$$ if (and only if) $(pto q)to(qto p)$ and $qto p$ always have the same truth value. Remember that $ato b$ is true except in the case where $a$ is true and $b$ is false.
First, suppose that $qto p$ is true. Then $(pto q)to(qto p)$ is true also, since the conclusion is true.
Second, suppose $qto p$ is false. Then $p$ is false, so $pto q$ is true. Therefore $(pto q)to(qto p)$ is false.
In all cases, the two statements have the same truth value. I'm not sure this proof is any more intuitive than a truth table. The statement itself is not very intuitive.
answered Feb 2 at 17:08
saulspatzsaulspatz
17.3k31435
$endgroup$
You can reason informally like this. $$((pto q)to(qto p))iff(qto p)$$ if (and only if) $(pto q)to(qto p)$ and $qto p$ always have the same truth value. Remember that $ato b$ is true except in the case where $a$ is true and $b$ is false.
First, suppose that $qto p$ is true. Then $(pto q)to(qto p)$ is true also, since the conclusion is true.
Second, suppose $qto p$ is false. Then $p$ is false, so $pto q$ is true. Therefore $(pto q)to(qto p)$ is false.
In all cases, the two statements have the same truth value. I'm not sure this proof is any more intuitive than a truth table. The statement itself is not very intuitive.
answered Feb 2 at 17:08
saulspatzsaulspatz
17.3k31435
answered Feb 2 at 17:08
saulspatzsaulspatz
17.3k31435
answered Feb 2 at 17:08
saulspatzsaulspatz
17.3k31435
answered Feb 2 at 17:08
saulspatzsaulspatz
17.3k31435
17.3k31435
add a comment |
add a comment |
$begingroup$
I think the key point here is the following:
For any propositions $p,q$, at least one of $prightarrow q$ and $qrightarrow p$ is true.
(They could both be true - in fact, they'll both be true exactly when $p$ and $q$ have the same truth value.)
This fact is really weird from the point of view of natural language; it's a feature of the way we define implication ("material implication") in formal logic. Namely, the only way "$arightarrow b$" can be false is if $a$ is true and $b$ is false, so in order for $prightarrow q$ and $qrightarrow p$ to each be false we'd have to have $p$ be true and $q$ be false and $q$ be true and $p$ be false - and this is clearly impossible.
So write $A$ for $prightarrow q$ and $B$ for $qrightarrow p$. The hypothesis you're considering is $Arightarrow B$, and the fact above says that we know $Avee B$ right from the get-go. But it should be clear that from $Arightarrow B$ and $Avee B$ we can conclude $B$.
OK, strictly speaking all this is saying is that $(prightarrow q)rightarrow (qrightarrow p)$ implies $qrightarrow p$. But the other direction should be easy to understand once this one's grasped: if the consequent of an implication is true, then the whole implication is automatically true (remember: an implication is false if and only if its antecedent is true and its consequent is false), so if $qrightarrow p$ is true then so is $Xrightarrow (qrightarrow p)$ for any $X$ - now just take $X$ to be $prightarrow q$.
answered Feb 2 at 18:39
Noah SchweberNoah Schweber
129k10152294
$endgroup$
add a comment |
$begingroup$
I think the key point here is the following:
For any propositions $p,q$, at least one of $prightarrow q$ and $qrightarrow p$ is true.
(They could both be true - in fact, they'll both be true exactly when $p$ and $q$ have the same truth value.)
This fact is really weird from the point of view of natural language; it's a feature of the way we define implication ("material implication") in formal logic. Namely, the only way "$arightarrow b$" can be false is if $a$ is true and $b$ is false, so in order for $prightarrow q$ and $qrightarrow p$ to each be false we'd have to have $p$ be true and $q$ be false and $q$ be true and $p$ be false - and this is clearly impossible.
So write $A$ for $prightarrow q$ and $B$ for $qrightarrow p$. The hypothesis you're considering is $Arightarrow B$, and the fact above says that we know $Avee B$ right from the get-go. But it should be clear that from $Arightarrow B$ and $Avee B$ we can conclude $B$.
OK, strictly speaking all this is saying is that $(prightarrow q)rightarrow (qrightarrow p)$ implies $qrightarrow p$. But the other direction should be easy to understand once this one's grasped: if the consequent of an implication is true, then the whole implication is automatically true (remember: an implication is false if and only if its antecedent is true and its consequent is false), so if $qrightarrow p$ is true then so is $Xrightarrow (qrightarrow p)$ for any $X$ - now just take $X$ to be $prightarrow q$.
answered Feb 2 at 18:39
Noah SchweberNoah Schweber
129k10152294
$endgroup$
add a comment |
$begingroup$
I think the key point here is the following:
For any propositions $p,q$, at least one of $prightarrow q$ and $qrightarrow p$ is true.
(They could both be true - in fact, they'll both be true exactly when $p$ and $q$ have the same truth value.)
This fact is really weird from the point of view of natural language; it's a feature of the way we define implication ("material implication") in formal logic. Namely, the only way "$arightarrow b$" can be false is if $a$ is true and $b$ is false, so in order for $prightarrow q$ and $qrightarrow p$ to each be false we'd have to have $p$ be true and $q$ be false and $q$ be true and $p$ be false - and this is clearly impossible.
So write $A$ for $prightarrow q$ and $B$ for $qrightarrow p$. The hypothesis you're considering is $Arightarrow B$, and the fact above says that we know $Avee B$ right from the get-go. But it should be clear that from $Arightarrow B$ and $Avee B$ we can conclude $B$.
OK, strictly speaking all this is saying is that $(prightarrow q)rightarrow (qrightarrow p)$ implies $qrightarrow p$. But the other direction should be easy to understand once this one's grasped: if the consequent of an implication is true, then the whole implication is automatically true (remember: an implication is false if and only if its antecedent is true and its consequent is false), so if $qrightarrow p$ is true then so is $Xrightarrow (qrightarrow p)$ for any $X$ - now just take $X$ to be $prightarrow q$.
answered Feb 2 at 18:39
Noah SchweberNoah Schweber
129k10152294
$endgroup$
I think the key point here is the following:
For any propositions $p,q$, at least one of $prightarrow q$ and $qrightarrow p$ is true.
(They could both be true - in fact, they'll both be true exactly when $p$ and $q$ have the same truth value.)
This fact is really weird from the point of view of natural language; it's a feature of the way we define implication ("material implication") in formal logic. Namely, the only way "$arightarrow b$" can be false is if $a$ is true and $b$ is false, so in order for $prightarrow q$ and $qrightarrow p$ to each be false we'd have to have $p$ be true and $q$ be false and $q$ be true and $p$ be false - and this is clearly impossible.
So write $A$ for $prightarrow q$ and $B$ for $qrightarrow p$. The hypothesis you're considering is $Arightarrow B$, and the fact above says that we know $Avee B$ right from the get-go. But it should be clear that from $Arightarrow B$ and $Avee B$ we can conclude $B$.
OK, strictly speaking all this is saying is that $(prightarrow q)rightarrow (qrightarrow p)$ implies $qrightarrow p$. But the other direction should be easy to understand once this one's grasped: if the consequent of an implication is true, then the whole implication is automatically true (remember: an implication is false if and only if its antecedent is true and its consequent is false), so if $qrightarrow p$ is true then so is $Xrightarrow (qrightarrow p)$ for any $X$ - now just take $X$ to be $prightarrow q$.
answered Feb 2 at 18:39
Noah SchweberNoah Schweber
129k10152294
answered Feb 2 at 18:39
Noah SchweberNoah Schweber
129k10152294
answered Feb 2 at 18:39
Noah SchweberNoah Schweber
129k10152294
answered Feb 2 at 18:39
Noah SchweberNoah Schweber
129k10152294
129k10152294
add a comment |
add a comment |
$begingroup$
It is indeed not intuitive, because the mathematically defined material implication ($to$) does not always line up with our intuitions when reading it is as an English 'if ... then ...' (see Paradoxes of Material Implication)
But, the way the material implication is defined, the following equivalence holds:
Implication
$$p lor q iff neg p lor q$$
With Implication, and some other equivalence principles you can now prove the equivalence you are asking about:
$$(pto q)to(qto p) overset{Implication}{iff}$$
$$neg (p to q) lor (qto p)overset{Implication}{iff} $$
$$neg (neg p lor q) lor (neg q lor p)overset{DeMorgan}{iff} $$
$$(p land neg q) lor neg q lor poverset{Absorption}{iff} $$
$$neg q lor poverset{Implication}{iff} $$
$$qto p$$
answered Feb 2 at 18:16
Bram28Bram28
64.5k44793
$endgroup$
add a comment |
$begingroup$
It is indeed not intuitive, because the mathematically defined material implication ($to$) does not always line up with our intuitions when reading it is as an English 'if ... then ...' (see Paradoxes of Material Implication)
But, the way the material implication is defined, the following equivalence holds:
Implication
$$p lor q iff neg p lor q$$
With Implication, and some other equivalence principles you can now prove the equivalence you are asking about:
$$(pto q)to(qto p) overset{Implication}{iff}$$
$$neg (p to q) lor (qto p)overset{Implication}{iff} $$
$$neg (neg p lor q) lor (neg q lor p)overset{DeMorgan}{iff} $$
$$(p land neg q) lor neg q lor poverset{Absorption}{iff} $$
$$neg q lor poverset{Implication}{iff} $$
$$qto p$$
answered Feb 2 at 18:16
Bram28Bram28
64.5k44793
$endgroup$
add a comment |
$begingroup$
It is indeed not intuitive, because the mathematically defined material implication ($to$) does not always line up with our intuitions when reading it is as an English 'if ... then ...' (see Paradoxes of Material Implication)
But, the way the material implication is defined, the following equivalence holds:
Implication
$$p lor q iff neg p lor q$$
With Implication, and some other equivalence principles you can now prove the equivalence you are asking about:
$$(pto q)to(qto p) overset{Implication}{iff}$$
$$neg (p to q) lor (qto p)overset{Implication}{iff} $$
$$neg (neg p lor q) lor (neg q lor p)overset{DeMorgan}{iff} $$
$$(p land neg q) lor neg q lor poverset{Absorption}{iff} $$
$$neg q lor poverset{Implication}{iff} $$
$$qto p$$
answered Feb 2 at 18:16
Bram28Bram28
64.5k44793
$endgroup$
It is indeed not intuitive, because the mathematically defined material implication ($to$) does not always line up with our intuitions when reading it is as an English 'if ... then ...' (see Paradoxes of Material Implication)
But, the way the material implication is defined, the following equivalence holds:
Implication
$$p lor q iff neg p lor q$$
With Implication, and some other equivalence principles you can now prove the equivalence you are asking about:
$$(pto q)to(qto p) overset{Implication}{iff}$$
$$neg (p to q) lor (qto p)overset{Implication}{iff} $$
$$neg (neg p lor q) lor (neg q lor p)overset{DeMorgan}{iff} $$
$$(p land neg q) lor neg q lor poverset{Absorption}{iff} $$
$$neg q lor poverset{Implication}{iff} $$
$$qto p$$
answered Feb 2 at 18:16
Bram28Bram28
64.5k44793
answered Feb 2 at 18:16
Bram28Bram28
64.5k44793
answered Feb 2 at 18:16
Bram28Bram28
64.5k44793
answered Feb 2 at 18:16
Bram28Bram28
64.5k44793
64.5k44793
add a comment |
add a comment |
$begingroup$
As a different perspective, we can use a propositions-as-types approach or the BHK interpretation. This approach works most naturally for constructive logic, but I find it enlightening when it is applicable. Luckily, this result is constructively true. In these interpretations, an implication $Pto Q$ is represented as a function from some type of evidence for $P$ to a type of evidence for $Q$. In other words, evidence for $Pto Q$ is a function from evidence for $P$ to evidence for $Q$. What constitutes evidence for an atomic proposition is left abstract. For example, to provide evidence for $Pto P$, we don't actually need to know what evidence for $P$ looks like; we can just provide a function that returns whatever evidence it is given, i.e. the identity function.
Below is a mechanized proof (in Agda) for the harder direction of the equivalence. This uses notation from the (typed) lambda calculus.
thm : {P Q : Set} → ((P → Q) → (Q → P)) → (Q → P)
thm f q = f (λ _ → q) q
What's going on is f represents the evidence for $(Pto Q)to(Qto P)$ which is to say a function that takes a function $Pto Q$ and evidence for $Q$ and produces evidence for $P$. We've also been given some evidence for $Q$, namely q. We then need to produce some evidence for $P$. f produces such evidence as long as we can give it evidence for $Pto Q$ and $Q$. We already have evidence for $Q$, so we just need to construct evidence for $Pto Q$. But if we know $Q$ (i.e. have evidence for it) then $Pto Q$ holds no matter what $P$ is. This is represented by the evidence for $Pto Q$ being the constantly q function which just ignores the evidence for $P$.
One nice thing about this approach is that it is fairly obvious what to do at each step. (In fact, it is so obvious that Agda produces exactly the above proof term itself, completely automatically.) If you have experience with programming (and particularly typed functional programming), many intuitions with respect to data flow and such make it very easy to see how to prove certain statements, or if they are not (constructively) provable.
answered Feb 3 at 1:42
Derek ElkinsDerek Elkins
17.7k11437
$endgroup$
add a comment |
$begingroup$
As a different perspective, we can use a propositions-as-types approach or the BHK interpretation. This approach works most naturally for constructive logic, but I find it enlightening when it is applicable. Luckily, this result is constructively true. In these interpretations, an implication $Pto Q$ is represented as a function from some type of evidence for $P$ to a type of evidence for $Q$. In other words, evidence for $Pto Q$ is a function from evidence for $P$ to evidence for $Q$. What constitutes evidence for an atomic proposition is left abstract. For example, to provide evidence for $Pto P$, we don't actually need to know what evidence for $P$ looks like; we can just provide a function that returns whatever evidence it is given, i.e. the identity function.
Below is a mechanized proof (in Agda) for the harder direction of the equivalence. This uses notation from the (typed) lambda calculus.
thm : {P Q : Set} → ((P → Q) → (Q → P)) → (Q → P)
thm f q = f (λ _ → q) q
What's going on is f represents the evidence for $(Pto Q)to(Qto P)$ which is to say a function that takes a function $Pto Q$ and evidence for $Q$ and produces evidence for $P$. We've also been given some evidence for $Q$, namely q. We then need to produce some evidence for $P$. f produces such evidence as long as we can give it evidence for $Pto Q$ and $Q$. We already have evidence for $Q$, so we just need to construct evidence for $Pto Q$. But if we know $Q$ (i.e. have evidence for it) then $Pto Q$ holds no matter what $P$ is. This is represented by the evidence for $Pto Q$ being the constantly q function which just ignores the evidence for $P$.
One nice thing about this approach is that it is fairly obvious what to do at each step. (In fact, it is so obvious that Agda produces exactly the above proof term itself, completely automatically.) If you have experience with programming (and particularly typed functional programming), many intuitions with respect to data flow and such make it very easy to see how to prove certain statements, or if they are not (constructively) provable.
answered Feb 3 at 1:42
Derek ElkinsDerek Elkins
17.7k11437
$endgroup$
add a comment |
$begingroup$
As a different perspective, we can use a propositions-as-types approach or the BHK interpretation. This approach works most naturally for constructive logic, but I find it enlightening when it is applicable. Luckily, this result is constructively true. In these interpretations, an implication $Pto Q$ is represented as a function from some type of evidence for $P$ to a type of evidence for $Q$. In other words, evidence for $Pto Q$ is a function from evidence for $P$ to evidence for $Q$. What constitutes evidence for an atomic proposition is left abstract. For example, to provide evidence for $Pto P$, we don't actually need to know what evidence for $P$ looks like; we can just provide a function that returns whatever evidence it is given, i.e. the identity function.
Below is a mechanized proof (in Agda) for the harder direction of the equivalence. This uses notation from the (typed) lambda calculus.
thm : {P Q : Set} → ((P → Q) → (Q → P)) → (Q → P)
thm f q = f (λ _ → q) q
What's going on is f represents the evidence for $(Pto Q)to(Qto P)$ which is to say a function that takes a function $Pto Q$ and evidence for $Q$ and produces evidence for $P$. We've also been given some evidence for $Q$, namely q. We then need to produce some evidence for $P$. f produces such evidence as long as we can give it evidence for $Pto Q$ and $Q$. We already have evidence for $Q$, so we just need to construct evidence for $Pto Q$. But if we know $Q$ (i.e. have evidence for it) then $Pto Q$ holds no matter what $P$ is. This is represented by the evidence for $Pto Q$ being the constantly q function which just ignores the evidence for $P$.
One nice thing about this approach is that it is fairly obvious what to do at each step. (In fact, it is so obvious that Agda produces exactly the above proof term itself, completely automatically.) If you have experience with programming (and particularly typed functional programming), many intuitions with respect to data flow and such make it very easy to see how to prove certain statements, or if they are not (constructively) provable.
answered Feb 3 at 1:42
Derek ElkinsDerek Elkins
17.7k11437
$endgroup$
As a different perspective, we can use a propositions-as-types approach or the BHK interpretation. This approach works most naturally for constructive logic, but I find it enlightening when it is applicable. Luckily, this result is constructively true. In these interpretations, an implication $Pto Q$ is represented as a function from some type of evidence for $P$ to a type of evidence for $Q$. In other words, evidence for $Pto Q$ is a function from evidence for $P$ to evidence for $Q$. What constitutes evidence for an atomic proposition is left abstract. For example, to provide evidence for $Pto P$, we don't actually need to know what evidence for $P$ looks like; we can just provide a function that returns whatever evidence it is given, i.e. the identity function.
Below is a mechanized proof (in Agda) for the harder direction of the equivalence. This uses notation from the (typed) lambda calculus.
thm : {P Q : Set} → ((P → Q) → (Q → P)) → (Q → P)
thm f q = f (λ _ → q) q
What's going on is f represents the evidence for $(Pto Q)to(Qto P)$ which is to say a function that takes a function $Pto Q$ and evidence for $Q$ and produces evidence for $P$. We've also been given some evidence for $Q$, namely q. We then need to produce some evidence for $P$. f produces such evidence as long as we can give it evidence for $Pto Q$ and $Q$. We already have evidence for $Q$, so we just need to construct evidence for $Pto Q$. But if we know $Q$ (i.e. have evidence for it) then $Pto Q$ holds no matter what $P$ is. This is represented by the evidence for $Pto Q$ being the constantly q function which just ignores the evidence for $P$.
One nice thing about this approach is that it is fairly obvious what to do at each step. (In fact, it is so obvious that Agda produces exactly the above proof term itself, completely automatically.) If you have experience with programming (and particularly typed functional programming), many intuitions with respect to data flow and such make it very easy to see how to prove certain statements, or if they are not (constructively) provable.
answered Feb 3 at 1:42
Derek ElkinsDerek Elkins
17.7k11437
answered Feb 3 at 1:42
Derek ElkinsDerek Elkins
17.7k11437
answered Feb 3 at 1:42
Derek ElkinsDerek Elkins
17.7k11437
answered Feb 3 at 1:42
Derek ElkinsDerek Elkins
17.7k11437
17.7k11437
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%2f3097480%2fwhy-is-a-proposition-implying-its-converse-equivalent-to-its-converse%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$
Because we can prove it.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:05
$begingroup$
Two parts proof : (i) $(q to p) vdash [(p to q) to (q to p)]$. Obvious using the tautology : $A to (B to A)$.
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06
$begingroup$
(ii) $[(p→q) → (q→p)] vdash (q to p)$. Less obvious...
$endgroup$
– Mauro ALLEGRANZA
Feb 2 at 17:06