Science and Technology news... :: View topic

herbzet · Guest

Daryl McCullough wrote:
[quote]
herbzet says...
Similarly for 'and'. We don>t define it; we give some axioms
for using it, and away we go. Some things must be accepted as
given just to kickstart the whole enterprise.

Yes, that>s right.
[/quote]
As I mentioned in the parent post to the one you are reponding to,
we may use other operators as primitive rather than "and". Just
want to be clear about that.

[quote]However, it is interesting that in
some systems of higher-order logic, the only operators
that need to be introduced is universal quantification
and implication.
[/quote]
After a very quick glance, I>m not sure how it all works:

[quote]The other logical operators are then definable. For
example:

A and B == forall propositions C, (A implies (B implies C)) implies C
[/quote]
If C is false (I>ll use '0' for 'false'), then (A -> (B -> C)) -> C is
equivalent to A & B:

(A -> (B -> 0)) -> 0 = ~(A -> (B -> 0))
= ~(A -> ~B)
= A & B

but if C is true (I>ll use '1') then (A -> (B -> C)) -> C is not
equivalent to A & B:

(A -> (B -> 1) -> 1 = 1 (because everthing implies a true proposition)
=/= A & B

so I>m confused.

[quote]A or B == forall propositions C,
((A implies C) implies ((B implies C) implies C))
[/quote]
(B -> C) -> C is itself equivalent to B v C, so I don>t see the need
for the more complex formulation.

[quote]not A == forall propositions C, A implies C
[/quote]
Or alternatively,

not A == A -> forall propositions C, C.

In Polish notation, PIpp, is, as Prior says, an interesting
candidate for Standard False Proposition.

If we have negation as primitive, we can get the other Boolean functions
with just conjunction as also primitive (or just disjunction).

[quote]exists x . B(x)
== forall propositions C, (forall x, B(x) implies C) implies C
[/quote]
My brain just gave out.

--
hz

Daryl McCullough · Guest

herbzet says...

[quote]Daryl McCullough wrote:

After a very quick glance, I>m not sure how it all works:

The other logical operators are then definable. For
example:

A and B == forall propositions C, (A implies (B implies C)) implies C

If C is false (I>ll use '0' for 'false'), then (A -> (B -> C)) -> C is
equivalent to A & B:

(A -> (B -> 0)) -> 0 = ~(A -> (B -> 0))
= ~(A -> ~B)
= A & B

but if C is true (I>ll use '1') then (A -> (B -> C)) -> C is not
equivalent to A & B:

(A -> (B -> 1) -> 1 = 1 (because everthing implies a true proposition)
=/= A & B

so I>m confused.
[/quote]
I didn>t say that "(A -> (B -> C)) -> C" is equivalent to A&B,
I said "Forall C, (A -> (B -> C)) -> C" is equivalent to A&B.

[quote]A or B == forall propositions C,
((A implies C) implies ((B implies C) implies C))

(B -> C) -> C is itself equivalent to B v C
[/quote]
How would you prove that they are equivalent? Using
what rules of inference? You can prove it using the
law of excluded middle, but that is itself expressed
in terms of "or". So that would be circular.

[quote]so I don>t see the need for the more complex formulation.
[/quote]
It>s not more complex. The definition
"Forall C, ((A -> C) -> (B -> C)) -> C"
is exactly what you need in order to reason about disjunctions.
The rule for reasoning about disjunctions is this:

If you know (A or B), and you are trying to prove C,
then you can do a "case split":

1. Prove C follows from A (That is, prove A -> C)
2. Prove C follows from B. (That is prove B -> C)
3. Therefore, C follows from A or B.

The second-order definition of "or" exactly captures this
property.

[quote]not A == forall propositions C, A implies C

Or alternatively,

not A == A -> forall propositions C, C.
[/quote]
Yes, that>s equivalent.

[quote]In Polish notation, PIpp, is, as Prior says, an interesting
candidate for Standard False Proposition.

If we have negation as primitive, we can get the other Boolean functions
with just conjunction as also primitive (or just disjunction).

exists x . B(x)
== forall propositions C, (forall x, B(x) implies C) implies C

My brain just gave out.
[/quote]
It>s not that hard. If C is any statement that does not involve
the variable x, then

"exists x . B(x)" -> C

is logically equivalent to

"forall x, B(x) -> C"

Once again, this just captures the way that existential quantifiers
are used in proofs. If you know "exists x, B(x)", and you want to
prove C, then what you can do is to introduce a new symbol, x
to represent something satisfying B(x). Then you prove C using
the assumption that B(x) holds. If you succeed, then what you>ve
done is to prove B(x) -> C, and since x is arbitrary, you>ve proved
"forall x, B(x) -> C".

--
Daryl McCullough
Ithaca, NY

John Jones · Guest

herbzet wrote:
[quote]
John Jones wrote:
Ross A. Finlayson wrote:

[...]

Where you carefully define your terms, the meanings are clear. Where
you don>t, they>re not.
An appeal to syntrax is fine. In that case syntax would seem to point to
this way of looking at it: 'A and B' refers to a new object. Let>s call
it C. C cannot be inferred from 'A' and 'B'.

Even though C has parts A and B, A and B do not summate to C even though
A and B can be summated. My problem is that the standard logical grammar
of 'A and B' is imprecise. We take on board an assumption to the effect
that something happens and makes sense when there is a conjunction. But
this something, maybe it>s C, is never specified.

Is the (positive) square root of 2 (sqrt(2)) ever specified? see belowjj

IOW, please define, as per Ross, "specified".

--
hz
[/quote]
A conjunction appears as the antithesis of 'and'. A conjunction takes
two truth values and yields one truth value. How it does this is never
described. Further, even the element associated with the single truth
value is never described/specified. On this account, conjunction,
surely, must be a vacuous notion.

The difficulty of noticing that we assert a vacuity when we assert a
conjunction must rank as a great mystery. I can only suppose that
tradition and rote learning has much to do with the maintenance of that
mystery. I am not being contrary - I actually cannot see, with the best
of charitable intentions, what could POSSIBLY be meant by a conjunction.
Truly.

John Jones · Guest

herbzet wrote:
[quote]
John Jones wrote:

[...]

But I would still like someone here to tell me what the
distinction is between '"A" and "B"' and '"A and B"'.

Well, this is very succinct.

Good show!

--
hz
[/quote]
Yes, thankyou. I will be appearing as the Star turn in Billy Smart>s
Rodeo Circus with them next week, as two flaming hoops I must jump through.

I have come to the conclusion that 1) conjunction was devised by
logicians to put the mockers on 'and' in the furtherance of the
elimination of meaning from the world, or 2) conjunction was a failed
logicians bright idea to eliminate plurality to get the job done quicker

