Re: Why are rules of inference not laws of sentential calculus?

On 1 Oct 2005 08:04:28 -0700, andrewspencers@xxxxxxxxx wrote:

>timvaz_059@xxxxxxxxxx wrote:
>> Nope. Rules of proof are not stated in the formal language, but
>> generally given in English. Formulas in a language are just collections
>> of symbols put together according to particular rules. They can't tell
>> you how to derive formulas from other formulas, which is why you need
>> rules of proof.
>But even if rules of proof are "generally" given in a natural language,
>they can be given in a formal language, right?

Of course. But if we're talking about proofs for a formal language
L then the rules of derivation are expressed in a language _other_
than L.

>If they can't be given
>in a formal language, then automated theorem provers can't be created.

And if you think about it this shows exactly why the two are
different.

I might write a sentential-calculus proof checker in Python.
The formulas of sentential calculus will be part of the input
to that program; the derivation rules will be part of the
program itself.

>And whatever language (natural or formal) in which the rules are given
>is a metalanguage of sentential calculus, right?

That's a little vague. But never mind that, let's say it's right.
If so it shows that the derivation rules are _not_ formulas of
the sentential calculus! Because the sentential calculus is
_not_ a metalanguage for the sentential calculus.

>> ((p->q) ^ p) -> q) is a theorem of the sentential calculus, but this
>> theorem is not the rule of detachment.
>But can't the rule of detachment be stated in a formal language, and if
>it can, then wouldn't it have the same form as this theorem of the
>sentential calculus?

If so that does not show that they are the same thing!

>And furthermore, wouldn't its variables range over
>the same things over which the variables of the aforementioned theorem
>range (sentences in the sentential calculus)? If so, then I don't
>understand why the rule and the theorem aren't the same thing, and why
>the rule can't be written in sentential calculus, but has to be written
>in a different formal language. And the answer can't be "because the
>rule's variables range over sentences of the sentential calculus, and
>such variables only exist in the metalanguage", because then the
>aforementioned theorem couldn't be a theorem of the sentential calculus
>either.

Look. Here's a typical derivation rule:

"If the current line is B and there exist previous
lines of the form A -> B and A then the current
line is correct."

Now show me a formula in the sentential calculus that
says that.

Hint: You can't do that, because formulas in the
sentential calculus do not say anything. In particular
the tautology ((A -> B) and A) -> B does not mention
lines in a proof.


************************

David C. Ullrich
.

Relevant Pages