I was thinking about cut elimination on my way back from work today due in large part to a post on the cut rule made by sigfpe on A Neighborhood of Infinity.
It occured to me that the fact that cut-free proofs can be so tremendously much larger than the cut-full ones and that directly constructing cut-full proofs is so difficult is a bit strange. It seems somehow unfair.
As I was thinking about this I realised that one could find cut-free proofs automatically and then reduce them with reverse cut-elimination to produce extremely cutfull proofs. These proofs should be very economical computationally. If one keeps the terms that correspond with the proofs along side, one should be able to obtain a source to source translation that might have performance benefits.
Another totally far-out idea came to me as well. Mathematicians often use lemmas repeatedly. Perhaps the process of finding cuts is generally useful. Specifically, if a lemma is useful in simplifying one proof, maybe it is more likely to be useful in simplifying other proofs. There should be statistical measures over random syntactically valid sentences that one could come up with to see if such lemmas exist.
The ideas of traditional corporatism and communism are diminisioning in importance. This results from a fundemental change in the economics of modern post industrial society.
The means of production was assumed, in communist theory, to be the instrument that the proletariate needed in order to avoid having their labor exploited by the owners of those means. Factories, farms and industrial occupations continue to exist in the west. The cost of these plants and farms is also much higher than it has every been in the past. Yet they employ fewer people and represent a shrinking segment of the economy.
The financial institution of the corporation was designed as a means of raising money in order pay for the means of production which include capital expenditures and the cost of wages. This leads to a political theory concerned with producing environments that are suitable for corporations to exist and proliferate.
Two questions need to be asked. Firstly, is this aforementioned phenomenon a real change in the economic structure or have the jobs simply been shifted elsewhere leading to the illusion of a post industrial economy in the first world. Secondly, if it is in fact a real change, what implications does it have towards political theory.
I don’t know enough about the first question to say for sure (if you could send me data/papers, that would be nice!). It seems to me that the factories in these outsourced-to countries that produce our phones, fabric and computers as well as an array of other goods must, on the whole, be fairly sophisticated. They tend to produce high quality goods with respect to the goods that were produced in former times (just decades ago). I suspect that in fact the number of laborers that they use is also much lower than it would have been in times past. For these reasons I think it is likely that the post industrial economy is not just a vestige of leveraging cheap labor in foreign economies but an actual global phenomenon which will have increasing importance as countries such as china, india and mexico fully industrialise and subsequently post-industrialise.
If in fact this is true what implications does it have to the idiologies of corporatism and communism?
Let us take for example the occupation of software engineer. In reality the only infrastructure that is needed to produce and disseminate products generated by a software engineer can be bought with a months wages. The costs of the means of production are now dominated by the cost of food and shelter.
Why then are software engineers overwelmingly employeed by corporations? The interests that are served by entering into contract for a corporation reduce to:
a) insurance against non-payment (wages)
b) social lubrication
The main reasons are social and technological. The institutions that would lubricate the formation of by-need organisations of programmers to take advantage of niches or requirements in the area of software design, do not yet exist. The old political doctrines of communism and corporatism are increasingly irrelevant to the software engineer as the software engineer (in the overwelming number of cases) already owns the capital means of production, yet the apparatus to despense with these institutions, while technically feasible, still requires mind share.