Re: Confused about Intuitionistic provability


Alan Smaill wrote:
> "Keith Ramsay" <kramsay@xxxxxxx> writes:
[...]
|> That the sentence pv~p, where p is a propositional variable, holds
|> in all models is equivalent to the law of excluded middle. If one
|> wants to say that it doesn't hold in all models, that is equivalent
|> to *denying* the law of excluded middle.
|
|Depends on how you parse "doesn't hold in all models"...

I only see one way to parse it that makes sense in context,
taking it as "not (holds in all models)". "(not holds) in
all models" is silly.

There's a version of the completeness theorem that says for
each sentence S,

(*) {S holds in every model} iff {S is a theorem of FOL}.

Taking FOL to be classical FOL, this is a classical
mathematical theorem. If we don't assume classical logic,
and take FOL to be intuitionist logic, I don't even know
whether it's possible for the result to be true, and I'm
pointing out that it isn't provable by principles that I
would normally use.

Taking "FOL" to be intuitionist logic, and letting S=pv~p,
this nonclassical (*) would imply the special case,

{pv~p holds in every model} iff
{pv~p is a theorem of intuitionist logic}.

We know however that pv~p isn't a theorem of intuitionist
logic. So this form of completeness would imply that

~{pv~p holds in every model}.

Now holding in every model is equivalent to holding for
every proposition P. Hence

~{(P) Pv~P},

and (P) Pv~P is a way to express the law of excluded middle.

|> Now people doing constructive
|> mathematics in general fail to affirm the law of excluded middle
while
|> doing constructive mathematics, but denying it is a different story.
|> Only some constructivists deny it. Intuitionists, in particular,
tend
|> to use assumptions that contradict classical logic, hence one of
them
|> might deny the law of excluded middle.
|
|that would be problematic, given that inutuitionists explicitly
|accept the negation of this denial, ie ~~(pv~p) is accepted.
|So asserting ~(pv~p) gives a contradiction straight away.

But it's not any specific case of the law of excluded middle
that's denied. You are correct that that would be a contradiction.
Denying the rule in general isn't.

By the usual classical proof, one can show that the law of
excluded middle LEM implies the existence of a function
f:[0,1]->R that is discontinuous. Intuitionists fairly often
follow Brouwer's reasoning that concludes every function
f:[0,1]->R is uniformly continuous. From

LEM -> (Ef) f is discontinuous

and

(f) f is uniformly continuous

one can deduce ~LEM.

These intuitionists regard both of the following:

~(P) Pv~P
(P) ~~(Pv~P)

as true. They deny the general rule, and also deny the
existence of a counterexample.

|The situation you have in mind, presumably, is where a set of
|axioms is constructively inconsistent, but not intuitionistically
|inconsistent. But still no instance of ~(pv~p) will be derivable.

No, this isn't the situation I have in mind. Yes, no instance
of ~(pv~p) is derivable.

|> I don't think even they make
|> enough assumptions to imply that only the sentences provable in
|> intuitionist logic hold in all models, however. There's this whole
|> twilight zone of principles like
|>
|> {~p -> (q v r)} -> {~p->q} v {~p->r}
|>
|> whose universal validity one would have not just not to affirm,
|> but to deny.
|
|has the same problem, since the double negation *is* valid.

Again, what this nonclassical completeness result (*)
implies is

~(P)(Q)(R) [{~P -> (Q v R)} -> {~P->Q} v {~P->R}].

Certainly you can't reasonably believe

(EP)(EQ)(ER) ~[{~P -> (Q v R)} -> {~P->Q} v {~P->R}],

but you don't have to.

|> I remember once skimming a paper that assumed classical logic,
|> but used Kripke models, that showed the equivalence of the set of
|> sentences holding in all Kripke models and the set of validities
|> of second-order logic. It wasn't clear to me how much of the
|> reasoning would be constructively satisfactory, but it at least
|> suggests that the set of validities of FOL could be something
|> very rich, unless the law of excluded middle is true.
|
|any idea what the reference is?

You know, I just remember running into it in the library, in
some well-known journal, several years ago. I bet I could find
it again with a search of Mathematical Reviews.

|presumably this is for some particular theory, rather than
|pure FOL?

No, just first-order logic as interpreted in Kripke models.

If you know about Kripke models, you'll recall that there's
a directed graph with data at each node. Given a sentence S
of second-order logic, the author contrives a formula in
first-order logic that are valid when the Kripke model is
something like a graph where the terminal nodes correspond
to the elements of a model M of S, and the nonterminal nodes
correspond to the subsets of M.

I'm not confident of the details, but I have a rough idea
of the kind of trick used.

Keith Ramsay

.

Relevant Pages