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 23 Dec 2009 17:58
Dear All

Lets define an operator M as follows:

M(A) := forall p ((A -> p) -> p)

In minimal logic we can show |- M A -> A
and |- exists p(p <-> A). Maybe in a weaker
logic, we can not show the above both,
but instead only some similar to:

exists p(p <-> A) <-> (M(A) <-> A)

But are we on the right track? 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?

Bye
From: William Elliot on 24 Dec 2009 05:01
On Wed, 23 Dec 2009, Jan Burse wrote:

> Lets define an operator M as follows:
>
> M(A) := forall p ((A -> p) -> p)
>
> In minimal logic we can show |- M A -> A

Oh? Then in classical logic you can show the same.

M(~p) <-> for all p (~p -> p -> p) left parenthesis convention
<-> for all p t
<-> t

Thus the claim, yields |- t -> ~p.

> and |- exists p(p <-> A). Maybe in a weaker
> logic, we can not show the above both,
> but instead only some similar to:
>
> exists p(p <-> A) <-> (M(A) <-> A)
>
> But are we on the right track? 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 still don't get it.
From: Jan Burse on 24 Dec 2009 07:06
William Elliot wrote:
> On Wed, 23 Dec 2009, Jan Burse wrote:
>
>> Lets define an operator M as follows:
>>
>> M(A) := forall p ((A -> p) -> p)
>>
>> In minimal logic we can show |- M A -> A
>
> Oh? Then in classical logic you can show the same.

Well yes, when we can show something in minimal logic,
then this is also valid in classical logic.

> M(~p) <-> for all p (~p -> p -> p) left parenthesis convention
> <-> for all p t
> <-> t
>
> Thus the claim, yields |- t -> ~p.

What you have done above is instantiating
A to -p. But I think the operator M has also
posed the restriction p not in A on it. So
substituting -p for A would not be valid.

This restriction is needed, otherwise my
derivation of |- M(A) -> A would not be valid
in minimal logic. The derivation uses the following
inference step:

G, C[p/D] |- E
------------------- (Left forall)
G, forall p C |- E

With C=((A -> p) -> p) and D=A. And it is assumed
that C[p/D] yields ((A -> A) -> A). But when
A contains p, then C[p/D] yields something else,
something ((A[p/A] -> A) -> A).

These technicalities have nothing to do with the
claim that it is a joke. See the other thread.

>> and |- exists p(p <-> A). Maybe in a weaker
>> logic, we can not show the above both,
>> but instead only some similar to:
>>
>> exists p(p <-> A) <-> (M(A) <-> A)
>>
>> But are we on the right track? 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 still don't get it.

This thread asks not anymore whether it is a
joke or not, but whether we can extend the russel
prawitz operator to comprehension of predicates.
So we cannot use QSAT anymore, we have to use some
logic which goes beyond propositional logic and of
course also beyond first order.

The naive set comprehension would be:

exists p forall y (y in p <-> A)

When using predicates some 2nd order logic we can formulate:

exists p forall y (p(y) <-> A)

You might easily identify the above two with a notion
of comprehension ("Aussonderung"). I do identify
with comprehension as well the following, which I might
call propositional comprehension:

exists p (p <-> A)

Propositional comprehension is not problematic. It is
derivable in minimal QSAT, and I don't see that it causes
any antinomies. Predicate comprehension on the other hand
is very problematic. Lets assume I have a very general
second order logic with predicate comprehension as above
as an axiom.

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

It then leads to the insight that this general 2nd order logic
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)
|- Ep Ay(p(y) <-> -y(y)) Ep Ay(p(y) <-> -y(y)) |- f
---------------------------------------------------
|- f

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.

But what raised my interested in the Russel Prawitz operator
was that it gave way to a reformulation of comprehension.
Since the equality I stepped over said:

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?

I would say no, wrong track. Guess why?

