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”.
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.