Questions tagged [intuitionistic-logic]
Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.
341
questions
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: ...
- 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 ...
- 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))...
- 473
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 ...
- 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{...
- 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 ...
- 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 ...
- 103
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^{[...
- 65
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 ...
- 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)\...
- 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 ...
- 73
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 ...
- 323
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 ...
- 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 ...
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 ...
- 73
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 ...
- 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....
- 17.8k
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 ...
- 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 ...
- 63
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}$-...
- 876
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 ...
- 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....
- 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 ...
- 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:
...
- 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 ...
- 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&...
- 536
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, ...
- 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 ...
- 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.
- 445
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,...
- 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 ...
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 ...
- 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 ...
- 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 ...
- 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 ...
- 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 ...
- 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 ...
- 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 ...
- 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.
- 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:
&...
- 143
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 ...
- 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 ...
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 ...
- 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 ...
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 ...
- 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 ...
- 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....
- 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 ...
- 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 ...
- 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?
- 17