Re: looking for a predicate hierarchy

On Mon, 25 Dec 2006 15:48:59 +0100 (CET), V.J. Kumar wrote:

"Dmitry A. Kazakov" <mailbox@xxxxxxxxxxxxxxxxx> wrote in
news:dlxa9cude3z$.1eaoremttucpv$.dlg@xxxxxxxxxx:

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.

Yes, it's a reasonable requirement to forbid using '~' directly. After
all, you can just define your '=>' with a truth table. Alas, it does
not save the logic from trivialization. Just substitute (A=>A) /\ ^(A=>
A) for F/\ not F in the Lewis proof, where F was an arbitrary formula
and its negation, not just a variable. '^' is of course the standard
negation -- you cannot forbid that, can you ?

No, I can, reasoning about reasoning were suspicious anyway. So => is not a
connective.

BTW, I also saw somewhere a third implication, let's denote it #>. To
compare all three:

=> [ ~xVy ]
T 0 1 _|_
--------------------
T 1 _|_ 1 _|_
0 1 1 1 1
1 T 0 1 _|_
_|_ T T 1 1

#> [ like => when T<->0 and _|_<->1 for the premise ]
T 0 1 _|_
--------------------
T 1 1 1 1
0 1 _|_ 1 _|_
1 T T 1 1
_|_ T 0 1 _|_

-> [ not xVy, like => when T<->_|_ for the premise ]
T 0 1 _|_
--------------------
T T T 1 1
0 1 1 1 1
1 T 0 1 _|_
_|_ 1 _|_ 1 _|_

=> is transitive and reflexive.

#> and => are equivalent upon "optimistic" inference (all paths where
implication yields either 1 or _|_).

not xVy looks strange. It has: T implies _|_, but not T, which is very
counterintuitive. Especially because _|_ implies T. So T->_|_ /\_|_->T, but
not T->T. That is the price for having T on the diagonal.

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