Proof of "Axioms" of Propositional Logic.

[Willem F Esterhuyse]

The file is attached.

Proof of Axioms of Propositional Logic wo name.pdf

[Phi for All]

!

Moderator Note

Our rules state that members must be able to participate in a discussion without opening any docs or following any links. Is there any reason you can't copy/paste the information you want the members to have?

 

[Willem F Esterhuyse]

I can't copy and paste here, because there are many figures in the text that does not show.

[dimreepr]

2 hours ago, Willem F Esterhuyse said:

I can't copy and paste here, because there are many figures in the text that does not show.

Then give us your synopsis. 

[Willem F Esterhuyse]

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 are graphs with doubly labelled 

vertices with edges carrying symbols. The proofs are very mechanical and does not 

require ingenuity to construct.

  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 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). 

  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)-(. 

A:AD distributes the Attractors and cut relations and places a Stopper on the cutted relation (see line 3 below). Stopper = "|-".
  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 in a line of structures as long as 
we replace every instance of the operators.

  We can prove: P OR P = P. 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 can prove AND-elimination, AND-introduction and transposition. We prove
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.

  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:SD
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.

[Willem F Esterhuyse]

Here is a better version:

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.

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".  
 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)

 A:AD distributes the Attractors and cut relations and places a Stopper on the 
chopped relation (see line 3 below). Stopper = "|-" or "-|".

  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 towards each other and attached to two 
different structures.

  We can prove: P OR P -> P. 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).

  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.

  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.

  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

Edited June 12, 2022 by Willem F Esterhuyse
Spaces got included. Word got included.

[dimreepr]

On 6/12/2022 at 8:36 PM, Willem F Esterhuyse said:

Here is a better version:

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.

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".  
 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)

 A:AD distributes the Attractors and cut relations and places a Stopper on the 
chopped relation (see line 3 below). Stopper = "|-" or "-|".

  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 towards each other and attached to two 
different structures.

  We can prove: P OR P -> P. 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).

  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.

  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.

  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

Prove it...

[Willem F Esterhuyse]

It has a justification for chopping up sentences added. Its a no-brainer.

[Willem F Esterhuyse]

I run the logic in mind and as a result discovered places in mind where language starts. Now I think pages at a time.

[Willem F Esterhuyse]

Here is the newest version of 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 

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: "is equivalent to" or "follows from and vice vesa".  

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.

  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

[dimreepr]

7 minutes ago, Willem F Esterhuyse said:

Here is the newest version of 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 

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: "is equivalent to" or "follows from and vice vesa".  

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.

  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

 

[studiot]

6 minutes ago, dimreepr said:

 

Like it. +1

[Eise]

Also +1. And then I wanted to know from where you got that, and found one, that I am afraid, is even more realistic:

[joigus]

An example is worth a thousand rules.

Can you give one?