Re: looking for a predicate hierarchy

"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 ?

Now, in
case you attempted to construct ~A from ~xVy using A=>0, that would be
equivalent to construction of 0.

No, not all. Such step is illegal because you logic language does not
include '0' connective, it's just ( FOUR, D , ^, /\, \/, => ), where
FOUR={0,1,_|_,T}, D={1, T}. The trivializing formula can produced with
just ^, => and /\. It's a legitimate formula !

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,+,*).

It is an arbitrary formula and its negation, not just a variable.

The
truth table of A/\notA is:

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

Right, that's just what prevents trivialization. Any arbitrary formula
and its negation produced using /\, \/ and ^ won't have the same effect
as using => would.


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


.