Re: reductio ad falsum versus reductio ad absurdum

On 28 Aug 2005 20:30:44 -0700, futurist <adamgolding@xxxxxxxxxxxxxxx> said:
>> What thesis? |- doesn't nest.
>
> ok, i guess that's the part i don't understand--why doesn't |- nest
> when -> can??

Because, unlike ->, |- is not a boolean logical connective. Rather,
"S |- Q" is an abbreviation in the *metalanguage* that we are using to
talk *about* the logical system in question for "There is a proof in the
system of Q from S", where Q is a sentence of the language of the system
and S is a set of sentences of the language. In the case where S is
only a singleton {P}, it is conventional to write "P |- Q" instead of
"{P} |- Q".

That said, there is in fact a *sense* in which |- can nest in certain
systems that are powerful enough to represent their own proof relations.
But that's another discussion.

.

Relevant Pages

  • Re: best method to perform operations on word lists
    ... current purpose it'll do the trick but any suggestion for optimization ... my $prev = 'nonesuch584685542256RANOM58544'; ... This didn't modify the list. ... hence my thoughts about language files. ...
    (comp.lang.perl.misc)
  • Re: Uncle Scrooge?
    ... (Is there any name that isn't the slang word for penis in some language ... Prev by Date: ...
    (alt.usage.english)
  • Re: Pseudocode in the wikipedia
    ... syntactical features of the language. ... Peace ... Bill Mill ... Prev by Date: ...
    (comp.lang.python)
  • Re: problem with variable
    ... tells me that they have zero regard for VB as a language and that I should ... VB.Net: "Fool me once..." ... Prev by Date: ...
    (microsoft.public.vb.general.discussion)
  • Re: Stack Pointer..?
    ... this isn't anything in the standard C language. ... Jack Klein ... FAQs for ... Prev by Date: ...
    (comp.lang.c)