[FOM] Isomorphic Structures in f.o.m.

[Harvey Friedman]

In f.o.m., isomorphic structures are of course not identical - that is
the most trivial case. But we do have that "anything" true of one is
true of the other.

I'm not sure that I have seen the optimal formulation of this principle.

The most widely quoted version in f.o.m. is

*the two structures share the same first order properties*

although this is not nearly as strong as

"the two structures share the same second order properties*

Here you can use higher order logic as well.

We can even build the cumulative hierarchy over the two domains, and
then say that the two structures share the same first order properties
within these two cumulative hierarchies.

In mathematics, we typically see isomorphic structures, where some
fact has been established about one structure, and we say that it
therefore obviously holds over the other structure. We do not
generally reprove the same fact about the other structure.

How does, should, or can these be handled in a theorem proving environment?

I see these possibilities.

1. Require that the fact be reproved about the second structure. Of
course, one may use cut and paste to the extent possible.
2. Formulate the right metatheorem (e.g., share the same first order
or higher order properties if isormorphic), prove the metatheorem, and
then apply it. The difficulty here is that to apply it, there is some
sort of self referential or potentially self referential maze one has
to negotiate. I.e., when you actually write down a moderately
complicated first order property, you have to give a name for it and
prove that it denotes a first order property, etcetera. Or, closely
related, add a rule of inference to the prover. Definitely awkward.
3. Formulate the right metatheorem, but still adhere to the raw proof
setup. This time, write a script that takes the first or second order
property (or variant, and actually produces a formal proof that the
property is preserved. You don't have to prove that the script is
written properly, but instead plug in the output, and see if the
prover accepts it.

It seems to me that the best strategy for incorporating "two
isomorphic structures have the same first or second or whatever
properties" is the script idea, 3. Any unnecessary complication or
subtlety in the guts of the interaction with the prover is total
anathema to me. From what I have seen, what appears to need to be done
in a general purpose situation to identify isomorphic structures goes
far beyond simple anathema.

On Sat, Mar 26, 2016 at 2:26 AM, Louis Garde <louis.garde at free.fr> wrote:
>
>
> Le 26/03/2016 00:39, Martin Davis a écrit :

> From my point of view, the discovery that the concept of 'logical
> consequence' can be identified with the set-theoretic concept of 'function'
> is the next big step in the same direction.
> This is the "proposition-as-type"paradigm ( see
> https://ncatlab.org/nlab/show/propositions+as+types ), at the heart of
> Martin-Löf type theory and HoTT.

>From my point of view, the very idea that "the concept of 'logical
consequence' can be identified with the set-theoretic concept of
'function' " is among the most absurd ideas I have ever come across.
Of course that does not preclude that something interesting might come
out of such ideas if presented in some philosophically coherent way,
say as formal analogies.
>
> Unfortunately, because of historical reasons, it seems that many people
> still believe that this identification leads to a restrictive logic.

I was wondering if people believe that this "identification" could
lead to insanity.

> Making the law of excluded middle optional is an enrichment for logic and
> mathematics, not a restriction ( see
> http://math.fau.edu/richman/Docs/philmath.pdf ).
>
The overwhelming majority of mathematicians do not appreciate such
"enrichment" of the foundations through the introduction of ideas of
dubious philosophical coherence. Of course, I am interested in making
points of view with dubious philosophical coherence, more
philosophically coherent. However, before that is done in very
convincing ways, elevating things to the status of foundations of
mathematics is grossly premature and highly misleading.

Harvey Friedman