/ Åke Persson/

System PV1 - null order expressions

Elements
a ("p and q are simultaneous satisfied"); d--1
b ("p and not-q are simultaneous satisfied"); d--2
c ("not-p and q are simultaneous satisfied"); d--3
d ("not-p and not-q are simultaneous satisfied"); d--4
 
e ("p, q and r are simultaneous satisfied"); d--132
f ("p, not-q and r are simultaneous satisfied"); d--133
g ("not-p, q and r are simultaneous satisfied"); d--134
h ("not-p, not-q and r are simultaneous satisfied"); d--135
i ("p, q and not-r are simultaneous satisfied"); d--136
j ("p, not-q and not-r are simultaneous satisfied"); d--137
k ("not-p, q and not-r are simultaneous satisfied"); d--138
l ("not-p, not-q and not-r are simultaneous satisfied"); d--139
Elemental form
1 a + b + c + d; a--28
 
p a + b; t--34
~p c + d
q a + c; t--37
~q b + d; t--50
 
(p&q) a; d--5
(p&~q) b; d--6
(~p&q) c; d--7
(~p&~q) d; d--8
 
(p&q&r) e; d--144
(p&~q&r) f; d--145
(~p&q&r) g; d--146
(~p&~q&r) h; d--147
(p&q&~r) i; d--148
(p&~q&~r) j; d--149
(~p&q&~r) k; d--150
(~p&~q&~r) l; d--151
 
(p&q) e + i; t--152
(p&~q) f + j; t--153
(~p&q) g + k; t--154
(~p&~q) h + l; t--155
 
(p&r) e + f; t--156
(p&~r) i + j; t--157
(~p&r) g + h; t--158
(~p&~r) k+ l; t--159
 
(q&r) e + g; t--160
(q&~r) i + k; t--161
(~q&r) f + h; t--162
(~q&~r) j + l; t--163
 
(pvq) a + b + c; d--12
(pv~q) a + b + d; t--51
(~pvq) a + c + d; t--52
(~pv~q) b + c + d; t--53
 
(p -> q) a + c + d; d--13
(p => q) a / (a + b); d--14
(q -> p) a + b + d; t--54
(q => p) a / (a + c); t--55
 
(p xor q) b + c; d--9
(p <-> q) a + d; d--11
(p <=> q) a / (a + b + c); d--15
Commutatives
(p&q) (q&p); a--23
(pvq) (qvp); t--75
(p xor q) (q xor p); t--76
(p <-> q) (q <-> p); t--77
(p <=> q) (q <=> p); t--78
Assosiatives
(p&(q&r)) (p&q&r); a--26
((p&q)&r) (p&q&r); t--170
Distributives
(p&(qvr)) ((p&r)v(p&r)) ; t--174
(pv(q&r)) ((pvq)&(pvr)) ; t--173
Connective normal form
1 p + ~p; a--27
 
p (p&q) + (p&~q); t--35
q (p&q) + (~p&q); t--36
~p (~p&q) + (~p&~q); t--38
~q (p&~q) + (~p&~q); t--39
 
(pvq) (p&q) + (p&~q) + (~p&q); t--44
(p -> q) (p&q) + (~p&q) + (~p&~q); t--42
(p => q) (p&q) / ((p&q) + (p&~q)); t--45
(q -> p) (p&q) + (p&~q) + (~p&~q); t--43
(q => p) (p&q) / ((p&q) + (~p&q)); t--46
(p xor q) (p&~q) + (~p&q); t--40
(p <-> q) (p&q) + (~p&~q); t--41
(p <=> q) (p&q) / ((p&q) + (p&~q) + (~p&q)); t--47
 
(ad-bc) (p&q)(~p&~q) - (p&~q)(~p&q); t--48
A(p,q) (p&q)(~p&~q) - (p&~q)(~p&q); t--49
Alternatives
(p -> q) (~pvq); t--56
(p -> q) ~(p&~q); t--57
(p <-> q) ~(p xor q); t--58
 
