Questions tagged [intuitionistic-logic]
Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.
1
vote
0answers
21 views
Is intuitionistic first-order logic with no function or relation symbols decidable?
Classical first-order logic with no function or relation symbols is decidable. If I'm not mistaken, this is essentially because any formula (with possible free variables) has truth value uniquely ...
3
votes
1answer
46 views
Constructivist proofs + LEM = classical math?
I have been told that constructivist/intuitionist logic is classical logic - LEM.
I see why LEM doesn't hold given the basic philosophy of constructivist mathematics, ehich I understand to be based ...
0
votes
0answers
46 views
How does $\neg \phi$ as $\phi \to \textbf{false}$ fit in intuitionist philosophy?
In intuitionist type theory that I know, $\neg \phi$ is interpreted as a function that takes a proof of $\phi$ and outputs a proof of false.
It seems to me that this is different from the way that ...
1
vote
1answer
50 views
Difference between proof of negation vs proof by contradiction in practice?
This article explains the difference between proof of negation and proof by contradiction, and this question has asked for a clarification.
I understand the difference in the abstract. If we don't ...
1
vote
0answers
12 views
Normal forms of proofs in intuitionistic logic?
In this post, Andrej Bauer says:
There is a theorem about normal forms of proofs in intuitionistic logic which tells us that every proof of a negation can be rearranged so that it ends with the ...
1
vote
0answers
21 views
Basic Constructive Modal Logic and Monoidal Endofunctors
I'm reading this paper by Kakutani :
http://nicosia.is.s.u-tokyo.ac.jp/~kakutani/files/aplas07.pdf
but I can't see how to use naturality of $m$ (given by the monoidal endofunctor modelling $\Box$) ...
1
vote
0answers
48 views
Type theoretic counterpart of calculus of constructions?
The Curry-Howard correspondence connects the simply typed calculus with proofs in propositional intuitionistic logic. This correspondence can be extended between System F (polymorphic typed calculus) ...
5
votes
0answers
57 views
Equivariant homotopy theory, topos theory and intuitionistic algebraic topology
This might be a very naive question, but I don't really see what would go wrong, so I'm wondering if this has already been done.
The idea is the following : equivariant homotpy theory as far as I can ...
2
votes
2answers
74 views
Syntactic proof that Peirce's law doesn't hold in simply-typed lambda calculus
This might have been asked before, but certainly I don't find any source. Even in the literature I've consulted, there is no such proof so far.
Context
In the context of the simply typed lambda ...
2
votes
1answer
59 views
Why should we adopt the cumulative universe convention?
In various sources on intuitionistic type theory, the universe of types is taken to be cumulative, i.e. $A:\mathcal U _i$ implies $A:\mathcal U_j$ whenever $i\le j$.
The question is: why do we have ...
0
votes
1answer
53 views
Propositional Intuitionistic Logic Question
Show that it is not the case that if $\models \lnot (A\land B)$ then $\models \lnot A$ or $\models \lnot B$.
Show $\models \lnot (A\land B)$ is true and neither $\models \lnot A$ not $\models \lnot ...
0
votes
0answers
49 views
Intuitionist Logic Question [duplicate]
Show that it is not the case that if ⊨ ¬(A ∧ B) then ⊨ ¬A or ⊨ ¬B.
Consider the formula ¬(p∧¬p).
Replace A with p and B with ¬p.
Validity: this is defined as truth preservation over all worlds of ...
3
votes
1answer
88 views
How Brouwer think about mathematics as a non linguistic phenomenon?
I have a course in mathematical logic and i heard some argument about intuitionism math.
I'am curious about it and i look at some book and i am just confused about phenomenon.
But i realized brouwer ...
3
votes
1answer
65 views
What kind of logical assumptions do I need for proving this topology theorem?
I have the following conjecture:
Definition. A topological space $(X,T)$ is connected iff there does not exist disjoint open sets $U,V\in T$ such that $U\cup V=X$.
Definition. A path $f$ ...
0
votes
1answer
32 views
Realizability model not realizing all of CZF
I would like to know some non-trivial examples of partial combinatory algebras whose realizability universe does not satisfy all of the axioms of Constructive Zermelo-Fraenkel (CZF) set theory.
Based ...
0
votes
1answer
56 views
relation between inquisitive logic and logic as games?
In the very intriguing thesis "Questions in Logic" Ivano A. Ciardelli shows how to build a semantics of questions that reduces to Truth Conditional logic for factual statements where ¬¬p = p, but has ...
6
votes
3answers
102 views
Propositional calculus and intuitionist logic
Having never had much exposure to formal mathematical logic, I have decided to embark on a quest to rectify this; unfortunately having been exposed to concepts from Intuitionistic Logic through my ...
2
votes
1answer
91 views
Prove constructively that $\log_2 3$ is irrational.
The usual proof that $\log_2 3$ is irrational is by contradiction. For instance:
Assume the negation: that $\log_2 3 = m/n$ for some integers $m$ and $n$. Then, by the property of logarithms, $2^{m/...
3
votes
1answer
74 views
Nondecreasing converging sequences without the LEM
A classical exercise for beginners in calculus is the following : let $(u_n)$ be a nondecreasing sequence of reals that converges to $0$. Show that $u_n\leq 0$ for all $n$.
There is a variation of ...
1
vote
0answers
68 views
showing that $(\lnot \lnot Q) \to Q$ is not an inutionistic tautology by using an ad hoc 3-valued logic?
I'm trying to prove that $\lnot \lnot Q \to Q$ is not an intuitionistic tautology by constructing a special finitely-valued logic with strictly more tautologies than intuitonistic logic ... and then ...
2
votes
1answer
68 views
how to prove that (P⊃Q)≡(¬Q⊃¬P) ( P ⊃ Q ) ≡ ( ¬ Q ⊃ ¬ P ) is disallowed in intuitionistic logic?
this is what I've tried;
define kripke model K=({0,1},≤,⊩) where ≤ is the (total) order relation over {0,1} defined by
0≤0 0≤ 11≤1,and ⊩ is a binary relation from {0,1} to the set of propositional ...
2
votes
1answer
79 views
Intuitionistic logic and derivation
It is my first approach to intuitionistic logic (IL) and, even if I understand the principle behind it, I struggle understanding when a sequent is derivable in IL and when is not. I know that IL ...
1
vote
0answers
42 views
Compact witness of satisfiability of a formula in intuitionistic logic
Given a formula in intuitionistic sentential logic, there is a nice, compact textual representation for a witness of its tautology, namely a program in a typed lambda calculus with introduction and ...
1
vote
4answers
117 views
Constructivity and Piecewise Functions
I'm currently exploring homotopy type theory and intuitionistic mathematics.
In constructive/intuitionistic mathematics, 2 features arise:
A proof of $\neg \neg A$ is not a proof of $A$.
All ...
4
votes
1answer
290 views
Can the axiom of choice be explicitly proved in (intuitionistic) predicate logic, or is something like intuitionistic type theory necessary?
In intuitionistic mathematics, an axiom of choice of the form
$$
\forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x, fx)
$$
is valid by the meaning of the quantifiers (comp. Dummett, ...
0
votes
0answers
75 views
How to prove that the following three tautologies of classical logic are disallowed in intuitionistic logic?
I need to prove that the following three tautologies are disallowed in intuitionistic logic.
The tautologies are:
1-double negation $\neg \neg P\equiv P$
2-Law of excluded middle $P \vee\neg P$
3-...
0
votes
0answers
74 views
Can this separating theorem imply yields the sign of a real number?
I am looking at the following separation theorem (called TH1):
$\neg(\exists a \in \mathbb{R}^{1 \times m } ( a A > 0)) \Rightarrow \exists b \in \mathbb{R}^n_+ (Ab=0).$
Here $A$ is a matrix in $\...
2
votes
1answer
92 views
Constructive Intermediate Value Theorem (IVT)
I'm trying to learn a bit about intuitionistic/constructive mathematics, as I want to understand a little about topos theory and homotopy type theory (HoTT). I'm confused as to why the intermediate ...
1
vote
2answers
48 views
Proof in constructive mathematics using decidability.
I am working in constructive mathematics that means without the law of excluded middle. One may also interpret this as working in inuitionistic logic.
Lets assume I have some set $A$ such that I ...
6
votes
3answers
179 views
Proof verification in constructive analysis
I want to proof something in constructive analysis, that means without the law of excluded middle (or, if one prefers this interpretation, in intuitionistic logic).
First some definitions:
$C(x_1,...
7
votes
1answer
106 views
Can we prove $1\neq 2$ using intuitionistic methods?
Can we prove $1\neq 2$ using intuitionistic methods? It is trivial to prove conventionally starting from Peano's Axioms, but it seems to require a proof by contradiction.
2
votes
1answer
153 views
What is the intuitive meaning of the Heyting algebra?
I'm curious about this.
As we all know, classical logic can be described as what is called the Boolean Algebra, in particular, you can think of figuring out the truth of a classical composite ...
1
vote
1answer
119 views
Why $\phi \lor \neg \phi $ is not allowed in intuitionistic logic? [closed]
Why is $\phi \lor \neg\phi$ not allowed in intuitionistic logic?
My professor said this was because intuitionistic logic must have concrete construction.
Further, why is it not possible to write a ...
1
vote
1answer
88 views
Total order on constructive real numbers
Is there a definition of the real numbers in constructive or intuitionistic logic such as the order is total, ie
$$ \forall x,y\in\mathbb{R},\; x \leq y \lor y \leq x $$
The classical proof of this ...
0
votes
1answer
43 views
Dual of powerset is not a complete Heyting algebra
The following excerpt comes from Sheaves and Logic by Fourman and Scott (Applications of Sheaves (1977), pag. 304):
I can't figure out where those two rules play a role in the proof that the powerset ...
5
votes
1answer
168 views
Metaphorical Story about the irrefutability of the law of excluded middle
One can refute in intutionistic logic that they cannot refute the law of excluded middle. The proof is a bit strange:
...
1
vote
1answer
74 views
Lie groups in synthetic differential geometry
I'm reading Mike Shulman's Synthetic Differential geometry (a small article for the "pizza seminar" it seems); and there's a part about Lie groups that I have trouble understanding.
Actually there ...
0
votes
1answer
45 views
Maximal (or prime) theories and their sets
Probably it is very simple lemma but I cannot see it. Suppose that we have intuitionistic propositional logic (in fact, it can be classical) and $W$ is the set of all prime (or maximal - in classical ...
1
vote
1answer
81 views
Enumerate propositional formulas that are classically valid, but intuitionistically invalid
tl;dr I'm looking for a syntactical way to enumerate tautologies in propositional logic that are not tautological in intuitionistic logic.
Intuitively, the theorems of propositional logic are ...
0
votes
0answers
32 views
Can temporal logic be included in the framework of modal logics K, 4, D, T? Substructural temporal logic?
I am reading the article "A uniform framework for substructural logics with modalities" https://easychair.org/publications/paper/d5zT which gives impression that K, 4, D, T (and some possible ...
1
vote
0answers
93 views
Proving the Glivenko theorem via Kripke models
We'll prove it in just one direction, since the other one is obvious. So, assume $\psi$ is a theorem of classical propositional logic. Prove that $\lnot \lnot \psi$ is a theorem of intuitionistic ...
2
votes
1answer
90 views
Proving $\lnot \lnot (\psi \lor \lnot \psi)$ is a theorem of intuitionistic propositional logic
Here, $\psi$ is some arbitrary formula.
The proof I've come up with is as follows.
Assume $\lnot \lnot (\psi \lor \lnot \psi)$ is not a theorem of IPL, which means there exists some Kripke model ...
3
votes
0answers
48 views
Internal frame homomorphisms and sheafification
Let $\mathcal{E}$ be an elementary topos with subobject classifier $\Omega$, and let $j : \Omega \to \Omega$ be a Lawvere-Tierney topology. $\Omega$ is naturally seen as a frame object internal to $\...
1
vote
1answer
67 views
Verifying my proof in intuitionistic logic
I need to prove that $ \neg Kp \rightarrow \neg p$ follows intuitionistically from $ p \rightarrow \neg \neg Kp$. May I ask someone to verify my proof?
In addition, I also possess a proof for $\...
2
votes
2answers
82 views
Does double negation elimination hold for decidable formulae in intuitionistic logic?
Let $P$ be a quantifier-free decidable formula, i.e. one can prove $P \lor \lnot P$.
Does it follow that $\lnot \lnot P \to P$ intuitionistically?
Informally, a decidability of a formula means ...
5
votes
1answer
106 views
Is equality $\neg \neg$-stable?
In an essay by Andrej Bauer, I read the following statement : "A statement built from the universal quantifier ∀, conjunction ∧, implication ⇒, and numerical equality = is ¬¬-stable, as can be easily ...
1
vote
1answer
61 views
Does the equivalence ($P \rightarrow Q$) $\iff$ ($\lnot P \lor Q$) hold in intuitionistic logic? [closed]
Does it maybe hold in one direction but not the other?
1
vote
1answer
99 views
Confusion around quantifiers in intuitionistic logic
As laid out in Joel Hamkins' A question for the mathematics oracle, I am interested in considering the possibility that some arithmetic sentences might not satisfy the law of the excluded middle.
...
2
votes
1answer
59 views
Infinitesimal Approaches To Differential Geometry As Conservative Extension
When studying differential geometry, I often feel that infinitesimal approaches would do a deal for the intuition. There also seems to exist various examples like synthetic differential geometry or ...
3
votes
2answers
93 views
What kinds of variables range over proofs?
I hope this question does not seem to obscure...
Consider the standard inference rule schema for, say, conjunction:
...
