Why $phi lor neg phi $ is not allowed in intuitionistic logic? [closed]
Clash Royale CLAN TAG#URR8PPP
up vote
0
down vote
favorite
Why is $phi lor negphi$ not allowed in intuitionistic logic?
My professor said this was because intuitionistic logic must have concrete construction.
Further, why is it not possible to write a truth table in intuitionistic logic?
logic intuitionistic-logic
edited Aug 28 at 18:50
Taroccoesbrocco
3,78151433
asked Aug 28 at 18:10
J C
417315
closed as off-topic by Andrés E. Caicedo, Tanner Swett, amWhy, Leucippus, Xander Henderson Aug 29 at 4:36
This question appears to be off-topic. The users who voted to close gave this specific reason:
- "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – amWhy, Leucippus, Xander Henderson
 |Â
show 3 more comments
up vote
0
down vote
favorite
Why is $phi lor negphi$ not allowed in intuitionistic logic?
My professor said this was because intuitionistic logic must have concrete construction.
Further, why is it not possible to write a truth table in intuitionistic logic?
logic intuitionistic-logic
edited Aug 28 at 18:50
Taroccoesbrocco
3,78151433
asked Aug 28 at 18:10
J C
417315
closed as off-topic by Andrés E. Caicedo, Tanner Swett, amWhy, Leucippus, Xander Henderson Aug 29 at 4:36
This question appears to be off-topic. The users who voted to close gave this specific reason:
- "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – amWhy, Leucippus, Xander Henderson
3
What is intruvistic?
– Umberto P.
Aug 28 at 18:13
2
I think the term you're after is "intuitionistic".
– Arthur
Aug 28 at 18:13
1
$philandnegphi$ is a contradiction in any kind of logic I know.
– Henning Makholm
Aug 28 at 18:31
1
I'm guessing that when you write $phi land neg phi$ (phi and not phi), you meant to write $phi lor neg phi$ (phi or not phi)? Is that right?
– Tanner Swett
Aug 28 at 18:39
1
The thing your professor was probably referring to was the disjunction $varphiveenegvarphi$; this is the one that is usually connected to whether or not you can form an explicit construction.
– Malice Vidrine
Aug 28 at 18:41
 |Â
show 3 more comments
up vote
0
down vote
favorite
up vote
0
down vote
favorite
Why is $phi lor negphi$ not allowed in intuitionistic logic?
My professor said this was because intuitionistic logic must have concrete construction.
Further, why is it not possible to write a truth table in intuitionistic logic?
logic intuitionistic-logic
edited Aug 28 at 18:50
Taroccoesbrocco
3,78151433
asked Aug 28 at 18:10
J C
417315
Why is $phi lor negphi$ not allowed in intuitionistic logic?
My professor said this was because intuitionistic logic must have concrete construction.
Further, why is it not possible to write a truth table in intuitionistic logic?
logic intuitionistic-logic
edited Aug 28 at 18:50
Taroccoesbrocco
3,78151433
asked Aug 28 at 18:10
J C
417315
edited Aug 28 at 18:50
Taroccoesbrocco
3,78151433
edited Aug 28 at 18:50
Taroccoesbrocco
3,78151433
edited Aug 28 at 18:50
Taroccoesbrocco
3,78151433
3,78151433
asked Aug 28 at 18:10
J C
417315
asked Aug 28 at 18:10
J C
417315
asked Aug 28 at 18:10
J C
417315
417315
closed as off-topic by Andrés E. Caicedo, Tanner Swett, amWhy, Leucippus, Xander Henderson Aug 29 at 4:36
This question appears to be off-topic. The users who voted to close gave this specific reason:
- "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – amWhy, Leucippus, Xander Henderson
closed as off-topic by Andrés E. Caicedo, Tanner Swett, amWhy, Leucippus, Xander Henderson Aug 29 at 4:36
This question appears to be off-topic. The users who voted to close gave this specific reason:
- "This question is missing context or other details: Please improve the question by providing additional context, which ideally includes your thoughts on the problem and any attempts you have made to solve it. This information helps others identify where you have difficulties and helps them write answers appropriate to your experience level." – amWhy, Leucippus, Xander Henderson
3
What is intruvistic?
– Umberto P.
Aug 28 at 18:13
2
I think the term you're after is "intuitionistic".
– Arthur
Aug 28 at 18:13
1
$philandnegphi$ is a contradiction in any kind of logic I know.
– Henning Makholm
Aug 28 at 18:31
1
I'm guessing that when you write $phi land neg phi$ (phi and not phi), you meant to write $phi lor neg phi$ (phi or not phi)? Is that right?
– Tanner Swett
Aug 28 at 18:39
1
The thing your professor was probably referring to was the disjunction $varphiveenegvarphi$; this is the one that is usually connected to whether or not you can form an explicit construction.
– Malice Vidrine
Aug 28 at 18:41
 |Â
