Re: Can ZFC prove Addition is Associative?



"G. Frege" wrote:
herbzet wrote:


For simplifying our discussion let's drop negation and just stick
to the "implicational part" of propositional logic, ok?

So Frege's system consisted of the following axioms (concerning
the "implicational part" of propositional logic):

B1 p -> (q -> p)
B2 (p -> (q -> r)) -> ((p -> q) -> (p -> r))
B3 (p -> (q -> r)) -> (q -> (p -> r))

Instead of removing B3 as deducible from B1 and B2, we
weaken B2:

C1 p -> (q -> p)
C2 (q -> r) -> ((p -> q) -> (p -> r))
C3 (p -> (q -> r)) -> (q -> (p -> r))

but this is no longer complete [...].


Right. See comments below.


So we strengthen the system by adding Hilbert's axiom (p -> (p -> q))
-> (p -> q), this way we get:

D1 p -> (q -> p)
D2 (q -> r) -> ((p -> q) -> (p -> r))
D3 (p -> (p -> q)) -> (p -> q)
D4 (p -> (q -> r)) -> (q -> (p -> r))

Right.

Just stumbled over the following historical fact:

In his article Logische Grundlagen der Mathematik [Logical Foundations
of Mathematics], 1922, D. Hilbert introduces an axiom system (as a
logical framework for mathematics). Again I'll just consider the
"implicational part" of propositional logic:

"I. Axioms for Implication

A -> (B -> A)

A -> (A -> B) -> (A -> B)

(A -> (B -> C)) -> (B -> (A -> C))

(B -> C) -> ((A -> B) -> (A -> C))"

This is exactly the system D1-D4.

Incidentally H. Curry introduced a logical system called /combinatory
logic/ in 1930 in which he used the combinators K, B, W, C as "basis".
Now these combinators just correspond to the mentioned axioms (from
above, i.e. the axioms of Hilbert's system):

1) A -> (B -> A) (K)
2) (B -> C) -> ((A -> B) -> (A -> C)) (B)
3) A -> (A -> B) -> (A -> B) (W)
4) (A -> (B -> C)) -> (B -> (A -> C)) (C)

See:
http://en.wikipedia.org/wiki/B%2CC%2CK%2CW_system

I've tried to get into combinatory logic, but haven't
found a treatment that is sufficiently elementary that I
can understand it. It's a pleasant surprise to see
you assert that these combinators correspond to these
axioms!


There's another combinator, S, which corresponds to the formula:

(A -> (B -> C)) -> ((A -> B) -> (A -> C)) (S)

i.e. Frege's well known axiom. Now S can be defined in terms of B, W,
C. (This means that it can be proved from axioms D2, D3, D4.)

S = B(B(BW)C)(BB).

In Curry & Feys' Combinatory Logic (1958) it is proved that S cannot
be defined if any of the combinators B, W, C is omitted. (Imho this
just means that Frege's axiom cannot be proved from the axiom system
D1-D4 if any of the formulas D2-D4 is omitted. With other words, such
a system would not be complete. So this should answer your original
question. :-)

Excellent.

Later, in (his book) Combinatory Logic, Curry switched to the two
combinators S and K as basis of his system.

These two combinators correspond two the two axioms:

F1 A -> (B -> A) (K)
F2 (A -> (B -> C)) -> ((A -> B) -> (A -> C)) (S)

i.e. to the first two axioms of Frege's system in Begriffsschrift! :-)

(Though I doubt that Curry got them directly from there. It's much
more probable that he got them from Lukasiwicz & Tarski's work.)

It's easy to define the other combinators already mentioned (B, W, C)
in terms of K and S:

B = S(KS)K.

W = SS(KI) (where I = SKK)

C = S(BBS)(KK).

(To each of this definitions there corresponds a proof of the related
formula from the axioms F1, F2.)

--------------------------------------------------------------

So it seems that finally all developments "converged" and lead to the
system:

A1 A -> (B -> A)
A2 (A -> (B -> C)) -> ((A -> B) -> (A -> C))

which are exactly the first two axioms in Frege's Begriffsschrift
(1879).*) If we add the axiom for negation introduced by Lukasiewicz
and Tarski (1930)

A3 (~A -> ~B) -> (B -> A)

we get a complete axiom system for propositional logic.


At http://en.wikipedia.org/wiki/Combinatory_logic#Logic
it says:

"The K and S combinators correspond to the axioms

AK: A -> (B -> A),
AS: (A -> (B -> C)) -> ((A -> B) -> (A -> C)),

and function application corresponds to the detachment
(modus ponens) rule

MP: from A and A -> B infer B.

The calculus consisting of AK, AS, and MP is complete for the
implicational fragment of the intuitionistic logic ..."

Offhand, I don't know if the implicational fragment of intuitionistic
logic is a proper subset of the implicational fragment of classical
logic.


F.

*) It's really an irony of history that the development of
propositional logic finally ended at its very starting point.

:-)

--
hz
.

Relevant Pages

  • Re: Can ZFC prove Addition is Associative?
    ... "I. Axioms for Implication ... logic/ in 1930 in which he used the combinators K, B, W, C as "basis". ... Now these combinators just correspond to the mentioned axioms (from ...
    (sci.logic)
  • Re: implications of false axioms
    ... Structures where the axioms are false confirm the the ... "LOCAL material implication", whatever, fine. ... in concept with what Tarski defined as "logical consequence". ...
    (sci.logic)
  • Re: implications of false axioms
    ... Structures where the axioms are false confirm the the ... So if you're not talking material implication, ... An individual model just gets to ...
    (sci.logic)
  • Re: Proving induction
    ... Actually the problem is not the counting it self, ... But the problem is rather having in the axioms ... But now turn the implication into a biconditional, ... you write the axioms and then only one interpretation works (which you ...
    (sci.logic)
  • Re: Can ZFC prove Addition is Associative?
    ... In his article Logische Grundlagen der Mathematik [Logical Foundations ... logical framework for mathematics). ... "I. Axioms for Implication ...
    (sci.logic)