Adequacy of a logic

Fri Jun 11 08:08:27 EDT 2021

Hello Patrik, hello fom-ers,

As Patrik correctly observes, I posed my question on fom, with the background required for posing it, 'in English'. In doing so I was mindful of the advice at https://cs.nyu.edu/mailman/listinfo/fom that 'technical details are not welcome'.

Patrik's comments about the ontological/methodological status of terms, sentences, etc. are rather orthogonal to my own concerns. I took it that readers of fom would be able to go along with some assumed basics in formal languages and systems of mathematical logic---that I would be able to use terms like 'sentence', 'proof', 'model', etc. with the widely understood meanings that they have for us all. These meanings, IMHO, are precise enough to be able to generate interesting discussion of the question posed.

By all means employ your own way of recovering, or re-constituting, or formally explicating, the meanings of these terms, so that you can then address my question: are the properties (1)-(5) that I listed for a logical system collectively sufficient for regimenting the deductive reasoning undertaken in mathematics and science?

Best regards,
Neil
________________________________
From: Patrik Eklund <peklund at cs.umu.se>
Sent: Friday, June 11, 2021 1:17 AM
To: Tennant, Neil <tennant.9 at osu.edu>
Cc: fom at cs.nyu.edu <fom at cs.nyu.edu>
Subject: Re: Adequacy of a logic

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/b357b90a/attachment-0001.html>