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
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
Facebook
Twitter
Instagram