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
2 answers
46 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: ...
user avatar
  • 11
1 vote
0 answers
35 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 ...
user avatar
  • 11
4 votes
2 answers
53 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))...
user avatar
0 votes
0 answers
19 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 ...
user avatar
  • 149
0 votes
1 answer
24 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{...
user avatar
  • 149
0 votes
2 answers
80 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 ...
user avatar
  • 939
0 votes
0 answers
32 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 ...
user avatar
0 votes
0 answers
22 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^{[...
user avatar
2 votes
1 answer
44 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 ...
user avatar
  • 2,105
0 votes
1 answer
57 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)\...
user avatar
  • 41
0 votes
1 answer
39 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 ...
user avatar
0 votes
0 answers
30 views

Help requested for understanding the proof that every Hintikka collection has a model.

I am working my way through https://www.researchgate.net/publication/243704264_Intuitionistic_Logic_Model_Theory_and_Forcing but am stuck on the assertion on page 21 that every Hintikka collection in ...
user avatar
4 votes
1 answer
98 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 ...
user avatar
  • 1,368
1 vote
0 answers
44 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 ...
user avatar
1 vote
0 answers
55 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 ...
user avatar
3 votes
1 answer
64 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 ...
user avatar
  • 6,496
12 votes
3 answers
927 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....
user avatar
4 votes
0 answers
79 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 ...
user avatar
  • 168
6 votes
2 answers
149 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 ...
user avatar
1 vote
1 answer
67 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}$-...
user avatar
1 vote
0 answers
37 views

Four propositions with certain properties

I am following a course in intuitionistic mathematics and I have been given an exercise about intuitionistic propositional logic. The problem Find four propositions $X_0, X_1, X_2, X_3$, such that ...
user avatar
  • 168
2 votes
0 answers
116 views

Learning roadmap for constructive mathematics

I just watched the talk "five stages of accepting constructive mathematics". I am very interested to learn constructive mathematics but have zero knowledge of constructive mathewmatics/logic....
user avatar
  • 19.3k
7 votes
3 answers
653 views

Looking for a simple proof of the independence of the law of excluded middle

I have seen a number of excellent posts on the difference between intuitionist propositional logic (IPL) and classical propositional logic (CPL), all of which state that IPL is agnostic on the law of ...
user avatar
  • 295
6 votes
1 answer
110 views

Arithmetic in intuitionistic logic

In the book The Foundations of Intuitionistic Mathematis by Kleene and Vesley, one finds a proof of the following sequent: $\vdash \forall p A(x_1+p) \& x_1 \leq x \supset \forall p A(x+p)$ where: ...
user avatar
  • 71
1 vote
0 answers
61 views

¬(A∨¬A)⊢¬B in paracomplete systems

I am considering a paracomplete logic where the principle ¬(A∨¬A)⊢¬B holds. What does it take for the principle to be explosive, such that we can infer any ¬B? If we have some statement that is ...
user avatar
  • 31
2 votes
0 answers
54 views

Reference to know the history of Superintuitionistic (intermediate) logics

There is any source in books or in the web about the history of development of the study of Superintuitionistic logics? By this concept I refer the wikipedia article called "Intermediate logic&...
user avatar
2 votes
1 answer
82 views

How to understand the Definitions of existential and disjunction of intuitionistic logic.

In the testbook I have learnt that with the natural deduction rules: $ A \lor B \to (A \to C) \to (B \to C) \to C$ $\exists x A \to \forall x ( A \to B) \to B$ after put $\bot$ into C, B respectively, ...
user avatar
  • 21
0 votes
1 answer
125 views

Is the Godel sentence considered true intuitionistically?

In classical logic, Godel shows that there are true statements undecidable for arithmetic, and consequently, that truth goes beyond a system of axioms ability for proof. My question is, given that ...
user avatar
  • 77
0 votes
1 answer
76 views

Question on Heyting algebras

Does $a \Rightarrow b = 1$ iff $a≤b$ hold for any complete Heyting algebra? If not, please provide a counterexample.
user avatar
4 votes
1 answer
136 views

How do you extend the topological semantics for intuitionistic propositional logic (IPC) to a semantics for intuitionistic first order logic (IFOL)?

How do you extend the topological semantics for intuitionistic propositional logic (IPC) to a semantics for intuitionistic first order logic (IFOL)? I tried the simplest thing that could possibly work,...
user avatar
  • 6,496
1 vote
1 answer
76 views

How does this formula $A\lor (A\to B)$ relate to intuitionistic logic?

It is my first approach to the proof theory of intuitionistic logic and I am considering a single-conclusioned Gentzen-style sequent calculus for it, namely $\bf G3i$ (Negri, Von Plato, Structural ...
user avatar
0 votes
1 answer
89 views

In homotopy type theory, what is this "mechanical way to create a new expression F' now depending on t' and an equivalence between F(T) and F'(T')"? [closed]

I've read a few slides on the topic citing the following quotation from an email, which, according to these slides, defines the biggest advantage of homotopy lambda calculus over other caculi of ...
user avatar
  • 109
3 votes
1 answer
88 views

Exercise verification: No topology over a finite set generates as a set of theorems precisely the intuitionistic tautologies.

This answer to this question I asked yesterday contains the following exercise (emphasis mine): Let $Σ$ denote the underlying set of the Sierpiński space. Are the propositional formulae $φ$ for which ...
user avatar
  • 6,496
3 votes
1 answer
76 views

Does the class of all topologies work as a semantics for IPC?

In this answer to this question I asked recently, the answerer said that the tautologies in the Sierpiński space are a proper superset of the intuitionistic tautologies. I'm wondering what I get when ...
user avatar
  • 6,496
1 vote
0 answers
60 views

A finite axiomatization for intuitionistic implicational logic.

I know that someone once gave a finite axiomatization for tautologies of classical propositional logic whose only connective is implication, but is there a finite axiomatization for tautologies of ...
user avatar
  • 13.3k
1 vote
0 answers
80 views

If $A \to 1$ is an epimorphism in a well-pointed topos, does $A$ have a global element?

In a well-pointed topos, it is simple to show that $A$ is an initial object if, and only if, there are no global elements $1 \to A$. Now suppose that $A \to 1$ is an epimorphism. Then $A$ cannot be an ...
user avatar
  • 19.5k
-1 votes
3 answers
84 views

$(p\rightarrow q)\vee (q\rightarrow r)$ imply peirce's law in intuitionistic logic? [closed]

Consider the system of intuitionistic implicational logic together with the axiom schema adding all instances of $$(p\rightarrow q)\vee(q\rightarrow r)$$ Does that make Peirce's law true? I have ...
user avatar
  • 41
-1 votes
1 answer
72 views

Are below sentences held in intuitionistic logic? [closed]

$(p \to (q \to r)) \to ((p \to r) \lor (q \to r))$ $(p \to (q \lor r)) \to ((p \to q) \lor (p \to r))$ are holded in intuitionistic logics? I could not found the model of intuitional logic that aboves ...
user avatar
  • 41
4 votes
1 answer
94 views

Is the formula $\neg\neg\forall x (\neg P(x) \,\vee\, \neg\neg P(x))$ provable in intuitionistic logic?

I understand that in propositional logic, $\neg\neg Q$ is intuitionistically provable whenever $Q$ is classically provable, but here there is a universal quantifier complicating things.
user avatar
  • 829
3 votes
1 answer
154 views

Is modal logic S4 translatable into intuitionistic logic? If not, what modal system is?

I have some questions about the translation of modal logic S4 into intuitionistic propositional logic (IPC). Famously, Gödel–McKinsey–Tarski found that the reverse is possible and it is said that: &...
user avatar
4 votes
0 answers
111 views

Is it not wrong that intuitionistic logic is hard to convey?

As someone who is now mostly working in constructive / intuitionistic logic ($\mathsf{IL}$) I am still wondering about the most concise way to spotlight the relevance to people who so far only know ...
user avatar
  • 2,738
2 votes
1 answer
69 views

Is there intuitionistic proof that $B \setminus (B \setminus A) = A$ for any sets $A \subseteq B$?

Let $A$ and $B$ be sets such that $A \subseteq B$. I am trying to investigate whether $A = B \setminus (B \setminus A)$. I am attempting to prove this by showing $(\forall x)[x \in A \Leftrightarrow x ...
user avatar
2 votes
1 answer
75 views

Superintuitionistic logics weaker then classical logic

I want to construct an example of a superintuitionistic logic which is a strict superset of $\operatorname{Int}$ and a strict subset of $\operatorname{Cl}$. I think that such logic can be obtained by ...
user avatar
  • 1,071
4 votes
2 answers
177 views

Constructive proof that any two natural numbers are either equal or not equal

I've been reading a bit about constructive mathematics and one of the first challenges I've found is to prove that any two natural numbers are either equal or not equal assuming only intuitionistic ...
user avatar
1 vote
0 answers
36 views

Modal Heyting Algebras

Is there a standard way to add modal operators over a Heyting algebra -- as it was done e.g. by Johnstone and Tarski for Boolean algebras? Does this provide a semantics to some version of ...
user avatar
  • 194
3 votes
1 answer
141 views

There does not exist an even prime greater than two: is there an intuitionistic proof?

My own feeble understanding of intuitionism is that it is constructive and that, by not accepting the law of excluded middle, proofs by contradiction are eschewed. For my background on the topic, see ...
user avatar
  • 38.1k
0 votes
0 answers
84 views

What is the algorithm for automated theorem proving in intuitionistic propositional logic?

In classical logic exists law of excluded middle: (a or not a). We can append not a to the knowledge base and show contradiction....
user avatar
  • 387
0 votes
1 answer
143 views

Can a proposition be false and its negation be false in Intuitionistic logic?

The principle of non-contradiction say that p and $\neg$ p can not be both true. If you consider the law of excluded middle as relevant, then either p or $\neg$ p is true, and thus the other is false ...
user avatar
  • 229
2 votes
0 answers
52 views

Equivalence of the Classical and Approximate Intermediate Value Theorems in Classical Logic

IVT (Classical) Let $f:\left[a,b\right]\to\mathbb{R}$ be continuous. If $f\left(a\right)<0$ and $f\left(b\right)>0$, then there exists $c\in\left(a,b\right)$ such that $f\left(c\right)=0$. In ...
user avatar
  • 1,853
0 votes
2 answers
91 views

How to prove that $\vdash \neg \neg (p \vee \neg p)$? (Natural Deduction) [closed]

I do know that double negation and LEM are equivalent, but can we prove $$\vdash \neg \neg (p \vee \neg p)$$ without using either of them, in a Fitch-style proof?
user avatar
  • 17

1
2 3 4 5
7