Re: Simple yet Profound Metatheorem

sradhakr says...

>So the outline of an intuitionistic proof of ~(P&~P) would be as follows.
>
>(1) Suppose, to the contrary, that P&~P, i.e., suppose that "Both P and
>~P are provable"..
>
>(2) The said proof of P&~P can be converted into the proof of an
>arbitrary proposition Q..
>
>(3) Therefore a proof of P&~P cannot exist. Hence, ~(P&~P).

If you interpret ~A as (A -> False), then you can prove
~(P&~P) as follows

First, prove the general schema

(P & (P -> Q)) -> Q

Then a special case is

(P & (P -> False)) -> False

which is the same thing as

~(P&~P)

So you don't need the rule "From False, conclude anything".

What is False? You can think of it as a primitive
propositional constant, with the axiom schema

False -> Q

for every proposition Q. Or you can think of False as the
second-order statement "forall propositions Q, Q".

--
Daryl McCullough
Ithaca, NY

.