Thank you, Valentin.
It is true that the double negation of PEM is provable intuitionistically, that is ~~(P \/ ~P) for all P:Prop, but it is not true the double negation of universally quantified PEM is provable, that is ~~(forall x:A.P x \/ ~ P x) is not provable, and indeed if we accept Church's priniciple we may want that ~ forall n:Nat.Hold(n) \/ ~Hold(n) is provable (Here Hold(n) means that the nth TM applied to n terminates).
Thorsten
On 03/10/2018, 08:38, "coq-club-***@inria.fr on b
ehalf of Valentin Blot" <coq-club-***@inria.fr on behalf of coq-***@valentinblot.org> wrote:
One has to be careful when dealing with negative translation and first-
order logic. The same argument does not go through because there are
formulas that do not intuitionistically imply their negative
translation. From P -> False in classical logic you still get Pn ->
False in intuitionistic logic (where Pn is the negative translation of
P), but from there you cannot conclude P -> False because you may not
have P -> Pn intuitionistically.
Valentin
Post by Shahab TasharrofiIn addition to what others said, you can also generalize it to first-
https://en.wikipedia.org/wiki/Double-negation_translation
On Tue, Oct 2, 2018 at 1:09 PM Guillaume Melquiond <
Post by Pierre CasteranPost by Pierre CasteranHi,
It's probably a folklore result, but I didn't find a good
reference
Post by Pierre Casteranin the litterature.
Sorry if it is the case.
Does there exists a sequent of propositional logic H1, H2, ...
, Hn
Post by Pierre Casteran|- False, which is provable in classical logic, but not in
intuitionnistic logic ?
All the examples I tried have been succesfully proved by
tauto.
Post by Pierre CasteranIf it does not exists, is there a known (constructive ?) proof
of that ?
Unless I am missing something, this is a corollary of the
double-negation translation (Glivenko). In other words, if P -> False is
provable in classical logic, then ((P -> False) -> False) -> False is
provable in intuitionistic logic, which intuitionistically implies P ->
False.
Best regards,
Guillaume
This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment.
Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored
where