Philosophy of quantifiers

Are quantifiers convenient fictions with fundamenta in re ? What does constructivism and dependent type theory have to say about this ? And functional interpretations ? 

Universal quantification is either an abbreviation for a expression of finite conjunctive knowledge or else something about concepts and not pluralities or extensions.

Universal quantification is determined by a computable function.

A universal Turing machine or equivalent machine (we will not discuss finiteness arguments here) is enough to check any proof or run proof-searches. And all machines imply human intentionality.

The first principle of synthetic a priori knowledge: that a specific computation of one machine can be taken as showing a certain (non-finitarily verifiable) property of the computations of another machine (for instance, output X cannot be produced from any input).  But this property itself may on the surface involve quantification in its expression. Again quantification needs to be seen as determined by a computable function or functional.

What is a typing judgment $t:T$ ? It is a statement that a given machine produces a certain output for input $t$ (inference) or $t$ and $T$ (checking).

Is there a particular philosophical interest in considering Boolean circuits or cellular automata (or neural network) models of universal Turing machines ?

It might be possible to elaborate an alternative version of formal logic, closer to the syntax and mechanisms of natural language and without any implicit extensionalismFF.  We call this system natural term logic (NTL).  The building blocks consists of primitive terms (denoted by capital letters) and primitive constructors (denoted by small-case letters).  To each term we associate a tag which can be $I$, $\omega$ or a number $n \geq 0$ and to each constructor we associate an ordered sequence of tags $t_1,...t_n,t$ denoted by $t_1 \times...\times t_n \rightarrow t$.  We form complex terms and associated to each of them a tag in the expected way. We indicate the tag of a term as $M^{(n)}$.  The most basic constructor corresponds to predication and is denoted simply by concatenation in some cases. There is also partial predication. The tag $i$ is for individual substances and $\omega$ is to indicate that a place in a constructor can accept any term. 

 NTL rejects unbounded quantifiers and does not presuppose extensionalism.  Universal quantification in its most basic form is given by a constructor $a$ of tag $1 \times 1 \rightarrow 0$. Thus for $M^{(1)}$ and $N^{(1)}$ we have the $0$ term (i.e. propositional term) $aMN$ which can be read 'all $M$ is $N$'. Likewise we a similar constructor for 'some'. Let $F^{(2)}$ be the primitive relation term of fatherhood. Then how do we form the $1$ term corresponding to having a father ? To we have implicit boundedness here too ? Before discussing this we can mention the we posit a class of constructors for relational terms which permute or diagonalize certain arguments.  But back to 'having a father'. We need a constructor $s^{1 \times 2 \rightarrow 1}$ such that $sMF$ would be read as 'being an M having an F'.  We can also deal with a unique existential quantifier.  

Can we conceive of a logic in which syntax and logic and intertwined (a way of dealing with non-denoting terms) ?

Notice the difference between relations and  (choice) functions.  We can take a binary relation $R$ and obtain a  (partial) function $cR$ which assigns each M to a possible F (if any).  This suggests that we should consider an alternative approach to NTL, closer to Church's intensional logic (but without variables and with bounded quantifier constructors) - or indeed to Stoic logic ! Each term will have a type. The genitive and other natural language constructions are clearly functional.  Thus for $M,N: \iota \rightarrow p$ we obtain $\Pi_1 MN : p$ and for $R: \iota\rightarrow \iota\rightarrow p$ we obtain $\Pi_2 MR : \iota \rightarrow p$, 'being the R of all M'.   We have a family of choice functions. For instance $cR: \iota \rightarrow \iota$  which corresponds to 'an R of something'  which is not the same as 'being the R of something'.  To define paternal grandfather we still need a combinatoric version of lambda terms (see our paper on Bealer's logic).

Being the father of someone's father, that is, $\lambda xy Fx\iota z Fzy$, which then is to be converted according to our formulation of Bealer's logic. The mechanisms of natural language for expressing multiple generality and logical constructions in general are wondrous and intricate.

Project: find a variable-free combinatoric version of our system ASOL  The metasyntactic operators can be expressed directly in the logic through the 'second-order' functions. 

Did the Stoics anticipate dependent type theory (DTT) ? If one argues that 'all men are mortal' would be implicatively expressed by the Stoics as: if something is a man then it is the case that that man is mortal - this corresponds to there being a term of type $\Pi$(x: man) mortal(x). This term is a 'function' which takes every man m to a proof of the proposition "m is mortal" (but this can also be another kind of type such as what is called a 'set' and even one that does not depend on $x$).  Of course there are other readings in dependent type theory. Anyhow so much remains to be understood about quantifications and the philosophical implications of homotopy type theory. 

If we take 'all men are mortal' as a function which takes each man $m$ into a witness or justification or proof or evidence or element in the set $mortal(m)$ which is a kind space for the mortality of each man.  Note that for adjectives such as 'big' this is necessary: a big flea does not use the same standard as a big house. The fibers have only an analogical correspondence. If we want to read a type for individual substances in an extensional way, the types for adjectives or qualities have to be considered otherwise. Notice how complex 'some A are B' is in DTT. 

See also our latest note on 'Natural Term Logic' (available on researchgate and academia.edu)