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

andrewspencers@xxxxxxxxx wrote:
>
> Tarski says on p. 47 of "Introduction to Logic and to the Methodology
> of Deductive Sciences",
> "Besides the rules of definition, of which we hve already spoken, we
> have other rules of a somewhat similar character, namely, the RULES OF
> INFERENCE or RULES OF PROOF. These rules, which must not be mistaken
> for logical laws, amount to directions as to how sentences already
> known as true may be transformed so as to yield new true sentences. In
> the proof carried out above, two rules of demonstration have been made
> use of: the RULE OF SUBSTITUTION and the RULE OF DETACHMENT (also known
> as the MODUS PONENS RULE)."
>
> He had previously already stated several laws of sentential calculus in
> both natural and formal language, including for example the law of
> hypothetical syllogism: "if p implies q and q implies r, then p implies
> r", i.e. "[(p->q) ^ (q->r)] -> (p -> r)" (prefixed by universal
> quantifiers for p, q, and r). He then says on p. 48, only in natural
> language,
> "The rule of detachment states that, if two sentences are accepted as
> true, of which one has the form of an implication while the other is
> the antecedent of this implication, then that sentence may also be
> recognized as true which forms the consequent of the implication."
> He doesn't state this rule in formal language, but wouldn't it be
> "[(p->q) ^ p] -> q"?
>
> So, if something like "[(p->q) ^ (q->r)] -> (p -> r)" is a logical law
> (i.e. law of sentential calculus), then why is "[(p->q) ^ p] -> q" not?

It's probably a hopeless task, but I will try another approach.
Consider this inference:

p -> q, p
---------- . . . . . . . . . . . . (1)
q

which (you claim) is somehow the same as the formula

((p -> q) ^ p) -> q . . . . . . . . (2)

One can describe what is going on here as follows. Take the premisses
("p -> q" and "p" in the example) and conjoin them with "^". Form the
conditional with that conjunction as the antecedent and the conclusion
as the consequent. Now (important result):

The inference is valid iff the conditional is tautological.

While that is true, there is a problem with the above procedure. How
will you form the conjunction if your language has no symbol for
conjunction (no "^", "&", or whatever)? There are sentential calculi in
which the only connectives are "~" (for "not") and "->", there is no
"^". I anticipate you replying that you will adopt this definition:

A ^ B is defined to be ~(A -> ~B).

But what if your language does not have "~" (or some symbol playing its
role)? There are such languages. Tarski himself studied the so-called
"pure implication" calculus in which the only connective is "->". In it
(1) is a valid rule and is adopted as a rule of inference. (2) isn't a
tautology, (2) isn't even well-formed.

Incidentally, there is a logical calculus in which the transformation
from (1) to (2) gets studied. It's called Gentzen's sequent calculus
and the transformation looks like this

p -> q, p => q
====================
(p -> q) ^ p => q
=====================================
=> ((p -> q) ^ p) -> q

The two steps from the stuff above the ===s to the stuff below them are
justified by rules in his calculus. I don't know any introductory texts
in which the sequent calculus is studied. There is

Kleene, S C "Introduction to metamathematics" Elsevier

but that is an advanced text. Gentzen's paper was translated in (two
numbers of) the American Philosophical Quarterly. Precise reference
somebody? It's also translated in

Gentzen, G; ed Szabo, M E "Collected Papers" North-Holland

[If you ever become interested in modal logic _and_ you like
\Lukasiewicz's notation, you might look at

Zeeman, J Jay "Modal logic" OUP

which has a very clear discussion of sentential sequent calculus
(classical and intuitionistic) but only as a prolegomenon to modal
logic.]

Another point, there are valid inferences of sentential calculus of this
kind

infinite set of formulae |- formula

(though Tarski probably doesn't discuss them) you can't turn that into

(conjunction of those infinitely many formulae) -> formula

because classical sentential calculus doesn't have infinite
conjunctions. [There is such a thing as infinitary logic (invented by
Scott and Tarski (ITMA)), but that's another story.]

--
I don't know who you are Sir, or where you come from,
but you've done me a power of good.
.

Relevant Pages

  • Re: Units as a checkable indicator of program errors
    ... scientists tracing through could probably pinpoint the line of ... our calculus of numbers. ... from Mathmatica no language supports units or unit checking, ... The Curl programming language has had built-in support for ...
    (comp.lang.misc)
  • Re: Alices exams
    ... As language is something you use and encounter every day, ... If learning an obscure and practically useless element of the arts, ... I'm not rubbishing maths in general, ... calculus to you personally, and frankly I wouldn't know calculus if it ...
    (uk.media.radio.archers)
  • Re: A higher math education
    ... my math goes up to Calculus I. So the Math ... >I know both English and Spanish very fluently. ... native language is not English are publishing in English. ...
    (sci.math)
  • Re: Cognitive Physics: the processing steps of thought
    ... It seems to me that as long as we use a language that does not ... expressed as a function word in lambda calculus. ... The '{' represents the defining word 'lambda', and '}' the end of the ...
    (comp.ai.philosophy)
  • Re: Cognitive Physics: the processing steps of thought
    ... It seems to me that as long as we use a language that does not ... expressed as a function word in lambda calculus. ... The '{' represents the defining word 'lambda', and '}' the end of the ...
    (comp.ai.philosophy)