Proof of "Axioms" of Propositional Logic: Synopsis

[talanum1]

Proof of "Axioms" of Propositional Logic:
Synopsis.
Willem F. Esterhuyse.
Abstract.
We introduce more basic axioms with which we are able to prove some

"axioms" of Propositional Logic. We use the symbols from my other article:

"Introduction to Logical Structures". Logical Structures (SrL) are graphs with

doubly labelled vertices with edges carrying symbols. The proofs are very

mechanical and does not require ingenuity to construct. It is easy to see that in

order to transform information, it has to be chopped up. Just look at a kid playing

with blocks with letters on them: he has to break up the word into letters to

assemble another word. Within SrL we take as our "atoms" propositions with

chopped up relations attached to them. We call the results: (incomplete)

"structures". We play it safe by allowing only relations among propositions to be

choppable. We will see whether this is the correct way of chopping up sentences

(it seems to be). This is where our Attractors (Repulsors) and Stoppers come in.

Attractors that face away from each other repels and so break a relation between

the two propositions. Then a Stopper attaches to the chopped up relation to

indicate it can't reconnect. So it is possible to infer sentences from sentences. The

rules I stumbled upon, to implement this, seems to be consistent. Sources differ

asto the axioms they choose but some of the most famous "axioms" are proved.

Modus Ponens occurs in all systems.

1. Introduction.
We use new operators called "Attractors" and "Stoppers". An Attractor ( symbol:
"-(" OR ")-") is an edge with a half circle symbol, that can carry any relation
symbol. Axioms for Attractors include A:AA (Axiom: Attractor Annihilation)
where we have as premise two structures named B with Attractors carrying the
"therefore" symbol facing each other and attached to two neighbouring structures:
B. Because the structures are the same and the Attractors face each other, and the
therefore symbols point in the same direction, they annihilate the structures B and
we are left with a conclusion of the empty structure. Like in:

((B)->-( )->-(B)) -<>- (Empty Structure).

where "-<>-" means: "if and only if". This also holds even if a Stopper carrying
"AND" is attached also onto the second "(B)".

A:AD reads as follows:

