FOM: FOL & SOL - extensional vs intensional

[Martin Davis]

I believe most issues Harvey and I were discussing/debating are pretty much 
resolved, but one contention remains unresolved.

I introduced the three sentences:
               (Ax,y,z)[S(x,y,z) <=> S(y,x,z)]                           (*)
and
       (AS)(Ax,y,z)[S(x,y,z) <=> S(y,x,z)],  (ES)(Ax,y,z)[S(x,y,z) <=> 
S(y,x,z)]
the first being of FOL and the other two of SOL. I said that the first 
expresses definite proposition only when an interpretation is specified 
while the second two express propositions outright.

Harvey insists that the kind of propositions one can properly associate 
with a sentence phi of FOL or SOL are propositions like "phi is valid" and 
"phi is satisfiable". The semantics he outlined is extensional. Sets and 
their members, etc. And he insists that that is the only legitimate way to 
talk about these matters. Now of course this extensional semantics is 
crucial for precision in the business of proving metamathematical theorems.

I mentioned in a previous posting that when Hilbert-Ackermann posed the 
problem of completeness of their axiomatization of FOL, they provided no 
recursive definition of "satisfaction". They simply called a sentence VALID 
if no matter what domain was chosen and no matter how the symbols (relation 
symbols were all they allowed) were interpreted, a true proposition 
(Aussage) would result. This intensional talk is inescapable when one talks 
about formalizing mathematics, e.g. in FOL with the ZFC axioms. One writes 
down a string of symbols phi and says:
      "phi expresses Cantor's Theorem that the cardinality of a power set 
of a given set is 					greater than that of the given set"
Now of course the fact that phi is provable in this system is equivalent to 
the validity of the implication A => phi where A is the conjunction of a 
suitable set of ZFC axioms. But when one explains in what sense Cantor's 
Theorem is provable in ZFC or in what sense the existence of 
non-constructible sets follows from ZFC + measurable cardinal, one is 
speaking intensionally about sentences in a manner that can not be fully 
captured by the discourse Harvey seems prepared to permit.

In connection with (*) above, consider the sentence:
           (Ax,y) (E!z)S(x,y,z) => (Ax,y,z)[S(x,y,z) <=> S(y,x,z)]       (**)
There is a clear sense in which for any particular interpretation,  this 
sentence of FOL expresses the proposition that if the ternary relation 
associated with S is that of a  binary operation, then that operation is 
commutative. We can readily note that that sentence is not valid and that 
it is satisfiable, but we must be allowed to say more.

If we move to SOL and consider the sentences obtained from (**) by 
prefixing the quantifiers (AS), (ES) , respectively, we obtain sentences 
that equally clearly express the false proposition "all binary operations 
are commutative" and the true proposition "some binary relations are 
commutative" respectively.

Martin








                           Martin Davis
                    Visiting Scholar UC Berkeley
                      Professor Emeritus, NYU
                          martin at eipye.com
                          (Add 1 and get 0)
                        http://www.eipye.com