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: William Elliot on 26 Dec 2009 02:53 On Fri, 25 Dec 2009, Jan Burse wrote: > 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) > "x in u" is not well formed/defined. >> 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. That is similar to NBG set theory which I described previously. Set(y) := exists p p(y) exists p forall y (y in P <-> A(y) & Set(y))
From: William Elliot on 26 Dec 2009 02:55 On Fri, 25 Dec 2009, Jan Burse wrote: > 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. > That does not allow construction of sets that contain sets. > 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) I've no knowledge of Russel Prawitz's modal operator. > 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 26 Dec 2009 06:03 William Elliot wrote: >> 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. >> > That does not allow construction of sets that contain sets. Thats why it is called 2nd order, and not higher order logic. >> exists (p <-> A) <-> (M(A) <-> A) > > I've no knowledge of Russel Prawitz's modal operator. Me neither, that's why i am posting. I stepped over it in the the following paper: The Russell-Prawitz Modality (1999) by Peter Aczel http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.5294 Proposition 22 raised my interest. Bye
From: William Elliot on 27 Dec 2009 06:18
On Sat, 26 Dec 2009, Jan Burse wrote: > William Elliot wrote: >>> 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. >>> >> That does not allow construction of sets that contain sets. > Thats why it is called 2nd order, and not higher order logic. > >>> exists (p <-> A) <-> (M(A) <-> A) >> >> I've no knowledge of Russel Prawitz's modal operator. > > Me neither, that's why i am posting. I stepped over it in the > the following paper: > > The Russell-Prawitz Modality (1999) > by Peter Aczel > http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.5294 > > Proposition 22 raised my interest. > I've not the facilites to read pdf and ps files. |