Logical Counterfactuals and Proposition graphs, Part 3

No­ta­tion note, are for lists, are for func­tions.

Note that many of the words and sym­bols I am us­ing are made up. When this maths is bet­ter un­der­stood, some­one should rein­vent the no­ta­tion. My no­ta­tion isn’t that great, but its hard to make good no­ta­tion when you are still work­ing out what you want to de­scribe.

A the­ory (of my new type, not stan­dard maths) T is for­mally defined to be,

Where are the the­o­ries sym­bols. Th­ese can be ar­bi­trary math­e­mat­i­cal ob­jects.

is the set of types, also ar­bi­trary.

is a func­tion.

Is also a func­tion.

An ex­pres­sion in a the­ory is defined re­cur­sively, it con­sists of a pair . Here and is an ex­pres­sion.


Some­times we will write , what we re­ally mean is , and We write when we want to re­fer to just and ig­nore

Ex­pres­sions have the re­stric­tion that the num­ber of el­e­ments of that is mapped to is the same as the num­ber of other ex­pres­sions.

We also in­sist that for all ,

The base case hap­pens when the empty list.

All ex­pres­sions are strictly finite math­e­mat­i­cal ob­jects. There are no self refer­en­tial ex­pres­sions.

Ex­pres­sions can be writ­ten

We can define equal­ity be­tween ex­pres­sions and re­cur­sively by say­ing iff and forall

The dis­tinc­tion be­tween ex­pres­sions is defined re­cur­sively.





Th­ese can be uniquely ex­pressed as strings made up of

Lets define to be the set of all pos­si­ble ex­pres­sions of type .

A func­tion is called ba­sic if it is con­stant, or it is the pro­jec­tion func­tion ( so for fixed ) or can be ex­pressed as

where is con­stant and each is a ba­sic func­tion of .

Note you can cross as much ex­tra junk into as you like and ig­nore it. If is ba­sic, so is .

Ba­sic func­tions can be said to have and

Ba­sic func­tions can be defined in the style of

Fi­nally, where and are ba­sic func­tions with the same do­mains and codomains.

We write to mean that the pair of ba­sic func­tions and are matched in . Ie where

We ex­press the con­cept that for ex­pres­sions that and there ex­ists and ex­pres­sions such that and by saying


We ex­press that such that and and as . (pre­vi­ous posts use for both con­cepts)

Lets cre­ate a new the­ory, called T1, this is a very sim­ple the­ory, it has only 1 con­stant, 2 func­tions and 2 sub­sti­tu­tion rules, with only a sin­gle type.

With the only con­stant be­ing 0. This the­ory can be con­sid­ered to be a weak the­ory of in­te­gers with only a +1 and −1 func­tion. It has a con­nected com­po­nent of its graph for each in­te­ger. Propo­si­tions are in the same graph if and only if they have the same . The­o­rems look like .

Now con­sider the the­ory T2 formed by the sym­bols

It turns out that this the­ory also has one con­nected com­po­nent for each in­te­ger, but this time, propo­si­tions are in the same com­po­nent if is the same.

When is a the­ory and similarly for T.

We can define the dis­joint union, to be the the­ory

Con­sider a func­tion and a func­tion ba­sic func­tions in , such that and where means .

Th­ese ar­ity con­di­tions mean that for any ex­pres­sion i n , we can define an ex­pres­sion in T

is the set of ex­pres­sions in . Call a tran­sjec­tion if it meets the con­di­tion that . For each meet­ing the above con­di­tions, there ex­ists ex­actly one tran­sjec­tion.

We can now define a re­la­tion.

We say iff there ex­ists a tran­sjec­tion such that in iff in . Call such tran­sjec­tions pro­jec­tions.

Say iff and .


and im­plies .


There ex­ists a and pro­jec­tions.

The com­po­si­tion of ba­sic maps is ba­sic, by the re­cur­sive defi­ni­tion.

The com­po­si­tion of tran­sjec­tions is a tran­sjec­tion.

So is a tran­sjec­tion.

For all , then

Hence is a pro­jec­tion.


Let be the iden­tity. The iden­tity map is a pro­jec­tion.


Sup­pose and are the­o­ries, with and tran­sjec­tions.

Sup­pose that for all we know that .

And the same when we swap with . Call and psu­doin­verses.

If we also know that for all a pair of ba­sic func­tions, that for all we know . Say that is ax­iom pre­serv­ing. Again we know the same when is swapped with , IE that is ax­iom pre­serv­ing.

Note that all these claims are po­ten­tially prov­able with a finite list of when the ex­pres­sions con­tain the ar­bi­trary con­stants .

All the stuff above im­plies that .


Con­sider . We know that . st there ex­ists and some such that and (or visa versa.)

This tells us that

If then . True be­cause is a ba­sic func­tion, and they pre­serve similar­ity.

Re­peat this to find that .

If then , and , so so .

On the other hand, if then be­cause the same rea­son­ing also ap­plies to . For any we know .

We know . But and are psu­doin­verses, so hence

There­fore . Sym­met­ri­cally, so

Re­mem­ber our the­o­ries and from ear­lier? The ones about a,b and f,g,h?

We can now ex­press the con­cept that they are ba­si­cally the same. .

We can prove this by giv­ing ba­sic func­tions for each sym­bol, that gen­er­ates tran­sjec­tions, and by show­ing that they are psu­doin­verses and ax­iom pre­serv­ing, we know they are pro­jec­tions and .

, , .

, , , .

For ex­am­ple, pick the sym­bol . To show that and are psu­doin­verses, we need to show that . We know .

To prove these tran­sjec­tions to be psu­doin­verses, do this with all sym­bols in .

Fi­nally we prove that is ax­iom pre­serv­ing. We must show that and that .

Like­wise .

is also ax­iom pre­serv­ing.

So .


We have for­mally defined a no­tion of a the­ory, and pro­vided a crite­ria for tel­ling when two the­o­ries are triv­ial dis­tor­tions of each other. This will al­low us no­tions of log­i­cal prov­abil­ity that aren’t de­pen­dent on an ar­bi­trary choice of for­mal­ism. By look­ing at all equiv­a­lent the­o­ries, weighted by sim­plic­ity, we can hope for a less ar­bi­trary sys­tem of log­i­cal coun­ter­fac­tu­als based on some­thing the­mat­i­cally similar to proof length, al­though kind of more con­tin­u­ous with grad­u­a­tions of partly true.

No comments.