Bye
From: William Elliot on 25 Dec 2009 04:34
On Thu, 24 Dec 2009, Jan Burse wrote:
> William Elliot wrote:
>> On Wed, 23 Dec 2009, Jan Burse wrote:
>>
>>> Lets define an operator M as follows:
>>>
>>> M(A) := forall p ((A -> p) -> p)

>> M(~p) <-> for all p (~p -> p -> p) left parenthesis convention
>> <-> for all p t
>> <-> t
>>
>> Thus the claim, yields |- t -> ~p.
>
> What you have done above is instantiating
> A to -p. But I think the operator M has also
> posed the restriction p not in A on it. So
> substituting -p for A would not be valid.

M(A) means
for all p, (A -> p -> p) left parenthesis convention
for any p not free in A.

> This restriction is needed, otherwise my
> derivation of |- M(A) -> A would not be valid
> in minimal logic. The derivation uses the following
> inference step:
>
> G, C[p/D] |- E
> ------------------- (Left forall)
> G, forall p C |- E

Huh? No.
G, C[p/D] |- E
-------------------
G, some p C |- E

Any prelude about free and bound variables?

In classical logic, M(A) -> A.
In natural negation, M(A) -> ~~A.

> With C=((A -> p) -> p) and D=A. And it is assumed
> that C[p/D] yields ((A -> A) -> A). But when
> A contains p, then C[p/D] yields something else,
> something ((A[p/A] -> A) -> A).

>>> and |- exists p(p <-> A). Maybe in a weaker
>>> logic, we can not show the above both,
>>> but instead only some similar to:
>>>
>>> exists p(p <-> A) <-> (M(A) <-> A)

The equivalence is trivial as both sides are theorems.

As A <-> A, if p not free in A, then exists p(p <-> A).
As A -> (A -> p -> p), A -> M(A) and from above, M(A) <-> A.

>>> But are we on the right track?

To what town are you going?

>>> 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?
>
> So we cannot use QSAT anymore, we have to use some
> logic which goes beyond propositional logic and of
> course also beyond first order.
>
QSAT?

> The naive set comprehension would be:
>
> exists p forall y (y in p <-> A)

> 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))

> You might easily identify the above two with a notion
> of comprehension ("Aussonderung"). I do identify
> with comprehension as well the following, which I might
> call propositional comprehension:
>
> exists p (p <-> A)
>
> Propositional comprehension is not problematic. It is
> derivable in minimal QSAT, and I don't see that it causes
> any antinomies. Predicate comprehension on the other hand
> is very problematic. Lets assume I have a very general
> second order logic with predicate comprehension as above
> as an axiom.
>
It's extremely self referent.

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

> It then leads to the insight that this general 2nd order logic
> 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)

> |- Ep Ay(p(y) <-> -y(y)) Ep Ay(p(y) <-> -y(y)) |- f
> ---------------------------------------------------
> |- f
>
> 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.
>
Reveiw the various solutions to Russel's paradox.

> But what raised my interested in the Russel Prawitz operator
> was that it gave way to a reformulation of comprehension.
> Since the equality I stepped over said:
>
> 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.)

> 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.
From: Jan Burse on 25 Dec 2009 07:48
William Elliot wrote:
>> G, C[p/D] |- E
>> ------------------- (Left forall)
>> G, forall p C |- E
>
> Huh? No.
> G, C[p/D] |- E
> -------------------
> G, some p C |- E
>
> 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

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.


>>>> 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?
>>
>> So we cannot use QSAT anymore, we have to use some
>> logic which goes beyond propositional logic and of
>> course also beyond first order.
>>
> QSAT?

QSAT = satisfaction problem for QBF, QBF =
quantified boolean formulae.
The acronym QSAT is derived from the acronym
SAT, SAT is more theoretical computer science
terminology.

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

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

>> 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
 |  Next  |  Last
Pages: 1 2 3
Prev: MADNESS IN EINSTEINIANA
Next: concept of Consistency as a variable, not a constant for math and physics #263: Correcting Math