Re: "Theorem" in Mendelson ?




Question wrote:
Also, Mendelson makes the non-necessity that proofs be derived from
axioms on the same page I quoted ("Introduction ot Mathematical
Logic," 4th ed. p. 34-5) where he reiterates, but even more clearly:

"A wf C is said to be a consequence in L of a set T [no better symbol
for gamma] of wfs if and only if there is a sequence B_1, ..., B_k of
wfs such that C is B_k and, for each i, either B_i is an axiom or B_i
is in T, or B_i is a direct consequence of some rule of inference of
some of the preceding wfs in the sequence. Such a sequence is called a
proof (or deduction) of C from T."

Yes! That is exactly what I said I bet Mendelson provides. That is
DIFFERENT from 'proof in L'.

He is given two definitions, each for a different relation. Or we can
even do it four ways:

(1) A proof of in L

(1a) A proof of C in L

(2) A proof in L from T

(2a) A proof of C in L from T

And (1) is just 'a proof in L from the empty set'

And (1a) is just 'a proof of C in L from the empty set'

That is all very standard treatment and Mendelson gives it just fine.
You can't just gloss over the difference when he talks about a proof in
L and also talks about a proof in L from T.

There is no contradiction or problem with Mendelson. You just have to
keep in mind the dfiference: proof in L vs. proof in L from T.

And my earlier meta-proof that only tautologies may appear on lines in
'a proof in L' is correct. And your rebuttal was incorrect, since, for
example, your proposed counterexample had B_1 that is not an axiom and
does not come from previous lines of the proof by a rule of inference.

On the other hand, your example IS a proof in L from T, where T is the
set of premises, i.e., in this instance, {B_1}. That is, your
non-tautologous B_1 is okay as a line in a proof of L from T, since B_1
is a member of T. But your non-tautologous B_1 is not a okay as a line
in a proof from L, since in just a proof from L there IS NO T from
which to draw premises and put them on lines in a proof.

A proof in L is something ensured to generate just tautologies.

A proof in L from T is something ensured to generate valid arguments -
conclusions (that might not be tautologies) that are tautologically
implied by premises (that might not themselves be tautologies).

And a proof in L is just a proof in L from the empty set.

Anyway, I see from your next paragraph (not quoted here) that you do
understand something of this difference. But I want to leave my remarks
here since I think they might help to enscapsulate this crucial
difference.

MoeBlee

.