Herbert Newman · Guest

On Mon, 27 Oct 2008 11:23:00 -0400 herbzet wrote:

[quote]
After a very quick glance, I>m not sure how it all works:

What we need is "quantification over propositions". Then we may _define_[/quote]

~A =df A -> (P)P ,

which "in effect" amounts to the more familiar

~A =df A -> _|_ .

[quote]
The other logical operators are then definable. For example:

A and B == forall propositions C, (A implies (B implies C)) implies C

Well, using my definition from above, I>d write[/quote]

A & B =df ~(A -> ~B)

( since in PC we have A -> B == ~(A & ~B) ).

[quote]
If C is false (I>ll use '0' for 'false'), then (A -> (B -> C)) -> C is
equivalent to A & B:

(A -> (B -> 0)) -> 0 = ~(A -> (B -> 0))
= ~(A -> ~B)
= A & B

Right. Now P(P) is false (from a semantical point of view).[/quote]

Hence we might define

_|_ =df (P)P .

Then of course the usual

~A =df A -> _|_

would be possible (in a second step).

[quote]
A or B == forall propositions C,
((A implies C) implies ((B implies C) implies C))

Again, I>d write[/quote]

A v B =df ~A -> B

( since in PC we have A -> B == ~A v B ).

[quote]
(A -> B) -> B is itself equivalent to A v B, so I don>t see the need
for the more complex formulation.

Agree. Imho the latter def. might do too. [Who knows...][/quote]

[quote]
not A == forall propositions C, A implies C

Or alternatively,

not A == A -> forall propositions C, C.

Right.[/quote]

[quote]
exists x . B(x)
== forall propositions C, (forall x, B(x) implies C) implies C

Again I>d write[/quote]

ExF(x) =df ~Ax~F(x).

Herb

herbzet · Guest

