Re: Simple yet Profound Metatheorem

Barb Knox wrote:
> In article <1134713007.253164.75100@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
> "sradhakr" <sradhakr@xxxxxxxxxx> wrote:
>
> >Barb Knox wrote:
> >
> >> If you want provability and truth to be the same, you can dispense with
> >> all the modal machinery and just use some existing well-thought-out
> >> constructive logic (e.g. Intuitionistic).
> >>
> >False. Truth and provability are *not* the same in
> >intuitionistic/constructive logics. If you claim otherwise, show me a
> >valid proof of the law of non-contradiction i.e., of ~(P&~P), in these
> >logics.
>
> OK, here's a Fitch-style Intuitionistic ND proof:
>
> 1. | P ^ ~P A
> |-------
> 2. | P 1 ^E
> 3. | ~P 1 ^E
> 4. ~(P ^ ~P) 1,2,3 RAA
>
>
> >Any "proof" of ~(P&~P) that you produce from contradictory
> >premises is not a valid proof in these logics.
>
> Eh? I've given a perfectly valid Intuitionistic proof. On what grounds
> do you object to it (if you do)?
>
*Any* proposition can be proven in intiuitionistic logic if you start
with the premise P&~P. The above "proof" is fundamentally flawed and
*should not* be accepted as a valid proof of ~(P&~P). The above "proof"
is indistinguishable from the case where you deduce an *arbitrary*
proposition (say, denoted by the "absurdity symbol") from P&~P and then
*substituted* ~(P&~P) for the absurdity symbol and claimed that as a
proof of ~(P&~P). It is obvious that any proposition can be proved that
way.

Indeed, if you think carefully, you will see that the very concept of
"proof" requires the law of non-contradiction in the first place and
you have already *presumed* ~(P&~P) in your so-called proof-- it is
totally absurd to claim an RAA proof of ~(P&~P). What you could do is
to make a straightforward, bald assertion of ~(P&~P) without claiming
to prove it. But that would violate the intuitionistic philosophy of
truth as provability. See the reference that I have cited in my earlier
post for my objections to ~(P&~P) as a theorem of a theory T in which P
is undecidable (i.e., neither provable nor refutable in T).

Regards, RS

.

Relevant Pages

  • Re: Godels Incompleteness and Nonmonotonic Logic
    ... >> provability to have to be decidable. ... > Decidability is a separate issue. ... If the logics we're talking about ... without any reference to Goedel theorems. ...
    (comp.lang.prolog)
  • Re: Godels Incompleteness and Nonmonotonic Logic
    ... >> provability to have to be decidable. ... > Decidability is a separate issue. ... If the logics we're talking about ... without any reference to Goedel theorems. ...
    (sci.logic)
  • Re: Simple yet Profound Metatheorem
    ... Truth and provability are *not* the same in ... >intuitionistic/constructive logics. ... >premises is not a valid proof in these logics. ...
    (sci.logic)
  • Re: Sorry Godel - All Truths are Provable
    ... truth-value of a statement has to coincide with its provability-value. ... Doesn't have to, but for most logics it does, ... Lemma 2: Completness of Provability: ... V The Completeness Theorem, 4.1 Completness Theorem ...
    (sci.logic)
  • Re: Simple yet Profound Metatheorem
    ... Truth and provability are *not* the same in ... intuitionistic/constructive logics. ... premises is not a valid proof in these logics. ...
    (sci.logic)