show 3 more comments
3
What is intruvistic?
– Umberto P.
Aug 28 at 18:13
2
I think the term you're after is "intuitionistic".
– Arthur
Aug 28 at 18:13
1
$philandnegphi$ is a contradiction in any kind of logic I know.
– Henning Makholm
Aug 28 at 18:31
1
I'm guessing that when you write $phi land neg phi$ (phi and not phi), you meant to write $phi lor neg phi$ (phi or not phi)? Is that right?
– Tanner Swett
Aug 28 at 18:39
1
The thing your professor was probably referring to was the disjunction $varphiveenegvarphi$; this is the one that is usually connected to whether or not you can form an explicit construction.
– Malice Vidrine
Aug 28 at 18:41
3
3
What is intruvistic?
– Umberto P.
Aug 28 at 18:13
What is intruvistic?
– Umberto P.
Aug 28 at 18:13
2
2
I think the term you're after is "intuitionistic".
– Arthur
Aug 28 at 18:13
I think the term you're after is "intuitionistic".
– Arthur
Aug 28 at 18:13
1
1
$philandnegphi$ is a contradiction in any kind of logic I know.
– Henning Makholm
Aug 28 at 18:31
$philandnegphi$ is a contradiction in any kind of logic I know.
– Henning Makholm
Aug 28 at 18:31
1
1
I'm guessing that when you write $phi land neg phi$ (phi and not phi), you meant to write $phi lor neg phi$ (phi or not phi)? Is that right?
– Tanner Swett
Aug 28 at 18:39
I'm guessing that when you write $phi land neg phi$ (phi and not phi), you meant to write $phi lor neg phi$ (phi or not phi)? Is that right?
– Tanner Swett
Aug 28 at 18:39
1
1
The thing your professor was probably referring to was the disjunction $varphiveenegvarphi$; this is the one that is usually connected to whether or not you can form an explicit construction.
– Malice Vidrine
Aug 28 at 18:41
The thing your professor was probably referring to was the disjunction $varphiveenegvarphi$; this is the one that is usually connected to whether or not you can form an explicit construction.
– Malice Vidrine
Aug 28 at 18:41
 |Â