((A)->-(B))->-( <-> )->-(A) []->-(B)->-(

where "[]->-" is a Stopper carrying "therefore" relation.

We also have the axiom: A:AtI (Attractor Introduction) in which we have a row
of structures as premise and conclusion of the same row of structures each with an
Attractor attached to them and pointing to the right or left. Like in:

A B C D <-> (A)-( (B)-( (C)-( (D)-(
OR:
A B C D <-> )-(A) )-(B) )-(C) )-(D)

where the Attractors may carry a relation symbol.

Further axioms are: A:SD says that we may drop a Stopper at either end of a line.
And A:ASS says we can exchange Stoppers for Attractors (and vice versa) in a
line of structures as long as we replace every instance of the operators. A:AL says
we can link two attractors pointing trowards each other and attached to two
different structures, if the relations they carry are the same. A:SED says we may drop
an enclosure and Stopper carrying "AND" if this occurs at either end of a sentence or
any amount of encloseures (attached to Stoppers carrying "AND") if they all occur at
the end of a sentence.

A:AOA reads: (A)-(+)-( )-(+)-(A) <-> (A),

where "-(+)-" = "OR".

We prove Modus Ponens (T:MP) as follows:

Line nr. Statement Reason
1 B B -> C Premise

2 (B)->-( (B -> C)->-( 1, A:AtI

3 (B)->-( )->-(B) []->-(C)->-( 2, A:AD

4 []->-(C)->-( 3, A:AA

5 (C)->-( 4, A:SD

6 (C)->-[] 5, A:ASS

7 C 6, A:SD

We see that the Attractors cuts two structures into three (line 2 to line 3). In 2 "(B -> C)" is a structure.

We can prove AND-elimination, AND-introduction and transposition. We prove

Theorem: AND introduction (T:ANDI):

1 A B Premise

2 A -(x)-( B -(x)-( 1, A:AtI

3 (A)-(x)-[] (B)-(x)-[] 2, A:ASS

4 (A)-(x)-[] B 3, A:SD

5 (A)-(x)-( B 4, A:ASS

6 (A)-(x)-(B) 5, T:AL

where "-(x)-" = "AND", and T:AL is a theorem to be proved by reasoning
backwards through:

1 A -(x)- B Premise

2 A -(x)- B -(x)-( 1, A:AtI

3 )-(x)-(A) []-(x)-(B)-(x)-( 2, A:AD

4 []-(x)-(A) )-(x)-(B)-(x)-[] 3, A:ASS

5 A )-(x)-(B) 4, A:SD.

where the mirror image of this is proved similarly (by choosing to place the
Stopper on the other side of "-(x)-").

Modus Tollens and Syllogism can also be proven with these axioms.

We prove and-elimination: T:ANDE: (A)-(x)-(B) <> (A)

Proof:

1 (A)-(x)-(B) Premise

2 )-(x)-(A) []-(x)-(B)-(x)-( 1, A:AtI, A:AD

3 []-(x)-(A) )-(x)-(B)-(x)-[] 2, A:ASS

4 (A) )-(x)-(B) 3, A:SD

5 (A) []-(x)-(B) 4, A:ASS

6 (A) 5, A:SED

We prove: Theorem (T:O): (A OR A) -> A:

1 A -(+)- A Premise

2 (A)-(+)-((A)-(+)-(_)) 1, truth table

3 )-(+)-(A) []-(+)-((A)-(+)-(_))-(+)-( 2, A:AtI, A:AD

4 (A) []-(+)-((A)-(+)-(_)) 3, A:ASS, A:SD, A:ASS

5 (A)-(+)-( []-(+)- )-(+)-(A) []-(+)-(_)-(+)-( 4, A:AtI, A:AD

6 (A)-(+)-( )-(+)-(A) []-(+)-(_)-(+)-( 5, T:ANDE

7 (A) [](+)-(_)-(+)-( 6, A:AOA

8 A 7, A:EED

where "()" is the empty structure (a structure that is always false). Line 6 is because we can write line 5 as: (A)-(+)-( )-(+)-(A) []-(+)-()-(+)-( AND (A)-(+)-( []-(+)-(A) []-(+)-(_)-(+)-(, since they have the same meaning.

We prove Syllogism:

1 A -> B B -> C Premise

2 (A -> B)->-( (B -> C)->-( 1, A:AtI

3 )->-(A)->-[] (B)->-( )->-(B) []->-(C)->-( 2, A:ADx2

4 (A)->-[] (B)->-( )->-(B) []->-(C) 3, A:ASS, A:SDx2, A:ASS

5 (A)->-[] []->-(C) 4, A:AA

6 (A)->-( )->-(C) 5, A:ASS

7 A -> C 6, A:AL

For the Syllogism in the following form:

No B is C
All A is B

therefore

No A is C,

we need a variant on A:AA:

A:AA2: ((B)-->--( )-->--(No B))-->--(_) ... --(| X

where the dots mean the negation is introduced to the remaining sentence where the LS is removed, and the rightmost operator is an Introductor introducing negation. This is also true for "No" preceding the other "(B)" only.

Then we prove this as follows:

1 C -->-- No B B -->-- All A Premise

2 (C -->-- No B)-->--( (B -->-- All A)-->--( 1, A:AtI

3 (C)-->--[] (No B)-->--( )-->--(B) []-->--(All A)-->--( 2, A:AD

4 (C)-->--[] []-->--(All A)-->--( --(|X 3, A:AA2

5 (C)-->--( )-->--(All A)-->--( --(|X 4, A:ASS

6 (No C)-->--(All A)-->--( 5, A:AL

7 (No C)-->--(All A) 6, A:ASS, A:SD

8 (No A)-->--(C) 7, T:Transposition

For:

All B is Some C
All B is Some A

we see that A:AA would give us Some A is Some C as required, without having to draw a Venn diagram. Problem is: we can swop "All B" and "Some C" as required for this Syllogism by A:AA, but not if we model "is" as "therefore". If we model it by "therefore" we get "No C therefore Some A". This is where "is" doesn't allign with "therefore".

Of course the other two cases also holds as:

A:AA3: ((No B)-->--( )-->--(B))-->--(_) ...--(|X

A:AA4(No B)-->--( )-->--(No B))-->--(_)

There remains the case:

All A is Some B
All B is All C

therefore

All A is Some C.

For this we need an axiom that includes "All C":

A:AA5: [(Some B)-->--( )-->--(All B) []-->--(All C)-->--( ]-->--(Some C).

where we used "[" instead of "(" since the other occurence would look like an Attractor.

For the syllogism of form:

All A is some B.
Some B is all C.

we see it does not follow that "All A is all C." since "some B" does not neccessarily mean the same as another instance of "some B". The following follows though: "It is possible that all A is all C."

We need another axiom: A:SAL:

A:SAL: [ )-->--(A) ... []-->-- )-->--(A) ... ]--<->--[ )-->--(A) ... ... ]

where the intuition is: "Attractor linked to (A)" has been stopped, and the dots represent any strings of incomplete structures.

We also need:

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

Now we can prove the axiom:

[(A)-->--((B)-->--(C))]--<->--[((A)-->--(B))-->--((A)-->--(C))]

by reasoning backwards through:

Proof:

Line # Statement Reason

1 ((A)-->--(B))-->--((A)->--(C)) Premise

2 )-->-- ((A)-->--(B))-->--((A)->--(C)) 1, A:AtI

3 )-->--((A)-->--(B)) []-->--((A)-->--(C))-->--( 2, A:AD

4 )-->-- )-->--((A)-->--(B) )-->-- []-->--((A)-->--(C))-->--( 3, A:AtI

5 )-->-- )-->--(A) []-->--(B)-->--( []-->-- )-->--(A) []-->-- []-->--(C)-->--( 4, A:AD, A:AM

6 )-->--(A) []-->--(B)-->--( []-->-- )-->--(A) []-->-- []-->--(C) 5, A:ASS, A:SD, A:ASS

7 )-->--(A) []-->--(B)-->--( []-->-- []-->--(C) 6, A:SAL

8 (A) []-->--(B)-->-- []-->-- []-->--(C) 7, T:AL

9 (A) []-->--((B)-->-- []-->-- []-->--(C)) 8, Choose Priority

10 (A) )-->--((B)-->-- )-->-- )-->--(C)) 9, A:ASS

11 (A)-->--((B)-->-- -->-- -->--(C)) 10, T:ALx3

12 (A)-->--((B)-->--(C)) 11, T:ANDEx2

where line 9 is because: in a line of incomplete structures, you may chose any priority. This I can't prove, it is taken as an axiom.

We need the following axiom:

A:AAS: (C)--(+)--( []-->-- )--(+)--(C) <> []-->--.

This does not contradict A:AOA since the Stopper can get coupled to a transformative idea.
Then we can prove the axiom from Principia Mathemtica:

(A)-->--(B) <> (((C)--(+)--(A))-->--((C)--(+)--(B)))

by reasoning backwards through:

1 ((C)--(+)--(A))-->--((C)--(+)--(B)) Premise

2 )-->-- ((C)--(+)--(A))-->--((C)--(+)--(B)) 1, A:AtI

3 )-->--((A)--(+)--(C)) []-->--((C)--(+)--(B))-->--( 2, A:AD, Commutivity

4 ((A)--(+)--(C)) []-->--((C)--(+)--(B)) 3, A:ASS, A:SD, A:ASS

5 ((A)--(+)--(C))--(+)--( []-->--((C)--(+)--(B))--(+)--( 4, A:AtI

6 )--(+)--(A)--(+)--[] (C)--(+)--( []-->--[ )--(+)--(C) []--(+)--(B)--(+)--( ] 5, A:AD

7 (A)--(+)--[] (C)--(+)--( []-->--[ )--(+)--(C) []--(+)--(B) 6, A:ASS, A:SD, A:ASS

8 (A)--(+)--[] (C)--(+)--( []-->-- )--(+)--(C) []-->-- []--(+)--(B) 7, A:AM

9 (A)--(+)--[] []-->-- []-->-- []--(+)--(B) 8, A:AAS

10 (A) []-->--(B) 9, T:ANDEx3

11 (A) )-->--(B) 10, A:ASS
12 (A)-->--(B) 11, T:AL

 

[luiza]

Tremendous Topic for an old person's Chat Site .

What was the purpose of your OP ?

 

[talanum1]

What is an "OP"?

The purpose is to show Propositional Logic, hence our Language, has "axioms" that can be proven using more basic axioms.

 

[ReinyDays]

What is an "OP"?

The purpose is to show Propositional Logic, hence our Language, has "axioms" that can be proven using more basic axioms.

Axioms cannot be proven ... if we could, we'd call them theorems ...

Can you prove the real numbers are closed under addition? ... can you prove the number 1 is uniquely qualified to be the scalar multiplication's identity? ... you know, actual axioms, not ones you make up ...

 

[luiza]

What is an "OP"?

Something that yours is most definitely not .

More PG -- Pretentious Garbage .

 

[ReinyDays]

What is an "OP"?

The purpose is to show Propositional Logic, hence our Language, has "axioms" that can be proven using more basic axioms.

OP = Original Post or Original Poster ...

You maybe need to re-think your purpose in life ... no one will read what you typed in ... all that work for nothing ...

 

[talanum1]

"Axioms cannot be proven ... if we could, we'd call them theorems ...".

The books call them "axioms", in my paper they are theorems. These "axioms" are shown amenable to proof by more basic axioms - making them more acceptable.

"Can you prove the real numbers are closed under addition? ..."

I can prove some axioms needed to prove these things.

Don't be negative: I got 5800 views on another forum.

 

[scruffy]

Don't be negative: I got 5800 views on another forum.

So why are you here?

It sounds like English is not your first language.

If you'd like to speak math you should start from the beginning. List and number your fundamental assumptions, define your operators, clarify your constraints.

Are you familiar with Judea Pearl's "do calculus"?

 

[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 nr. 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]

""true" ->O" evaluates to "false".

 

[talanum1]

since (A)-(+)-((X|)--(_) ->O) <> (A)-(+)-false <> (A).

 

[talanum1]

My logic gives a reason why some "axioms" of Propositional Logic are true. It also uses simpler axioms, in my opinion. This is what we must strive for.

 

[talanum1]

The reason why MP-proof is a big deal is because I consider the usual proof of MP to be circular.

 

[talanum1]

If you'd like to speak math

I don't want to speak math I want to speak Logic i.e. words.

Are you familiar with Judea Pearl's "do calculus"?

No. Why is it similar?

 

[scruffy]

No. Why is it similar?

It isn't. It's variational. The opposite of static logic, or complimentary to it. A takeoff on perturbation, which they call interference. It answers the question "what happens if I..."

For instance - they want me to play baseball on Saturday unless it rains. What happens if I steal all the bases Friday night? The probabilities change, right?

Do-calculus is a formal system for extracting causality by exchanging action with data.