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
97 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 ...
Yeshe Tenley's user avatar
1 vote
0 answers
102 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
  • 527
0 votes
0 answers
49 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
130 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
29 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 ...
Yeshe Tenley's user avatar
2 votes
1 answer
49 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
86 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,522
1 vote
0 answers
107 views

Has this logic already been studied?

I have been spending the better part of a year thinking about the subtleties involved in balancing natural language intuitions for logic with the power and efficacy that Classical Logic and ...
PW_246's user avatar
  • 991
2 votes
1 answer
120 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
1 vote
1 answer
96 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
83 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
  • 133
2 votes
1 answer
51 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
72 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
67 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
67 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
100 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
  • 343
1 vote
0 answers
117 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
398 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 ...
Just a homo sapiens's user avatar
1 vote
2 answers
63 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,522
1 vote
1 answer
83 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
  • 991
4 votes
1 answer
403 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
  • 343
7 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
  • 991
0 votes
1 answer
102 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
187 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
  • 369
1 vote
0 answers
43 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
  • 991
0 votes
0 answers
85 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
  • 4,961
2 votes
1 answer
80 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
  • 991
0 votes
0 answers
70 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
  • 991
6 votes
1 answer
412 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
  • 111
9 votes
1 answer
668 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,119
4 votes
1 answer
90 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
  • 991
3 votes
1 answer
108 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
  • 991
2 votes
2 answers
179 views

Is there a sheaf model where the Weak Markov's principle fails?

We define a real number $x$ to be pseudopositive if $\forall y \in \mathbb{R}$ we have $ \neg \neg (x > y) \vee \neg \neg (y > 0) $. The Weak Markov's Principle (WMP) is the axiom that every ...
saolof's user avatar
  • 639
1 vote
2 answers
144 views

In what sense are proofs that rely on the Law of the Excluded Middle really proofs?

As a non-mathematician, it seems to me that the Law of Excluded Middle is merely an axiom when it comes to proofs that employ it. Can we really rely on such proofs? In what sense are they valid? EDIT ...
chasly - supports Monica's user avatar
2 votes
1 answer
75 views

In intuitionistic FOL, does $\forall x \forall y (P(x) \lor Q(y))$ imply $(\forall x, P(x)) \lor (\forall y, Q(y))$?

Of course, in classical logic, if you have $\forall x \forall y (P(x) \lor Q(y))$, then you can conclude $(\forall x, P(x)) \lor (\forall y, Q(y))$: if you didn't have that, then there would be $x$ ...
Daniel Schepler's user avatar
0 votes
1 answer
101 views

Question about an extension of Intuitionistic Logic

Kurt Gödel introduced a mapping from Intuitionism to Classical S4 Modal Logic as follows: $A’=\Box A$ where $A$ is a positive atomic formula. $(\sim A)’=\Box \sim (A’)$ $(A \land B)’=A’ \land B’$ $(A \...
PW_246's user avatar
  • 991
3 votes
1 answer
123 views

What subclass of topological spaces validate the theorems of classical logic?

I know that there is a topological semantics for intuitionistic logic. But that raises the question, precisely what subclass of topological spaces corresponds to classical logic? Basically, I am ...
user107952's user avatar
  • 19.2k
2 votes
1 answer
132 views

Completeness of intuitionistic propositional logic

I want to study the semantics of intuitionistic propositional logic. Fix a topological space $X$, let $\Gamma\models^X A$ denote that $A$ is valid under $\Gamma$ in the algebra of all open sets of $X$....
wxkj99's user avatar
  • 61
2 votes
0 answers
117 views

Does "Every set of $\mathbb{R}$ is Lebesgue measurable" imply some weakened LEM?

I would like to know if the Reverse Mathematics has a conclusion for this axiom ($\text{LM}$:Every set of $\mathbb{R}$ is Lebesgue measurable). I have tried to translate this axiom into a halting ...
Ember Edison's user avatar
13 votes
0 answers
127 views

Is it known whether there are atoms in the complete lattice of intermediate logics?

By "intermediate logic" I mean a (non-trivial) propositional logic at least as strong as intuitionistic logic whose set of theorems is closed under modus ponens and closed under substitution ...
RichardBerry's user avatar
2 votes
0 answers
67 views

What if the metatheory is itself intuitionistic?

Usually, even in intuitionistic logic, the metatheory is classical. That is, to give just one example, either something is a theorem of intuitionistic logic, or it is not. That is an example of a ...
user107952's user avatar
  • 19.2k
2 votes
2 answers
52 views

Is this formula provable in intuitionistic first-order logic?

I know that in classical first-order logic, the formula $(\exists x)( \exists y) x \neq y \rightarrow (\forall x)(\exists y) x \neq y$ is a theorem. Is it also a theorem of intuitionistic first-order ...
user107952's user avatar
  • 19.2k
1 vote
1 answer
76 views

How many fragments of second-order (classical/intuitionistic) logic are there using only $\exists$/$\forall$?

Question: How many fragments of second-order (classical/intuitionistic) logic are there using only the quantifiers $\exists$/$\forall$? Specifically only those "fragments of second order (...
hasManyStupidQuestions's user avatar
1 vote
0 answers
86 views

Question on the translation from Intuitionism to S4 Modal Logic

Below is the standard translation from Intuitionistic Propositional Logic to Classical S4 Modal Logic: P:▢P PvQ:PvQ P&Q:P&Q ~P:▢~P P->Q:▢(P->Q). My question is thus: if the semantics for ...
PW_246's user avatar
  • 991
3 votes
1 answer
77 views

Using Heyting algebras outside of Intuitionistic Propositional Calculus.

I am looking for examples of proofs or constructions that rely on a Heyting algebra. Furthermore, said examples must use the fact that Heyting algebras can be considered semantics for IPC, but be ...
Jason's user avatar
  • 655
1 vote
1 answer
82 views

How to prove rigorously that neither the universal nor the existential quantifier can define the other in intuitionistic logic?

I know that in classical first-order logic, each of the universal and existential quantifier can be used to define the other, and I suspect that in intuitionistic first-order logic, neither can define ...
user107952's user avatar
  • 19.2k
3 votes
1 answer
164 views

Does the intuitionistic logic contain classical (in a sense)?

Is it true that for every finite set of axioms $a_0$, ..., $a_n$, if a statement $t$ follows from these axioms in the classical first-order predicate logic, then in intuitionistic first-order ...
porton's user avatar
  • 4,961
0 votes
1 answer
95 views

is the NNO in a sheaf topos a model of classical PA?

In their book Models for Smooth Infinitesimal Analysis Moerdijk and Reyes claim that the natural number object in any Grothendieck topos is a model of all classical provable statements of first order ...
Nico's user avatar
  • 3,998
3 votes
1 answer
217 views

Curry-Howard Isomorphism For Classical Logic

I wonder if there is some direct proof of how $\lambda$-$\mu$-calculus maps to classical logic via the Curry-Howard correspondence. Just like one can verify a valid sentence in propositional logic by ...
fweth's user avatar
  • 3,522
0 votes
0 answers
64 views

How to efficiently enumerate all valid propositional formulas from implicational fragment of intuitionistic logic?

A set of valid Propositional logic formulas is decidable. A set of implicational propositional formulas is a subset of this set. If we limit Axiom schemas by removing Axiom schema 3 (Peirce's law) we ...
Oleg Dats's user avatar
  • 415

1
2 3 4 5
9