Friday, July 11, 2025

Prop. 1 of Proclus' Elements of Theology and Brouwer's intuitionism

The proof of the first proposition of Proclus' Elements of theology is among the most difficult to understand from a formal point of view.  Here is out attempt to make some sense of it using concepts which are also employed in Brouwer's intuitionism (or certain forms of finitism) -  the proof then assumes a structure somewhat like the standard proof of König's lemma.

The proposition reads: every multitude partakes in some way or another of the One.  We take 'multitude' to be represented by a mereological relational system in the form of a tree.

Consider the following interpretation. Proclus assumes that no tree  can have more than a countably infinite number of nodes (and hence branches) because, for him,  there is no infinity greater than countable infinity (the cardinality of the natural numbers). 

Hence there does not exist a tree in which every node has at least one successor and a fortiori in which each node has infinitely many successors- because then the set of branches would be of the cardinality of the continuum.

Proclus' proposition attempts to characterize trees with countable many branches.

Here are at least three types. Type 1 may have finitely many infinitely branching nodes but all branches of finite length.  Thus it participates of unity in a type 1 way (we may think of the terminal node as a 'unity').

Type 2 may have infinite branches but only finitely many nodes with more than one branch passing through them. Would Proclus accept this ? What are we to make of such chains (perhaps they express return-to-self) ? 

Type 3 has finitely branching nodes and finite length branches (what in intuitionism is called a 'barred spread').   Note that in a finitely branching tree if the length of the finite branches is not bounded then - in classical mathematics - König's lemma implies that the tree has an infinite branch.  The contrapositive of this lemma - called the fan theorem - is in fact intuitionistically valid. Thus Type 3 trees must  have bounds for the length of their branches. This is certainly a participating in 'unity' and 'limit' ! 

The following considerations may also have a connection to Proclus' proposition, but we leave this for future study: a basic fact about logic is the need to work with (complete) Boolean algebras or (complete) Heyting algebras as truth values. And that predicates assign such values to each elements of a set (Boolean-valued models, tripos, etc.).  A 'set' is a hierarchical structured tree in which at each level 'membership'  is assigned an algebraic value.  Consider also the authentic meaning of dense and generic subsets of a partially ordered set $P$. If P represents a an infinite 'tree' but in which branches can join,  we can think of P as being linearly ordered representing possible states of (finite, imperfect) information  regarding an object along time. A dense subset is a kind of sequence of bars which guarantees for a given set that as time progresses that set will also progress. A generic set represents a the infinite continuous information trajectory of a possible cohesive object. But a generic set is more than that, it is a kind of amalgamation and transcendent diagonalization of cohesive objects - which belong to the transitive model M in question.  Since it touches all it can be entirely none (when  $f = \cup G$ it is a like a synthesis, integration and transcending of all the limited and possibly contradictory points of view in the ground model M). Cohen's forcing proof (ignoring the for the moment the highly questionably philosophical value of transitive models  of ZF and indeed ZF(C) as a foundation for mathematics) seems to be a rather ad hoc combination of many different ideas and tricks (stemming from Skolem's fundamental insight on countable models) which definitely demands further clarification, simplification and refinement. What about when sheaf semantics comes in. Predicates with generalized truth values correspond to sheaves over the truth values.  In the sheaf semantics approach to forcing the generic object is not required (or is implicitly constructed).  Consider the forcing poset $P$ used to falsify the continuum hypothesis. An alternative would be to take $P$ as a pure poset and to construct a presheaf explicitly which associates to each $p \in P$ a finite function in the form of a finite subset of $B \times N$ satisfying the expected compatibility conditions (i.e. functorial conditions), where $B$ is some large cardinal (and any such finite subset is represented uniquely by some $p$). Then the presheaf topos on $P$ is already an intuitionistic model which falsifies the continuum hypothesis, since we can construct the expected mono in a coherent way ? The double negation topology (which corresponds to the dense topology on $P$) is used only to obtain a Boolean topos ?  It appears that this is not so: the double negation (or dense) topology is required for the local mono condition which makes the total sheaf morphism mono.  There is a very deep philosophy behind this sheaf theoretic construction. An object that cannot exist at once can yet exist spread out through time (or a space of situations) if it does so in a coherent way (the globality of a sheaf is determined essentially by its local qualities: thus if something is locally a mono in a coherent way, the sheaf morphism is mono). A fundamental insight is missing to understand the logical and model theoretic properties of the category of sheaves. Note we are considering presheaves over $P$ which unlike a topological space has no maximal element.   Could we construct a topos in which there is a bounded non-constant holomorphic function ? The construction above is like a completion and like a limit and like the construction of infinitesimals (and internalization of flux into an object). The construction of a topos of sheaves in which every function is continuous is just as interesting and important (if not substantially more) than the forcing methods for transitive ZF models. The same goes for the discovery of the topos theoretic version of forcing. Indeed, consider the sheaf model in which all functions are continuous. Classically, continuous functions have the cardinality of the continuum, while general real functions have that of $P\mathbb{R}$. 

No comments:

Post a Comment

A reconstruction of Boethius' logic in Topicis Differentiis

https://www.academia.edu/144302123/A_reconstruction_of_Boethius_logic_in_De_Topicis_Differentiis