Adequacy of a logic

[Patrik Eklund]

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>