prop

Top-level context. Propositional Calculus.

Description:

To keep this module self-contained, most of the results in equiv and order are duplicated here.

Theorems:

Name	Comment
2bitr
2bitrd
2false-eq
2true-eq
3syl	Inference chaining two syllogisms.
4anass
4anass2
4orass
4orass2
<2bitr
<2bitr<
<2bitrd
<2bitrg
<>bitr
<>bitrd
<anabs<
<anabs>
<anabsi<
<anabsi>
<and
<bsylan<
<bsylan<>
<bsylan>
<imtr
<imtrd
<imtrg
<neg	From a wff and its negation, anything is true.
>2bitr
>2bitr<
>2bitrd
>2bitrg
><bitr
><bitrd
>and
>andc
>andi
>bi
>bid
>bii
>dfor
>dford
>imtr
>imtrd
>imtrg
>neg	From a wff and its negation, anything is true.
>nor
a1dd	Deduction introducing a nested embedded antecedent.
abai
ad2an<<
ad2an<>
ad2an><
ad2an>>
adan<
adan<<
adan<>
adan>
adan><
adan>>
an-false
an-false<
an-true
an-true<
an.andi<
an.andi>
an.nim
an.or
an.or2di
an.ordi<
an.ordi>
an12ass
an23ass
anabs<
anabs>
anabsan<
anabsan>
anabsi<
anabsi>
anass
anasss
anasss<
anc2<
anc2>
anc<
anc>
ancom
ancom-alt	Commutativity of conjunction.
ancoms
ancomsd
anidm
anidms
anmp11
anmp12
anmp121
anmp21
anmp22
anmp<
anmp<>
anmp<>d
anmp<>i
anmp<d
anmp<i
anmp>
anmp>d
anmp>i
anmpd
ax1bi
ax2-converse	Converse of axiom ax2.
baib<
baib>
banc<
banc>
banmp<
banmp>
bcom12
bcon
bcon<
bcon>
bi-imp-justification
bi.bldan<
bi.bldan<>
bi.bldan<>d
bi.bldan<d
bi.bldan>
bi.bldan>d
bi.bldanan<
bi.bldanan>
bi.bldbi<
bi.bldbi<>
bi.bldbi<>d
bi.bldbi<d
bi.bldbi<t
bi.bldbi>
bi.bldbi>d
bi.bldbi>t
bi.bldim<
bi.bldim<>
bi.bldim<>d
bi.bldim<d
bi.bldim<t
bi.bldim>
bi.bldim>d
bi.bldim>t
bi.bldneg
bi.bldnegd
bi.bldor.idm
bi.bldor<
bi.bldor<>
bi.bldor<>d
bi.bldor<d
bi.bldor<t
bi.bldor>
bi.bldor>d
bi.nxor
bi<
bi<an
bi<anc
bi<cd
bi>
bi>an
bi>anc
bi>cd
bicom
bicomi
biexmid
bimabs
birefl
birefli
bitr
bitr-an
bitr<
bitr<d
bitrd
bjao
bmp<
bmp>
bmpd<
bmpd>
bmpi<
bmpi>
bmto<
bmto<d
bmto<i
bmto>
bmto>d
bmto>i
bneg>
brpi21
brpi21<
brpi21<d
brpi21d
brpi22
brpi22<
brpi22<d
brpi22d
brpi32
brpi32<
brpi33
brpi33<
brpi43
brpi44
bsylan9
bsylan9r
bsylan<
bsylan<>
bsylan>
case
casean<
casean>
cased
cased2
casei
caseii
caseiii
com12	Swap antecedents.
com12i	Inference that swaps (commutes) antecedents in an implication.
com13i	Commutation of antecedents. Swap 1st and 3rd.
com14i	Commutation of antecedents. Swap 1st and 4th.
com23i	Commutation of antecedents. Swap 2nd and 3rd.
com24i	Commutation of antecedents. Swap 2nd and 4th.
com34i	Commutation of antecedents. Swap 3rd and 4th.
com3li	Commutation of antecedents. Rotate left.
com3ri	Commutation of antecedents. Rotate right.
com4li	Commutation of antecedents. Rotate left.
com4ri	Commutation of antecedents. Rotate right.
com4ti	Commutation of antecedents. Rotate twice.
con	Contraposition.
con<	Contraposition.
con>	Contraposition.
conb
conb<
conb<i
conb>
conb>i
dfbi
dfbi2
dfbi3
dfim.an
dfim.an<
dfim.or
dfor2
dfor>
dfor>d
eq.iman+
eq.iman-
exmid
exp
exp-pre
exp31
exp32
exp3a
exp41
exp42
exp43
exp44
exp45
exp4a
exp4b
exp4c
exp4d
false-eq
false-eqi
false-eqii
id	Principle of identity
idd	Principle of identity with antecedent.
im-true
im.an
im.andi
im.andi-x
im.bidi
im.bidian
im.bidian-ri
im.bldan<
im.bldan<>
im.bldan<>d
im.bldan<d
im.bldan>
im.bldan>d
im.bldanan<
im.bldanan>
im.bldor<
im.bldor<>
im.bldor<>d
im.bldor<d
im.bldor>
im.bldor>d
im.imbi
im.imdi<
im.nan
im.or
imabs	Absorption of redundant antecedent.
imabs3<	Inference absorbing redundant antecedent.
imabs3>	Inference absorbing redundant antecedent.
imp
imp-pre
imp31
imp32
imp3a
imp41
imp42
imp43
imp44
imp45
imp4a
imp4b
imp4c
imp4d
impac
impexp
imtr-an
ja-pre
jaao
jao
jaod
jaoi
jc-pre
jca
jcad
jcai
jct<
jct>
jcti<
jcti>
mp2	A double modus ponens inference.
mpclosed	Closed form of modus ponens.
mpclosedan
mpd	A modus ponens deduction.
mpd2	Modus ponens inference with commutation of antecedents.
mpdd	A nested modus ponens deduction.
mpi	A nested modus ponens inference.
mpid	A nested modus ponens deduction.
mpii	A double nested modus ponens inference.
mto
mto2
mto2d
mto2i
mto3
mto3d
mto3i
mtod
mtoi
nan.or
nbn
ncase
ncased
ncasei
neg+	Proof by contradiction.
neg-	Reduction ad absurdum.
neg<	Double negation.
neg>	Converse of double negation.
nexmid
nor.an
or-false
or-true
or.an
or.an2di
or.andi<
or.andi>
or.ordi<
or.ordi>
or12ass
or23ass
or<
or<i
or>
or>i
orabs-lattice
orass
orcom
orel<
orel>
oridm
peirce	Peirce's axiom.
pm2.6
pm2.85
pm3.26im
pm3.27im
pm3.2im
pm3.4
pm3.48
pm3.81
pm4.8
praeclarum
rpb32<<
rpb32<>
rpb32><
rpb32>>
rpb33<<
rpb33<>
rpb33><
rpb33>>
rpb<<
rpb<>
rpb><
rpb>>
rpi32	A syllogism rule of inference.
rpi32d	A nested syllogism deduction.
rpi33	A syllogism rule of inference.
rpi33d	A nested syllogism deduction.
rpi43	A syllogism rule of inference.
rpi44	A syllogism rule of inference.
rpn21!
rpn22
rpn22!
rpn22con
siman
siman<
siman>
syl	An inference version of the transitive laws for implication.
syl34	Inference joining two implications.
syl34d	Deduction combining antecedents and consequents.
syl9	A nested syllogism inference with different antecedents.
syl9r	A nested syllogism inference with different antecedents.
syl<	A closed form of syllogism.
syl>
sylan12
sylan9
sylan9r
sylan<
sylan<>
sylan<>d
sylan<>i
sylan<d
sylan<i
sylan>
sylan>d
sylan>i
sylanc
sylc	A syllogism inference combined with contraction.
syld	Syllogism deduction.
syld-closed	A closed form of syllogism deduction.
syld2	Syllogism inference with commutation of antecedents.
syld3	Syllogism inference with common nested antecedent.
syldan
syldd	Nested syllogism deduction.
tbt
true-eq
xor.an
xor.nbi
xor.or
xorid