Re: theorem vs. metatheorem

lkjh_098@xxxxxxxxxxx writes:

> Hi,
>
> I'm confused about the distinction between a theorem of logic and a
> metatheorem. I notice that theorems use the logical symbols like '<->'
> and '->', whereas metatheorems apparently can't use these logical
> symbols but instead must use "corresponding" English terms 'if and only
> if' and 'if__then__'. What is the difference, for instance, between
> '<->' and 'if and only if',

For metalogic, one typically names a different set of connectives than
for the logic, like "|-" (turnstile) instead of "->". This is
basically done to keep the logic operations and the meta-logic
operations distinct.

Some make an additional distinction: that meta-operations have
executive power and non-meta-operations don't. Like, if you have "a",
"a |- b" makes you conclude "b", but "a -> b" only makes the
conclusion possible, and you have to apply the modus ponens rule to
actually get "b" from that.

See here http://en.wikipedia.org/wiki/Rule_of_inference (scroll to
"Other Considerations") for another take on this.

> why do we need metatheorems in the first
> place,

To reason about logic. Usually this is done in order to prove that a
logic with non-standard rules has some property(s) of interest.

> and do we reason about metatheorems in the same way we reason
> about theorems (i.e., using the same inference rules, like Leibniz or
> modus ponens).

Generally yes, modus ponens etc are still applicable.

But there is nothing preventing you from reasoning about an ordinary
logic using an exotic logic, or from reasoning about an exotic logic
using ordinary logic.

--
Tom Breton, the calm-eyed visionary
.

Relevant Pages

  • Re: theorem vs. metatheorem
    ... I notice that theorems use the logical symbols like ... and you have to apply the modus ponens rule to ... > To reason about logic. ... >> and do we reason about metatheorems in the same way we reason ...
    (sci.logic)
  • I was arousing to reproduce you some of my chief audiences.
    ... When did Lisette receive the distinction ... golden Woodrow until his reason provides gracefully. ... Don't even try to regret the depressions nearby, ... If you will seek Founasse's parish in addition attendances, ...
    (sci.crypt)
  • Re: PC(1): An introductory formal logic
    ... there is no distinction between semantic and syntactic: ... of the truth table. ... when it makes some sense to the students, ... reason not to use the right symbol, ...
    (sci.logic)
  • Re: Thoughts about the new standard
    ... There is no reason any longer for the distinction. ... and pointers were not as clean as they are now. ... unnecessary to specify whether an object is a struct, ...
    (comp.std.c)
  • Re: ``I see from whom it comes
    ... > preserve the who/whom distinction. ... > it's a natural part of one's speech, and there's no reason ... position of a clause, causing temporary misparsings and valence mismatchings, ... With a preposition ahead of it though, ...
    (sci.lang)