Skip to main content

Questions tagged [intuitionistic-logic]

Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.

Filter by
Sorted by
Tagged with
1 vote
1 answer
65 views

How can infinitesimals be invertible in SIA?

I read that infinitesimals in SIA can be invertible: https://en.wikipedia.org/wiki/Smooth_infinitesimal_analysis In typical models of smooth infinitesimal analysis, the infinitesimals are not ...
Mike_bb's user avatar
  • 889
2 votes
1 answer
53 views

Do the monotone maps from a poset into a Heyting algebra form a Heyting algebra?

I am interested in generalizing the fact that the up-sets of a poset always form a Heyting algebra. Let $P$ be a poset and $H$ a Heyting algebra. $\operatorname{Hom}(P,H)$ can be made a bound lattice ...
user4614475's user avatar
0 votes
1 answer
47 views

How to prove $\exists x (x=a)$ in intuitionistic logic

How do you prove $\exists x (x=a)$ intuitionistically, where $a$ is a constant symbol? Classically, one has $$ [\neg\exists x (x=a)]^1\vdash \forall x (\neg x=a) \vdash\neg a = a \vdash \bot \vdash^1 \...
10012511's user avatar
  • 684
1 vote
0 answers
73 views

Does Dan Willard demonstrate that classical logics with the Law of the Excluded Middle versus those with Double Negation Elimination are distinct?

Context: Dan Willard's 2020 review paper of his work on Self-Verifying Theories/Self-Justifying Axiom Systems (SJAS) is titled "How the Law of Excluded Middle Pertains to the Second ...
jpt4's user avatar
  • 61
1 vote
0 answers
49 views

Is intuitionistic logic a subsystem of classical logic?

Joan Moschovakis' Intuitionistic Logic claims: "Although intuitionistic analysis conflicts with classical analysis, intuitionistic Heyting arithmetic is a subsystem of classical Peano arithmetic....
shea's user avatar
  • 31
5 votes
1 answer
189 views

Type theory vs "Theory On Top of Logic" mantra in Set Theories

I have a question about (especially second part of) following statement following statement from wikipedia emphasizing intrinsical feature in which type theory substantially differs from set theories: ...
user267839's user avatar
  • 7,315
2 votes
1 answer
74 views

Identity in Heyting algebras or not

In some computation over a Heyting algebra, I ended up with the following formula: $$\Big[(x\to y)\to z\Big]\to \Big[\big(x\to(y\vee z)\big)\vee \big((x\to(y\vee z))\to z\big)\Big]$$ I wonder if it is ...
Evgeny Kuznetsov's user avatar
5 votes
2 answers
123 views

Why does countability misbehave in intuitionistic logic

On page 3 of this paper https://arxiv.org/pdf/2404.01256.pdf I spotted the claim: Definitions of countability in terms of injection into ℕ misbehave intuitionistically, because a subset of a ...
Y.X.'s user avatar
  • 4,203
2 votes
1 answer
105 views

Busy Beaver function in intuitionistic ZF

Let $BB$ denote the Busy Beaver function. Constructively there is no obvious way to prove that the Busy Beaver function is total (e.g. a Turing machine may neither halt nor not halt), and I have heard ...
C7X's user avatar
  • 1,311
2 votes
0 answers
100 views

Constructive Proofs in Elementary Real Analysis

In considering the theorem cited here uniform continuity and equivalent sequences , which states that where $f:X \rightarrow \mathbb{R}$ is a function, the following two conditions are equivalent: (a) ...
Noah 's user avatar
  • 63
1 vote
1 answer
81 views

False statements in intuitionistic logic

In the explanations of intuitionistic logic I've been reading (1, 2, 3), especially in the explanation of the semantics, I don't understand how a proposition being false influences the situation. ...
bobismijnnaam's user avatar
0 votes
1 answer
46 views

Is it decidable whether a classically valid first-order formula is also intuitionistically valid?

Intuitionistic first-order predicate logic is not decidable for arbitrary formulas. However, suppose that we are given a formula of first-order predicate logic that is classically valid. Is there a ...
Adam Dingle's user avatar
1 vote
1 answer
45 views

What is the correct way to interpret the Intuitionistic rules of Kleene's sequent (Gentzen) system G1 (in sec. 77 of Kleene I.M. 1952)

