This itself is a technique I’ve never seen before. Might be interesting to think about whether it has any other applications.
It reminds me of this. Given two sets of polynomials S and T, a set of polynomials whose vanishing set is the union of vanishing sets of these two is {st|s∈S,t∈T}. For the axioms from the post, E has the class of models that is the union of the classes of models for A, B, and C.
Actually the interpretation of \Box_E as its own proof system only requires the other systems to be finite extenions of PA, but I should mention that requirement! Nonetheless even if they’re not finite, everything still works because \Box_E still satisfies necessitation, distributivity, and existence of modal fixed points.
The thing in the post is an infinite conjunction. What you propose doesn’t work, it lets a single proof use axioms from multiple source systems, making it too strong. (Edit: This is wrong, everything is fine except my arguments in this subthread that I’ve now struck through.) What we need is the intersection of the three theories, or triples of proofs.
But really, there is no need for □E to be a proof system, as the intersection of those three it has necessitation and distributivity, and that’s all the lemma needs.
No, the thing in the post is three infinite conjunctions, disjuncted together.
The issue with infinite conjunctions is that they are not valid in typical logics, since typical logics only permit finite-length sentences.
What you propose doesn’t work, it lets a single proof use axioms from multiple source systems, making it too strong.
No, the “or”s between the conjunctions means that a proof has to work using axioms from only one of the source systems. The OP does the same (since “or” is the same as ∨).
In fact, if we pretend that infinite conjunctions make sense, then we can prove my axioms from OP’s axioms. For any triple of axiom sets (a,b,c), we can simply project those out from the OP’s axiom to prove my corresponding axiom.
No, the thing in the post is three infinite conjunctions
Well yes, I meant any one of them is an infinite conjunction, which is the strange thing that some logics won’t permit.
For any triple of axiom sets (a,b,c), we can simply project those out from the OP’s axiom to prove my corresponding axiom.
This doesn’t work, for example if all three systems have tautology (1) as an axiom, let b=c=1 and let a be a singleton. Then at least all axioms of A become axioms in your system (edit: wrong), which clearly shouldn’t happen for E, and can’t be derived from that disjunction of infinite conjunctions. Like, X doesn’t follow from X∨Y.
This doesn’t work, for example if all three systems have tautology (1) as an axiom, let b=c=1 and let a be a singleton. Then at least all axioms of A become axioms in your system, which clearly shouldn’t happen for E
No. For each axiom a of A, “a or tautology” becomes an axiom. But “x or tautology” is itself a tautology for any x, so this isn’t a problem; “a or tautology” does not imply “a”.
At first glance, it seems like thinking of E as a proof system requires A, B and C to be finitely axiomatizable.
But I suppose that can be fixed, by instead giving E an infinite family of axioms:
For any finite sets of axioms a, b, and c of A, B, and C, E would have the axiom (conjunction of a) or (conjunction of b) or (conjunction of c).
(This itself is a technique I’ve never seen before. Might be interesting to think about whether it has any other applications. 🤔)
It reminds me of this. Given two sets of polynomials S and T, a set of polynomials whose vanishing set is the union of vanishing sets of these two is {st|s∈S,t∈T}. For the axioms from the post, E has the class of models that is the union of the classes of models for A, B, and C.
Actually the interpretation of \Box_E as its own proof system only requires the other systems to be finite extenions of PA, but I should mention that requirement! Nonetheless even if they’re not finite, everything still works because \Box_E still satisfies necessitation, distributivity, and existence of modal fixed points.
Thanks for bringing this up.
https://en.m.wikipedia.org/wiki/Compactness_theorem
(or if you like arcane ramblings some of whose fragments might suddenly make sense within a year, https://ncatlab.org/nlab/show/compactness+theorem)
The thing in the post is an infinite conjunction.
What you propose doesn’t work, it lets a single proof use axioms from multiple source systems, making it too strong.(Edit: This is wrong, everything is fine except my arguments in this subthread that I’ve now struck through.) What we need is the intersection of the three theories, or triples of proofs.But really, there is no need for □E to be a proof system, as the intersection of those three it has necessitation and distributivity, and that’s all the lemma needs.
No, the thing in the post is three infinite conjunctions, disjuncted together.
The issue with infinite conjunctions is that they are not valid in typical logics, since typical logics only permit finite-length sentences.
No, the “or”s between the conjunctions means that a proof has to work using axioms from only one of the source systems. The OP does the same (since “or” is the same as ∨).
In fact, if we pretend that infinite conjunctions make sense, then we can prove my axioms from OP’s axioms. For any triple of axiom sets (a,b,c), we can simply project those out from the OP’s axiom to prove my corresponding axiom.
Well yes, I meant any one of them is an infinite conjunction, which is the strange thing that some logics won’t permit.
This doesn’t work, for example if all three systems have tautology (1) as an axiom, let b=c=1 and let a be a singleton.Then at least all axioms of A become axioms in your system(edit: wrong), which clearly shouldn’t happen for E, and can’t be derived from that disjunction of infinite conjunctions. Like, X doesn’t follow from X∨Y.No. For each axiom a of A, “a or tautology” becomes an axiom. But “x or tautology” is itself a tautology for any x, so this isn’t a problem; “a or tautology” does not imply “a”.
That’s true. Sorry for not being careful, everything checks out. Something seems to have short-circuited in my mind.