New Language Below Language

I invented new Logic to prove “axioms” of Propositional Logic, but first a bit about myself: I come form a smallholding north of Pretoria, South Africa. I guess I was a bit privileged, having both my parents around and a roof over my head. I was educated at various Primary Schools and Pretoria North Highschool. My father wanted to put me in a boys only school, but luckily that didn’t pan out. I wouldn’t have survived it. Further education was first year Engineering study at University of Pretoria. The new logic came to me much later and I devised it in order to be able to prove Modus Ponens in the object language. For this I devised operators called “Attractors” and “Stoppers”. These served well in proving other “axioms” of Propositional Logic as well. Have a pleasant read.

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. A:SED says we may drop an enclosure and Stopper carrying
“AND” if this occurs at either 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.

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 occurrence would look like an Attractor.

Hello Willem (@talanum_1) and welcome to Peaceful Science. :slight_smile:

It looks like your post is a long copy/paste from another source. Please take a few minutes to see if you can clean that up to make it more readable. I’m going to move your post to “Side Conversation” where others can more easily help you (because comment approval is not needed).

You might be better off removing much of the text and instead posting a link to another source which might retain the original formatting, if any.

Also, please take a moment to tell us a bit about yourself.

I got another “axiom” proven:

We need an axiom of negation redistribution:

A:NR: [ )–>-- –(x)–(~B)]–<>–[ )-x->-- –(x)–(B)]

and of Stopper irrelevancy in A:AL:

A:SI: [(A) )–>-- –(x)–(B)]–>–[(A)–>–(B)]

which also holds for “)-x->–”. Where in both cases the Attractor is assumed attached to structure “B”.

We prove: Theorem (T:CE): ((A)–(x)–(~B))–>–(~((A)–>–(B))) as follows.

Proof:
1 (A)–(x)–(~B) Premise
2 )–(x)–(A) –(x)–(~B)–(x)–( 1, A:AtI, A:AD
3 (A) –(x)–(~B) 2, A:ASS, A:SD, A:ASS
4 )–>–(A) )–>-- –(x)–(~B) 3, A:AtI
5 (A) )-x->-- –(x)–(B) 4, A:ASS, A:SD, A:ASS, A:NR
6 (A)-x->–(B) 5, A:SI

  1. Soundness of SrL.

For soundness we must show that: Theorem (T:C): if a formula F is deriveable then it is valid.

Proof: We must show the axioms are valid, and equivalence replacement is valid, then since it is known that T:MP preserves validity SrL will be proven sound.

Since we assume the operations specified by the axioms are doable, they must be valid if they are stateable in the system of ideas we use (derivability’s default). That equivalence replacement preserves validity follows since for any P: P <> P, so the theorem follows.

https://www.researchgate.net/publication/372884650_Proof_of_Axioms_of_Propositional_Logic

Bio:

No, then I don’t know if the viewers actually viewed it. In any case it is less convenient.

You don’t know if anybody read your copy-n-paste in here either. I, for example, did not. But since you did not invite an actual conversation on the topic – no question, no challenge, no query for feedback, nor a response to anything; it’s hard to parse just what the point of any of this is at all, frankly – you wouldn’t know that. Nor would it have made a difference.

1 Like

I don’t know why A:NR is true since: [(A)–>–(~B)]–x–>–[(A)–x–>–(B)], but it must be true to enable proof of T:CE.

It does in fact follow for the restricted truth table of “–>–”:

AB A -->-- B
00 X
01 X
10 0
11 1

where X means “don’t care”.

Respectfully, it doesn’t matter if anyone can view it when the notation is so obscure that no one can understand it. I’m not sure what your purpose is in posting here at all. If your only purpose is to waste everyone’s time, then please do it somewhere else.

4 Likes

You already posted the link. It is easy to understand.

IOSR Journal of Mathematics is commonly considered a predatory journal. Just saying. And that abstract (which is as far as I’m willing to go) reinforces the idea; no legitimate reviewer would have accepted it.

1 Like

What actually is the point of this? Simply reimplementing propositional logic with a different set of axioms doesn’t seem a worthwhile exercise.

1 Like

If you’ve read it you would see that it isn’t a reimplementation of propositional logic - it lies below propositional logic and can prove some of it’s “axioms” based on just ideas about Attractors and Stoppers.

Isn’t the whole point of axioms that they can’t be proven? If they could be proven they wouldn’t need to be axioms…

2 Likes

That is why I put “axioms” in inverted commas. In the system of Propositional Logic they can’t be proven but I extended language so that they can.

And in order to do that you introduced “ideas about Attractors and Stoppers”. So, what you did (if you did) is introduce new axioms in a new language, wherein the axioms of propositional logic would turn out to be theorems. You created a complicated alternative to something simplicity was the whole point of, all in the hopes of solving something that wasn’t an actual problem.

I contend that it is simpler. With PL you need ingenuity to prove theorems (so it actually was a problem), in SrL you don’t - so which is simpler? The point of this is the beauty of it.

Respectfully, I do not understand what “needing ingenuity” means here, or how it is a problem.

The one that takes fewer rules to prove more theorems in fewer steps.

“Needing ingenuity” means it can’t be automated. My proofs all start with A:AtI and then A:AD in which your only choice is on which side to put the Stopper. A program could do these two and then iterate where to place the Stopper, so it can be automated.

Alright then. Best of luck.