How To Proof of "Axioms" of Propositional Logic: Synopsis.

May 15, 2023
10
0
30
Visit site
Here is the Synopsis:

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

as to 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 neighboring 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: "is equivalent to" or "follows from and vice versa".
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 throwards each other and attached to two
different structures.
We prove Modus Ponens 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: Theorem (T:O): (A OR A) -> A:
1 A -(+)- A Premise
2 A -(+)- A -(+)-( 1, A:AtI
3 )-(+)-(A) []-(+)-(A)-(+)-( 2, A:AD
4 []-(+)-(A) )-(+)-(A)-(+)-[] 3, A:ASS
5 A )-(+)-(A) 4, A:SDx2
6 A []-(+)-(A) 5, A:ASS
and from this (on introduction of a model taking only structures with truth tables
as real) we can conclude that A holds as required (structure A with a Stopper attached
to it does not have a truth table associated with it).
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
 
May 15, 2023
10
0
30
Visit site
I can actually prove the axiom: A OR A -> A, without resorting to metalogical interpretation. We need 2 more axioms:

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

and

A:EED: we can drop an empty structure anywhere in a sentence together with Stoppers and Attractors attached to it.

Here is the proof:

Line # Statement Reason

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
6 (A)-(+)-[] -(+)-( )-(+)-(A) []-(+)-(_)-(+)-( 5, A:AD
8 -(+)-[] (A) []-(+)-(_)-(+)-( 6, A:AOA + Stopper
9 -(+)-[] (A) 8, A:EED
10 (A) 9, A:SD

where "(_)" is the empty structure, "(A)" is structure A. The first Attractor in lines 5 and 6 are assumed attached to (A).
 
May 15, 2023
10
0
30
Visit site
AND-elimination is proved by reasoning backwards through the proof of T:ANDI above and then using the fact (axiom) that: "(A) (B) -> (A)" or "(A) (B) -> (B)".

The default relation is "Exist together" and it has the same truth table as "AND".
 
Last edited:
May 15, 2023
10
0
30
Visit site
Actually we need another axiom for T:O. Line 8's reason is undefined. Here is the axiom

A:NSD: (A)-(+)-[] -(+)-( <-> (A)-(+)-(.

Then we have from line 6 above:

6 (A)-(+)-[] -(+)-( )-(+)-(A) []-(+)-(_)-(+)-( 5, A:AD
7 (A)-(+)-( )-(+)-(A) []-(+)-(_)-(+)-( 6, A:NSD
8 (A) []-(+)-(_)-(+)-( 7, A:AOA
9 (A) 8, A:EED.
 
Last edited:
May 15, 2023
10
0
30
Visit site
Actually we can prove A:NSD as follows:

1 (A)-(+)-[] -(+)-( Premise
2 (A)-(+)-( -(+)-[] 1, A:ASS
3 (A)-(+)-[] 2, T:ANDE
4 (A)-(+)-( 3, A:ASS
 
May 15, 2023
10
0
30
Visit site
Actually A:AtI is just valid for Attractors carrying "therefore", "and", "or" or "if and only if".

I allow other relations to exist like: "is relevant to" and "as set against".
 
Last edited:
May 30, 2022
67
0
550
Visit site
By the truth table for "therefore" we have (Q > not-Q) = not-Q. But on the other hand we have that not-Q cannot follow from Q since: (true > false)> false.
 
Last edited:
May 30, 2022
67
0
550
Visit site
In fact we need another two axioms to prove Modus Tollens:

A:AN: (A)->-( )->-(~A) <-> (~(_))

and:

A:TNE: (A)->-( (~(_)) <-> (~A)

We prove Modus Tollens:

Line # Statement Reason
1 A -> B ~B Premise
2 )->-(A -> B) )->-(~B) 1, A:AtI
3 )->-(A)->-[] (B)->-( )->-(~B) 2, A:AD
4 )->-(A)->-[] (~(_)) 3, A:AN
5 (A)->-[] (~(_)) 4, A:ASS, A:SD, A:ASS
6 (A)->-( (~(_)) 5, A:ASS
7 (~A) 6 A:TNE

where "(~(_))" is the negated empty structure (a structure that is always true) and "(~A)" is structure A negated.
 
Last edited:
May 30, 2022
67
0
550
Visit site
We show that (A->-B ~B ->-C) <> A->-C cannot be proven.

Proof:
Line # Statement Reason
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:AN
6 (A)->-( (~(_)) )->-(C) 5, A:ASS

and because we got the Attractors pointing at the negated empty structure we cannot do a A:EED to line 6 so the proof reach a dead end.
 
Last edited:
May 30, 2022
67
0
550
Visit site
No-one noticed I used T:MP to prove T:MP. In going from the premises with A:AtI, I really reasoned as follows:

Line# Statement Reason
1 A A->B premise
2 (A A ->B) -> ((A)->-( ((A)->-(B))->-( ) Instance of A:AtI
3 (A)->-( ((A)->-(B))->-( 1, 2, T:MP

However T:MP can be proven by truth table.
 
May 30, 2022
67
0
550
Visit site
Note that due to T:ANDE and T:ANDI and T:MP we can apply an axiom to a sub-statement i.e. if a statement has a sub-statement Q and this is the same as the antecedent of an axiom, we can just replace the sub-statement with the conclusion of the axiom.
 
Last edited:
May 30, 2022
67
0
550
Visit site
Note that the line: "(A)-(x)-(B)" reads: "structure A AND structure B exists" an not:
"(A) attached to an Attractor carrying AND". The last bracket in the line gives it away.
 
May 30, 2022
67
0
550
Visit site
Note that even though we have (A)->-(A) = true, A:AA goes to the empty structure (which is always false). It just goes to show that Attractors changes the level of abstraction such that the result of application is false while without the Attractors the sentence is true.

Even though "False AND A = False" we see that leaving out the Empty Structure allows us to conclude "A" from "(_) AND A". This is because "(_) AND A" has a different meaning than "False AND A". This is where we need to test consistency (it is consistent with T:MP being true).
 
Last edited:
May 30, 2022
67
0
550
Visit site
Curry's paradox can be shown to not exist if we apply a restriction of substitution like in algebra: if replacing a variable x in a sentence S with y then ALL the x's in the formula must be replaced. Curry's paradox is proved as follows:

1 X:= (X->y) Premise
2 X -> X Tautology
3 X -> (X->Y) 1,2, Substitution
4 X->Y 3, contraction
5 X 1,4, Substitution
6 Y 4,5, T:MP

where Y is any false statement. With substitution so restricted line 3 is invalid. I think Principia Mathematica don't employ this restriction of substitution.
 
Last edited:
May 30, 2022
67
0
550
Visit site
We won't want to allow substitution of only one B in a sentence S, since then we can derive from the axiom "A:AA" and "B <-> A":

(B)->-( )->-(A) <-> (_)

which should be invalid by A:AL.
 
May 30, 2022
67
0
550
Visit site
Note that the sentence: "(A)->-[] (B)" does not mean that now the relation between A and B no longer holds. It just means the relation as written is temporarily broken for derivation purposes.

We can see this as follows:

1 (A)->-[] (B) Premise
2 (A)->-( (B) 1, A:ASS
3 )->-(A)->-( )->-(B) 2, A:AtI
4 []->-(A)->-[] []->-(B) 3, A:ASS
5 (A)->-[] []->-(B) 4, A:SD
7 (A)->-( )->-(B) 5, A:ASS
8 (A)->-(B) 7. A;AL

Then the reasoning is as follows: the two sentences are equivalent but can't be identical so "(A)->-[] (B)" must contain a temporarily broken relation for derivation purposes.
 
Last edited:
May 30, 2022
67
0
550
Visit site
Note that in SrL it is not always valid to just exclude a substructure on the basis of metalogical interpretation and on the fact that it doesn't have a truth table.

For example we can try to infer (A)->-(B) from the empty structure as follows:

1 (_) Premise
2 (A)->-( )->-(A) 1, A:AA
3 (A)->-( )->-(A) (B)->-( )->-(B) 2, A:AA
4 (A)->-( )->-(B) )->-(A) (B)->-( 3, rearrange
5 (A)->-(B) )->-(A) (B)->-( 4, A:AL
6 (A)->-(B) []->-(A) (B)->-[] 5, A:ASS

Now we must have a refuted axiom of metalogic that says "(A)->-(B)" does not follow.
 
Last edited: