Re: looking for a predicate hierarchy

On Sun, 24 Dec 2006 16:59:18 +0100 (CET), V.J. Kumar wrote:

"Dmitry A. Kazakov" <mailbox@xxxxxxxxxxxxxxxxx> wrote in
news:1hqbtgcvxtpln.kwy2q4wiyosc.dlg@xxxxxxxxxx:

Your argumentation seems to be based on an assumption that

(A /\ not A) => B

were somehow equivalent to

{ A, not A } |= B

but that's wrong.

It is not wrong thanks to the deduction theorem, but let's not dwell on
it. Instead, let's forget about models, trivialization and stuff.
Here's a simple proof for simple minds courtesy of Lewis and ? circa 1930
that any formula in classic logic can be proved given a contradiction:

1. A and not A
2. A -- from step 1
3. A or F -- where F an arbitrary formula
4. not A -- from step 1
5. F -- because of 3 and 4

Step 5 is known by a weird name of disjunctive syllogism, given the
knowledge that (A or F) hold *and* that A does not, surely F must hold.
The proof shows that admitting contradiction trivializes classic locgic.

In a logic that handles contradiction step 5 is invalidated by allowing A
and ^A to hold at the same time thus making step 5 incorrect -- F may or
may not hold. By introducing your '~' connective, you revive step 5, now
~A and A cannot hold at the same time as can easily be seen from the '~'
truth table. So the formula (A and ~A) trivializes your logic.

Aha, but ~ is not allowed for use [*]. ~A is not a formula. Now, in case
you attempted to construct ~A from ~xVy using A=>0, that would be
equivalent to construction of 0. So you are back to where you started from,
before the step 1. It is true that 0=>F, but that's not yet trivial. To
show the logic trivial you need 0. But 0 cannot be constructed using an
arbitrary A, not, /\ (as well as V,+,*). The truth table of A/\notA is:

A A/\notA
0 0
1 0
_|_ _|_ -- non-trivial
T T - non-trivial

---------------
* The logic is intuitionistic in the sense that ~, which is a
set-complement in {0,1}^2, is thrown away. So ~A cannot be obtained from A.

--
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de
.