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
0 answers
31 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 (y < x) \vee \neg \neg (y > 0) $. The Weak Markov's Principle (WMP) is the axiom that every ...
  • 567
1 vote
2 answers
116 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 ...
1 vote
1 answer
56 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$ ...
0 votes
1 answer
65 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 \...
  • 427
3 votes
1 answer
105 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 ...
  • 16.8k
2 votes
1 answer
83 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$....
  • 61
2 votes
0 answers
114 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 ...
10 votes
0 answers
111 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 ...
2 votes
0 answers
52 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 ...
  • 16.8k
2 votes
2 answers
40 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 ...
  • 16.8k
1 vote
1 answer
60 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 (...
1 vote
0 answers
66 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 ...
  • 427
3 votes
1 answer
55 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 ...
  • 533
1 vote
1 answer
50 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 ...
  • 16.8k
3 votes
1 answer
117 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 ...
  • 4,893
0 votes
1 answer
69 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 ...
  • 3,031
3 votes
1 answer
169 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 ...
  • 2,948
0 votes
0 answers
53 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 ...
  • 415
-3 votes
1 answer
152 views

Why do intuitionists think that proving $\neg \neg P$ merely constitutes a proof of the inexistence of a proof for $\neg P$?

In every case of $\neg \neg P$ that I've come across, the statement $\neg P$ has been disproven. Never has such a proof merely been proof for the inexistence of a proof for $\neg P$. Take the ...
0 votes
0 answers
50 views

Measure and Integration theory based on intuitionism

Measure and integration theory uses the axiom of choice extensively, for example the idea behind σ-algebra is that there are non-measurable sets (in the sense of lebesgue) like Vitali set, but on the ...
  • 123
5 votes
4 answers
273 views

What is the reasoning behind the negation definition in Intuitionistic Logic Forcing and Set Theory Forcing?

In Kunen page 96 - of 10th impression 2006: (p $\Vdash^* \neg A) \iff $ $\forall q \leq p \; \neg \; (q \Vdash^* A)$ Similarly in https://www.logicmatters.net/resources/pdfs/LogicStudyGuide.pdf on ...
user avatar
4 votes
3 answers
394 views

The simplication of left implication rule in intuitionistic sequent calculus

The original left implication rule in sequent calculus for intuitionistic logic is $$ \dfrac{\Gamma, A \supset B \vdash A \quad \Gamma,A \supset B, B \vdash C}{\Gamma, A \supset B \vdash C} $$ There ...
  • 367
0 votes
1 answer
91 views

Model theory of intuistionistic logic

The Tarskian interpretation of first order logic, $I=I_{S,\alpha}$, where $S$ is a first order structure w.r.t. the signature $\Sigma$, and $\alpha$ is a variable assignment, assign either $T$ or $F$ ...
  • 11k
4 votes
1 answer
275 views

Is there a reverse double-negation translation?

There are many double-negation translations $f$, each with the property that $\vdash\varphi$ classically iff $\vdash f(\varphi)$ intuitionistically. Is there a translation the other way? ...
  • 193
1 vote
0 answers
83 views

Do we have a translation from intuitionistic logic to classical logic which can translate all formulas with their precise meaning?(not only theorems)

I want to know if there is a translation from intuitionistic propositional logic formulas to classical propositional logic formulas satisfying the properties I'm looking for. Actually first part of my ...
4 votes
1 answer
111 views

Is (Hausdorff $\implies$ Unique Limits) intuitionistic?

It's well known that in Hausdorff topological spaces, limits of convergent sequences are unique and essentially the only proof I know (which appears very natural) is: Suppose $(x_i)$ is a convergent ...
  • 2,681
4 votes
3 answers
246 views

is proof by contradiction essential for proving the Pigeonhole Principle? [duplicate]

The standard way to prove the Pigeonhole Principle that, putting $n+1$ pigeons into $n$ pigeonholes necessitates the existence of at least one pigeonhole with at least 2 pigeons is by contradiction. ...
user avatar
1 vote
1 answer
61 views

Constructive Proof that Intuitionistic Higher-Order Logic is Conservative over Constructive First-Order Logic

In the classical setting, we know that higher-order logic is conservative over first-order logic. More precisely, consider a classical first-order many-sorted theory $T$, and consider some sentence $\...
  • 29.2k
4 votes
2 answers
183 views

Can a formula with only unique variables be an intuitionistic tautology?

Consider intuitionistic propositional formulae, using only the connective "$\rightarrow$" and absurdity . Can there exist a formula such that it is a theorem/tautology and every pair of ...
  • 533
0 votes
1 answer
77 views

Why is this infinite series _intuitionistically_ Cauchy?

I'm currently writing a short paper on Intuitionism for uni. The subject of this paper is the decay of the intermediate value theorem under intuitionism. I have found a proof for this but I have a ...
2 votes
0 answers
70 views

Examples of Intuitionistic Proof

For uni I need to write a paper and give a presentation on intuitionism, and I am looking for nice examples of theorems or other results to prove or disprove intuitionistically. One example I found ...
1 vote
2 answers
144 views

Intuitionistic logic, tree-like Kripke model

There is a tree-like Kripke model in which the set of worlds $\mathfrak{W}$ is ordered as a tree: (a) there is a smallest world $W_0$ (b) for any $W_i \ne W_0$ there is a unique preceding world $W_k: ...
  • 11
2 votes
0 answers
56 views

Is Kleene's realizability recursive?

Kleene introduced realizability as a practical semantical interpretation of Heyting Arithmetic (see link for definition). The key result he proved is that provability of $\varphi$ in HA implies the ...
  • 21
4 votes
2 answers
152 views

distribution of disjunction and conjunction over each other in intuitionistic logic

I can't find any references as to whether or not the usual properties of disjunction and conjunction distributing over each other hold in intuitionistic logic. Consider: $$(1) \ \ (p \vee (q \& r))...
0 votes
0 answers
21 views

Proof of the Local Deduction Theorem, for one of many logics

(I also asked this in MathOverflow) I'm looking for a proof of the Local Deduction Theorem for any one of many logics. That is, a proof of the statement: $\Sigma \bigcup \{\phi\} \models \psi$ iff for ...
  • 149
0 votes
1 answer
27 views

An exercise in fuzzy logics built from a t-norm

(I also asked this in MathOverflow) Consider the following t-norm: $ a * b = \begin{cases} \text{$2ab,$} &\quad\text{if $a, b$}\le1/2\\ \text{$min\{a, b\}$} &\quad\text{...
  • 149
0 votes
2 answers
107 views

Intuitionistic logic: double negation and LOEM removed?

Why are double negation and the law of excluded middle excluded from the theory vs one of classical logic? I see that the law of the excluded middle $\lnot(p \land \lnot p)$ requires double negation ...
  • 1,021
0 votes
0 answers
33 views

What Are the Smallest Totally Ordered Set and the Conditional Valuation Rule Needed for Intuitionistic Countermodels for Propositions in IPC?

According to the Wikipedia article on Heyting algebras: Every totally ordered set that has a least element 0 and a greatest element 1 is a Heyting algebra (if viewed as a lattice). In this case p→q ...
0 votes
0 answers
30 views

Filter on Heyting algebra

Consider the first order intuitionistic logic. Let $H$ be an Heyting algebra, let $F$ be a filter on $H$ and let $V:\text{Frm} \rightarrow H$ be an evaluation function. Suppose that $b \rightarrow V^{[...
  • 165
3 votes
1 answer
64 views

Is a Hetying algebra with coexponetials Boolean?

Suppose we have a Heyting algebra $\mathcal A$ with coexponentials. Specifically, for every $a, b : \mathcal A$ we have an object $b \backslash a$ with the properties that $b \le a \lor (b \backslash ...
  • 2,165
0 votes
1 answer
61 views

$ \bigcap _{i \in I} (A\cup S_i) \subset A\cup \bigcap _{i \in I} S_i $ on the intutionistic logic

I want to prove below for nonempty I on the intuitionistic logic. $$ \bigcap_{i\in I} (A\cup S_i) \subset A \cup\bigcap_{i \in I} S_i $$ This is equivalent to next. $$ (\forall x)(\phi\lor\psi_x)\...
  • 51
1 vote
1 answer
76 views

Help calculating relative pseudo-complements in a Heyting algebra/lattice

I'm trying to work some examples of relative pseudo-complements in lattices, to make sure I understand them. I wonder if anybody could check my examples, and tell me if I'm correct or if I've ...
5 votes
1 answer
245 views

Existence elimination in Lean 3

Lean 3 is a theorem prover that implements the calculus of inductive constructions. Differently than Coq, Lean 3s kernel works proof irrelevant. This means that in the kernel of Lean all proofs of the ...
  • 3,031
1 vote
0 answers
53 views

Prove that propositional Aczel slash is closed under deduction

I have already proved that $ \Gamma |\phi \Rightarrow \Gamma \vdash_{IPC} \phi $. On the other hand, I have tried to prove the other side. I used induction on the length of the proof.(I used natural ...
1 vote
0 answers
56 views

Strange pattern in numbers why is the series of absolute differences always 0? [duplicate]

Put any four numbers in a row, say, 77 73 29 179. Under the first number write the difference between it and the second number. Under the second number put the difference ...
3 votes
1 answer
76 views

Upper bound for size of topology needed to falsify a non-tautology in IPC

I was attempting to answer this question with an algorithm based on an answer I gave as an exercise posed by Z.A.K here. I think it is easy to show the decidability of IPC by converting to S4 and then ...
  • 9,246
13 votes
3 answers
1k views

Can we make intuitionistic logic "intuitive"?

This is something I am wondering about, because all the formulations I've seen of the logic seem fairly difficult to grasp, e.g. lists of abstract axioms that have a few missing versus classical logic....
4 votes
0 answers
87 views

Prove in $NI$ that $\neg\neg\exists x\forall y[P(y) \to P(x)]$

I have been tasked to prove a slightly different version of the Drinker's paradox: $\vdash_{NI} \neg\neg\exists x\forall y[P(y) \to P(x)]$ Where ${NI}$ stands for natural deduction in intuitionistic ...
  • 180
6 votes
2 answers
195 views

Is there a decision procedure for *monadic* intuitionist first-order logic?

In Ch. 19 of the 4th edition of Methods of Logic, Quine gives a decision procedure for classical monadic first order logic (technically it's a decision procedure for what he calls "Boolean ...
1 vote
1 answer
80 views

What does this typed lambda-calculus notation mean?

In Definition 3.2 (page 12) of Gallier's 'Constructive Logics Part I: A Tutorial on Proof Systems and Typed Lambda-Calculi' he sets out the rules for his typed $\lambda^{\to, +, \times, \perp}$-...

1
2 3 4 5
8