In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans. That is, given a set of axioms, the only propositions that can exist are those that ...

learn more… | top users | synonyms

4
votes
1answer
78 views

Equivalence between Peirce's law and Excluded Middle in Intuitionistic logic

I'm searching for a intuitionistically valid proof of the formula : $[((P→Q)→P)→P] ↔ (P \lor \lnot P)$ using the "standard" Hilbert-style axiom system from Kleene [1952], for ...
2
votes
2answers
112 views

Equivalence between middle excluded law and double negation elimination in Heyting algebra

It's well-know that in intuitionistic logic, middle excluded law and double negation elimination are equivalent. For example, in Johnstone - Topo theory, I read that, in a Heyting algebra, $p\vee\neg ...
3
votes
1answer
74 views

Is intuitionistic naive set theory consistent?

I'm asking because the usual argument that a set either belongs in itself or not doesn't apply. I did a quick search and it appears that the logic is also required to be contraction free. If it's ...
1
vote
1answer
145 views

How is the double negation translation similar to CPS in functional programming languages?

In Wikipedia's Double-negation translation article, I found that any formula in classical logic has its double negation as its intuitionist equivalent: It is also possible to define φN by ...
1
vote
2answers
92 views

Is it possible to prove that the encoding of existentials in System F is valid?

In Girard's Proofs and Types, under item 11.3.5, second-order existential quantification is encoded in System F using universal quantification as follows: $$ \Sigma X.V \equiv \Pi Y. (\Pi X.(V \to ...
2
votes
1answer
136 views

What if 'proof by contradiction' is not a valid method of proof?

I've just been reading this question about the existence (or lack thereof) of contradictions in maths. I've been wondering: What if 'proof by contradiction' is not a valid method to (dis)prove a ...
7
votes
4answers
171 views

How or why does intutionistic logic proof negations from within the theory, constructively?

I'm having a little of a cognitive dissonance why, in intuitionistic logic, it's possible to show stentences like $(\neg A \land \neg B) \implies \neg(A\lor B).$ In plain text: If 'A isn't true' as ...
5
votes
1answer
220 views

What do ultrafinitists think about Graham's number?

I know ultrafinitists want to require not only that mathematical objects be constructible, but be constructible given finite resources (such as time). So I wonder about something like the famous ...
1
vote
1answer
49 views

Completeness theorem for intuitionistic logic

Reading from Wikipedia about intuitionistic logic, I am guessing that there is a formal proof system for intuitionistic logic. (Note: My knowledge of intuitionistic logic is almost nil). My ...
11
votes
2answers
1k views

Do De Morgan's laws hold in propositional intuitionistic logic?

In Wikipedia page on intuitionistic logic, it is stated that excluded middle and double negation elimination are not axioms. Does this mean that De Morgan's laws, stated $$ \lnot (p \land q) \iff ...
3
votes
2answers
55 views

Contraposition in intuitionistic logic?

I read that contraposition $\neg Q \rightarrow \neg P$ in intuitionistic logic is not generally equivalent to $P \rightarrow Q$. If this is right, in what case can this contraposition ...
1
vote
1answer
48 views

$(\forall x,\, p\vee q(x))\leftrightarrow p\vee\forall x,\, q(x)$

Consider the logical formula $(\forall x,\, p\vee q(x))\leftrightarrow p\vee\forall x,\, q(x)$ where x does not appear free in p. This formula is not derivable in intuitionistic logic, but it is in ...
2
votes
2answers
64 views

Equivalence between $\neg\neg\bot$ and $\bot$ in intuitionistic logic.

As the title says, why are those two equivalent? I can find a simple derivation (using natural deduction) of $\bot$ from $\neg\neg\bot$, but i fail at proving the other implication.
5
votes
1answer
146 views

Example of an interesting theorem that fails in intuitionistic set theory but is classically valid?

I'm interested in intuitionistic set theories at the moment. I know that lots of principles imply LEM and so fail intuitionistically, and also a few basic principles - linear ordering of ordinals, for ...
0
votes
2answers
53 views

Compound interest coumpounded n time per year formula. $A=P\left(1+\frac{r}{n}\right)^{nt}$ intuition behind it.

I know that the compound interest formula for the interest compounded annually is given by $$A=P(1+r)^t$$ I know the intuition behind it. But why the compound interest formula for the interest ...
2
votes
2answers
90 views

Goedel's completeness theorem in and/or for intuitionistic first order logic

Warning: I am neither a logician nor a set theorist, just curious about foundations of classical and intuitionistic mathematics. Therefore it might well be that the things to come are plain wrong, and ...
3
votes
1answer
71 views

What is the purpose of defining the negation of a proposition A as A $\rightarrow \bot$?

I know that this definition is unrelated to the law of the excluded middle, but as a beginner in logic (I've studied the first half of Chiswell and Hodges' Mathematical Logic), the use of the name ...
-4
votes
2answers
76 views

How is Goedel's 1st incompleteness theorem related to the Axioms of a theory

i am thinking of various connections and formulations of Goedel's 1st incompleteness theorem. Apart from connections to Turing's Halting Problem and Algorithmic Complexity Theory, i am looking for ...
8
votes
1answer
251 views

Axiom of Choice - Type Theory (Proof)

Background In Intuitionistic Type Theory (p. 27-28), Martin Löf provides a proof of the axiom of choice that is constructively valid. This version is considerably weaker than the ordinary set theory ...
1
vote
2answers
54 views