Jan Burse wrote:
[quote]herbzet schrieb:
Jan Burse wrote:
John Jones schrieb:

So in 2) a conjunction is no more than a logically insignificant
translation. Also, 2) assumes that truths can be totalised, or assembled
in truth tables. Truth tables are of no value when the objecthood or
descriptions of their elements is in doubt.

Ernst Specker constructed a paradox out of that.
He invented the operator |, which stands for
lets say "comensurable". And then a and b is only
defined when a|b holds.

Out of that it can be shown that the leibniz equality
(a and b) and (c and d) = (a and c) and (b and d)
does not necessarely hold. There is also a physical
interpretation of |.

Its all quite fun.

It does sound like fun. Got a reference?

--
hz

Sure:

http://www.iumj.indiana.edu/IUMJ/dfulltext.php?year=1968&volume=17&artid=17004
[/quote]
Thanks.

Kochen & Specker "The Problem of Hidden Variables in Quantum Mechanics" [1966]
Section 7 "The logic of quantum mechanics".

Also discussed at http://en.wikipedia.org/wiki/Kochen-Specker_theorem .

--
hz

Ross A. Finlayson · Guest

herbzet wrote:
[quote]
Daryl McCullough wrote:
herbzet says...
Similarly for 'and'. We don>t define it; we give some axioms
for using it, and away we go. Some things must be accepted as
given just to kickstart the whole enterprise.
Yes, that>s right.

As I mentioned in the parent post to the one you are reponding to,
we may use other operators as primitive rather than "and". Just
want to be clear about that.

However, it is interesting that in
some systems of higher-order logic, the only operators
that need to be introduced is universal quantification
and implication.

After a very quick glance, I>m not sure how it all works:

The other logical operators are then definable. For
example:

A and B == forall propositions C, (A implies (B implies C)) implies C

If C is false (I>ll use '0' for 'false'), then (A -> (B -> C)) -> C is
equivalent to A & B:

(A -> (B -> 0)) -> 0 = ~(A -> (B -> 0))
= ~(A -> ~B)
= A & B

but if C is true (I>ll use '1') then (A -> (B -> C)) -> C is not
equivalent to A & B:

