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.
Thursday, January 16, 2020
Subscribe to:
Post Comments (Atom)
No comments:
Post a Comment