paradoxes and deductive theorem again

[iepos@tunes.org]

Greetings TUNESters...

I'm bringing up the deductive theorem (and paradoxes) once again because
the issue still seems unresolved to me. It is clear that in the presence
of an implication "->" with modus ponens that it is unsafe to have
these axioms without restriction:

I: p -> p
B: (p -> q) -> (r -> p) -> r -> q
C: (p -> q -> r) -> q -> p -> r
W: (p -> p -> q) -> p -> q
K: p -> q -> p

As was mentioned awhile last time I think, the W axiom seems to be the
most dangerous (yet it cannot be given up unless useful things like
"(x -> y -> z) -> (x -> y) -> x -> z" are also, from which W follows
by C and I).

Anyhow, it was suggested that the problem be solved by restricting
the axioms to cases in which it is known "p", "q", and "r" are 
"propositions". This seems reasonable, but it is not clear to me
how one can judge if something is a "proposition". Can someone
give an intuitive way to judge?

I'm afraid somebody is going to answer, "Well, that's easy. It's a 
proposition iff its not self-referential; after all, all the paradoxes 
come from self-referential statements, right?", but I don't think that
is satisfactory. For consider this dialogue:

Socrates: What Plato is about to say is not true.
Plato: Socrates has spoken truely.

This is sort of a drawn-out liar's paradox, but it is significant
in that it apparently does not involve a self-referential statement.
Someone analyzing the situation may argue this way. Socrates' statement
isn't self-referential, so we can use the deductive theorem on it.
So we "suppose" that Socrates' statement is true. Under this
assumption, this means that Plato's statement (that Socrate's statement
was true) is not true; this is a contradiction, so our assumption
must not have been true. So, Socrates is not telling the truth.
So, Plato is not not telling the truth, and thus Socrates is not not
telling the truth (contradictory with what we previously proved,
that Socrates is not telling the truth). So, we proved a contradiction;
this seems to indicate that the deductive theorem requires more care
than one might have thought. And the problem does not stem from
"not"; a similar problem would occur if Socrates said 
"If what Plato is about to say is true, then Z"; it would be possible
by similar reasoning to prove Z, no matter what it is (if a contradiction 
does not bother you, this should).

Another question: if the deductive theorem is restricted to some sort
of proposition-hood, is it necessary that the assumption _and_ the
hypothetically proven thing both be propositions, or is it only necessary 
for the assumption. I think this may depend on the way "proposition-hood"
is formulated, but I'm guessing that only the assumption will need
the restriction.

So, what is in common among the paradoxes, if not self-reference?
Well, Socrates and Plato's statements reference each other; this
seems to suggest that mutual reference is as bad as self-reference.
A solution that suggests itself is some sort of odd "type system"
whereby every considered object (including statements) is assigned
a "level" (maybe a natural number); the level assigned does not matter 
except it must be greater than or equal to the level of all the objects it 
is constructed from (defined in terms of); this would rule out mutual 
reference since two levels could not both be greater than each other.
However, we don't really want to rule out mutual reference entirely
(as other odd theories based on this kind of type system have);
we are only considering restrictions for the deductive theorem. So,
perhaps we would only require the assignment of a level on an object
as a condition for use as an assumption in the deductive theorem.

This solution does not really seem like a very good one to me. In
particular, it seems to require a logic system on top of the logic
system to determine if assignment of a level is possible. Also,
what should happen in the case that a referenced entity has no available
definition in the system (it is taken as a primitive); should it be
assumed that the entity is not "constructed" from one of the objects
already introduced (which would yield a mutual reference)? I don't
think so (this would probably allow the restriction on the deductive
theorem to be worked around entirely).

Hmm... I'm getting sleepy, and I wish these silly paradoxes would just
go away, or that someone could just explain precisely what is wrong
about our reasoning and why the deductive theorem usually works
but not always. Maybe I should just give up, saying: "who cares about the
deductive theorem? there's no such thing as truth anyway, it's all just 
theories; everyone's known that since Godel" (;)). Anyhow, at least,
I'd like to know about the deductive theorem for practical purposes...
in what cases it is useful to postulate it. 

Comments... ?

Oh, and by the way, that computing system thing I was working on
earlier is still coming, at least in my head. I started coding in
C and almost went insane and have started working in Java (for lack
of anything better) since I don't particularly care about speed.
Still I haven't decided how the system will handle "conditional commands"
and conjunctions of commands ("do this and this, I don't care what
order") and disjunctions of commands ("do this or this, I'm not telling
you which I want") and such; I planned on using an operator to chain
commands together in a sequence ("do this, and then do this"), but there is 
clearly a correspondence between logical operators connecting statements 
yielding new statements and operators connecting commands yielding new 
commands (so it would make sense to reuse the logical operators in some
way). I've also been considering whether I should adopt the convention
that commands all have results (a getchar-like command when executed
would result in the read character; other commands might result in
tuples of results; some might not have meaningful results); on the
other hand, it would probably be more sophisticated to drop that
funny paradigm and instead realize that commands usually have
specific executions which may have various properties (including "results");
commands that need depend on the behavior of previously executed commands 
could refer to the properties of their executions. The "chaining" construct
that connects two commands together ("do one; when finished do the next")
will probably take an abstraction over a command as the second parameter,
which will be applied to the execution of the first when it is executed
(a second command is naturally described as a function of the behavior
of the previous)... anyway, this is all tentative, but i'm going to
decide sometime, and will probably end up doing it both ways.
One is probably not going to work (actually, they're probably
both not going to work).

well, i think i've babbled enough.

- iepos