2
votes
2answers
91 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
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 ...
1
vote
1answer
48 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
46 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
61 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.
3
votes
1answer
64 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 ...
3
votes
1answer
65 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
150 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
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
76 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
248 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
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 ...
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
246 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
139 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
187 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
140 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 ...
4
votes
1answer
136 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
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 ...
0
votes
1answer
143 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 ...