I'm having difficulty understanding the sequent/Gentzen proof system in section 8 of a paper by Gurevich [G1977], and he defines that system by telling the reader to modify the system G1 from Kleene's ...
tuiowalu's user avatar
3 votes
0 answers
71 views

Can This Classical-Kleene Combination for Intuitionistic Fragment $\{ \neg, \vee, \wedge \}$ Be Extended to Include $\rightarrow$?

Over a year ago, I worked out a classical-Kleene combination logic that worked to preserve intuitionistic tautologies over the intuitionistic fragment with operators $\{ \neg, \vee, \wedge \}$, which ...
Joshua Harwood's user avatar
3 votes
1 answer
93 views

Would the Following Table Strategy Work as an Intuitionistic Decision Procedure?

I had previously sought some insight for handling logical operators in the Rieger-Nishimura lattice and, with assistance here, was able to work out a fairly rigorous way. To the best of my ability, I ...
Joshua Harwood's user avatar
2 votes
2 answers
167 views

Are There Universal Entailments Under the Rieger-Nishimura Lattice for Conditionals When the Antecedent is Higher on It?

I'm working on a bottom-up (atomics-to-proposition) intuitionistic decision procedure, and I encountered some fruits with the Rieger-Nishimura lattice. Specifically, I am looking at this article from ...
Joshua Harwood's user avatar
1 vote
2 answers
64 views

Can intuitionistic propositional logic prove that if the negations of two statements are equivalent, so are the original statements?

I know that classical propositional logic can prove the formula $(\neg P \leftrightarrow \neg Q) \rightarrow (P \leftrightarrow Q)$. But, can intuitionistic propositional logic prove it? If not, can ...
user107952's user avatar
  • 21.3k
1 vote
0 answers
171 views

“Meet” of Zorn’s Lemma and Law of Excluded Middle

Work in intuitionistic logic (IL), and assume ZF. The Axiom of Choice (AC) implies both Zorn’s Lemma (ZL) and the law of excluded middle (EM). Furthermore, AC is the “join” of ZL and EM, since we can ...
Gavin Dooley's user avatar
  • 1,122
6 votes
1 answer
307 views

Non-constructiveness and finite mathematics

It is known that the multiplicative group $(\mathbb{Z}/p\mathbb{Z})^{\times}$ is cyclic. However, known proofs are all "non-constructive" in the sense that they don't rely on a direct ...
Weier's user avatar
  • 785
4 votes
2 answers
214 views

LEM and the curry-howard correspondence

The curry-howard correspondence rests upon constructive/intuitionistic logic. Proof checkers only work because they are guaranteed to halt. Proof checkers are built on the simply typed lambda calculus ...
user avatar
1 vote
1 answer
210 views

How to prove that $\lnot(a \neq b)$ doesn't imply $a=b$ in intuitionistic logic?

I tried to prove that $\lnot(a \neq b)$ doesn't imply $a=b$ in intuitionistic logic. I used LEM for this proof: $\lnot(a \neq b)$ : $a=b$ $\lor$ $a \neq b$ Let $a=b$. Then statement $a \neq b$ is ...
Mike_bb's user avatar
  • 889
0 votes
0 answers
81 views

Is there any logic system which ENTIRELY rejects non-contradiction of any kind for any sentence (i.e. all contradictions are true)? Is this possible?

I've recently learned about paraconsistent and intuitionistic logic, and dialetheism. According to the Stanford Encyclopedia of Philosophy's page on Dialetheism, it states: Dialetheism is the view ...
setszu's user avatar
  • 101
5 votes
2 answers
210 views

Proof that LEM is equivalent to the well-ordering of $\Bbb{N}$

John L. Bell's Intuitionistic Set Theory contains an exceedingly slick demonstration that the law of excluded middle is equivalent to the well-ordering of the natural numbers $\Bbb{N} := \{ 0, 1, 2, .....
Rivers McForge's user avatar
0 votes
1 answer
68 views

Proof of contradiction vs refutation by contradiction and what is/isn't allowed in constructive logic?

Here it is stated that constructive logic allows refutation by contradiction: The proposition to be proved is ¬P. Assume P. Derive falsehood. Conclude ¬P. But not indirect proof: The ...
user avatar
2 votes
1 answer
58 views

