27
votes
Accepted
If you used intuitionistic logic in real life, would you not sound absurd?
As Conifold comments, a real-life intuitionist would not shy away from assuming LEM ... when appropriate. Intuitionism merely permits the failure of LEM, it doesn't assert that it always occurs. For ...
- 3,417
26
votes
Why was intuitionist logic abandoned?
Intuitionistic logic is certainly not abandoned in math. Even if most people use classical logic, there is still a large community of people who work with intuitionistic foundations, look up for ...
- 360
24
votes
Is p→p a theorem in intuitionistic logic?
Yes it is.
You cannot derive LEM from it because the so-called Material implication equivalence does not hold in Intuitionistic logic.
The first two axioms in your list are enough to derive A → A:
(1) ...
- 41.1k
20
votes
Is p→p a theorem in intuitionistic logic?
In intuitionistic logic, the statement p -> q is best read as "From a proof of p we can obtain a proof of q". Thus, p -> p is trivially true.
On the other hand, p v q can be read as &...
- 1,167
15
votes
Accepted
Is p→p a theorem in intuitionistic logic?
As other answers say, P → P is indeed provable in intuitionistic logic. But it’s worth unpicking the argument that led you to this question. Essentially you argue: we think of P → Q as equivalent to ...
- 1,096
12
votes
Do intutionists think the law of the excluded middle is universally, metaphysically false?
Intuitionists reject the LEM, but they don’t reject proof of negation. That is, if A can be demonstrated to imply an absurdity, then A is false to an intuitionist. See here https://ncatlab.org/nlab/...
- 1,756
10
votes
Accepted
Was Kant an Intuitionist about mathematical objects?
You're right to see some resonances between intuitionism and Kant. However, there's no uncontroversial sense in which you could blithely categorize Kant as an intuitionist. I'm not sure I've ever seen ...
- 2,433
10
votes
If you used intuitionistic logic in real life, would you not sound absurd?
Propositions in intuitionistic logic are probably best understood as statements about provability. P ʌ Q means that you can prove P and prove Q, ¬P means that from P you can derive a contradiction, ∃x....
- 1,304
8
votes
If you used intuitionistic logic in real life, would you not sound absurd?
You give the example:
Amy said you didn't go to school yesterday.
She lied about it though!
So you did go to school?
What makes you say that?
The issue here is that typically you ...
- 31.5k
7
votes
Why was intuitionist logic abandoned?
Artificial Intelligence is one discipline that over the last 50 years has looked for models of logic to deal with bounded rationality, and while connectionist models are all the rage and are being ...
- 35.6k
6
votes
Accepted
Why do constructive mathematicians claim that mathematical truth is temporal?
See in Enrico Martino, Intuitionistic Proof Versus Classical Truth: The Role of Brouwer’s Creative Subject in Intuitionistic Mathematics (Springer, 2018), Chapter 11 Temporal and Atemporal Truth in ...
- 41.1k
6
votes
If you used intuitionistic logic in real life, would you not sound absurd?
There are ways we could apply normal propositional logic that might seem insane. We might utter a contradiction (any contradiction), look our interlocutor squarely in the eye, and then confidently ...
- 22.6k
5
votes
What is the relationship between intuitionistic logic and 3-value logic?
A few points can be made here.
In the modern way that the Law of Excluded Middle is defined, it is a syntactic statement. It states that "φ ∨ ¬φ" is a theorem of logic. It is the Principle ...
- 31.5k
5
votes
Do intutionists think the law of the excluded middle is universally, metaphysically false?
In a nutshell, the answer to the title question is: no.
See: Luitzen Egbertus Jan Brouwer, Unreliability of the logical principles (new English transl. of the original 1908):
Now the principium ...
- 41.1k
4
votes
Accepted
What is the difference in logic between strong and weak negation?
There is a logic called bi-intuitionistic logic, which combines elements of intuitionistic and dual intuitionistic logics. It includes a strong intuitionistic implication connective and the ...
- 31.5k
4
votes
Accepted
Is there a reference list of classic tautologies that are not intuitionistic tautologies for propositional logic?
I don't know of any external, more comprehensive list, but here are some of what I'd claim the most prominent statements that are valid classically but not intuitionistically:
(¬A→⊥)→A (reductio ad ...
- 2,651
4
votes
Accepted
Theory build on the top of a Logic
The basic concept is that of Formal systems: a rigorously specified language with some (zero or more) axioms (initial formulas) and rules of inference (prescriptions how to derive new formuals from ...
- 41.1k
3
votes
What is the Normal Form of Proofs in Intuitionist Logic?
@conifolds linked answer is good. Let me provide a complementary perspective.
By the curry-howard correspondence,
a normal form is a lambda term that can no longer be reduced. if we associate lambda ...
- 3,060
3
votes
If you used intuitionistic logic in real life, would you not sound absurd?
Here's a discussion that might help:
Boss: EMPLOYEE! Did you complete that very important assignment I told you to do yesterday?
Employee: What? You didn't give me a new assignment yesterday! In ...
- 2,005
3
votes
understanding intuitionistic logic
An interesting thing to point out is that the "rules" you have correspond to what we call BHK Interpretation.
Exercice 1
The main problem is that you don't use the new meaning given to the negation ¬...
- 926
3
votes
Accepted
Does Not(A and not-A) = Not(A nand A) in intuitionistic logic?
~(A&~A) is not equal to ~(A nand A) in any logic. (A nand A) is ~(A&A) by definition, so ~(A nand A) is equivalent to ~~(A&A). Now consider the assignment of truth values, A=F. For ~(A&...
- 13.1k
3
votes
Accepted
Some questions about the material conditional and entailment in intuitionist math
There are different ways of understanding intuitionism. For Brouwer, it is a theory about mathematical reasoning that is sharply at odds with the logicism of Frege and Russell. Mathematics is not ...
- 31.5k
2
votes
Does intuitionistic negation of A mean that there does not exist a proof of A?
It is not the same. The semantics of intuitionistic logic is proof theoretic, so A → B is interpreted as "given a proof of A a proof of B can be constructed". Then A → F means a contradiction can be ...
- 44.2k
2
votes
Accepted
Is there a version of intuitionistic logic, or at least some sort of logic, where ¬¬𝘈 → 𝘈 is kept but LEM is not?
In one sense there is a straightforward answer to your question just by saying you can invent any logic you like. If you want to create a logic with ¬¬A → A as a theorem but not A ∨ ¬A then go ahead. ...
- 31.5k
2
votes
Accepted
What is the relationship between intuitionistic logic and 3-value logic?
In answer to the last question: is there any work where intuitionistic logic is used as a base for either classical logic or 3-value logic just by adding axioms or other features?
It's not in the ...
- 622
2
votes
What is ⊥ called in paraconsistent logic?
In a logic system that accepts true contradictions but not the law of noncontradiction, the symbol ⊥ (usually called "bottom" or "falsum") may represent something different than a ...
- 46
2
votes
Is there a modal modification of the law of excluded middle that may render constructive?
There are some moments in intuitionistic logic that resemble the options you've considered. Here's one from the SEP article on intuitionistic logic:
While ∀x¬¬(A(x) ∨ ¬A(x)) is a theorem of ...
- 22.6k
2
votes
Do intutionists think the law of the excluded middle is universally, metaphysically false?
In systems that do not reject the law of the excluded middle, there can be undecidable propositions, which means that the syntax is incomplete.
This is based on a very bad misconception. The ...
- 799
Only top scored, non community-wiki answers of a minimum length are eligible