Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

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
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: ...