Tagged Questions

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

1
vote
2answers
86 views

Proving the non-derivability of formula using the of the kripke model

I try proving the non-derivability of $(p\to q) \to \lnot p \lor q$, using the of the kripke model. I tried using different combinations of $Wi$, but I get fail.
0
votes
1answer
50 views

Why do you only need to show validity in one world when using trees in institutionist/constructivist logic?

Depicted below, my prof used a tree to prove that an argument is valid according to intuitionist logic. However, I can't find a contradiction in world 0. Why is invalidity ascertained when all ...
4
votes
3answers
70 views

Seeking help to understand a simple Kripke model

I'm reading A Brief Introduction to the Intuitionistic Propositional Calculus, at page 7, there is a simple Kripke model represented by a graph, I interpret it as: $W = \{w_1, w_2\}$ $w_1 \ge w_2$ ...
0
votes
0answers
39 views

Existence of a basis in constructive vector spaces

As I was trying to review forgotten knowledge on Vector Spaces in wikipedia, I read that the existence of a basis follows from Zorn lemma, hence equivalently from the axiom of choice. Actually, the ...
4
votes
1answer
104 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 ...
3
votes
1answer
80 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 ...
2
votes
2answers
140 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 ...
1
vote
2answers
94 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
140 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 ...
1
vote
1answer
52 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 ...
3
votes
2answers
67 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
65 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.
0
votes
2answers
57 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 ...
5
votes
1answer
149 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 ...
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
78 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 ...
2
votes
2answers
99 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 ...
1
vote
2answers
57 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
68 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
67 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
165 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
84 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
100 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
93 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 ...
8
votes
1answer
263 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 ...
2
votes
1answer
113 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 ...
7
votes
4answers
175 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 ...
2
votes
1answer
94 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
268 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
147 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
212 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 ...
1
vote
1answer
160 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 ...
6
votes
1answer
164 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
161 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 ...
5
votes
1answer
225 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 ...
4
votes
1answer
141 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 ...
4
votes
4answers
168 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 ...
0
votes
1answer
145 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)
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 ...