The Leibniz-Hilbert program in philosophy

This continuously updated post will be dedicated to the work of Edward Zalta and his team: Object Theory and its deployment in axiomatic metaphysics, currently in the form of the massive Principia Logica-Metaphysica.  It will also be dedicated to its implementation using proof assistants (such as Isabelle/HOL) as well as the logical and mathematical-semantical aspects of Object Theory. See the page of the Stanford Metaphysics Research Lab.

The paradox of semantics is that sometimes semantics can itself become the basis of a purely logical interpretation of the theory (and even its formalization using proof assistants). Indeed semantics are often formalized directly in formal mathematics projects.

Frege's original system in the Grundlagen and Grundgesetzen is second-order logic with an term-forming extension operator $\hat{x}. \phi(x)$.  Frege had the notorious Law V as well as comprehension, which in this version can be stated as the axiom-scheme

\[ \exists F.  \forall x. (Fx \leftrightarrow \phi(x) )\] 

In other versions of second-order logic (such as Zalta's) this is guaranteed by the construction of relation-terms $\lambda x. \phi(x)$.

Question: in what sense can Zalta's encoding relation be considered as a substitute for Frege's extension term-forming operator ?  True, Zalta's system has relation-terms $\lambda x_1....x_n. \phi(x)$. The enconding relation is like a second-order extension (we can consider sets of properties) but reflected into a subcategory of 'abstract' individual objects (like Fregean extensions).  Properties and properties of properties are all definable, hence there are only countably many.

Instead of a concept $F$ determining a bunch of objects,  an object $o$ determines a bunch of concepts. Instead of $xF$ we could write $F\in x$ ! Our comprehension axiom-scheme is:

\[ \exists x.  \forall F. (F \in x  \leftrightarrow \phi(F) )\] 

Extensions of concepts are philosophically and logically problematic.  But bunches of properties are more crystalline and stable. Zalta's whole approach could be called Platonic set theory.

Frege's approach to arithmetic can be adapted.  For instance we can consider an abstract object $x$ such that if it encodes $F$ then it encodes all $G$ equinumerous to $F$.