Thursday, January 16, 2020

One of the axiom sets for two-valued propositional calculus got discovered by Wajsberg, which with some letter substitution would become as follows:

A1: CxCyx

A2: CCxCyzCCxyCxz

A3W: CCCx00x

It turns out that A3W consists of a special case in that a more general tautology A3 can get formulated in the sense that we can obtain A3W by uniform substitution from A3, but we cannot obtain A3 by uniform substitution from A3W.  A3 is as follows:

A3: CCCxy0x

The notation of a letter or constant on the left side of a '/' with a letter or constant on the blank indicates that we will substitute whatever lies on the left with whatever lies on the right.

To check the soundness of A3 we can set up the following equations:

C00 = 1, C10 = 0, C01 = 1, C11 = 1.

A3 x/0 y/0 yields CCC0000.  So, CCC0000 = CC100 = C00 = 1.

A3 x/0 y/1 yields CCC0100.  So, CCC0100 = CC100 = C00 = 1.

A3 x/1 y/0 yields CCC1001.  So, CCC1001 = CC001 = C11 = 1.

A4 x/1 y/1 yields CCC1101.  So, CCC1101 = CC101 = C01 = 1.

Consequently, CCCxy0x is a tautology.

Now we substitute y with 0 in A3 obtaining CCCx00x.

Therefore, since the above axiom set of Wajsberg consists of an axiom set for C-0 propositional calculus, it follows that {CxCyx, CCxCyzCCxyCxz, CCCxy0x} makes for an axiom set for C-0 propositional calculus under the rules of uniform substitution and detachment.

The author wants to note that N1: {CxCyx, CCxCyzCCxyCxz, CNCxyx} is not a basis for C-N propositional calculus.  To see this we only need to check that if we define N as follows N0 = 0, and N1 = 0, and define C as how it usually gets defined propositional calculi, then CNCxyx = 1.  But, the law of Clavius CCNxxx, with x/0 becomes CCN000, and

CCN000 = CC000= C10 = 0.  Thus, the law of Clavius is not derivable in system N1 under uniform substitution and detachment.


No comments:

Post a Comment