Database CLASSICAL FIRST-ORDER LOGIC WITH EQUALITY Propositional calculus
Table of Contents - 1.2. Propositional calculus
Propositional calculus deals with general truths about well-formed formulas
(wffs) regardless of how they are constructed. The simplest propositional
truth is , which can be read "if something is true, then it
is true" - rather trivial and obvious, but nonetheless it must be proved from
the axioms (see theorem id ).
Our system of propositional calculus consists of three basic axioms and
another axiom that defines the modus-ponens inference rule. It is attributed
to Jan Lukasiewicz (pronounced woo-kah-SHAY-vitch) and was popularized by
Alonzo Church, who called it system P2. (Thanks to Ted Ulrich for this
information.) These axioms are ax-1 , ax-2 , ax-3 , and (for modus
ponens) ax-mp . Some closely followed texts include [Margaris ] for the
axioms and [WhiteheadRussell ] for the theorems.
The propositional calculus used here is the classical system widely used by
mathematicians. In particular, this logic system accepts the "law of the
excluded middle" as proven in exmid , which says that a logical statement
is either true or not true. This is an essential distinction of classical
logic and is not a theorem of intuitionistic logic.
All 194 axioms, definitions, and theorems for propositional calculus in
Principia Mathematica (specifically *1.2 through *5.75) are axioms or
formally proven. See the Bibliographic Cross-References at mmbiblio.html for a complete cross-reference from sources used to its formalization in the
Metamath Proof Explorer.
Recursively define primitive wffs for propositional calculus
wn wi
The axioms of propositional calculus
ax-mp ax-1 ax-2 ax-3
Logical implication
mp2 mp2b a1i 2a1i mp1i a2i mpd imim2i syl 3syl 4syl mpi mpisyl id idALT idd a1d 2a1d a1i13 2a1 a2d sylcom syl5com com12 syl11 syl5 syl6 syl56 syl6com mpcom syli syl2im syl2imc pm2.27 mpdd mpid mpdi mpii syld syldc mp2d a1dd 2a1dd pm2.43i pm2.43d pm2.43a pm2.43b pm2.43 imim2d imim2 embantd 3syld sylsyld imim12i imim1i imim3i sylc syl3c syl6mpi mpsyl mpsylsyld syl6c syl6ci syldd syl5d syl7 syl6d syl8 syl9 syl9r syl10 a1ddd imim12d imim1d imim1 pm2.83 peirceroll com23 com3r com13 com3l pm2.04 com34 com4l com4t com4r com24 com14 com45 com35 com25 com5l com15 com52l com52r com5r imim12 jarr jarri pm2.86d pm2.86 pm2.86i loolin loowoz
Logical negation
con4 con4i con4d mt4 mt4d mt4i pm2.21i pm2.24ii pm2.21d pm2.21ddALT pm2.21 pm2.24 jarl jarli pm2.18d pm2.18 pm2.18OLD pm2.18dOLD pm2.18i notnotr notnotri notnotriALT notnotrd con2d con2 mt2d mt2i nsyl3 con2i nsyl nsyl2 notnot notnoti notnotd con1d con1 con1i mt3d mt3i nsyl2OLD pm2.24i pm2.24d con3d con3 con3i con3rr3 nsyld nsyli nsyl4 pm3.2im jc jcn jcnd impi expi simprim simplim pm2.5g pm2.5 conax1 conax1k pm2.51 pm2.52 pm2.521g pm2.521g2 pm2.521 expt impt pm2.61d pm2.61d1 pm2.61d2 pm2.61i pm2.61ii pm2.61nii pm2.61iii ja jad pm2.61iOLD pm2.01 pm2.01d pm2.6 pm2.61 pm2.65 pm2.65i pm2.21dd pm2.65d mto mtod mtoi mt2 mt3 peirce looinv bijust0 bijust
Logical equivalence
wb df-bi impbi impbii impbidd impbid21d impbid dfbi1 dfbi1ALT biimp biimpi sylbi sylib sylbb biimpr bicom1 bicom bicomd bicomi impbid1 impbid2 impcon4bid biimpri biimpd mpbi mpbir mpbid mpbii sylibr sylbir sylbbr sylbb1 sylbb2 sylibd sylbid mpbidi syl5bi syl5bir syl5ib syl5ibcom syl5ibr syl5ibrcom biimprd biimpcd biimprcd syl6ib syl6ibr syl6bi syl6bir syl7bi syl8ib mpbird mpbiri sylibrd sylbird biid biidd pm5.1im 2th 2thd monothetic ibi ibir ibd pm5.74 pm5.74i pm5.74ri pm5.74d pm5.74rd bitri bitr2i bitr3i bitr4i bitrd bitr2d bitr3d bitr4d syl5bb syl5rbb syl5bbr syl5rbbr syl6bb syl6rbb syl6bbr syl6rbbr 3imtr3i 3imtr4i 3imtr3d 3imtr4d 3imtr3g 3imtr4g 3bitri 3bitrri 3bitr2i 3bitr2ri 3bitr3i 3bitr3ri 3bitr4i 3bitr4ri 3bitrd 3bitrrd 3bitr2d 3bitr2rd 3bitr3d 3bitr3rd 3bitr4d 3bitr4rd 3bitr3g 3bitr4g notnotb con34b con4bid notbid notbi notbii con4bii mtbi mtbir mtbid mtbird mtbii mtbiri sylnib sylnibr sylnbi sylnbir xchnxbi xchnxbir xchbinx xchbinxr imbi2i jcndOLD bibi2i bibi1i bibi12i imbi2d imbi1d bibi2d bibi1d imbi12d bibi12d imbi12 imbi1 imbi2 imbi1i imbi12i bibi1 bitr3 con2bi con2bid con1bid con1bii con2bii con1b con2b biimt pm5.5 a1bi mt2bi mtt imnot pm5.501 ibib ibibr tbt nbn2 bibif nbn nbn3 pm5.21im 2false 2falsed 2falsedOLD pm5.21ni pm5.21nii pm5.21ndd bija pm5.18 xor3 nbbn biass biluk pm5.19 bi2.04 pm5.4 imdi pm5.41 pm4.8 pm4.81 imim21b
Logical conjunction
wa df-an pm4.63 pm4.67 imnan imnani iman pm3.24 annim pm4.61 pm4.65 imp impcom con3dimp mpnanrd impd impcomd ex expcom expdcom expd expcomd imp31 imp32 exp31 exp32 imp4b imp4a imp4c imp4d imp41 imp42 imp43 imp44 imp45 exp4b exp4a exp4c exp4d exp41 exp42 exp43 exp44 exp45 imp5d imp5a imp5g imp55 imp511 exp5c exp5j exp5l exp53 pm3.3 pm3.31 impexp impancom expdimp expimpd impr impl expr expl ancoms pm3.22 ancom ancomd biancomi biancomd ancomst ancomsd anasss anassrs anass pm3.2 pm3.2i pm3.21 pm3.43i pm3.43 dfbi2 dfbi biimpa biimpar biimpac biimparc adantr adantl simpl simpli simpr simpri intnan intnanr intnand intnanrd adantld adantrd pm3.41 pm3.42 simpld simprd simprbi simplbi simprbda simplbda simplbi2 simplbi2comt simplbi2com simpl2im simplbiim impel mpan9 sylan9 sylan9r sylan9bb sylan9bbr jca jcad jca2 jca31 jca32 jcai jcab pm4.76 jctil jctir jccir jccil jctl jctr jctild jctird iba ibar biantru biantrur biantrud biantrurd bianfi bianfd baib baibr rbaibr rbaib baibd rbaibd bianabs pm5.44 pm5.42 ancl anclb ancr ancrb ancli ancri ancld ancrd impac anc2l anc2r anc2li anc2ri pm4.71 pm4.71r pm4.71i pm4.71ri pm4.71d pm4.71rd pm4.24 anidm anidmdbi anidms imdistan imdistani imdistanri imdistand imdistanda pm5.3 pm5.32 pm5.32i pm5.32ri pm5.32d pm5.32rd pm5.32da sylan sylanb sylanbr sylanbrc syl2anc syl2anc2 sylancl sylancr sylancom sylanblc sylanblrc syldan sylan2 sylan2b sylan2br syl2an syl2anr syl2anb syl2anbr sylancb sylancbr syldanl syland sylani sylan2d sylan2i syl2ani syl2and anim12d anim12d1 anim1d anim2d anim12i anim12ci anim1i anim1ci anim2i anim12ii anim12dan im2anan9 im2anan9r pm3.45 anbi2i anbi1i anbi2ci anbi1ci anbi12i anbi12ci anbi2d anbi1d anbi12d anbi1 anbi2 anbi1cd pm4.38 bi2anan9 bi2anan9r bi2bian9 bianass bianassc an21 an12 an32 an13 an31 an12s ancom2s an13s an32s ancom1s an31s anass1rs an4 an42 an43 an3 an4s an42s anabs1 anabs5 anabs7 anabsan anabss1 anabss4 anabss5 anabsi5 anabsi6 anabsi7 anabsi8 anabss7 anabsan2 anabss3 anandi anandir anandis anandirs sylanl1 sylanl2 sylanr1 sylanr2 syl6an syl2an2r syl2an2 mpdan mpancom mpidan mpan mpan2 mp2an mp4an mpan2d mpand mpani mpan2i mp2ani mp2and mpanl1 mpanl2 mpanl12 mpanr1 mpanr2 mpanr12 mpanlr1 mpbirand mpbiran2d mpbiran mpbiran2 mpbir2an mpbi2and mpbir2and adantll adantlr adantrl adantrr adantlll adantllr adantlrl adantlrr adantrll adantrlr adantrrl adantrrr ad2antrr ad2antlr ad2antrl ad2antll ad3antrrr ad3antlr ad4antr ad4antlr ad5antr ad5antlr ad6antr ad6antlr ad7antr ad7antlr ad8antr ad8antlr ad9antr ad9antlr ad10antr ad10antlr ad2ant2l ad2ant2r ad2ant2lr ad2ant2rl adantl3r ad4ant13 ad4ant14 ad4ant23 ad4ant24 adantl4r ad5ant12 ad5ant13 ad5ant14 ad5ant15 ad5ant23 ad5ant24 ad5ant25 adantl5r adantl6r pm3.33 pm3.34 simpll simplld simplr simplrd simprl simprld simprr simprrd simplll simpllr simplrl simplrr simprll simprlr simprrl simprrr simp-4l simp-4r simp-5l simp-5r simp-6l simp-6r simp-7l simp-7r simp-8l simp-8r simp-9l simp-9r simp-10l simp-10r simp-11l simp-11r pm2.01da pm2.18da impbida pm5.21nd pm3.35 pm5.74da bitr biantr pm4.14 pm3.37 anim12 pm3.4 exbiri pm2.61ian pm2.61dan pm2.61ddan pm2.61dda mtand pm2.65da condan biadan biadani biadaniALT biadanii pm5.1 pm5.21 pm5.35 abai pm4.45im impimprbi nan pm5.31 pm5.31r pm4.15 pm5.36 annotanannot pm5.33 syl12anc syl21anc syl22anc syl1111anc mpsyl4anc pm4.87 bimsc1 a2and animpimp2impd
Logical disjunction
wo df-or pm4.64 pm4.66 pm2.53 pm2.54 imor imori imorri pm4.62 jaoi jao1i jaod mpjaod ori orri orrd ord orci olci orc olc pm1.4 orcom orcomd orcoms orcd olcd orcs olcs olcnd unitreslOLD orcnd mtord pm3.2ni pm2.45 pm2.46 pm2.47 pm2.48 pm2.49 norbi nbior orel1 pm2.25 orel2 pm2.67-2 pm2.67 curryax exmid exmidd pm2.1 pm2.13 pm2.621 pm2.62 pm2.68 dfor2 pm2.07 pm1.2 oridm pm4.25 pm2.4 pm2.41 orim12i orim1i orim2i orim12dALT orbi2i orbi1i orbi12i orbi2d orbi1d orbi1 orbi12d pm1.5 or12 orass pm2.31 pm2.32 pm2.3 or32 or4 or42 orordi orordir orimdi pm2.76 pm2.85 pm2.75 pm4.78 biort biorf biortn biorfi pm2.26 pm2.63 pm2.64 pm2.42 pm5.11g pm5.11 pm5.12 pm5.14 pm5.13 pm5.55 pm4.72 imimorb oibabs orbidi pm5.7
Mixed connectives
jaao jaoa jaoian jaodan mpjaodan pm3.44 jao jaob pm4.77 pm3.48 orim12d orim1d orim2d orim2 pm2.38 pm2.36 pm2.37 pm2.81 pm2.8 pm2.73 pm2.74 pm2.82 pm4.39 animorl animorr animorlr animorrl ianor anor ioran pm4.52 pm4.53 pm4.54 pm4.55 pm4.56 oran pm4.57 pm3.1 pm3.11 pm3.12 pm3.13 pm3.14 pm4.44 pm4.45 orabs oranabs pm5.61 pm5.6 orcanai pm4.79 pm5.53 ordi ordir andi andir orddi anddi pm5.17 pm5.15 pm5.16 xor nbi2 xordi pm5.54 pm5.62 pm5.63 niabn ninba pm4.43 pm4.82 pm4.83 pclem6 bigolden pm5.71 pm5.75 ecase2d ecase3 ecase ecase3d ecased ecase3ad ccase ccased ccase2 4cases 4casesdan cases dedlem0a dedlem0b dedlema dedlemb cases2 cases2ALT dfbi3 pm5.24 4exmid consensus pm4.42 prlem1 prlem2 oplem1 dn1 bianir jaoi2 jaoi3 ornld
The conditional operator for propositions
wif df-ifp dfifp2 dfifp3 dfifp4 dfifp5 dfifp6 dfifp7 ifpdfbi anifp ifpor ifpn ifptru ifpfal ifpid casesifp ifpbi123d ifpbi123dOLD ifpbi23d ifpimpda 1fpid3
The weak deduction theorem for propositional calculus
elimh dedt con3ALT
Abbreviated conjunction and disjunction of three wff's
w3o w3a df-3or df-3an 3orass 3orel1 3orrot 3orcoma 3orcomb 3anass 3anan12 3anan32 3ancoma 3ancomb 3anrot 3anrev anandi3 anandi3r 3anidm 3an4anass 3ioran 3ianor 3anor 3oran 3impa 3imp 3imp31 3imp231 3imp21 3impb 3impib 3impia 3expa 3exp 3expb 3expia 3expib 3com12 3com13 3comr 3com23 3coml 3jca 3jcad 3adant1 3adant2 3adant3 3ad2ant1 3ad2ant2 3ad2ant3 simp1 simp2 simp3 simp1i simp2i simp3i simp1d simp2d simp3d simp1bi simp2bi simp3bi 3simpa 3simpb 3simpc 3anim123i 3anim1i 3anim2i 3anim3i 3anbi123i 3orbi123i 3anbi1i 3anbi2i 3anbi3i syl3an syl3anb syl3anbr syl3an1 syl3an2 syl3an3 3adantl1 3adantl2 3adantl3 3adantr1 3adantr2 3adantr3 ad4ant123 ad4ant124 ad4ant134 ad4ant234 3adant1l 3adant1r 3adant2l 3adant2r 3adant3l 3adant3r 3adant3r1 3adant3r2 3adant3r3 3ad2antl1 3ad2antl2 3ad2antl3 3ad2antr1 3ad2antr2 3ad2antr3 simpl1 simpl2 simpl3 simpr1 simpr2 simpr3 simp1l simp1r simp2l simp2r simp3l simp3r simp11 simp12 simp13 simp21 simp22 simp23 simp31 simp32 simp33 simpll1 simpll2 simpll3 simplr1 simplr2 simplr3 simprl1 simprl2 simprl3 simprr1 simprr2 simprr3 simpl1l simpl1r simpl2l simpl2r simpl3l simpl3r simpr1l simpr1r simpr2l simpr2r simpr3l simpr3r simp1ll simp1lr simp1rl simp1rr simp2ll simp2lr simp2rl simp2rr simp3ll simp3lr simp3rl simp3rr simpl11 simpl12 simpl13 simpl21 simpl22 simpl23 simpl31 simpl32 simpl33 simpr11 simpr12 simpr13 simpr21 simpr22 simpr23 simpr31 simpr32 simpr33 simp1l1 simp1l2 simp1l3 simp1r1 simp1r2 simp1r3 simp2l1 simp2l2 simp2l3 simp2r1 simp2r2 simp2r3 simp3l1 simp3l2 simp3l3 simp3r1 simp3r2 simp3r3 simp11l simp11r simp12l simp12r simp13l simp13r simp21l simp21r simp22l simp22r simp23l simp23r simp31l simp31r simp32l simp32r simp33l simp33r simp111 simp112 simp113 simp121 simp122 simp123 simp131 simp132 simp133 simp211 simp212 simp213 simp221 simp222 simp223 simp231 simp232 simp233 simp311 simp312 simp313 simp321 simp322 simp323 simp331 simp332 simp333 3anibar 3mix1 3mix2 3mix3 3mix1i 3mix2i 3mix3i 3mix1d 3mix2d 3mix3d 3pm3.2i pm3.2an3 mpbir3an mpbir3and syl3anbrc syl21anbrc 3imp3i2an ex3 3imp1 3impd 3imp2 3impdi 3impdir 3exp1 3expd 3exp2 exp5o exp516 exp520 3impexp 3an1rs 3anassrs ad5ant245 ad5ant234 ad5ant235 ad5ant123 ad5ant124 ad5ant125 ad5ant134 ad5ant135 ad5ant145 ad5ant2345 syl3anc syl13anc syl31anc syl112anc syl121anc syl211anc syl23anc syl32anc syl122anc syl212anc syl221anc syl113anc syl131anc syl311anc syl33anc syl222anc syl123anc syl132anc syl213anc syl231anc syl312anc syl321anc syl133anc syl313anc syl331anc syl223anc syl232anc syl322anc syl233anc syl323anc syl332anc syl333anc syl3an1b syl3an2b syl3an3b syl3an1br syl3an2br syl3an3br syld3an3 syld3an1 syld3an2 syl3anl1 syl3anl2 syl3anl3 syl3anl syl3anr1 syl3anr2 syl3anr3 3anidm12 3anidm13 3anidm23 syl2an3an syl2an23an 3ori 3jao 3jaob 3jaoi 3jaod 3jaoian 3jaodan mpjao3dan mpjao3danOLD 3jaao syl3an9b 3orbi123d 3anbi123d 3anbi12d 3anbi13d 3anbi23d 3anbi1d 3anbi2d 3anbi3d 3anim123d 3orim123d an6 3an6 3or6 mp3an1 mp3an2 mp3an3 mp3an12 mp3an13 mp3an23 mp3an1i mp3anl1 mp3anl2 mp3anl3 mp3anr1 mp3anr2 mp3anr3 mp3an mpd3an3 mpd3an23 mp3and mp3an12i mp3an2i mp3an3an mp3an2ani biimp3a biimp3ar 3anandis 3anandirs ecase23d 3ecase 3bior1fd 3bior1fand 3bior2fd 3biant1d intn3an1d intn3an2d intn3an3d an3andi an33rean an33reanOLD
Logical "nand" (Sheffer stroke)
wnan df-nan nanan nanimn nanor nancom nannan nanim nannot nanbi nanbi1 nanbi2 nanbi12 nanbi1i nanbi2i nanbi12i nanbi1d nanbi2d nanbi12d nanass
Logical "xor"
wxo df-xor xnor xorcom xorcomOLD xorass excxor xor2 xoror xornan xornan2 xorneg2 xorneg1 xorneg xorbi12i xorbi12iOLD xorbi12d anxordi xorexmid
Logical "nor"
wnor df-nor norcom norcomOLD nornot nornotOLD noran noranOLD noror nororOLD norasslem1 norasslem2 norasslem3 norass norassOLD
True and false constants
Universal quantifier for use by df-tru Equality predicate for use by df-tru The true constant The false constant
Truth tables
Implication Negation Equivalence Conjunction Disjunction Alternative denial Exclusive disjunction Joint denial
Half adder and full adder in propositional calculus
Full adder: sum Full adder: carry