(A -> (B -> 1) -> 1 = 1 (because everthing implies a true proposition)
=/= A & B

so I>m confused.

A or B == forall propositions C,
((A implies C) implies ((B implies C) implies C))

(B -> C) -> C is itself equivalent to B v C, so I don>t see the need
for the more complex formulation.

not A == forall propositions C, A implies C

Or alternatively,

not A == A -> forall propositions C, C.

In Polish notation, PIpp, is, as Prior says, an interesting
candidate for Standard False Proposition.

If we have negation as primitive, we can get the other Boolean functions
with just conjunction as also primitive (or just disjunction).

exists x . B(x)
== forall propositions C, (forall x, B(x) implies C) implies C

My brain just gave out.

--
hz
[/quote]
I wouldn>t worry about it, it doesn>t really say anything.

If P and not P, that>s generally considered inconsistent with the law of
excluded middle. That>s about, boundary and mereology in parts. It>s
both the putting apart and taking together.

It>s either, or, neither, nor, yes and no.

It>s like, "My Magic Eight Ball tells me no."

Regards,

Ross F.

Daryl McCullough · Guest

Herbert Newman says...
[quote]
On Mon, 27 Oct 2008 11:23:00 -0400 herbzet wrote:

After a very quick glance, I>m not sure how it all works:

What we need is "quantification over propositions". Then we may _define_

~A =df A -> (P)P ,

which "in effect" amounts to the more familiar

~A =df A -> _|_ .

The other logical operators are then definable. For example:

A and B == forall propositions C, (A implies (B implies C)) implies C

Well, using my definition from above, I>d write

A & B =df ~(A -> ~B)

( since in PC we have A -> B == ~(A & ~B) ).
[/quote]
The advantage of using the definition that I>ve given
is that it works both classically and constructively.

[quote]A or B == forall propositions C,
((A implies C) implies ((B implies C) implies C))

Again, I>d write

A v B =df ~A -> B

( since in PC we have A -> B == ~A v B ).
[/quote]
Same comment.

[quote]exists x . B(x)
== forall propositions C, (forall x, B(x) implies C) implies C

Again I>d write

ExF(x) =df ~Ax~F(x).
[/quote]
Same comment again.

--
Daryl McCullough
Ithaca, NY

herbzet · Guest

Daryl McCullough wrote:

[quote]The advantage of using the definition that I>ve given
is that it works both classically and constructively.
[/quote]
Ah.

--
hz

herbzet · Guest

Daryl McCullough wrote:
[quote]herbzet says...
Daryl McCullough wrote:

After a very quick glance, I>m not sure how it all works:

The other logical operators are then definable. For
example:

A and B == forall propositions C, (A implies (B implies C)) implies C

If C is false (I>ll use '0' for 'false'), then (A -> (B -> C)) -> C is
equivalent to A & B:

(A -> (B -> 0)) -> 0 = ~(A -> (B -> 0))
= ~(A -> ~B)
= A & B

but if C is true (I>ll use '1') then (A -> (B -> C)) -> C is not
equivalent to A & B:

(A -> (B -> 1) -> 1 = 1 (because everthing implies a true proposition)
=/= A & B

so I>m confused.

I didn>t say that "(A -> (B -> C)) -> C" is equivalent to A&B,
I said "Forall C, (A -> (B -> C)) -> C" is equivalent to A&B.
[/quote]

OK, I get it:

If A&B is true, then so is (A -> (B -> C) -> C, regardless of the
value of C, i.e, forall C.

If A&B is false then so is Forall C (A -> (B -> C) -> C because
(A -> (B -> C)) -> C will be false for any false C.

[quote]A or B == forall propositions C,
((A implies C) implies ((B implies C) implies C)) [1]

(B -> C) -> C is itself equivalent to B v C

How would you prove that they are equivalent? Using
what rules of inference? You can prove it using the
law of excluded middle, but that is itself expressed
in terms of "or". So that would be circular.
[/quote]

It just happens that disjunction can be defined in terms
of implication alone. I>m not responsible.

[quote]so I don>t see the need for the more complex formulation.

It>s not more complex. The definition
"Forall C, ((A -> C) -> (B -> C)) -> C"
is exactly what you need in order to reason about disjunctions.
[/quote]
This is not the definition [1] you gave above, and is not equivalent
to the definition you gave above.

What you mean is: The definition
"Forall C, ((A -> C) & (B -> C)) -> C"
is exactly what you need in order to reason about disjunctions.
And that is equivalent to the definition [1] above by exportation.

[quote]The rule for reasoning about disjunctions is this:

If you know (A or B), and you are trying to prove C,
then you can do a "case split":

1. Prove C follows from A (That is, prove A -> C)
2. Prove C follows from B. (That is prove B -> C)
3. Therefore, C follows from A or B.

The second-order definition of "or" exactly captures this
property.
[/quote]

OK, I understand.

[quote]not A == forall propositions C, A implies C

Or alternatively,

not A == A -> forall propositions C, C.

Yes, that>s equivalent.

In Polish notation, PIpp, is, as Prior says, an interesting
candidate for Standard False Proposition.

If we have negation as primitive,
[/quote]
or defined as above,

[quote]we can get the other Boolean functions
with just conjunction as also primitive (or just disjunction).
[/quote]
Or just implication.

[quote]exists x . B(x)
== forall propositions C, (forall x, B(x) implies C) implies C

My brain just gave out.

It>s not that hard. If C is any statement that does not involve
the variable x, then

"exists x . B(x)" -> C

is logically equivalent to

"forall x, B(x) -> C"

Once again, this just captures the way that existential quantifiers
are used in proofs. If you know "exists x, B(x)", and you want to
prove C, then what you can do is to introduce a new symbol, x
to represent something satisfying B(x). Then you prove C using
the assumption that B(x) holds. If you succeed, then what you>ve
done is to prove B(x) -> C, and since x is arbitrary, you>ve proved
"forall x, B(x) -> C".
[/quote]
I want to think about this a little bit more.

--
hz


www.GetXFactor.com Leading Technology, Science, Agriculture News and information	Part of the Identityscape.com network... getxfactor.com jmoodmusic.com smartbusinesschoices.com mintdepot.com lowfaresalways.com evangelicalview.com shoppingpodder.com soproudlywehail.com webnews.ws currenthumor.com

Science and Technology news... Forum Index -> Logic Forum	Goto page Previous 1, 2, 3, 4
Page 4 of 4