Questions tagged [intuitionistic-logic]
Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.
297
questions
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 ...
