Proof of "Axioms" of Propositional Logic: Synopsis

[talanum1]

Note that there is a space next to an Attractor: "...-->--( ..." and not next to a bracket: "...-->--((...".

[talanum1]

Actually we must restrict A:AM so that we can't prove "(A)--(x)--(B)" from "(A)--(+)--(B)" for example. Thus we need axioms:

A:AM2: )--(x)-- ((A) []--(+)--(B)) <> )--(x)--(A) []--(+)--(B)

where we see the attractor not going to "(B)" too. Similarly:

A:AM3: )--(x)-- ((A) []-->--(B)) <> )--(x)--(A) []-->--(B)

and:

A:AM4: )--(+)-- ((A) []-->--(B)) <> )--(+)--(A) []-->--(B)

and:

A:AM5: )---- ((A) []--(+)--(B)) <> )----(A) []--(+)--(B)

where "----" means: "is relevant to", and

A:AM6: )---- ((A) []-->--(B)) <> )----(A) []-->--(B).

[talanum1]

My proof of Modus Ponens is no good: A:AA allows us to write: "(B)->-( )->-(B) (C) -<>- (C)". But then we can prove "false" -<>- "true" by and elimination. So I'm back to square 1.

We can however still prove "and elimination" and "and introduction" since they don't use this axiom.

I challenge anyone to come up with a proof of Modus Ponens - one that isn't circular like the usual "proof".

[talanum1]

We could just change A:AA to have the empty structure on RS, but then indicate that we reasoned through a logical singularity by appending: "->O". A:AA: ((B)->-( )->-(B))-<>-((_) ->O). Then ""false" ->O" evaluates to "true". We add the axiom A:TAT: true )->-(C) -<>-(C).

Then we change the MP proof to:

Line number Statement Reason
1 B B -> C Premise
2 (B)->-( (B -> C)->-( 1, A:AtI
3 (B)->-( )->-(B) []->-(C)->-( 2, A:AD
4 true []->-(C)->-( 3, A:AA
5 true )->-(C)->-[] 4, A:ASS
6 true )->-(C) 5, A:SD
7 (C) 6, A:TAT

[talanum1]

We require "true ->O" to evaluate to "true" - so it's a strange logical singularity.

No I looked again "true ->O" must evaluate to "false".

[talanum1]

No it must evaluate to "true" in one case and to "false" in other cases - a requirement contrary to the laws of thought.

[talanum1]

I can just leave out the offending proof but then the logic is not complete.

[talanum1]

It must evaluate to "false".