In Frege proof systems, how to understand 2 if then? [closed]
$begingroup$
For axioms, e.g.
$(p_1 supset p_3) supset (p_2 supset p_3) supset (p_1 lor p_2 supset p_3)$
My understanding is if ($p_1$ can infer $p_2$, and $p_2$ can infer $p_3$), then (if $p_1$ is true or $p_2$ is true, then $p_3$ is true).
If so, how to understand the 2nd $supset$, why not use $land$?
logic propositional-calculus
edited Dec 8 '18 at 23:34
Davide Giraudo
127k16153268
asked Dec 6 '18 at 7:10
Steven YangSteven Yang
1
$endgroup$
closed as unclear what you're asking by Mauro ALLEGRANZA, amWhy, José Carlos Santos, Leucippus, John B Dec 9 '18 at 2:46
Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.
add a comment |
$begingroup$
For axioms, e.g.
$(p_1 supset p_3) supset (p_2 supset p_3) supset (p_1 lor p_2 supset p_3)$
My understanding is if ($p_1$ can infer $p_2$, and $p_2$ can infer $p_3$), then (if $p_1$ is true or $p_2$ is true, then $p_3$ is true).
If so, how to understand the 2nd $supset$, why not use $land$?
logic propositional-calculus
edited Dec 8 '18 at 23:34
Davide Giraudo
127k16153268
asked Dec 6 '18 at 7:10
Steven YangSteven Yang
1
$endgroup$
closed as unclear what you're asking by Mauro ALLEGRANZA, amWhy, José Carlos Santos, Leucippus, John B Dec 9 '18 at 2:46
Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.
2
$begingroup$
I think you need another parenthesis-- implication not associative.
$endgroup$
– coffeemath
Dec 6 '18 at 7:20
add a comment |
$begingroup$
For axioms, e.g.
$(p_1 supset p_3) supset (p_2 supset p_3) supset (p_1 lor p_2 supset p_3)$
My understanding is if ($p_1$ can infer $p_2$, and $p_2$ can infer $p_3$), then (if $p_1$ is true or $p_2$ is true, then $p_3$ is true).
If so, how to understand the 2nd $supset$, why not use $land$?
logic propositional-calculus
edited Dec 8 '18 at 23:34
Davide Giraudo
127k16153268
asked Dec 6 '18 at 7:10
Steven YangSteven Yang
1
$endgroup$
For axioms, e.g.
$(p_1 supset p_3) supset (p_2 supset p_3) supset (p_1 lor p_2 supset p_3)$
My understanding is if ($p_1$ can infer $p_2$, and $p_2$ can infer $p_3$), then (if $p_1$ is true or $p_2$ is true, then $p_3$ is true).
If so, how to understand the 2nd $supset$, why not use $land$?
logic propositional-calculus
logic propositional-calculus
edited Dec 8 '18 at 23:34
Davide Giraudo
127k16153268
asked Dec 6 '18 at 7:10
Steven YangSteven Yang
1
edited Dec 8 '18 at 23:34
Davide Giraudo
127k16153268
asked Dec 6 '18 at 7:10
Steven YangSteven Yang
1
edited Dec 8 '18 at 23:34
Davide Giraudo
127k16153268
edited Dec 8 '18 at 23:34
Davide Giraudo
127k16153268
edited Dec 8 '18 at 23:34
Davide Giraudo
127k16153268
127k16153268
asked Dec 6 '18 at 7:10
Steven YangSteven Yang
1
asked Dec 6 '18 at 7:10
Steven YangSteven Yang
1
asked Dec 6 '18 at 7:10
Steven YangSteven Yang
1
1
closed as unclear what you're asking by Mauro ALLEGRANZA, amWhy, José Carlos Santos, Leucippus, John B Dec 9 '18 at 2:46
Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.
closed as unclear what you're asking by Mauro ALLEGRANZA, amWhy, José Carlos Santos, Leucippus, John B Dec 9 '18 at 2:46
Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.
2
$begingroup$
I think you need another parenthesis-- implication not associative.
$endgroup$
– coffeemath
Dec 6 '18 at 7:20
add a comment |
2
$begingroup$
I think you need another parenthesis-- implication not associative.
$endgroup$
– coffeemath
Dec 6 '18 at 7:20
2
2
$begingroup$
I think you need another parenthesis-- implication not associative.
$endgroup$
– coffeemath
Dec 6 '18 at 7:20
$begingroup$
I think you need another parenthesis-- implication not associative.
$endgroup$
– coffeemath
Dec 6 '18 at 7:20
add a comment |
2 Answers
2
active
oldest
votes
$begingroup$
The lack of parentheses introduces an ambiguity in the formula.
See e.g. Herbert Enderton, A Mathematical Introduction to Logic, Academic Press (2nd ed., 2001), page 33 on omitting parentheses :
we adopt the following conventions : [...]
The negation symbol applies to as little as possible.
The conjunction and disjunction symbols apply to as little as possible,
given that convention 2 is to be observed.
Where one connective symbol is used repeatedly, grouping is to the right: $α → β → γ$ is $α → (β → γ)$.
Thus, I'll read the formula as :
$(P to Q) to [(R to Q) to ((P lor R) to Q)]$.
It is simply Disjunction elimination written as a tautology instead of as a rule.
See Hilbert-style axioms system for intuitionistic logic (but why Frege's ?).
From it, we can recover the rule using modus ponens twice :
$(P to Q), (R to Q) vdash (P lor R) to Q$.
If we read the formula that way, your interpretation is correct : we can use $land$ instead to express the same logical principle.
See Exportation :
$((varphi land psi) to sigma) equiv (varphi to (psi to sigma))$.
answered Dec 6 '18 at 7:40
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
$endgroup$
$begingroup$
He says 'and', but there's no connective like that in his formula.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 13:13
$begingroup$
No, I'm not joking at all. If $land$ isn't a primitive connective, it can't get used for the basis of the system. In Polish notation CCpqCCrqCAprq is "If, if p, then q, then if, if r, then q, then if p or r, then q" while CKCpqCrqCAprq is "if both if p, then q, and if r then q, then if either p or r, then q". Also, there's no guarantee that if CCpqCCrqCAprq is at the basis of the system, that replacing it with CKCpqCrqCAprq will result in the same system.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 23:08
add a comment |
$begingroup$
No.
It's more like:
"If, if p1, then p3, then if, if p2, then p3, then if p1 or p2, then p3."
In your translation you have a conjunction as the antecedent, having two conditionals as the conjuncts of that conjuction. But, the formula says that the antecedent is a conditional "if p1, then p3".
There does exist a relationship via the exportation and importation laws that Mauro referenced, but such a relationship concerns formulas that differ.
In general, two 'if-thens' can get understood as multiple if-thens.
answered Dec 7 '18 at 13:18
Doug SpoonwoodDoug Spoonwood
8,12212244
$endgroup$
add a comment |
2 Answers
2
active
oldest
votes
2 Answers
2
active
oldest
votes
active
oldest
votes
active
oldest
votes
$begingroup$
The lack of parentheses introduces an ambiguity in the formula.
See e.g. Herbert Enderton, A Mathematical Introduction to Logic, Academic Press (2nd ed., 2001), page 33 on omitting parentheses :
we adopt the following conventions : [...]
The negation symbol applies to as little as possible.
The conjunction and disjunction symbols apply to as little as possible,
given that convention 2 is to be observed.
Where one connective symbol is used repeatedly, grouping is to the right: $α → β → γ$ is $α → (β → γ)$.
Thus, I'll read the formula as :
$(P to Q) to [(R to Q) to ((P lor R) to Q)]$.
It is simply Disjunction elimination written as a tautology instead of as a rule.
See Hilbert-style axioms system for intuitionistic logic (but why Frege's ?).
From it, we can recover the rule using modus ponens twice :
$(P to Q), (R to Q) vdash (P lor R) to Q$.
If we read the formula that way, your interpretation is correct : we can use $land$ instead to express the same logical principle.
See Exportation :
$((varphi land psi) to sigma) equiv (varphi to (psi to sigma))$.
answered Dec 6 '18 at 7:40
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
$endgroup$
$begingroup$
He says 'and', but there's no connective like that in his formula.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 13:13
$begingroup$
No, I'm not joking at all. If $land$ isn't a primitive connective, it can't get used for the basis of the system. In Polish notation CCpqCCrqCAprq is "If, if p, then q, then if, if r, then q, then if p or r, then q" while CKCpqCrqCAprq is "if both if p, then q, and if r then q, then if either p or r, then q". Also, there's no guarantee that if CCpqCCrqCAprq is at the basis of the system, that replacing it with CKCpqCrqCAprq will result in the same system.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 23:08
add a comment |
$begingroup$
The lack of parentheses introduces an ambiguity in the formula.
See e.g. Herbert Enderton, A Mathematical Introduction to Logic, Academic Press (2nd ed., 2001), page 33 on omitting parentheses :
we adopt the following conventions : [...]
The negation symbol applies to as little as possible.
The conjunction and disjunction symbols apply to as little as possible,
given that convention 2 is to be observed.
Where one connective symbol is used repeatedly, grouping is to the right: $α → β → γ$ is $α → (β → γ)$.
Thus, I'll read the formula as :
$(P to Q) to [(R to Q) to ((P lor R) to Q)]$.
It is simply Disjunction elimination written as a tautology instead of as a rule.
See Hilbert-style axioms system for intuitionistic logic (but why Frege's ?).
From it, we can recover the rule using modus ponens twice :
$(P to Q), (R to Q) vdash (P lor R) to Q$.
If we read the formula that way, your interpretation is correct : we can use $land$ instead to express the same logical principle.
See Exportation :
$((varphi land psi) to sigma) equiv (varphi to (psi to sigma))$.
answered Dec 6 '18 at 7:40
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
$endgroup$
$begingroup$
He says 'and', but there's no connective like that in his formula.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 13:13
$begingroup$
No, I'm not joking at all. If $land$ isn't a primitive connective, it can't get used for the basis of the system. In Polish notation CCpqCCrqCAprq is "If, if p, then q, then if, if r, then q, then if p or r, then q" while CKCpqCrqCAprq is "if both if p, then q, and if r then q, then if either p or r, then q". Also, there's no guarantee that if CCpqCCrqCAprq is at the basis of the system, that replacing it with CKCpqCrqCAprq will result in the same system.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 23:08
add a comment |
$begingroup$
The lack of parentheses introduces an ambiguity in the formula.
See e.g. Herbert Enderton, A Mathematical Introduction to Logic, Academic Press (2nd ed., 2001), page 33 on omitting parentheses :
we adopt the following conventions : [...]
The negation symbol applies to as little as possible.
The conjunction and disjunction symbols apply to as little as possible,
given that convention 2 is to be observed.
Where one connective symbol is used repeatedly, grouping is to the right: $α → β → γ$ is $α → (β → γ)$.
Thus, I'll read the formula as :
$(P to Q) to [(R to Q) to ((P lor R) to Q)]$.
It is simply Disjunction elimination written as a tautology instead of as a rule.
See Hilbert-style axioms system for intuitionistic logic (but why Frege's ?).
From it, we can recover the rule using modus ponens twice :
$(P to Q), (R to Q) vdash (P lor R) to Q$.
If we read the formula that way, your interpretation is correct : we can use $land$ instead to express the same logical principle.
See Exportation :
$((varphi land psi) to sigma) equiv (varphi to (psi to sigma))$.
answered Dec 6 '18 at 7:40
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
$endgroup$
The lack of parentheses introduces an ambiguity in the formula.
See e.g. Herbert Enderton, A Mathematical Introduction to Logic, Academic Press (2nd ed., 2001), page 33 on omitting parentheses :
we adopt the following conventions : [...]
The negation symbol applies to as little as possible.
The conjunction and disjunction symbols apply to as little as possible,
given that convention 2 is to be observed.
Where one connective symbol is used repeatedly, grouping is to the right: $α → β → γ$ is $α → (β → γ)$.
Thus, I'll read the formula as :
$(P to Q) to [(R to Q) to ((P lor R) to Q)]$.
It is simply Disjunction elimination written as a tautology instead of as a rule.
See Hilbert-style axioms system for intuitionistic logic (but why Frege's ?).
From it, we can recover the rule using modus ponens twice :
$(P to Q), (R to Q) vdash (P lor R) to Q$.
If we read the formula that way, your interpretation is correct : we can use $land$ instead to express the same logical principle.
See Exportation :
$((varphi land psi) to sigma) equiv (varphi to (psi to sigma))$.
answered Dec 6 '18 at 7:40
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
edited Dec 8 '18 at 10:33
answered Dec 6 '18 at 7:40
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
answered Dec 6 '18 at 7:40
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
answered Dec 6 '18 at 7:40
Mauro ALLEGRANZAMauro ALLEGRANZA
66.9k449115
66.9k449115
$begingroup$
He says 'and', but there's no connective like that in his formula.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 13:13
$begingroup$
No, I'm not joking at all. If $land$ isn't a primitive connective, it can't get used for the basis of the system. In Polish notation CCpqCCrqCAprq is "If, if p, then q, then if, if r, then q, then if p or r, then q" while CKCpqCrqCAprq is "if both if p, then q, and if r then q, then if either p or r, then q". Also, there's no guarantee that if CCpqCCrqCAprq is at the basis of the system, that replacing it with CKCpqCrqCAprq will result in the same system.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 23:08
add a comment |
$begingroup$
He says 'and', but there's no connective like that in his formula.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 13:13
$begingroup$
No, I'm not joking at all. If $land$ isn't a primitive connective, it can't get used for the basis of the system. In Polish notation CCpqCCrqCAprq is "If, if p, then q, then if, if r, then q, then if p or r, then q" while CKCpqCrqCAprq is "if both if p, then q, and if r then q, then if either p or r, then q". Also, there's no guarantee that if CCpqCCrqCAprq is at the basis of the system, that replacing it with CKCpqCrqCAprq will result in the same system.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 23:08
$begingroup$
He says 'and', but there's no connective like that in his formula.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 13:13
$begingroup$
He says 'and', but there's no connective like that in his formula.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 13:13
$begingroup$
No, I'm not joking at all. If $land$ isn't a primitive connective, it can't get used for the basis of the system. In Polish notation CCpqCCrqCAprq is "If, if p, then q, then if, if r, then q, then if p or r, then q" while CKCpqCrqCAprq is "if both if p, then q, and if r then q, then if either p or r, then q". Also, there's no guarantee that if CCpqCCrqCAprq is at the basis of the system, that replacing it with CKCpqCrqCAprq will result in the same system.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 23:08
$begingroup$
No, I'm not joking at all. If $land$ isn't a primitive connective, it can't get used for the basis of the system. In Polish notation CCpqCCrqCAprq is "If, if p, then q, then if, if r, then q, then if p or r, then q" while CKCpqCrqCAprq is "if both if p, then q, and if r then q, then if either p or r, then q". Also, there's no guarantee that if CCpqCCrqCAprq is at the basis of the system, that replacing it with CKCpqCrqCAprq will result in the same system.
$endgroup$
– Doug Spoonwood
Dec 7 '18 at 23:08
add a comment |
$begingroup$
No.
It's more like:
"If, if p1, then p3, then if, if p2, then p3, then if p1 or p2, then p3."
In your translation you have a conjunction as the antecedent, having two conditionals as the conjuncts of that conjuction. But, the formula says that the antecedent is a conditional "if p1, then p3".
There does exist a relationship via the exportation and importation laws that Mauro referenced, but such a relationship concerns formulas that differ.
In general, two 'if-thens' can get understood as multiple if-thens.
answered Dec 7 '18 at 13:18
Doug SpoonwoodDoug Spoonwood
8,12212244
$endgroup$
add a comment |
$begingroup$
No.
It's more like:
"If, if p1, then p3, then if, if p2, then p3, then if p1 or p2, then p3."
In your translation you have a conjunction as the antecedent, having two conditionals as the conjuncts of that conjuction. But, the formula says that the antecedent is a conditional "if p1, then p3".
There does exist a relationship via the exportation and importation laws that Mauro referenced, but such a relationship concerns formulas that differ.
In general, two 'if-thens' can get understood as multiple if-thens.
answered Dec 7 '18 at 13:18
Doug SpoonwoodDoug Spoonwood
8,12212244
$endgroup$
add a comment |
$begingroup$
No.
It's more like:
"If, if p1, then p3, then if, if p2, then p3, then if p1 or p2, then p3."
In your translation you have a conjunction as the antecedent, having two conditionals as the conjuncts of that conjuction. But, the formula says that the antecedent is a conditional "if p1, then p3".
There does exist a relationship via the exportation and importation laws that Mauro referenced, but such a relationship concerns formulas that differ.
In general, two 'if-thens' can get understood as multiple if-thens.
answered Dec 7 '18 at 13:18
Doug SpoonwoodDoug Spoonwood
8,12212244
$endgroup$
No.
It's more like:
"If, if p1, then p3, then if, if p2, then p3, then if p1 or p2, then p3."
In your translation you have a conjunction as the antecedent, having two conditionals as the conjuncts of that conjuction. But, the formula says that the antecedent is a conditional "if p1, then p3".
There does exist a relationship via the exportation and importation laws that Mauro referenced, but such a relationship concerns formulas that differ.
In general, two 'if-thens' can get understood as multiple if-thens.
answered Dec 7 '18 at 13:18
Doug SpoonwoodDoug Spoonwood
8,12212244
answered Dec 7 '18 at 13:18
Doug SpoonwoodDoug Spoonwood
8,12212244
answered Dec 7 '18 at 13:18
Doug SpoonwoodDoug Spoonwood
8,12212244
answered Dec 7 '18 at 13:18
Doug SpoonwoodDoug Spoonwood
8,12212244
8,12212244
add a comment |
add a comment |
2
$begingroup$
I think you need another parenthesis-- implication not associative.
$endgroup$
– coffeemath
Dec 6 '18 at 7:20