Results 1 to 3 of 3

Thread: Proof of "Axioms" of Propositional Logic: Synopsis

  1. #1
    New Member
    Join Date
    Apr 2025
    Location
    Tshwane, South Africa
    Posts
    9
    Thanks
    0
    Thanked 0 Times in 0 Posts

    Proof of "Axioms" of Propositional Logic: Synopsis

    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

    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 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 trowards each other and attached to two
    different structures, if the relations they carry is 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 &nbsp;)-(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 &nbsp;)->-(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.

    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."
    Last edited by Dave A; 14-Apr-25 at 07:43 AM. Reason: inserted noparse tags

  2. #2
    New Member
    Join Date
    Apr 2025
    Location
    Tshwane, South Africa
    Posts
    9
    Thanks
    0
    Thanked 0 Times in 0 Posts

    Proof of T:Transposition

    For a proof of T:Transposition see: "Academia.edu" and search for: "Proof of "Axioms" of Propositional Logic. WF Esterhuyse."


  3. #3
    New Member
    Join Date
    Apr 2025
    Location
    Tshwane, South Africa
    Posts
    9
    Thanks
    0
    Thanked 0 Times in 0 Posts
    I can prove another "axiom". As follows:

    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

Similar Threads

  1. Sage - Processing Supplier Invoices - Type "Access Denied"
    By Nurisha in forum Accounting Forum
    Replies: 2
    Last Post: 20-Sep-22, 01:32 PM
  2. [Question] How to "delete"/"cancel out" a duplicated cashbook transaction
    By michellepace in forum Accounting Forum
    Replies: 1
    Last Post: 25-Mar-20, 06:17 PM
  3. Unable to view "calculation" or "dispute" - e-filing
    By Boeriemore in forum Tax Forum
    Replies: 3
    Last Post: 14-Sep-15, 09:38 AM
  4. Zuma Controversy " Cast the First Stone...""
    By sgafc in forum South African Politics Forum
    Replies: 23
    Last Post: 17-Feb-10, 03:02 PM

Tags for this Thread

Did you like this article? Share it with your favourite social network.

Did you like this article? Share it with your favourite social network.

Posting Permissions

  • You may not post new threads
  • You may not post replies
  • You may not post attachments
  • You may not edit your posts
  •