When do DeMorgan's laws hold in a Heyting algebra

I'm working a bit with Heyting algebras (which are pseudocomplemented distributive lattives, right?) and I have a question about DeMorgan's laws. I know that, in general, it's not the case that $-(X ...
3
votes
1answer
66 views

Intuitionistic Linear Logic

I am currently going through some papers that use the "intuitionistic version" of Girard's Linear Logic. Problem is, i seem to find very little literature on it. There is a lot done on Linear Logic ...
1
vote
1answer
66 views

If $\phi$ is $\Delta^{0}_{1}$ in the language of arithmetic, does Heyting Arithmetic prove $\forall x [\phi (x) \vee \neg \phi (x)]$?

PA is conservative over HA for $\Pi^{0}_{2}$ sentences. If $\phi$ is $\Delta^{0}_{1}$, then $\forall x [\phi (x) \vee \neg \phi (x)]$ is equivalent to a $\Pi^{0}_{2}$ sentence. Since PA trivially ...
4
votes
5answers
156 views

Is there a simple example of how the law of the excluded middle can be inapplicable?

Why does a logic system not use the law of the excluded middle? I studied non-classical logic (intuitionistic and modal) where double negation can't be removed and the law of excluded middle can't be ...
4
votes
0answers
83 views

Defining “Penon Infinitesimals”.

In this lecture (which is accompanied by these slides), right near the end (so page 9 in the pdf of the slides; I don't think you have to watch the lecture), P. Johnstone refers to the "Penon ...
4
votes
2answers
98 views

Non-upper bounds without excluded middle

Motivated by an earlier question, I'm curious if we can prove the following statement without the law of excluded middle: Let $E$ be a set of real numbers. A number $x$ is said to be an upper ...
2
votes
2answers
81 views

Double negation distributes over conjunction

In Exercise I.1.11.(ii) of Johnstone's Stone Spaces, it is claimed that in any Heyting algebra, $$\lnot\lnot (a \land b) = \lnot\lnot a \land \lnot\lnot b.$$ It is easy to see one direction: Since ...
4
votes
1answer
138 views

Model theory for intuitionistic predicate logic: a non-empty domain?

In classical logic we tend to make the assumption that the domain of quantification is non-empty. This isn't (too) problematic because classical mathematicians assume a language/mind/proof independent ...
2
votes
1answer
111 views

Unprovable Equivalence in Type Theory

Let $\prec$ be a binary relation on a set $A$… A predicate $P(x)$ set $(x:A)$ is said to be progressive with respect to $(A,\prec)$ if \begin{equation} (\forall a:A)\Big((\forall b:A)\big(b \prec a ...
6
votes
1answer
155 views

Understanding a proof of Diaconescu's theorem

I am trying to walk through the proof of Diaconescu's theorem that the axiom of choice implies the law of excluded middle at http://plato.stanford.edu/entries/intuitionism/#ChoAxi. To paraphrase: ...
2
votes
1answer
92 views

Show formulas which are valid according to Brouwer-Heyting-Kolmogorov interpretation [closed]

How can I show, that the following formulae are valid according to Brouwer-Heyting-Kolmogorov interpretation? $(A \land B) \to (B \land A)$ $\neg (A \lor B) \to (\neg A \land \neg B)$ $A \land (B ...
8
votes
2answers
249 views

Minimal difference between classical and intuitionistic sequent calculus

Consider propositional logic with primitive connectives $\{{\to},{\land},{\lor},{\bot}\}$. We view $\neg \varphi$ as an abbreviation of $\varphi\to\bot$ and $\varphi\leftrightarrow\psi$ as an ...
3
votes
1answer
144 views

Axioms based on $\leftrightarrow, \lor, \bot$ for propositional intuitionistic logic?

Propositional intuitionistic logic can be axiomatized based on $\;\to, \land, \lor, \bot\;$, with modus ponens $$ \text{from }\; \phi \;\text{ and }\; \phi \to \psi \;\text{ infer }\; \psi $$ as the ...
5
votes
3answers
195 views

How can some statements be consistent with intuitionistic logic but not classical logic, when intuitionistic logic proves not not LEM?

I've heard that some axioms, such as "all functions are continuous" or "all functions are computable", are compatible with intuitionistic type theories but not their classical equivalents. But if they ...
0
votes
1answer
144 views

A question on intuitionistc propositional logic

Prove that: Two finite rooted frames are isomorphic iff they validate the same formulas. (This is an exercise in the book "Modal Logic" by A.Chagrov and M.Zakharyaschev)
2
votes
1answer
159 views

Intuitionism - is it fundamentally different than “ordinary” mathematics.

I have recently had a conversation with a person who considered intuitionism to be a valid alternative for the "usual" kind of mathematics. Clearly, intuitionism differs from the type of mathematical ...
4
votes
4answers
163 views

Help proving $ \sim \sim (p \to q),\sim \sim p \vdash \sim \sim q $ with intuitionistic axioms

Rule modus ponens: $ p, p \to q \vdash q $ Axioms A1 $ p \to (q \to p) $ A2 $ (p \to (q \to r)) \to ((p \to q) \to (p \to r)) $ A3 $ (p \land q) \to p $ A4 $ (p \land q) \to q $ A5 $ p \to ...