Hi Vaughan, I hesitate to say anything specifically about Goldbach's conjecture, but let me comment at least on "proof ... exists". The very basic, simple and first idea of "lativity" is that it was never good that symbolic logic was ``freed from its undue obsession with the forms of ordinary algebra'', like Principia writes in its PREFACE, referring to Peano having said that, but Peano never did say that. Peano did say "We shall generally write signs on a single line" (Lat. Signa plerumque in eadem linea scribemus), but he didn't say "For a monadic term and formula construction, just go with a magma; don't care about multi-sortedness and universal algebra, they won't do any good". I don't know who to blame, Russell or Whitehead, for fake reference to Peano, but I tend to choose Russell. He had struggled with substitution, and PM continued to struggle with substitution. Everybody else did, over decades to come, until GdM II is printed and beyond. If we say "a conjecture is true", what do we mean? Do we mean that the formula (sentence formed categorically from underlying terms, again formed categorically, and based on signatures, whether denoted a la Benabou or not) is true, where that 'true' is the boolean constant in the underlying signature? Or do we mean that it is "true" that we can find a proof for that conjecture, i.e. "proof ... exists" is "true". Lativity would say that the latter "true" is not the "true" we have as sorted in the signature. I've often commented that "P is true" and "|-P is true" cannot use the same "true". PM struggled with this, GdM struggled with this. P is a formula, |-P is not. There may be a proof for P, but it makes no sense saying there may or may not be a proof for |-P. John Stuart Mill was very smart. He said “nothing but a Proposition can be an object of proof”. Gödel thinks differently, as Bw and Bew are of the same type, kind of. It's good if formalization proceeds latively, from signature to term to sentence to entailment to proof rules to proofs ...", and even better if always "closing the door behind you" so that nobody comes up with viewing a proof sequence as a constant operator in the starting point signature. I feel uncomfortable to speak of a "lative axiomatization", unless by "axiomatization" we mean "from signature to term to sentence to entailment to proof rules to proofs", because then, by definition of lativity, axiomatization is lative. So, within syntax, we should keep things apart, and also, as far as borderlines are concerned, between object and meta. We shouldn't shift things in meta sometimes to be used objectively or vice versa. Numbers and numerals are on different sides of that borderline. GdM writes about Nummern and Ziffern, but does not really make that borderline explicit. And indeed, I'm sad to say, GdM never tried out rigour concerning types. Neither did Grundzüge. And Gödel 1931 is extremely illative in these respect along the whole progression of "from signature to term to sentence to entailment to proof rules to proofs". On GdM, already at its starting point, in GdM I §1, GdM "departs even further from such rigour by making a dubious statement basically saying that a boolean predicate symbol complies with its arity but need not be bound to respect any specific typing of its domain, as long as satisfiability of a formula is invariant under a one-to-one mapping of one typing to another". I put that in quotation marks because I quote directly from drafting I presently have on what I have called a "dialogue" between GdM II §§4-5 and Gödel 1931. I'm trying to use categorical terms constructions and "categorically lative axiomatization" to explain why and where things go wrong. So, to your question "Would you then call the conjecture undecidable?", I am unable to provide an answer until I understand latively what is meant by "conjecture" as related to formula or entailment or something else, and what is understood as "decidable" as related to a more lative definition of "proof sequence" including all its ingredients. I don't think PM's, GdM's and Gödel's notions of "decidability" are mutually isomorphic. Putting symbols one by one in sequence is "no good", not good at all. Russell made a fake reference to Peano, and even if Russell would have said being freed from the burden of algebra is something good without referring to Peano, I would say Russell's approach is "no good". Foundations must be revisited. Foundations need category theory more than category theory needs foundations. I would invite everybody to think about the way foundations might be revisited using categorical constructions, and thereby making logical constructions much more "lative" than they are in traditional foundations of logic (and computing for that matter), and in particular for the reason to finally get rid of self-referentiality and malicious use of antinomies. Doing so will make discussions on answers to your question, Vaughan, really interesting. That's my credo. Has been for a long time. Best, Patrik On 2024-02-08 08:20, Vaughan Pratt wrote: On Sun, Feb 4, 2024 at 11:30 PM Patrik Eklund <peklund@cs.umu.se<mailto:peklund@cs.umu.se>> wrote: [...] Not clear to me what David precisely means by "no new", but in our case we have been used to say "logic must be lative" in the sense that "first terms, then sentences from terms" and no new terms from that, and "then entailment constructions from sentences" so that no new sentences are constructed from entailment. Here is where logic mixes "true" and "provable", and this is the very spot which allows Gödel to "prove" incompleteness using the Liar and Richard's technique. [...] Patrik, how does "lative" bear on Goldbach's conjecture in the event that it is true, and furthermore provably so in some consistent non-lative recursively enumerable axiomatization of arithmetic, but for which it can be shown that no proof of the conjecture exists in any lative axiomatization? Would you then call the conjecture undecidable? Vaughan Pratt You're receiving this message because you're a member of the Categories mailing list group from Macquarie University. To take part in this conversation, reply all to this message. View group files<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=files&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Leave group<https://outlook.office365.com/owa/categories@mq.edu.au/groupsubscription.ashx?source=EscalatedMessage&action=leave&GuestId=6bf90c14-94d1-45b7-a0b5-9dd447734d27> | Learn more about Microsoft 365 Groups<https://aka.ms/o365g>