Is Resolution Intuitionistically Valid?

Specifically, is it intuitionistically valid to deduce $Q$ from $P\vee Q$ and $\neg P\vee Q$? The proof I could come up with uses the law of exclusive middle, and I feel that you can probably come up ...
Tesla Daybreak's user avatar
0 votes
1 answer
87 views

Formalizing Real World Sentence In Intuitionistic Logic?

In my local supermarket, there is a notice with a recall, in the end it says: This warning does not imply that the damage was caused by the producer, manufacturer, importer, or distributor My first ...
fweth's user avatar
  • 3,574
2 votes
1 answer
188 views

Is the fundamental theorem of algebra true for constructive complex numbers?

I wonder whether the fundamental theorem of algebra holds in intuitionistic logic, using constructive complex numbers. (To get around the fact that in general we cannot compute the degree of a ...
Daniel Schepler's user avatar
2 votes
1 answer
115 views

What is the nature of the double negated axiom of choice?

Under what circumstances is the principle $$nnaoc : (\Pi x:A. \lnot \lnot B_x) \implies \lnot \lnot (\Pi x: A. B_x)$$ valid? So the axiom of choice, but using double negation instead of propositional ...
tailcalled's user avatar
-1 votes
1 answer
98 views

where can I read the whole proof of impossibility of proving Law of Excluded middle without proof by contradiction in Natural deduction? [duplicate]

Intuitionistic logic can't prove as many sentences as classical logic, for example: Peirce's Law; Reductio Ad Absurdum; Double Negation Elimination; and Tertium Non Datur, which are all equivalent in ...
blahblah's user avatar
  • 143
2 votes
1 answer
71 views

Find an inhabitant for type $\phi$

I am studying from Sorensen's book (Lectures on the Curry-Howard isomorphism, ed. 2006) and there is a type that is said to be inhabited, but I need to find the inhabitant. However, I can't find it. ...
Νικολέτα Σεβαστού's user avatar
0 votes
1 answer
100 views

How to prove that a formula is intuitionistically valid using Kripke semantics?

I want to know how to use Kripke semantics so that I can prove that a formula is intuitionistically valid. I think that all others cases will clear out if I understand the case of implication. Let's ...
Νικολέτα Σεβαστού's user avatar
2 votes
1 answer
83 views

Intuitionistic proof of $((p\rightarrow q)\rightarrow p)\rightarrow\neg \neg p$

I need to prove that the $\psi=((p\rightarrow q)\rightarrow p)\rightarrow\neg \neg p$ is intuitionistically valid. I tried using the topology of open sets of $\mathbb{R}$ and an arbitrary valuation, ...
Νικολέτα Σεβαστού's user avatar
0 votes
1 answer
81 views

What meta-theoretic principles are we supposed to adopt when studying formal logic/system?

Also, how do different sets of principles affect the results we can get in our meta-theory? The more concrete questions that lead me to ask the above two questions are stated below. If we are studying ...
Michael's user avatar
  • 407
2 votes
1 answer
110 views

Intuitionistic well-orderings of uncountable sets

The well-ordering principle has always been considered to be highly unconstructive, as far as I know. However, I think intuitionistic mathematics can be compatible with the existence of a well-...
Keplerto's user avatar
  • 463
1 vote
0 answers
130 views

Does Curry-Howard correspondence mean that everyone who writes a program is doing intuitionistic mathematics?

As far as I know, the first statement of the correspondence is between two formal theories named simply typed lambda calculus and intuitionistic propositional logic, which maps types to formulas and ...
Senmorta's user avatar
2 votes
3 answers
524 views

What are the examples for intuitionistic logic?

I have been curious about intuitionistic logic for some time and I want to know about it and I have a question, the law of the excluded middle and double negation elimination seem completely logical ...
user avatar
1 vote
2 answers
86 views

Well-Ordering Principle From Recursion Theorem

As far as I understand, in intuitionistic logic we have neither (i) the well-ordering principle nor (ii) the recursion theorem. But can one deduce one from the other? I believe we cannot deduce (ii) ...
fweth's user avatar
  • 3,574
2 votes
1 answer
104 views

Is there a simpler Kripke counter-model for this formula?

$\forall x \neg \neg \phi(x) \to \neg \neg \forall x \phi(x)$ is not intuititionistically valid. I can come up with a complicated Kripke counter-model as follows: Let there be a countably infinite ...
PW_246's user avatar
  • 1,338
4 votes
1 answer
428 views

doubly negated intuitionistic formulas

What is an example of some doubly negated statement in intuitionistic logic that is not equivalent to its classical version? Some background: for every statement $P$ we can find a classically ...
Keplerto's user avatar
  • 463
9 votes
3 answers
2k views

Why is the Principle of Explosion considered constructive?

I read over this post Why is the principle of explosion accepted in constructive mathematics? and still have some thoughts/questions. One of the answers mentions that a formula is constructively valid ...
PW_246's user avatar
  • 1,338
0 votes
1 answer
112 views

Would a constructive proof that intuitionstic ZF has a nonconstructive model be a problem for the intuitionist?

It is my understanding it is provable in ZFC+zero sharp that intuitionistic ZF has a nonconstructive model. (Here I am assuming the existence of zero sharp only to guarantee that ZFC has a ...
shipwaymg's user avatar
2 votes
3 answers
192 views

How to solve $(x-1)(x-2)=0$ constructively?

I want to prove that $$(x-1)(x-2)=0\Leftrightarrow x=1, 2$$ $\Leftarrow$ is easy. The problem is $\Rightarrow$. Assuming $x\neq 1, 2$, we can derive $1=0$ by dividing both sides of $(x-1)(x-2)=0$ by $...
BonBon's user avatar
  • 398
1 vote
0 answers
44 views

Strategies for proving completeness for an extension of Intuitionistic Logic

Recently I’ve been working on axiomatizing a logic that results from adding a new operator to standard Intuitionistic Logic. I use $\sim$ for standard intuitionistic negation, and $\neg$ for the new “...
PW_246's user avatar
  • 1,338
0 votes
0 answers
89 views

Reducing any formal system to intuitionistic or classical logic

Does the following provability hold in intuitionistic logic? $\vdash a_0\Rightarrow(a_1\Rightarrow(\dots\Rightarrow(a_n\Rightarrow a_k)\dots))$ for $0\leq k\leq n$ $a_0\Rightarrow (a_1\Rightarrow(\...
porton's user avatar
  • 5,103
2 votes
1 answer
82 views

Question on Intuitionistic Modal Logic

In the intuitionistic version of the modal logic K (IK), the following is a theorem: $(\Diamond p \to \Box q) \to \Box( p \to q)$. However, given the definitions for $\Box$ and $\Diamond$, I think I ...
PW_246's user avatar
  • 1,338
0 votes
0 answers
73 views

Need Help With First Order Intuitionistic Tableaux

I have a question about semantic tableaux for Intuitionistic FOL. I’ll post a sample tableaux that I’m pretty sure I’m doing wrong, and then I’ll post a sequent calculus approach to show where I get ...
PW_246's user avatar
  • 1,338
6 votes
1 answer
484 views

Is intuitionist logic two-valued?

On this page https://en.wikipedia.org/wiki/Principle_of_bivalence : Intuitionistic logic is a two-valued logic but the law of excluded middle does not hold. On this page https://en.wikipedia.org/...
Fnifni's user avatar
  • 121
9 votes
1 answer
777 views

How is the “ Axiom of choice is trivial in intuitionistic logic”?

In slide 28 of these slides, the author claims that the “Axiom of choice is trivial in intuitionistic logic” and that classical logic makes it a “ monster from outer space”. How is it trivial when it’...
Lave Cave's user avatar
  • 1,157
4 votes
1 answer
94 views

Is there a non-constructive proof-functional logic

I understand that classical logic preserves truth, is bivalent, and contains non-constructive proofs. In contrast, intuitionistic logic preserves justification/verification for a proof, is not ...
PW_246's user avatar
  • 1,338
3 votes
1 answer
123 views

Intuitionistic Logic vs Constant Domains

Quantified modal logic is a controversial field, specifically since it forces one to consider what is meant by “world” in Kripke Semantics. For example, the formula $\Box \forall x \varphi \implies \...
PW_246's user avatar
  • 1,338

1
2 3 4 5
9