by Sven Nilsen, 2022
Prop v0.26 is released!
Prop is a library for Propositional Logic with types in Rust.
I want to explain a little about this release, as it reaches a new milestone in the research on foundation of Path Semantics.
This version of Prop adds Exponential Propositions (using semantics of HOOO), which is formalized as the following eight axioms:
a^b => (a^b)^c(a => b^a) => b^a(a^b)^c => a^(b ⋀ c)(a^b)^a(a^⊤ ⋁ ⊥^a) ⋁ ⊥^(a^⊤ ⋁ ⊥^a)(⊥^(a == b) ∧ ⊥^(b == c)) => (a == c)^⊤(a □ b)^c == (a^c □ b^c)c^(a □ b) == (c^a □[¬] c^b)Here, □ means any binary logical operator (and, or, eq, imply).
There are 16 such operations in total, but only 4 are implemented since the rest can be derived.
The expression □[¬] is the dual logical operator by the symmetric normal path by ¬. These are the operators you can derive if you give the same equational form as De Morgan’s laws.
In addition there are two new axioms for Path Semantics:
(a == b) ⋀ ¬(a^⊤ ⋁ ⊥^a) => (a ~~ b)~a ⋀ (a == b)^⊤ => ~bOK, so why is this a big deal?
It is now understood that Path Semantics requires two new operators ^ (power) and ~ (qubit).
The ^ power operator might be understood as a Category Theory Exponential extension of Propositional Logic.
The ~ qubit operator might be understood as a pseudo-random source,
the next bit in a data stream, or lifting up to a higher homotopy level.
You can also think about it as a way of extending to many-value logic from two-value logic.
In short, these two new operators gives a lot new power to Propositional Logic, which might renew some interest in it (most researchers did not think it was much left to find there). Basically, it shows that there is another way of extending PL to higher dimensional mathematics than simply adding more powerful quantifiers.
By extending PL this way, I also made it more complex (Whops!).
This complexity also explains why formalizing Path Semantics has been so hard. In homotopy level 1, there are 16 logical binary operators, which are those everybody uses. In homotopy level 2, there are over 4 BILLION logical binary operators (2^32). 4-value logics live in homotopy level 2. In the next levels above that, there are:
Have fun scrolling the number in level 6:
1297697410448600346538135939031222035519728998700232084778543406238891850334076587129694423527303789473987996649748036250082317297862768096218198670173239042717243022404097405358815383304467520506016644412538620827664539590981133764939559889792881228022688086387013159779474659377228904660169451046977211569734880854126915463239386217836496696394119476173179833969555344970609797275119509074848382649401987542136420071348640341362674535922153064214928764822074773723105483968708166268391770001008193546523866907057414757404671950237688337348889336470255095022937678634206826776953401707839620349125443294562166015762041130046137078304507285578022169570112201489325577731123168662277782774175060360171925158129387447235460016960647395805695215807380983699032255008369041788431642510192930958332314819211877161067761083492745514752985497572005591098300898501362642140331600815207942822100023617638152801392095870047020586430664761145703707938535906464406225255478970566082524079758186098468463624073204527508260284048962987191501560528120556297523750493275728157552504092216062654422454903614664854707523432470828142420198725979347441441153726933242354091395389601490357550432526686664921480152112368216565882267653305092881044402210015692351775891368301146414351981968923350373884448126606724415090942918312718285342778976990207729827271369182128651357747021196541162375775864442262272153790454445842771953191553371532285370457313533801325474998460876129865738698744711785842767536060631433138044176622498313429867186433040976399943263724380738286727261473007118657345412394415247329923139297422468472074973105376268973641269265766763550078055034204797006653822418032652646514526001315721600841383643905592770018559411242071334524097130309230341753863086433457304332201258143789693310794050368139526486425810515920526690514966426657735297009822822347308821059461601928047577404088595982353448715973318764903612555984878557394689727581475898934959903510650539523742387358493028687147999727868782905595440800670060908385225123633807300055026747539139596139699572013416469479147050202026035823595658241564260446273117491733149544139183746349729775131574234475326952793240708302248933142582357669936354521381623946955024586401006691321883101748742366234089670835411314692531612234047518081809098799701912741535499566760826901138816147745050571154414816928387311642876344456295168525833275257389289089002855575634203975416381552717491969566299428479451557318976731232361052347688093782450759172496613457785426674586796341558349801020810439696683918494133116675377012157259822338829144906520875137659210690851412992747336492326914326688736069877775771817439628583041620269827979325221988483150742648764196519796064219048218581790238796107433591494903767305623499779161623829491394153438577602753296015872912403939133781995669305118750402512528595977334351459763436583313632905069902953475008068913625365490282617160080393262801172330313146148236745449921164948060806911452069815451549857673708623443802874549340502789744414566660268553543566910755632036051772333652210319136753402028349537857280475205705938845645749930586645051732086272786583983061014900742914501299157138806769790024767722750633585764520182070926356100664138850210715705598842122905532688122285662818997869709358741389382818551074714596490081150107374227933685329986845487543930253675616739882062385836491209598753928114457207376576356255107028642034175437122941195648806083085549982368852278066886136087399156800246270140823155995306361156851746204728297233434496857940379371424957968305685415799097530416332358418536606933116174315215327097663282370339032753068632038435102853566876821617976116764083041289405510235702138673206084233412415977601761552494634402751172069930297017193063865055410231671763544260826996010519413376980317677626223193586838527728173723646908915741191050522407467628834478108728633562456189294949972907072217835516032768065884130726042757123496466996641424573962320966764049957703899302070352183284617821442035886042565424815190185607850336275339789767440541239244969508140362837460506154194733006766882061115814920468876280572493497117209685427909368149860795633997946052586776078940905667705642198211724479972324896764242258402262954862503531240323448374982115808740282888904588259700595206248104595240127900801503490967825067529653117701159787653102842260359451835029603941483333188517120844494235705765414044718522420703999784968967892709894636845967827768197323409343104494220034948026747051910930855371819909486828996182563646818626752659938545654081089955366580546278471380839211695493074974418621269683720940027491064776543824006365637843286379190389074049228943087667090419445854074062458815715066335645273655551762071864833938653812714755489303912189289249791427033572312255750132692158245570011930244438550785983827405238706612842402776718110713673430107593004180336747715384598315488260995655046945837985356787156536989126867235288282769656063048530249588946471234472131973601315870490469871433260386093197064710657885805829743893244275588028819074466906030714862761545813522171421020133884168241983512478748442083201937260172820273409005526650193325470249073091805786606060858378895109345350695626788146217788690663147695114726616794137652420096127458684110437426367896052974371764756234020770269534434111728507595798614972033157716166985275365617494263241070561088405182564846615164214637734671747042841816392654568855171198670204310647596770041328176272480084582031716294514384653096571740071416236945808538413410300289298927252395528565432762746902299537728883871891888920180175626831912680526523939831682287344731935250988843132573781950303895403679727132795397488289174164965209702135337312021434334312951732630812726685025763392191097985766249699687119504279835501519449709324409415408073124865462545188189851584962820403391548396601373059528432677446640585197923376516971120013543334131938417888061074117612732303756778467970163777923331639234305215709299572337761757035510153856294832610278918707689049035382129356527046941595295240080735531452932093120954708385449412443070924916585818586680574886184182869327998509170260455635446673449213667468574497166352796712515091327645628750241110507759853113479841485935309248994530027404986592273392579816513233358532974083317237346360753309422925190491271424500891419608328395756832810762266683352128675634710527614321150264678943631196036179171716403147146831648828350037974238822550903062247261364597892072925954092413870637316678081963842074813957351386937129800909906306557789158351467739260857109711439017680124989017079743044145771243475158059147388018714931793406684348047066043445686177403209935784881349886420722418431870954052668401631196236306698392457910980406842887671834754179287753604831182219354347006159916298311506700806419133922129045611604789404880962986447269926587853558493111142546189040791544888879533624391117247722961529184560333182143385935164557921429635788460812145451792228269895641717313447855596174724491244793968842948355957576317391057576885263334995728821917585989247726539952718769475840182868192342315042817482680980989496896501755261761502450606171506098974822921493874400207047960353579365573551102433938746563463036728374276870017575273546411534018816856133958796375525337544207431860691381011828338496128914496884503314383707471558515557061617255675934959405747919509467910252801546835131737202162139136
Remember, this is just binary operators, it is not about very deep theorems that might exist out there. However, considering that this complexity is larger than the number of atoms in the observable universe, I believe there might be something interesting, somewhere.
Now, by extending PL with ^ and ~ using these new axioms,
one can in principle prove theorems of any these levels (it will just take a VERY long time).
Are there any missing axiom such that not all theorems in these levels are provable? I don’t know. ;)
Nope! Do not use them if you do not want to take the risk.
There have been no inconsistency detected so far.
I also wrote a solver script that extracted out the functional depencies and checked the proofs for circular reasoning.
In Rust, a function pointer fn(A) -> B can not capture variables from the environment.
This constraint matches the semantics of Exponential Propositions perfectly.
With other words, the Exponential Propositions are expressions of which programs can be written in a stricter sense than general lambdas/closures. The HOOO axioms makes it possible to reason about these programs without having a direct construction.
If one can prove that some program is constructible from the axioms,
then it should be possible to write that program using a function pointer fn(A) -> B.
In Sequent Calculus, it is common to use Γ and ⊢ to express that something is provable in a certain context.
The ⊢ operator might be thought of as a left-to-right version of the ^ operator.
For example, Γ ⊢ a can be translated as a^Γ. Or, Γ, b ⊢ a can be translated as a^(Γ ⋀ b).
However, Sequent Calculus does not have the same HOOO axioms, which is new for Exponential Propositions in Propositional Logic.
In Modal Logic, there are □ (necessary) and ◇ (possible) operators.
The □a expression might be thought of as a^⊤ and ◇a might be thought of as ⊥^(⊥^a).
However, this is a simplified picture, as the full theory requires more careful proper use of Avatar Extensions.