(p => q) (p&q) / p; t--59
(p <=> q) (p&q) / (pvq); t--60
Negations
p 1 - ~p; t--29
~p 1 - p; t--30
~~p p; t--31
 
~0 1; t--32
~1 0; t--33
 
~(p&q) (~pv~q); t--117
~(pvq) (~p&~q); t--118
~(p -> q) (p & ~q); t--119
~(p => q) (p => ~q); t--120
~(p xor q) (~p <-> ~q); t--121
~(p <-> q) (~p xor ~q); t--122
~(p <=> q) (p xor q) / (pvq); t--123
Function f(p,p)
(p&p) p ; t--79
(pvp) p; t--80
(p -> p) 1; t--81
(p => p) p / p; t--82
(p xor p) 0; t--83
(p <-> p) 1; t--84
(p <=> p) p / p; t--85
Function f(p,~p)
(p&~p) 0; a--24
(pv~p) 1; t--86
(p -> ~p) ~p; t--87
(p => ~p) 0 / p; t--88
(p xor ~p) 1; t--89
(p <-> ~p) 0; t--90
(p <=> ~p) 0; t--91
Function f(p,0)
(p&0) 0; t--92
(pv0) p; t--93
(p -> 0) ~p ; t--94
(p => 0) 0 / p; t--95
(p xor 0) p; t--96
(p <-> 0) ~p; t--97
(p <=> 0) 0 / p; t--98
Function f(p,1)
(p&1) p; a--25
(pv1) 1; t--99
(p -> 1) 1; t--100
(p => 1) p / p; t--101
(p xor 1) ~p; t--102
(p <-> 1) p; t--103
(p <=> 1) p; t--104
Correlation factor
A(p,q) (ad-bc); d--16
A(p,~q) - (ad-bc); t--69
A(~p,q) - (ad-bc); t--70
A(~p,~q) (ad-bc); t--71
 
pq a - ad + bc; t--72
(p&q) pq + (ad-bc); t--73
(p&q) pq + A(p,q); t--74
Function f(p,q,(ad-bc))
a pq + (ad-bc); t--105
b p - pq - (ad-bc); t--106
c q - pq - (ad-bc); t--107
d 1 - p - q + pq + (ad-bc); t--108
 
(pvq) p + q - pq - (ad-bc); t--109
(p -> q) 1 - p + pq + (ad-bc); t--110
(p => q) (pq - (ad-bc)) / p; t--111
(q -> p) 1 - q + pq + (ad-bc); t--112
(q => p) (pq - (ad-bc)) / q; t--113
(p xor q) p + q - 2pq - 2(ad-bc); t--114
(p <-> q) 1 - p - q + 2pq +2(ad-bc); t--115
(p <=> q) (pq - (ad-bc)) / (p + q - pq - (ad-bc)); t--116
Function f(p,q,p&q)
(pvq) p + q - (p&q); t--61
(p -> q) 1 - p + (p&q); t--62
(p => q) (p&q) / p; t--59
(q -> p) 1 - q + (p&q); t--63
(q => p) (p&q) / q; t--64
(p xor q) p + q - 2(p&q); t--65
(p <-> q) 1 - p - q + 2(p&q); t--66
(p <=> q) (p&q) / (p + q - (p&q); t--67
Function f(p,q,pvq)
(p&q) p + q - (pvq); t--68
Modus ponens f(p,p -> q) , f(p,p => q)
(p&(p -> q)) (p&q); t--125
(p&(p => q)) no rules available at null order level; t--126
p(p => q) (p&q); t--127
Modus tollens f(~q,p -> q) , f(~q,p => q)
(~q&(p -> q)) (~p&~q); t--128
(~q&(p => q)) no rules available at null order level; t--129
Counter position
(p -> q) (~q -> ~p); t--130
(p => q) (~q => ~p); t--131
Paradox of material implication
(~p&(p -> q)) ~p; t--124