# Questions tagged [intuitionistic-logic]

Intuitionistic logic refer constructive logic, a logical system avoiding deduction rules like *Reductio ad absurdum*.

231 questions
Filter by
Sorted by
Tagged with
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 ...
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 ...
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 ...
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 ...
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$ ...
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 (...
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 ...
30 views

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