Russel Prawitz Operator, the interesting Case
in [Logic]
|
Prev: MADNESS IN EINSTEINIANA
Next: concept of Consistency as a variable, not a constant for math and physics #263: Correcting Math
From: Jan Burse on 25 Dec 2009 07:57 Jan Burse wrote: >> (p <-> q) <-> for all y (p(y) <-> q(y)) >> >> (Tangle prelude about bound and free variables referred to committee.) > > You can use <-> in the above, but I would rather > prefer = in the above. Since p and q are predicates > and thus they cannot be used in propositional positions. > So we would have: > > p = q <-> for all y (p(y) <-> q(y)) > > Does this give me comprehension? Do you claim that? > I guess no and I think it is independent of > comprehension, its just some extensionality. Actually the above would give extensionality and congruence. Extensionality is the following: for all y (p(y) <-> q(y)) -> p = q Congruence is the following: p = q, p(y) -> q(y). But we can ask for predicate comprehension even in a logic that does not have equality "=" at all. Comprehension is just question of existence of certain predicates: exists p forall y (p(y) <-> A) Bye
From: William Elliot on 25 Dec 2009 09:30 On Fri, 25 Dec 2009, Jan Burse wrote: > William Elliot wrote: >>> G, C[p/D] |- E >>> ------------------- (Left forall) >>> G, forall p C |- E Ok, I get it. >> Any prelude about free and bound variables? > > Well yes and no. We have a (Left forall) and > a (Left exists) rule in minimal QSAT. Here I > repeat the minimal QSAT quantifier rules (already > posted in the joke thread): > > G, A[p/B] |- C G |- A, p not in G > ------------------ (Left forall) --------------- (Right forall) > G, forall p A ]- C G |- forall p A > > G |- A[p/B] G, A |- C p not in G, C > ---------------- (Right exists) ------------------ (Left exists) > G |- exists p A G, exists p A |- C > > So the (Left exists) does not involve a substitution > of a propositional variable for a propositional formula. > Only the (Left forall) and the (Right exists) does. > > The (Left forall) comes up when I proof |- M(A) -> A. > > -------- (Id) > A |- A > --------- (Right ->) -------- (Id) > |- A -> A A |- A > ----------------------------------- (Left ->) > (A -> A) -> A |- A > ----------------------------- (Left forall) > forall p((A -> p) -> p) |- A > -------------------------------- (Right ->) > |- forall p((A -> p) -> p) -> A > Ok. > The side condition is needed in moving from (A -> p) -> p > to (A -> A) -> A. Its not part of the inference rule > (Left forall) itself. It is part of what we expect the > propositional variable for propositional formula substitution > to yield. > >>>>> exists p(p <-> A) <-> (M(A) <-> A) >> >> The equivalence is trivial as both sides are theorems. > Yes, thanks. That is what makes it a joke for me. > It's not needed, useless and since M(A) <-> A, M(A) is superfluous. >>>>> But are we on the right track? >> To what town are you going? > LoL. > >>>>> What if we want to have an alternative formulation for comprehension >>>>> with parameter, will something as follows work: >>>>> >>>>> exists p forall y(p(y) <-> A) <-> (?? A <-> A) >>>>> >>>>> I have doubts. Guess why? I know nothing about QSAT and SAT. >>> When using predicates some 2nd order logic we can formulate: >>> >>> exists p forall y (p(y) <-> A) >> >> exists p for all y (p(y) <-> A(y)) > > Yes, of course you can also write it like this. > A(y) and especially A need some explaination about bound and free. >>> The second order logic would be general in the sense that >>> predicates can be arguments to other predicates. Thus together >>> with the comprehension axiom, we would have for comprehension >>> from A=-y(y): >>> >>> exists p forall y(p(y) <-> -y(y)). >>> >> Russel's paradox. > > Yes, that is what one can create. > >>> It then leads to the insight that this general 2nd order logic B>>> is inconsistent. Because we can easily derive, even in >>> minimal logic: >>> >>> ... >>> --------------------- >>> x(x) <-> -x(x) |- f >>> ------------------------- (Left forall) >>> Ay (x(y) <-> -y(y)) |- f >>> --------------------------- (Left exists) >> >> No. As x() is higher type than (x), >> y can't be substituted for both x() and (x) > > Yes, that would be one of the restrictions that would > exclude russel's paradox and the like. See below: > >>> One remedy would be to disallow the formation of expressions >>> such as -y(y). So proper 2nd order logic would be two sorted, >>> and a formation of -y(y) would not be possible. Another remedy >>> would be to change comprehension itself, i.e. side condition >>> on y and/or p. > y(y) it's self would be not allowed. However there's the problem with replacing x with y in y(x) > Reveiw the various solutions to Russel's paradox. > > Yes, if Russel's paradox were at stake. But it is not > here. See below: > >>> exists p(p <-> A) <-> (M(A) <-> A) >>> >>> But it is only an equality for propostional comprehension. Can >>> we do something similar also for predicate comprehension? Can >>> it be expressed somehow with a modal operator? >>> >> (p <-> q) <-> for all y (p(y) <-> q(y)) >> >> (Tangle prelude about bound and free variables referred to committee.) > > You can use <-> in the above, but I would rather > prefer = in the above. Since p and q are predicates > and thus they cannot be used in propositional positions. > So we would have: > > p = q <-> for all y (p(y) <-> q(y)) > > Does this give me comprehension? Do you claim that? > I guess no and I think it is independent of > comprehension, its just some extensionality. ZF comprehension in 2nd order logic. forall u some s forall x (s(x) <-> A(x) & u(x)) >>> I would say no, wrong track. Guess why? >> >> You're forcing unlimited self reference in the same way that >> Russel and other early set theorist were forcing unlimited >> self reference. > > No, No, Russel's paradox is not really at stake here. Only > question whether we can characterize predicate comprehension > with some russel prawitz operator or not. > > Note the difference between having a comprehension axiom, > which we have seen rendering the calculus inconsistent, > if we are not careful, and a characterization theorem, > which would not do any harm at all. If we have a characterization > theorem: > > predicate comprehension <-> russel prawitz operator formulation > > We do not postulate predicate comprehension. And we might > even have such a theorem as a bove in the precence of > Russel's paradox. > > Bye >
From: William Elliot on 25 Dec 2009 09:42 On Fri, 25 Dec 2009, Jan Burse wrote: > Jan Burse wrote: >>> (p <-> q) <-> for all y (p(y) <-> q(y)) >>> >>> (Tangle prelude about bound and free variables referred to committee.) >> >> You can use <-> in the above, but I would rather >> prefer = in the above. Since p and q are predicates >> and thus they cannot be used in propositional positions. >> So we would have: >> >> p = q <-> for all y (p(y) <-> q(y)) >> >> Does this give me comprehension? Do you claim that? >> I guess no and I think it is independent of >> comprehension, its just some extensionality. > > Actually the above would give extensionality > and congruence. Extensionality is the following: > > for all y (p(y) <-> q(y)) -> p = q > for all y (p(x,y) <-> q(y)) -> (p(x) = q)? > Congruence is the following: > > p = q, p(y) -> q(y). > > But we can ask for predicate comprehension even > in a logic that does not have equality "=" at > all. Comprehension is just question of existence > of certain predicates: > > exists p forall y (p(y) <-> A) forall u exists p forall y (p(y) <-> A(y) & u(y)) forall u exists p forall y (p(y) <-> (A & u)(y)) Either that or use stratisfication or exists p forall y (p(y) <-> A(y) & set(y)) exists p forall y (p(y) <-> (A & set)(y)) set(x) = exists a a(x).
From: Jan Burse on 25 Dec 2009 10:33 William Elliot schrieb: > ZF comprehension in 2nd order logic. > > forall u some s forall x (s(x) <-> A(x) & u(x)) > Ok, I didn't know this formulation, with the conjoined u(x). But I think comprehension is ok in minimal 2nd order. We do not need to do anything about it, since the following axiom would also work in typed minimal second order logic: exists p forall y (p(y) <-> A), with the following provisio: p : i -> o (p is a variable ranging over predicates) y : i (y is a variable ranging over individuals) p does not occur in A. You cannot do Russels's paradox in the above. Its not the general 2nd order logic where it was allowed to form -y(y). Since it is 2nd order logic with two sorts, than the above seems not to be problematic. Prawitz even mentions cut-elimination for it. But again question is not about tweeking the a comprehension axiom, but about obtaining a theorem that relates predicate comprehension to some Russel Prawitz like modal operator, like it was done for propositional comprehension: exists (p <-> A) <-> (M(A) <-> A) Can we do (currently ignoring the joke) something similar for predicate comprehension, thus can we fill in the blank ?? in the following: exists p forall y (p(y) <-> A) <-> (?? A <-> A) The blank ?? is here: (>>>??<<<< A <-> A). This I consider the interesting case of Russel Prawitz Operator. And my claim is, that although the question for a Russel Prawitz Operator is a legitimate interesting one, I think we will not be able to obtain such an operator for some grounds. Guess what grounds? (Its not the Russel's Paradox) Bye
From: Jan Burse on 25 Dec 2009 10:48
Jan Burse schrieb: > William Elliot schrieb: > >> ZF comprehension in 2nd order logic. >> >> forall u some s forall x (s(x) <-> A(x) & u(x)) >> Ok, I see what you want to do. ZF, forall u exists s forall x(x in s <-> A(x) & x in u) > But I think comprehension is ok in minimal 2nd order. > We do not need to do anything about it, since the > following axiom would also work in typed minimal > second order logic: > > exists p forall y (p(y) <-> A), > > with the following provisio: > > p : i -> o (p is a variable ranging over predicates) > > y : i (y is a variable ranging over individuals) > > p does not occur in A. > Look, since the stuff is typed, we have implictly an u in second order logic. Its the u representing the i. So although we write in typed 2nd order logic: exists p forall y (p(y) <-> A(y)) This would be: exists p forall y (y in p <-> A(y) & y in i) Which is an instance of the ZF comprehension schema (forall u instantiated by i). So in effect p will be subset of i, where i is the sort of the individuals. Bye |