Re: looking for a predicate hierarchy

"Dmitry A. Kazakov" <mailbox@xxxxxxxxxxxxxxxxx> wrote in
news:jl3iup5zix87.d4njwfc8n3h1.dlg@xxxxxxxxxx:

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.

If => is not a connective, then you lose ability to say for example "if it
rains we stay at home; it rains, so we stay at home". So without the
most basic rule of inference, how can you call your system a logic at all
?


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


Yhis trivializes your logic.

#> [ 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 _|_

This also trivializes your logic: (A->A) /\ ^(A->A has an empty model.

-> [ 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 _|_


For this, both the inference rule and the deduction theorem do not hold,
it's the same as if you did not define any implication.


=> 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.


.