Questions tagged [intuitionistic-logic]
Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.
231
questions
2
votes
1answer
60 views
Are geometric arguments using infinitesimals valid?
This question pertains to smooth infinitesimal analysis as presented in the book A Primer of Infinitesimal Analysis by John Bell. The book uses intuitionistic logic.
Let $\Delta$ denote the set of ...
1
vote
1answer
41 views
Context in Type Theory
I am reading a book on type theory. On page 105, the author says that
If one views valid contexts as theories (in the sense of ordinary logics) a consistent context corresponds to a consistent ...
3
votes
1answer
52 views
Given an inhabited type in simply-typed lambda calculus (w/no basics, just variables), is there a combinator of that type that is no longer than it?
Apologies if I've got some of the terminology here wrong, typed lambda calculus is a bit new to me.
Let's say we've got a type in simply-typed lambda calculus with no basic types (functions and type ...
2
votes
1answer
43 views
Universal Quantifier in Intuitionistic Logic
I have a very basic question about $\forall$ in intuitionistic first-order logic (IQL). It is well-known that in intuitionistic propositional logic (IPL), (\ref{dnlem}) and (\ref{dndne}) are both ...
0
votes
1answer
40 views
Non-existence of a dischargeable hypothesis
I meet a question about the existence/non-existence of a dischargeable hypothesis. The question is as follows: in intuitionistic logic, if for every proposition $X$, it cannot be the case that $X$ ...
2
votes
1answer
45 views
proof intuitionist logic
So here is the proposition I'd like to prove:
a ∨ ¬a ⊢((a→b)→a)→a
I have tried many way to find a proof, and always end up in a mess...
for example:
a ∨ ¬a ⊢((a→b)→a)→a
a ⊢((a→b)→a)→a (...
0
votes
1answer
32 views
Proof of Angles going beyond 90 deg in Trigonometry [duplicate]
Since we’re introduced to trigonometric ratios in terms of opposite, perpendicular and hypotenuse, all of which are a part of a right angled triangle. This defines the ratios for angles greater than 0 ...
0
votes
0answers
30 views
Questions about Intuitionistic Logic
Are the following theorems of Intuitionistic Logic?
$\Vdash \varphi \implies \lnot \lnot \varphi$
$\Vdash \lnot \lnot\varphi \implies \varphi$
$\Vdash (\varphi \implies \lnot\psi) \implies (\...
0
votes
0answers
48 views
Proof of Angles going beyond 90 degrees in Trigonometry
Since we’re introduced to trigonometric ratios in terms of opposite, perpendicular and hypotenuse, all of which are a part of a right angled triangle. This defines the ratios for angles greater than 0 ...
2
votes
1answer
40 views
Semantic explanation for converting intuitionistic logic into classical logic by adding LEM as an axiom
I have a question about converting intuitionistic logic (IL) into classical logic (CL) by adding LEM as an axiom. IL is usually understood as a logic without LEM.
$$\textrm{LEM}:=A\vee\neg A.$$
In ...
5
votes
1answer
41 views
Intermediate logics and strong algebraic completeness
As a setup, suppose that you have a usual propositional language $\mathcal L$ over a set of propositional variables $Var$ and with symbols $\land,\lor,\rightarrow,\bot$ in the usual way. Let $L$ be an ...
1
vote
1answer
22 views
Two non-isomorphic intuitionistic Kripke frames satisfying different formulas.
I am struggling with the following problem:
Being given two non-isomorphic intuitionistic Kripke frames $F_1$ and $F_2$ there is a formula $\phi$ such as:
$$
F_1 \models \phi\ and\ F_2 \not \models \...
1
vote
1answer
147 views
The legitimacy of topos theory and intuitionism.
This is an exercise in critical thinking. I am not looking, therefore, for opinions on the matter; rather: I would like to know the evidence (whatever that might mean).
Background:
I have a ...
1
vote
1answer
20 views
Accessibility relation in non-classical logics: hereditary or not?
Recently, I am reading course materials on intuitionistic and modal logics. I have two questions about the notion of accessibility relation in Kripke semantics for intuitionistic and modal logics. ...
2
votes
1answer
39 views
Definition of proposition in a constructive setting
In a typical discrete math course, we are taught that a proposition is something that is either true or false but not both, which seems to be based on a classical interpretation.
How would one go ...
2
votes
2answers
69 views
Are constant functions continuous in constructive mathematics?
The standard proof that a constant function $c: X \to Y$, $x \mapsto y_0$ is continuous proceeds as follows: if $U \subseteq Y$ is open, then either $c^{-1}(U)=X$ if $y_0 \in U$, or $c^{-1}(U)=\...
8
votes
1answer
86 views
About Gödel-Gentzen negative translation
I have a question about Gödel-Gentzen negative translation. According to the Wikipedia article for negative translations, "a sentence $\phi$ may not imply its negative translation $\phi^{\rm N}$". I ...
0
votes
1answer
94 views
Possible worlds with different formal semantics
I want to ask a basic question regarding modal logic: is it formally possible that a statement such as $$\forall x(P(x)\vee\neg P(x))$$ is true at a world $w_1$, but not in another world $w_2$?
For ...
0
votes
1answer
39 views
Watered down axiom of choice
I'm wondering what the following statement is equivalent to in an intuitionistic framework.
For a union of sets $C = \bigcup\limits_{i \in I} X_i,$ if $S \in C,$ there
exists $s \in I$ such that $...
0
votes
0answers
35 views
intuitionistic probability theory
I wonder whether the law of excluded middle not being available in intuitionistic logic might provide an obstacle when working with an axiomatization of probability theory using the Kolmogorov axioms. ...
1
vote
1answer
35 views
Provide a Kripke model to prove that $\neg(\neg P\lor \neg Q\lor R)\to (P\land Q \land R)$ is false in intuitionistic logic
Could anyone check my working please?
Provide a Kripke model to prove that $\neg(\neg P\lor \neg Q\lor \neg R)\to (P\land Q \land R)$ is false in intuitionistic logic.
Here $k_0$ forces $\neg(\neg ...
0
votes
1answer
57 views
Resource suggestion for practicing modal logic and intuitionistic logic
any suggestion ( Book , Pdf , online resource , ... ) for solving problems about
modal logic and intuitionistic logic and it would be really great if there was a solution for it .
4
votes
1answer
64 views
Proving $\Gamma \vdash \phi$ Implies $\Gamma \vDash \phi$ (for Institutionistic propositional logic and Heying algebras)
I'm trying to prove that $\Gamma \vdash \phi$ implies $\Gamma \vDash \phi$ (for Institutionistic propositional logic and Heying algebras), by induction with respect to natural deduction proofs of ...
1
vote
0answers
65 views
For which logic output of funcntion $\tau$ will be K logic?
We have
$ L = \{\land , \lor , \to , \bot , \lnot \} $
and
$L_\Box = \{\land , \lor , \to , \bot , \lnot ,\Box \}$
and then we define function $\tau : L \to L_\Box$ like below
$\tau(p) = \...
2
votes
1answer
52 views
Satisfaction relation in Intuitionistic Logic
I would like to clarify what concerns me in satisfaction relation in Kripke frames for intuitionistic logic (INT). Firstly, is it a true statement that given a Kripke Model $$M = \langle W, R, \models ...
7
votes
1answer
133 views
Relation between Heyting algebras and Intuitionistic logic
We can associate a logic to an algebra in the following way:
Let $(A, \leq)$ be an algebra and $D \subseteq A$ a set of designated elements. Then we define a valuation as $v: Prop \to A$. Then we ...
3
votes
1answer
62 views
What does intuitionism/constructivism say about this proof?
The Wikipedia article on Euler's totient function lists, in the Growth rate section, the following:
$$\varphi(n)<\frac{n}{e^\gamma\log\log n}\quad\text{ for infinitely many }n$$
and says: "The ...
2
votes
1answer
230 views
A Question About the Order of Learning from the Book “Lectures on the Curry-Howard Isomorphism” (1998)
I'm learning from this book: https://disi.unitn.it/~bernardi/RSISE11/Papers/curry-howard.pdf
(Lectures on Curry-Howard Isomorphism - 1998 version) for some project. And due to time constraints, I ...
1
vote
1answer
54 views
In Intuitionistic Kripke semantics, is proving a formula not forced at one node the same as proving it not derivable/invalid?
I am having trouble understanding whether proving a formula not forced at one node in Kripke semantics is the same as proving that it is not derivable/invalid in Intuitionistic logic.
For example, ...
0
votes
0answers
25 views
Can we prove using intuitionist logic that $\neg \exists r: \forall x: [P(x,r) \iff \neg P(x,x)]$
Can we prove using intuitionist logic that $\neg \exists r: \forall x: [P(x,r) \iff \neg P(x,x)]$ where $P$ is a binary logical predicate?
2
votes
1answer
38 views
What are the restrictions on substitution of terms in Hilbert-style calculus vis-à-vis intuitionistic logic?
I apologize if the title of this question can be better formulated, but I recently encountered a situation where what I thought was valid substitution led to an incorrect thing—at least I think.
I ...
7
votes
1answer
181 views
Introductions to intuitionistic logic?
Short version: What is a good shortish introduction to intuitionistic logic, accessible to a relative beginner in logic?
Long version: I'm revising the frequently used Teach Yourself Logic Study ...
0
votes
0answers
39 views
How HSAT (Heyting satisfiability) can be proven to be PSPACE-COMPLETE if not every intuitionistic formula has disjunctive or alternative normal form?
There's a proof in R. Statman, Intuitionistic propositional logic is polynomial-space complete. Is it constructive? Would that be possible to formulate HSAT without reffering to second order classic ...
0
votes
1answer
56 views
Does every intuitionistic formula have disjunctive or conjuctive normal form?
As in title - does every intuitionistic formula have disjunctive and conjuctive normal form? I guess that this is correct but I couldn't find any information on that.
2
votes
1answer
54 views
Does constructive dilemma hold in intuitionistic logic?
I mean this law:
$ (( p \Rightarrow r) \wedge (q\Rightarrow r) \wedge (p \vee q)) \Rightarrow r$
It seems to me that it does hold for INT. Is there any non-esoteric logic that excludes that law?
0
votes
1answer
90 views
$A \rightarrow \neg \neg A$ in constructive logic with and without explosion
I have been reading about constructive logic and I also recently became aware of minimal logic. My understanding of minimal logic is not clear, and I don't get how it is defined, or what suffices as a ...
3
votes
2answers
162 views
Proof methods w/o Contradiction (Intuitionistic Frameworks of Math)
Regarding the standard formulation of the division algorithm:
If $a,b$ are integers with $b > 0$, then there exists unique $q,r$ such
that $a = bq + r$ with $0 \leq r < b$.
The standard ...
0
votes
1answer
67 views
Does the BHK interpretation induce a category?
I was recently introduced to the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic, and since I am just starting out with basic category theory and have heard that topos logic is ...
3
votes
1answer
94 views
Relation between classical implication and intuitionistic implication
Recently, I have read an article on combining classical and intuitionistic implications. On page 9, in their Proposition 6, the authors say that
$$A\Rightarrow((A\Rightarrow B)\rightarrow (A\...
5
votes
1answer
83 views
What is the definition of an embedding of one logic in another?
An oft-cited result about intuitionistic logic is that
Proposition 1. Classical logic can be embedded into intuitionistic logic.
This is the Godel-Gentzen double-negation translation: given a ...
3
votes
1answer
122 views
Does the law of the excluded middle hold for finite sets in intuitionist set theory?
There are local laws of the excluded middle in intuitionist logic, for instance I believe you can prove in Heyting Arithmetic that for all $\Sigma_1$ propositions, that $p \vee \neg p$. Is there ...
0
votes
0answers
49 views
Can you define non-effectively calculable function in constructive mathematics?
Pretty simple just what the title says.
Can you define non-effectively calculable functions in constructive mathematics?
Does this answer differ in any way if it were in an intuitionistic logic?
0
votes
0answers
73 views
Defining sets in intuitionistic logic
I'm somewhat familiar with the school of intuitionistic logic. I know that an intuitionistic logician thinks of infinity as constructive as apposed to complete. Thus a intuitionistic logician cannot ...
1
vote
1answer
103 views
Doesn't cut elimination make intuitionistic logic equivalent to classical logic?
Suppose we have a proof by contradiction of $A$, meaning we've proven $(A \to \bot) \to \bot$.
If we eliminate all cuts in the proof, then the last step of the proof will be an implication ...
1
vote
1answer
88 views
How exactly does the currry-howard formalization of logic capture the semantics of LEM not holding?
Let $p$ be a proposition and $P$ the collection of propositions. In classical logic, the law of excluded middle holds, and we can model the semantics of this as saying that there is a function $\text{...
0
votes
0answers
58 views
Proof of the Disjunction Property for propositional Intuitionistic Logic, using Normalization for natural deduction
I'm doing a Proof Theory course and this is an exercise. I've tried a few things but nothing works. Any help would be much appreciated. (Note it's regular Normalization, not strong).
1
vote
1answer
115 views
Equivalence Between Law of Excluded Middle and Self-Implication
We know that $P \to Q$ is equivalent to $\neg P \lor Q$, as can be verified easily in truth table. Now suppose we have proof for self-implication below
[the axiom system is Lukasiewicz's, with L1: $P ...
2
votes
1answer
98 views
Noetherian sets without LEM
A noetherian ring can be defined as a ring in which any nonempty set of ideals has a maximal element. They're pretty nice objects. One can obviously generalize this to a bunch of different algebraic ...
5
votes
2answers
156 views
Difference between $\lambda$-$\mu$-calculus and intuitionistic type theory + LEM for classical proofs?
I have some experience with using type theory to do proofs in intuitionistic logic. If I want to prove theorems that require classical logic, I simply pose the law of excluded middle (LEM) as an axiom....
2
votes
0answers
54 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 ...
