Patrik Eklund peklund at cs.umu.se
Fri Jun 11 01:17:04 EDT 2021

Dear Neil, Dear all,

The notion "set of sentences" is a non-construction.

The "set of terms" is similar. It is not mathematically and
constructively defined, It is defined in English language or whatever
translation but nevertheless in a natural language.

It goes like this:

"There is a set of variables and they are all. There is a signature of a
set of sorts and and a set of (n-ary) operators over these sorts. All
constants (0-ary operators) are terms. If omega : s1 x ... x sn -> s is
an operators and t1, ..., tn are all terms, respectively, of sort s1,
..., sn, then omega(t1,...,tn) is a terms. Nothing else is a terms."

Many well say that this is just the reflection of a precise definition
in set theory about the set of terms. Well, show me that precise
definition. And clearly, it is not a set unless the set of sorts is
one-pointed. There is one set of terms for each sort.

Making it precise in set theory is possible, but indeed, show it to me.
Making it precise in category theory is more elegant. We've done it. And
it wasn't all that easy to do it, I can tell you. We had an older
one-sorted version which was a mix of categorical constructions and set
theory, and when we made it multi-sorted and fuzzy categorical, it was
indeed not as trivial as many would think it is.

The advantage of doing it categorically is that you immediately ask "why
construct the term functior only as a functor over Set, the category of
sets and functions, and not over any category". It won't work over any
category. You need it to be extendable to a monad because otherwise
substitutions won't compose as Kleisli morphisms. But you can do it over
any monoidal closed category. This is very general, and these is
Extremely useful in applications. We've done that too (e.g. in our Fuzzy
Terms paper). Once in a conference outside Bremen I presented this
constructive view and criticized the "English language version". Some in
the audience were so angry so they almost threw me out. That was for me,
as a professor in computer science, a turning point when I finally
realized that many computer scientists have a math complex they can't
explain. These computer scientists believe that computer science
embraces more math than math itself.

Anyway, we didn't stop there. The next in line was the sentence functor.
We do not have full solution for that but we have examples e.g. of a
Horn clause sentence functor. Note also that the sentence functor is
usually not extendable to a monad. If it is, sentences are in fact
terms, like in propositional calculus of lambda calculus. In lambda
calculus the sentence functor in fact coincides with the term functor.
but only after the lambda term functor has been constructed. We did that
in the 75 Church seminar in St Andrews years ago. The audience was very
quiet. Not angry, but quiet. Including Barendregt. Whereas the English
version of terms is "correct", the English version of lambda terms is
not. It leads to undesirable terms that need to be removed. We've shown
how to do it (appears also in Fuzzy Terms).

---

Why these categorical constructions of terms and sentences. Clearly,
because we can then proceed with the categorical constructions of
entailment, models, axioms, inference rules, moving towards 'logic' as a
categorical object. It's not fully developed. Goguen and Meseguer
started it with institutions and entailment systems, but in their
treatment, signature are left out until they give specific examples of
logic. We include the term monad into the logic object.

---

This is also why I have said that logic must be "lative". We are
latively constructing pieces in logic using one piece and constructing
another. We need a signature to construct terms. We close the door to
that part. Then we need terms to construct sentences. We close the door
to that. Then we construct entailment based on sentences, etc etc. We
don't keep everything in one and the same bag, and we find it strange
that it is allowed to number everything in that one and the same bag.
This is my objection against Gödel's numbering.

---

Neil's (1)-(4) is similarly "in English". I would be curious to see a
categorical construction of that. The model functor is tricky indeed,
and it was a hurdle for Goguen and Meseguer, as it has been a hurdle for
us. It's been a while now since I looked at what we did, but I'm coming
back to every once in a while, like now with Neil's mail.

---

Let me finish this my response by underlining that the the category of
sets is not all there is.to work with in these contexts. There's much
more.

Call me anytime over Zoom or Skype, and I can talk you through our
constructions.

Best,

Patrik

On 2021-06-09 15:12, Tennant, Neil wrote:

> In the following, "the set X of sentences has a model" will mean that
> there is an interpretation of the non-logical vocabulary of the
> sentences in X that makes all of them true. We can also express this by
> saying "X is satisfiable".
>
> Assume you have a logical system S of proof for which the following
> propositions hold:
>
> 0. S-proofs are finite. So the set of premises of any S-proof is
> finite. The relation "Y is an S-proof of the sentence P whose premises
> form the set X" is effectively decidable.
>
> 1. If X is a set of sentences that has no model, then there is an
> S-proof of absurdity from premises in X.
>
> 2. If there is an S-proof of absurdity whose premises form the set X,
> then X has no model.
>
> 3. If X has a model, and every model of X makes P true, then there is
> an S-proof of P from premises in X.
>
> 4. If X has a model, and there is an S-proof of P from premises in X,
> then every model of X makes P true.
>
> The combination of (1) and (2) can be thought of as "soundness and
> completeness of S with respect to unsatisfiable sets of sentences".
>
> The combination of (3) and (4) can be thought of as "soundness and
> completeness of S with respect to satisfiable sets of sentences".
>
> Note that (1) entails that every logically false sentence Q can be
> refuted in S; that is, there is an S-proof of absurdity from (the
> singleton of) Q.
>
> Note that (3) entails that every logically true sentence Q can be
> proved outright in S; that is, Q is the conclusion of an S-proof from
> the empty set of premises.
>
> My question for the list is this:
>
> What extra condition, if any, not already entailed by (0), (1), (2),
> (3), and (4) can possibly be required of any logic that is to be
> adequate for the formal regimentation of the deductive reasoning that
> is involved in mathematics and science?
>
> Here, being adequate is to be understood as being able to furnish
> whatever proofs and disproofs might be required as fully formal
> regimentations of the deductive reasoning that is involved in these
> areas of intellectual endeavor. We include, of course, theorem-proving
> in mathematics from decidable sets of mathematical axioms; discovery of
> inconsistencies in proposed axiom-sets; making scientific predictions
> from scientific hypotheses combined with statements of initial and
> boundary conditions for experiments; and discovery of any conflicts
> that could arise between such predictions and the
> observations/measurements that might result from experimental testing.
>
> Neil Tennant
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210611/09383465/attachment-0001.html>