show 3 more comments
1 Answer
1
active
oldest
votes
up vote
6
down vote
accepted
Intuitionistic logic does not consider $philornegphi$ to be universally valid because that's the way "intuitionistic logic" is defined.
The word "intuitionistic" refers to the intuitionists, a grouping of mathematicians who in the first part of the 1900s made up one side of a Great Controversy about what should be considered a valid proof. Among the arguments they didn't accept were ones of the form
Either $phi$ is true or it is not. We don't know which, but in each of those cases $psi$ must be true, so $psi$ is definitely true.
What we call "intuitionistic logic" today is, however, not the work of the intuitionists themselves. On the contrary the most prominent intuitionists tended to vehemently deny that the validity of an argument could be reduced to a system of rigid rules -- they appealed instead to the mathematician's intuition, hence the name. The system taught in modern textbooks is later workers' attempt to nevertheless find a formal definition that would align more-or-less with what the intuitionists were known to consider good proofs.
So arguably "the reason" why intuitionistic logic doesn't allow the law of excluded middle is simply that it is designed to mimic the opinions of Brouwer and his followers, who did not accept arguments of the above form.
From a modern perspective one might say that intuitionistic logic is by definition the study of what is still provable if one excludes appeals to the law of excluded middle (or other principles that turn out to be equivalent to it).
Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it. (The logic is only one part of this program; one also needs to choose one's axioms so they correspond to meaningful "constructive" steps). This is of importance in computer science and allied fields of mathematics, which is a main reason intuitionistic logic is still being studied as more than a technical curiosity.
It so turns out that the resulting notion of provability cannot be described using truth tables in the simple way classical propositional logic can. This is not a design goal, however -- it's just what happens to follow from the set of proof rules we're studying.
answered Aug 28 at 18:48
Henning Makholm
230k16296526
Intuitionistic logic also arises naturally in category theory, as it is very closely related to the notion of a cartesian closed category. For example, Heyting algebras are precisely the lattices which are cartesian closed categories. Toposes are systems of intuitionistic higher order logic (aka intuitionistic set theory).
– Hurkyl
Aug 28 at 19:00
+1: nice answer: out of interest, can you name some early intuitionists apart from Brouwer who scorned formalism?
– Rob Arthan
Aug 28 at 20:35
@RobArthan: No; I am not that familiar with the history. (In fact I cannot name any early intuitionists apart from Brouwer, full stop, except to the extent Kronecker is usually considered a forerunner -- but he was a generation or so earlier).
– Henning Makholm
Aug 28 at 20:43
@HenningMakholm: interesting! I have a suspicion (completely unsupported by any real historical research on my part) that it was only Brouwer himself amongst the early writers on intuitionism who had an aversion to formalism viewed as the arithmetization of metamathematics and that others such as Heyting and Kolmogorov revelled in it.
– Rob Arthan
Aug 28 at 20:52
"Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it." For example, the typical interval halving proof of the intermediate-value theorem invokes the so-called lesser limited principle of omniscience (llpo). In the context of the ivt, llpo is how we are able to decide either $fleft(frac12(a+b)right) geq c$ or else $fleft(frac12(a+b)right) leq c$. However llpo is known to be nonconstructive. +1 for thorough answer
– Matt A Pelto
Aug 28 at 22:39
 |Â
show 2 more comments
1 Answer
1
active
oldest
votes
1 Answer
1
active
oldest
votes
active
oldest
votes
active
oldest
votes
up vote
6
down vote
accepted
Intuitionistic logic does not consider $philornegphi$ to be universally valid because that's the way "intuitionistic logic" is defined.
The word "intuitionistic" refers to the intuitionists, a grouping of mathematicians who in the first part of the 1900s made up one side of a Great Controversy about what should be considered a valid proof. Among the arguments they didn't accept were ones of the form
Either $phi$ is true or it is not. We don't know which, but in each of those cases $psi$ must be true, so $psi$ is definitely true.
What we call "intuitionistic logic" today is, however, not the work of the intuitionists themselves. On the contrary the most prominent intuitionists tended to vehemently deny that the validity of an argument could be reduced to a system of rigid rules -- they appealed instead to the mathematician's intuition, hence the name. The system taught in modern textbooks is later workers' attempt to nevertheless find a formal definition that would align more-or-less with what the intuitionists were known to consider good proofs.
So arguably "the reason" why intuitionistic logic doesn't allow the law of excluded middle is simply that it is designed to mimic the opinions of Brouwer and his followers, who did not accept arguments of the above form.
From a modern perspective one might say that intuitionistic logic is by definition the study of what is still provable if one excludes appeals to the law of excluded middle (or other principles that turn out to be equivalent to it).
Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it. (The logic is only one part of this program; one also needs to choose one's axioms so they correspond to meaningful "constructive" steps). This is of importance in computer science and allied fields of mathematics, which is a main reason intuitionistic logic is still being studied as more than a technical curiosity.
It so turns out that the resulting notion of provability cannot be described using truth tables in the simple way classical propositional logic can. This is not a design goal, however -- it's just what happens to follow from the set of proof rules we're studying.
answered Aug 28 at 18:48
Henning Makholm
230k16296526
Intuitionistic logic also arises naturally in category theory, as it is very closely related to the notion of a cartesian closed category. For example, Heyting algebras are precisely the lattices which are cartesian closed categories. Toposes are systems of intuitionistic higher order logic (aka intuitionistic set theory).
– Hurkyl
Aug 28 at 19:00
+1: nice answer: out of interest, can you name some early intuitionists apart from Brouwer who scorned formalism?
– Rob Arthan
Aug 28 at 20:35
@RobArthan: No; I am not that familiar with the history. (In fact I cannot name any early intuitionists apart from Brouwer, full stop, except to the extent Kronecker is usually considered a forerunner -- but he was a generation or so earlier).
– Henning Makholm
Aug 28 at 20:43
@HenningMakholm: interesting! I have a suspicion (completely unsupported by any real historical research on my part) that it was only Brouwer himself amongst the early writers on intuitionism who had an aversion to formalism viewed as the arithmetization of metamathematics and that others such as Heyting and Kolmogorov revelled in it.
– Rob Arthan
Aug 28 at 20:52
"Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it." For example, the typical interval halving proof of the intermediate-value theorem invokes the so-called lesser limited principle of omniscience (llpo). In the context of the ivt, llpo is how we are able to decide either $fleft(frac12(a+b)right) geq c$ or else $fleft(frac12(a+b)right) leq c$. However llpo is known to be nonconstructive. +1 for thorough answer
– Matt A Pelto
Aug 28 at 22:39
 |Â
show 2 more comments
up vote
6
down vote
accepted
Intuitionistic logic does not consider $philornegphi$ to be universally valid because that's the way "intuitionistic logic" is defined.
The word "intuitionistic" refers to the intuitionists, a grouping of mathematicians who in the first part of the 1900s made up one side of a Great Controversy about what should be considered a valid proof. Among the arguments they didn't accept were ones of the form
Either $phi$ is true or it is not. We don't know which, but in each of those cases $psi$ must be true, so $psi$ is definitely true.
What we call "intuitionistic logic" today is, however, not the work of the intuitionists themselves. On the contrary the most prominent intuitionists tended to vehemently deny that the validity of an argument could be reduced to a system of rigid rules -- they appealed instead to the mathematician's intuition, hence the name. The system taught in modern textbooks is later workers' attempt to nevertheless find a formal definition that would align more-or-less with what the intuitionists were known to consider good proofs.
So arguably "the reason" why intuitionistic logic doesn't allow the law of excluded middle is simply that it is designed to mimic the opinions of Brouwer and his followers, who did not accept arguments of the above form.
From a modern perspective one might say that intuitionistic logic is by definition the study of what is still provable if one excludes appeals to the law of excluded middle (or other principles that turn out to be equivalent to it).
Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it. (The logic is only one part of this program; one also needs to choose one's axioms so they correspond to meaningful "constructive" steps). This is of importance in computer science and allied fields of mathematics, which is a main reason intuitionistic logic is still being studied as more than a technical curiosity.
It so turns out that the resulting notion of provability cannot be described using truth tables in the simple way classical propositional logic can. This is not a design goal, however -- it's just what happens to follow from the set of proof rules we're studying.
answered Aug 28 at 18:48
Henning Makholm
230k16296526
Intuitionistic logic also arises naturally in category theory, as it is very closely related to the notion of a cartesian closed category. For example, Heyting algebras are precisely the lattices which are cartesian closed categories. Toposes are systems of intuitionistic higher order logic (aka intuitionistic set theory).
– Hurkyl
Aug 28 at 19:00
+1: nice answer: out of interest, can you name some early intuitionists apart from Brouwer who scorned formalism?
– Rob Arthan
Aug 28 at 20:35
@RobArthan: No; I am not that familiar with the history. (In fact I cannot name any early intuitionists apart from Brouwer, full stop, except to the extent Kronecker is usually considered a forerunner -- but he was a generation or so earlier).
– Henning Makholm
Aug 28 at 20:43
@HenningMakholm: interesting! I have a suspicion (completely unsupported by any real historical research on my part) that it was only Brouwer himself amongst the early writers on intuitionism who had an aversion to formalism viewed as the arithmetization of metamathematics and that others such as Heyting and Kolmogorov revelled in it.
– Rob Arthan
Aug 28 at 20:52
"Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it." For example, the typical interval halving proof of the intermediate-value theorem invokes the so-called lesser limited principle of omniscience (llpo). In the context of the ivt, llpo is how we are able to decide either $fleft(frac12(a+b)right) geq c$ or else $fleft(frac12(a+b)right) leq c$. However llpo is known to be nonconstructive. +1 for thorough answer
– Matt A Pelto
Aug 28 at 22:39
 |Â
show 2 more comments
up vote
6
down vote
accepted
up vote
6
down vote
accepted
Intuitionistic logic does not consider $philornegphi$ to be universally valid because that's the way "intuitionistic logic" is defined.
The word "intuitionistic" refers to the intuitionists, a grouping of mathematicians who in the first part of the 1900s made up one side of a Great Controversy about what should be considered a valid proof. Among the arguments they didn't accept were ones of the form
Either $phi$ is true or it is not. We don't know which, but in each of those cases $psi$ must be true, so $psi$ is definitely true.
What we call "intuitionistic logic" today is, however, not the work of the intuitionists themselves. On the contrary the most prominent intuitionists tended to vehemently deny that the validity of an argument could be reduced to a system of rigid rules -- they appealed instead to the mathematician's intuition, hence the name. The system taught in modern textbooks is later workers' attempt to nevertheless find a formal definition that would align more-or-less with what the intuitionists were known to consider good proofs.
So arguably "the reason" why intuitionistic logic doesn't allow the law of excluded middle is simply that it is designed to mimic the opinions of Brouwer and his followers, who did not accept arguments of the above form.
From a modern perspective one might say that intuitionistic logic is by definition the study of what is still provable if one excludes appeals to the law of excluded middle (or other principles that turn out to be equivalent to it).
Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it. (The logic is only one part of this program; one also needs to choose one's axioms so they correspond to meaningful "constructive" steps). This is of importance in computer science and allied fields of mathematics, which is a main reason intuitionistic logic is still being studied as more than a technical curiosity.
It so turns out that the resulting notion of provability cannot be described using truth tables in the simple way classical propositional logic can. This is not a design goal, however -- it's just what happens to follow from the set of proof rules we're studying.
answered Aug 28 at 18:48
Henning Makholm
230k16296526
Intuitionistic logic does not consider $philornegphi$ to be universally valid because that's the way "intuitionistic logic" is defined.
The word "intuitionistic" refers to the intuitionists, a grouping of mathematicians who in the first part of the 1900s made up one side of a Great Controversy about what should be considered a valid proof. Among the arguments they didn't accept were ones of the form
Either $phi$ is true or it is not. We don't know which, but in each of those cases $psi$ must be true, so $psi$ is definitely true.
What we call "intuitionistic logic" today is, however, not the work of the intuitionists themselves. On the contrary the most prominent intuitionists tended to vehemently deny that the validity of an argument could be reduced to a system of rigid rules -- they appealed instead to the mathematician's intuition, hence the name. The system taught in modern textbooks is later workers' attempt to nevertheless find a formal definition that would align more-or-less with what the intuitionists were known to consider good proofs.
So arguably "the reason" why intuitionistic logic doesn't allow the law of excluded middle is simply that it is designed to mimic the opinions of Brouwer and his followers, who did not accept arguments of the above form.
From a modern perspective one might say that intuitionistic logic is by definition the study of what is still provable if one excludes appeals to the law of excluded middle (or other principles that turn out to be equivalent to it).
Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it. (The logic is only one part of this program; one also needs to choose one's axioms so they correspond to meaningful "constructive" steps). This is of importance in computer science and allied fields of mathematics, which is a main reason intuitionistic logic is still being studied as more than a technical curiosity.
It so turns out that the resulting notion of provability cannot be described using truth tables in the simple way classical propositional logic can. This is not a design goal, however -- it's just what happens to follow from the set of proof rules we're studying.
answered Aug 28 at 18:48
Henning Makholm
230k16296526
edited Aug 28 at 23:10
answered Aug 28 at 18:48
Henning Makholm
230k16296526
answered Aug 28 at 18:48
Henning Makholm
230k16296526
answered Aug 28 at 18:48
Henning Makholm
230k16296526
230k16296526
Intuitionistic logic also arises naturally in category theory, as it is very closely related to the notion of a cartesian closed category. For example, Heyting algebras are precisely the lattices which are cartesian closed categories. Toposes are systems of intuitionistic higher order logic (aka intuitionistic set theory).
– Hurkyl
Aug 28 at 19:00
+1: nice answer: out of interest, can you name some early intuitionists apart from Brouwer who scorned formalism?
– Rob Arthan
Aug 28 at 20:35
@RobArthan: No; I am not that familiar with the history. (In fact I cannot name any early intuitionists apart from Brouwer, full stop, except to the extent Kronecker is usually considered a forerunner -- but he was a generation or so earlier).
– Henning Makholm
Aug 28 at 20:43
@HenningMakholm: interesting! I have a suspicion (completely unsupported by any real historical research on my part) that it was only Brouwer himself amongst the early writers on intuitionism who had an aversion to formalism viewed as the arithmetization of metamathematics and that others such as Heyting and Kolmogorov revelled in it.
– Rob Arthan
Aug 28 at 20:52
"Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it." For example, the typical interval halving proof of the intermediate-value theorem invokes the so-called lesser limited principle of omniscience (llpo). In the context of the ivt, llpo is how we are able to decide either $fleft(frac12(a+b)right) geq c$ or else $fleft(frac12(a+b)right) leq c$. However llpo is known to be nonconstructive. +1 for thorough answer
– Matt A Pelto
Aug 28 at 22:39
 |Â
show 2 more comments
Intuitionistic logic also arises naturally in category theory, as it is very closely related to the notion of a cartesian closed category. For example, Heyting algebras are precisely the lattices which are cartesian closed categories. Toposes are systems of intuitionistic higher order logic (aka intuitionistic set theory).
– Hurkyl
Aug 28 at 19:00
+1: nice answer: out of interest, can you name some early intuitionists apart from Brouwer who scorned formalism?
– Rob Arthan
Aug 28 at 20:35
@RobArthan: No; I am not that familiar with the history. (In fact I cannot name any early intuitionists apart from Brouwer, full stop, except to the extent Kronecker is usually considered a forerunner -- but he was a generation or so earlier).
– Henning Makholm
Aug 28 at 20:43
@HenningMakholm: interesting! I have a suspicion (completely unsupported by any real historical research on my part) that it was only Brouwer himself amongst the early writers on intuitionism who had an aversion to formalism viewed as the arithmetization of metamathematics and that others such as Heyting and Kolmogorov revelled in it.
– Rob Arthan
Aug 28 at 20:52
"Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it." For example, the typical interval halving proof of the intermediate-value theorem invokes the so-called lesser limited principle of omniscience (llpo). In the context of the ivt, llpo is how we are able to decide either $fleft(frac12(a+b)right) geq c$ or else $fleft(frac12(a+b)right) leq c$. However llpo is known to be nonconstructive. +1 for thorough answer
– Matt A Pelto
Aug 28 at 22:39
Intuitionistic logic also arises naturally in category theory, as it is very closely related to the notion of a cartesian closed category. For example, Heyting algebras are precisely the lattices which are cartesian closed categories. Toposes are systems of intuitionistic higher order logic (aka intuitionistic set theory).
– Hurkyl
Aug 28 at 19:00
Intuitionistic logic also arises naturally in category theory, as it is very closely related to the notion of a cartesian closed category. For example, Heyting algebras are precisely the lattices which are cartesian closed categories. Toposes are systems of intuitionistic higher order logic (aka intuitionistic set theory).
– Hurkyl
Aug 28 at 19:00
+1: nice answer: out of interest, can you name some early intuitionists apart from Brouwer who scorned formalism?
– Rob Arthan
Aug 28 at 20:35
+1: nice answer: out of interest, can you name some early intuitionists apart from Brouwer who scorned formalism?
– Rob Arthan
Aug 28 at 20:35
@RobArthan: No; I am not that familiar with the history. (In fact I cannot name any early intuitionists apart from Brouwer, full stop, except to the extent Kronecker is usually considered a forerunner -- but he was a generation or so earlier).
– Henning Makholm
Aug 28 at 20:43
@RobArthan: No; I am not that familiar with the history. (In fact I cannot name any early intuitionists apart from Brouwer, full stop, except to the extent Kronecker is usually considered a forerunner -- but he was a generation or so earlier).
– Henning Makholm
Aug 28 at 20:43
@HenningMakholm: interesting! I have a suspicion (completely unsupported by any real historical research on my part) that it was only Brouwer himself amongst the early writers on intuitionism who had an aversion to formalism viewed as the arithmetization of metamathematics and that others such as Heyting and Kolmogorov revelled in it.
– Rob Arthan
Aug 28 at 20:52
@HenningMakholm: interesting! I have a suspicion (completely unsupported by any real historical research on my part) that it was only Brouwer himself amongst the early writers on intuitionism who had an aversion to formalism viewed as the arithmetization of metamathematics and that others such as Heyting and Kolmogorov revelled in it.
– Rob Arthan
Aug 28 at 20:52
"Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it." For example, the typical interval halving proof of the intermediate-value theorem invokes the so-called lesser limited principle of omniscience (llpo). In the context of the ivt, llpo is how we are able to decide either $fleft(frac12(a+b)right) geq c$ or else $fleft(frac12(a+b)right) leq c$. However llpo is known to be nonconstructive. +1 for thorough answer
– Matt A Pelto
Aug 28 at 22:39
"Even more, though, intuitionistic logic is well suited for expressing arguments in a style where proving something exists also provides an algorithm for constructing it." For example, the typical interval halving proof of the intermediate-value theorem invokes the so-called lesser limited principle of omniscience (llpo). In the context of the ivt, llpo is how we are able to decide either $fleft(frac12(a+b)right) geq c$ or else $fleft(frac12(a+b)right) leq c$. However llpo is known to be nonconstructive. +1 for thorough answer
– Matt A Pelto
Aug 28 at 22:39
 |Â
show 2 more comments
3
What is intruvistic?
– Umberto P.
Aug 28 at 18:13
2
I think the term you're after is "intuitionistic".
– Arthur
Aug 28 at 18:13
1
$philandnegphi$ is a contradiction in any kind of logic I know.
– Henning Makholm
Aug 28 at 18:31
1
I'm guessing that when you write $phi land neg phi$ (phi and not phi), you meant to write $phi lor neg phi$ (phi or not phi)? Is that right?
– Tanner Swett
Aug 28 at 18:39
1
The thing your professor was probably referring to was the disjunction $varphiveenegvarphi$; this is the one that is usually connected to whether or not you can form an explicit construction.
– Malice Vidrine
Aug 28 at 18:41