There has been quite a lot of interest in the IKL logic developed in the IKRIS project. The properties of this logic are by no means yet fully determined, so we are still exploring in some of these areas.
The purpose of this page is to collect together a number of on-going observations, examples, comments and generally stuff about IKL which may be of wider interest.
Some IKL inconsistencies.
These are inconsistent:
(= L (that (not (L)))) (cl-comment 'Liar paradox')
(forall (x)(iff (R x)(not (R R)) )) (cl-comment 'Russell paradox')
(forall (x)(iff (K x)
(= x (that (forall (y)(if (K y)(not (y)) ))) ) )) (cl-comment 'Kripke paradox')
(forall (x)( ( that (not (x)) ) ))
(( that (forall (x)(not (x))) ))
But note that (forall (x)(not (x))) is consistent ! (Consistent in CL, in fact.)
So this last pair is a firm counterexample (given the current model theory, anyway) to the universal applicability of the T-condition (the equivalence of ((that S)) and S for any WF sentence S) the point being that the former, but not the latter, requires a proposition to exist with the T-conditions of the sentence, ie true when the sentence is; the second manages to be satisfiable by allowing all propositions to be false, but when we have the T-conditions on one of them, we would get a paradoxical situation.
We could declare by fiat that a true proposition must exist in every IKL model, but that seems like a get-out. And it would allow CL entailments that weren't IKL-valid :-((
Are there any other ways to falsify T? I can't think of any, but then I didnt think of this one until recently.
Perhaps more constructive, what 'reasonable' conditions on S would exclude this case? One obvious one is to not allow a quantification over propositions - a pattern (quantifier (p)(... (p) ...)) - inside any proposition name. That seems reasonable, and it would also exclude the Kripke case. Still, I wonder if there might not be a way to sneak past this and still get the meat of the examples.
An interesting entailment pattern
Given an IKL sentences S1 containing a proposition name (that S2), this is a valid entailment:
S1 |= (exists (x)(and S1[x/(that S2)] (iff (x) S2) ))
The interest of this is that S1[x/(that S2)] has one fewer proposition name in it than S1 does, so by iterating we can get back to a sentence entirely written in CL which must be satisfied in every model of S1. Call this the CL-reduction of S1, reduct(S1).
This might provide a route to constructing IKL interpretations from CL interpretations (?)
More on the universal denial
(( that (forall (x)(not (x))) ))
is especially interesting. It is false in all models; but the interesting part is, that one cannot even construct an interpretation for it at all unless there are at least two items in the universe. If U is a singleton {i} then the propname ( that (forall (x)(not (x))) ) must denote it (since it is required to denote something), and then we have a paradoxical situation since if <> is in rel(i) then (forall (x)(not (x))) must be true, by T, so <> must not be in rel(i); and if it is not, then also by T, there must be something in U with <> in its relational extension; but i is the only member of U. So a singleton universe here breaks the T-condition.
Maybe we should not be worried about this, since this example already breaks T. Still, it bothers me.
Can one construct an example which requires the universe to have three members? I don't think so, in fact. The pressure in this example comes from the need to have two truth-values assigned to propositions in the universe.
Following the construction in the previous section gives this as the CL-reduction:
(exists (y)(and (y) (iff (y) (forall (x)(not (x)) )) ))
which is, of course, unsatisfiable, but also on the face of it seems to only require one thing in the CL universe. Why is this simply unsatisfiable, while the denial itself is more paradoxical? On the face of things they seem to have the same essential content. Its because in this case we merely have an existential, whereas in the denial case there is a name, which must denote. If proposition names could fail to denote, that case would be as harmless as this is. In fact, if we modify the definition of reduction to use a skolem name rather than an existential, we might get exactly the same phenomenon...
(and (A)(iff (A)(forall (x)(not (x)) ))) ??
Well, if U={i} then A denotes i, and if rel(i) contains <> then the second conjunct is false and if it does not then the first one is. So again, this is no more paradoxical than (and p (not p)). Damn. WHY is the folded case so troublesome when the CL reduction is so clear?
Because the reduction allows the 'iff' to be simply false, which corresponds to allowing the T condition to relax at that point. Ah yes. We only get back from the CL interpretation to an IKL one if all the 'iff's are true, because they embody the T-condition. Put another way, there are two ways for the reduction to fail: by the original sentence being false, or by the T-condition being unsatisfiable in that model.
So, to directly construct an IKL interpretation of S from a CL interpretation I of reduct(S), we need it to be the case that all the proposition biconditionals in reduct(S) are true in I. So we need to be circumspect when reduct(S) is false in I.
Q: Can the conjunction of the prop. biconditonals be itself inconsistent in CL?? That would provide us with a paradox-factory :-) I thikn not, in fact, but thats only a very vague intuition.