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
0
votes
0answers
10 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 ...
3
votes
2answers
102 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 ...
0
votes
0answers
44 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....
0
votes
1answer
104 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 ...
2
votes
0answers
48 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 ...
0
votes
2answers
76 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?
2
votes
0answers
79 views

What does the principle of implosion imply from a truth-value gap?

The principle of implosion (verum ex quodlibet) states that a valid formula follows from anything. It is expressed: B ⊨ A ∨ ¬A Consider some paracomplete or intuitionistic logic in which the law of ...
0
votes
1answer
69 views

$\mathrm{int}( \mathrm{c\ell}(U)) = U$ implies every open set is closed

Can someone provide a proof or counterexample to the following conjecture? Conjecture: if $X$ is a topological space such that every open set $U \subseteq X$ satisfies $\mathrm{int}( \mathrm{c\ell}(U))...
3
votes
2answers
65 views

Is $(p \to q) \to (\neg q \to \neg p)$ a theorem in (Johansson's) minimal logic?

From a related question we know that $(P\to Q)\to (\neg Q \to \neg P)$ is a theorem in intuitionistic logic. I'm asking if that's also true for the positive fragment of intuitionistic logic aka ...
2
votes
2answers
102 views

Can a set have a complement in intuitionistic ZF?

Does IZF (ZF formulated in intuitionistic logic) prove that for any set $a$, $\{x: x \notin a \}$ does not exist?
0
votes
1answer
91 views

Gentzen Style Intuitionistic Sequent Proofs

I am trying to provide intuitionistic sequent proofs (Gentzen Style) for a few statements. The rules that I have are the rule of assumption, conjunction introduction and elimination, disjunction ...
6
votes
1answer
51 views

Truncation and fixed finite domain

Let $P$ be a type, $||P||$ denotes a mere proposition obtained by truncating $P$. Let $D$ be a type and $A:D\rightarrow\textsf{U}$, then $\Pi x:D.A(x)$ is a well-formed type. Assuming that we are ...
2
votes
0answers
71 views

Why do intuitionistic connectives preserve open sets in the topological interpretation of IPC?

Is there a deeper significance to the fact that the topological intepretation of the connectives of intuitionistic propositional calculus sends open sets to open sets? Let $(\varphi)^*$ refer to the ...
0
votes
1answer
69 views

Prove double negation of LEM in intuitionistic logic

I understand that in intuitionistic logic, the law of excluded middle $P \lor \lnot P$ and double negation elimination $\lnot \lnot P \to P$ are not true in general (for every proposition $P$). ...
0
votes
2answers
74 views

Is $\lnot\lnot\forall x(A(x)\vee\neg A(x))$ a theorem of intuitionistic logic?

I have a short question. I know that $\neg\neg(A\vee\neg A)$ is a theorem of intuitionistic logic. What about $\neg\neg\forall x(A(x)\vee\neg A(x))$?
6
votes
0answers
51 views

Disjoint union types in MLTT

In MLTT, by identifying propositions as types (and vice versa), a proposition carries the information regarding how a proof of the proposition is constructed. My question is related to this. Let $P:\...
0
votes
0answers
39 views

Showing every state in an intuitionistic model verifies ¬¬p → p

I'm working on a question in the field of intuitionistic logic: In an intuitionistic model, assume p ∨ ¬p is verified at the root state. Give a brief argument showing that every state in the model ...
1
vote
1answer
68 views

In homotopy type theory, prove that law of excluded middle implies reduction ad absurdum

It's about Excercise 2 from here: While the principle of excluded middle $P\vee\neg P$ ( tertium non datur) is not provable, prove its double negation using the propositions as types translation: $\...
2
votes
1answer
69 views

How to show that a valid rule is not derivable in intuitionistic propositional calculus.

First a word on notation, let the following be an inference rule that takes $\Gamma$ (a set of well-formed formulas) as premises and has $\psi$ (a well-formed formula) as a conclusion. This is ...
9
votes
1answer
108 views

A question about impredicative type theory

I am playing with impredicative type theories (CC and UTT). I am not quite familiar with the distinction between $\textsf{Prop}$ and $\textsf{Type}$ as it is not available in MLTT. Here is my question....
7
votes
1answer
87 views

Universal Quantifier $\forall$ and Generalized Conjunction $\bigwedge$ in intuitionistic logic

I have a question about $\forall xA(x)$ and $\bigwedge\! A(a_i)$ (= $A(a_1)\wedge...\wedge A(a_n)$). In classical logic, the universal statement $\forall xA(x)$ can be understood as a generalized ...
3
votes
1answer
93 views

Context in context of Type Theory

I am reading a book on homotopy type theory or let me better say 'the' book of HoTT. On page 416, the author intruduces a judgment that includes the ctx (context) formalism. The judgment $$(x_1 : ...
2
votes
5answers
213 views

ex falso quodlibet in natural deduction (ND)?

My understanding of inference rules is that they should be intuitively acceptable (like axioms). But my only intuition for ex falso quodlibet in natural deduction is not immediate but comes from its ...
3
votes
2answers
104 views

In what sense does Homotopy type theory “model types as spaces”

I've read at multiple points (e.g. here) that homotopy type theory "models" types as spaces. I can understand informally that we can "think of" types as spaces, in a vague sense. ...
2
votes
2answers
119 views

In Homotopy Type Theory, how do the continuous notions of spaces and paths, match the discrete notions of constructible terms and proofs?

Context: I'm starting with being interested in type theory as a framework within which to do mathematics (e.g. practically, using proof assistants based on type theory), and my understanding is that ...
6
votes
1answer
59 views

A question about intuitionistic logic

I find it hard to understand the following formula in intuitionistic logic, where $P\neq\perp$ and $P\not\leftrightarrow(\neg\neg\exists xQ(x)\rightarrow\exists xQ(x))$: $$P\rightarrow(\neg\neg\exists ...
6
votes
1answer
81 views

$A\rightarrow(\neg\neg B\rightarrow B)$ in intuitionistic logic

I have a basic question about intuitionistic logic. Here are two propositions in intuitionistic logic, where $B$ is not $\neg\neg$-stable (that is, it is not the case that $\neg\neg B\rightarrow B$): $...
5
votes
2answers
91 views

Converse of $(A\rightarrow B)\rightarrow((B\rightarrow C)\rightarrow(A\rightarrow C))$

I have a basic question about the following proposition. $(A\rightarrow B)\rightarrow((B\rightarrow C)\rightarrow(A\rightarrow C))$ I can prove it in intuitionistic logic. But I wonder if we have the ...
3
votes
1answer
83 views

Is the existential quantifier commutative in intuitionistic higher order logic?

In higher order logic, one sometimes defines the existential quantifier by $$(\exists x. \phi(x)) := (\forall \rho.(\forall x.\phi(x)\to\rho)\to\rho).$$ I am having trouble proving that $$(\exists x.\...
0
votes
1answer
152 views

Does there exist a topos with these $n+2$ truth values?

This question is based on the answers to this question. The Question: Let $n\in\Bbb N$. Let $N$ be a set with $n+2$ elements, labelled $0$ to $n$, and the $(n+2)$th element labelled $\infty$. Suppose ...
1
vote
1answer
83 views

What is the intuitionist / contructivist view of the Fermat theorem proof?

Since Wiles proof is in essence proof by contradiction, it relies on the law of excluded middle. Which as I understand intuitionists / constructivists do not accept as an axiom. So what is their view ...
0
votes
0answers
49 views

$(A \to B) \to (\lnot A \lor B)$ intutionistically valid?

Can anybody explain if the formula $(A \to B) \to (\lnot A \lor B)$ is intuitionistically valid? If I understood the logic right, it is not but I am not sure, because a am not able to provide a ...
6
votes
1answer
199 views

How Do Heyting Algebras Relate To Logic?

My question is, broadly speaking, how are Heyting algebras related to logic ? It would be great if someone could answer this question without being too technical (or point to easy to read literature). ...
8
votes
1answer
134 views

Independence of connectives in intuitionistic logic

Consider the intuitionistic propositional logic with $\neg, \vee, \land, \to$ as primitive connectives. My question is, can any three of these connectives be used to define the remaining one? So, I am ...
4
votes
1answer
103 views

In intuitionistic first-order logic, can the “nothing” quantifier define either of the universal or existential quantifiers?

In classical first-order logic, the nothing quantifier $Nx$, which means "there are no x such that", can define both the universal and existential quantifiers. I suspect this is not the case ...
1
vote
1answer
61 views

Type Theory Rules For The Empty Type

I would like some help choosing the rules for the empty type. I am trying to setup a typed lambda calculus with sums like in Extensional Normalisation and Type-Directed Partial Evaluation for Typed ...
2
votes
0answers
70 views

Literature On Simple Type Theory

I am wondering where I can find literature describing the rules for a simple type theory with just products, sums, function types, unit and the empty type. Robert Harper describes such a theory 3 ...
2
votes
1answer
56 views

Does $\forall x (\phi(x) \vee \neg \phi(x))$ imply (2) $\forall x \phi (x) \vee \neg \forall x \phi(x)$ in intuitionistic logic?

Does (1) $\forall x (\phi(x) \vee \neg \phi(x))$ imply (2) $\forall x \phi (x) \vee \neg \forall x \phi(x)$ in intuitionistic logic? It seems to me that it does not, and my heuristic is this: (1) &...
2
votes
0answers
53 views

Defining function by overlapping cases in constructive logic

Is it possible to define a function by cases in intuitionistic logic where the cases possibly overlap and the function values disagree in the overlapping area? In particular, if I am working with real ...
2
votes
1answer
56 views

Identity and substitution in Intuitionistic Logic

I am a beginner in mathematical logic. I have a basic question about identity propositions in intuitionistic logic. For example, from $(*)$ and $(**)$: $$\Gamma\vdash a=b\quad\quad(*)\quad\quad\quad\...
4
votes
0answers
45 views

Is there an intuitionistic proof of “it is impossible to simulate a die with a guaranteed to terminate process involving coin flips”?

Recently, I happened to be thinking again about the question: "Is it possible to simulate a fair six-sided die using only fair coin flips?" One type of answer which tends to be given is ...
4
votes
1answer
115 views

Type theory and constructivist mathematics with paraconsistent logic?

Type theory, together with the Curry-Howard correspondence is a formal system for stating formal proofs of intuitionistic logic, which is used in constructive mathematics. Intuitionistic logic differs ...
0
votes
2answers
66 views

Intuitionistic “atomic” proof of negation?

In the view of logic in terms of type theory (cf. the Curry-Howard correspondence), the type $\neg P$ is defined as $P\to False$, and a proof of $\neg P$ is therefore a function that takes a proof of $...
2
votes
2answers
68 views

How does the “proofs as programs” correspondence work for equality?

The equality relation $=$ can be represented as a type, just as any other propostion in the Curry-Howard correspondence. I understand the sense in which the basic logical symbols $\land,\lor,\to, \...
2
votes
1answer
95 views

Strongly constructive proofs: Proofs that don't make use of decidability?

I was thinking about counting argumens from the perspective of constructivist / intuitionistic logic: A typical counting argument might have the following pattern: Suppose we have a finite set $S$ ...
1
vote
0answers
77 views

A proof step involving the law of the excluded middle

In the answer provided to the question https://mathoverflow.net/questions/296440/modal-collapse-upon-addition-of-the-law-of-the-excluded-middle-to-an-intuitionis, a proof is given, showing that a ...
1
vote
1answer
62 views

Confusion with Brouwer's Counterexample for Points on a Continuum Being Ordered

I'm reading about intuitionism, and I've come across an argument put forth by L. E. J. Brouwer that claims to be a counterexample to the statement that $\mbox{The points of the continuum form an ...
2
votes
0answers
35 views

Is Smetanich's logic the second from the top in the lattice of intermediate logics?

Consider the lattice of consistent superintuitionistic logics, also known as intermediate logics. Smetanich's logic is the logic obtained from intuitionistic logic by adding the axiom $((\neg q \...
5
votes
1answer
86 views

Logic of the even weaker excluded middle

There exists a superintuitionistic propositional logic where $\neg p \vee \neg \neg p$ is a theorem, but $p \vee \neg p$ is not a theorem. It is called the logic of the weak excluded middle. That ...
3
votes
0answers
83 views

Category of presheaves and logic

Let ${\bf C}$ be a small category. As is well known, the category of presheaves ${\bf Set^C}$ is cartesian closed: it can be a model of intuitionistic propositional logic. Can it also be a model of ...

1
2 3 4 5 6