5
votes
4answers
593 views

What is a constructive proof of $\lnot\lnot(P\vee\lnot P)$?

Glivenko's theorem says that $\lnot\lnot P$ is a theorem of intuitionistic logic whenever $P$ is a theorem of classical logic. Is it closely related to the so-called Gödel–Gentzen negative translation ...
3
votes
3answers
457 views

Adequacy theorem for propositional calculus

I have been thinkig about the following classical theorem of propositional calculus: Adequacy Theorem: if $A$ is a tautology then $A$ is provable by the logical axioms Now "$A$ is a tautology" ...