We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

Extended Kripke lemma and decidability for hypersequent substructural logics

00:00

Formale Metadaten

Titel
Extended Kripke lemma and decidability for hypersequent substructural logics
Untertitel
Q/A Session A - Paper A6.F
Serientitel
Anzahl der Teile
56
Autor
Lizenz
CC-Namensnennung 3.0 Deutschland:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
Identifikatoren
Herausgeber
Erscheinungsjahr
Sprache

Inhaltliche Metadaten

Fachgebiet
Genre
Mathematische LogikKategorie <Mathematik>EntscheidungstheorieKalkülResultanteTermVertauschungsrelationDesign by ContractMathematische LogikEntscheidungstheorieAussage <Mathematik>Lemma <Logik>TheoremVertauschungsrelationDesign by ContractXMLComputeranimation
DatenstrukturMathematische LogikTypentheorieAusdruck <Logik>EntscheidungstheorieBeweistheorieFormale GrammatikKalkülKomplex <Algebra>TheoremGebundener ZustandKlasse <Mathematik>SchnittmengeWort <Informatik>SequenzenkalkülTouchscreenObjekt <Kategorie>DatenstrukturFormale SpracheMathematische LogikNatürliche ZahlValiditätAusdruck <Logik>Derivation <Algebra>EntscheidungstheorieAussage <Mathematik>BeweistheorieKalkülKomplex <Algebra>TheoremVertauschungsrelationGebundener ZustandDesign by ContractComputeranimation
DatenstrukturFolge <Mathematik>Mathematische LogikAusdruck <Logik>Derivation <Algebra>BildschirmmaskeEinfach zusammenhängender RaumIntuitionistische MathematikCASE <Informatik>SchnittmengeEin-AusgabeSequenzenkalkülMultimengeSchlussregelDatenstrukturMathematische LogikFunktion <Mathematik>Ausdruck <Logik>Logischer SchlussAussage <Mathematik>Einfach zusammenhängender RaumFunktionalIntuitionistische LogikKalkülMultiplikationEin-AusgabeSchlussregelDesign by ContractComputeranimation
Ausdruck <Logik>Intuitionistische LogikTheoremVollständigkeitSequenzenkalkülRechter WinkelMathematische LogikKategorie <Mathematik>Ausdruck <Logik>Derivation <Algebra>Aussage <Mathematik>Intuitionistische LogikKalkülResultanteTheoremWärmeübergangVollständigkeitComputeranimation
Mathematische LogikTopologieTypentheorieKategorie <Mathematik>Ausdruck <Logik>Derivation <Algebra>BeweistheorieBildschirmmaskeKalkülMomentenproblemResultanteKontrollstrukturSchnittmengeSequenzenkalkülEliminationsverfahrenArithmetischer AusdruckSchnitt <Mathematik>SchlussregelMinkowski-MetrikMathematische LogikKategorie <Mathematik>Ausdruck <Logik>Derivation <Algebra>EntscheidungstheorieAussage <Mathematik>BeweistheorieIntuitionistische LogikKalkülLeistung <Physik>MaßerweiterungTheoremWurzel <Mathematik>EliminationsverfahrenArithmetischer AusdruckKontrast <Statistik>SchlussregelMinkowski-MetrikComputeranimation
Mathematische LogikKategorie <Mathematik>Intuitionistische LogikIntuitionistische MathematikKalkülLambda-KalkülAdditionSequenzenkalkülWeb-SeiteDifferenteRechenbuchSchlussregelAssoziativgesetzDesign by ContractDatenstrukturMathematische LogikAxiomKategorie <Mathematik>Einfach zusammenhängender RaumIntuitionistische LogikKalkülLinearisierungSpannweite <Stochastik>UmwandlungsenthalpieEndliche ModelltheorieKonstruktor <Informatik>Kontrast <Statistik>NeuroinformatikKlassische PhysikSchlussregelCliquenweiteAssoziativgesetzDesign by ContractComputeranimation
InformatikMathematische LogikAxiomKategorie <Mathematik>Einfach zusammenhängender RaumIntuitionistische MathematikSpannweite <Stochastik>UmwandlungsenthalpieEndliche ModelltheorieKonstruktor <Informatik>SchlussregelDesign by ContractDatenstrukturMathematische LogikFunktion <Mathematik>AxiomKategorie <Mathematik>Ausdruck <Logik>Logischer SchlussAussage <Mathematik>Einfach zusammenhängender RaumFunktionalIntuitionistische LogikKalkülMultiplikationLinearisierungSpannweite <Stochastik>Ein-AusgabeUmwandlungsenthalpieEndliche ModelltheorieKonstruktor <Informatik>Kontrast <Statistik>NeuroinformatikKlassische PhysikSchlussregelCliquenweiteAssoziativgesetzDesign by ContractComputeranimation
AxiomatikFormale SpracheMathematische LogikNatürliche ZahlFuzzy-MengeModallogikTypentheorieKategorie <Mathematik>GrenzschichtablösungEntscheidungstheorieIntuitionistische MathematikKalkülLambda-KalkülMaßerweiterungPhysikalisches SystemResultanteVertauschungsrelationZahlenbereichLinearisierungFuzzy-LogikKartesische KoordinatenRichtungEndliche ModelltheorieDifferenteKontextbezogenes SystemMultiplikationsoperatorSchlussregelDesign by ContractAxiomatikBildverarbeitungFormale SpracheMathematische LogikParadoxonFuzzy-MengeFunktion <Mathematik>ModallogikTypentheorieAxiomGrenzschichtablösungEntscheidungstheorieAussage <Mathematik>Einfach zusammenhängender RaumFormale GrammatikKalkülMaßerweiterungPhysikalisches SystemResultanteTheoremVertauschungsrelationLinearisierungEin-AusgabeFuzzy-LogikKartesische KoordinatenSoft ComputingEndliche ModelltheorieLineare LogikKontextbezogenes SystemDesign by ContractComputeranimation
Mathematische LogikAxiomKategorie <Mathematik>Rekursive FunktionEntscheidungstheorieBeweistheorieFunktionalIntuitionistische MathematikKalkülKomplex <Algebra>MaßerweiterungResultanteTeilmengeViereckParametersystemCASE <Informatik>Gebundener ZustandKlasse <Mathematik>SequenzenkalkülEinsMathematische LogikKategorie <Mathematik>Ausdruck <Logik>EntscheidungstheorieHill-DifferentialgleichungIntuitionistische LogikKalkülKomplex <Algebra>MaßerweiterungResultanteMinkowski-MetrikComputeranimation
AlgorithmusAusdruck <Logik>Derivation <Algebra>KalkülParametersystemSequenzenkalkülRechenbuchNeuroinformatikSchlussregelAlgorithmusDerivation <Algebra>EntscheidungstheorieAnalytische FortsetzungBeweistheorieKalkülLokales MinimumParametersystemComputeranimation
Folge <Mathematik>Ordnung <Mathematik>RelativitätstheorieTransformation <Mathematik>Derivation <Algebra>BeweistheorieLemma <Logik>PunktSuchbaumKartesische KoordinatenKonditionszahlSymboltabelleSchlussregelDesign by ContractTopologieGenerator <Informatik>Derivation <Algebra>EntscheidungstheorieBeweistheorieLemma <Logik>Lokales MinimumParametersystemInstantiierungKartesische KoordinatenSchlussregelDesign by ContractComputeranimation
DiagrammBeweistheorieInstantiierungElement <Gruppentheorie>SchlussregelTopologieGenerator <Informatik>Derivation <Algebra>EntscheidungstheorieBeweistheorieLokales MinimumParametersystemInstantiierungKartesische KoordinatenElement <Gruppentheorie>SchlussregelDesign by ContractComputeranimation
AlgorithmusFolge <Mathematik>Ausdruck <Logik>Derivation <Algebra>Arithmetisches MittelBeweistheorieRadikal <Mathematik>Verzweigendes ProgrammParametersystemSuchbaumSchnittmengeRichtungElement <Gruppentheorie>Folge <Mathematik>TopologieGenerator <Informatik>Kategorie <Mathematik>Ausdruck <Logik>Derivation <Algebra>UnendlichkeitEntscheidungstheorieBeweistheorieInverser LimesKette <Mathematik>Lemma <Logik>Lokales MinimumRadikal <Mathematik>KonstanteParametersystemInstantiierungKartesische KoordinatenElement <Gruppentheorie>SchlussregelIdentitätsverwaltungDesign by ContractComputeranimation
Ausdruck <Logik>BeweistheorieKette <Mathematik>ResultanteExistenzsatzSchnittmengeWeb SiteKonditionszahlTupelFolge <Mathematik>TopologieKategorie <Mathematik>Ausdruck <Logik>UnendlichkeitEntscheidungstheorieBeweistheorieInverser LimesKette <Mathematik>Lemma <Logik>Radikal <Mathematik>ParametersystemKonstruktor <Informatik>IdentitätsverwaltungComputeranimation
Folge <Mathematik>Mathematische LogikGenerator <Informatik>Kategorie <Mathematik>ForcingGruppenoperationKalkülTeilbarkeitParametersystemSchlussregelFolge <Mathematik>Mathematische LogikKategorie <Mathematik>Ausdruck <Logik>GruppenoperationKalkülLemma <Logik>TeilbarkeitParametersystemTupelSchlussregelComputeranimation
AxiomatikFolge <Mathematik>Formale SpracheFormale SemantikKategorie <Mathematik>Inverser LimesKalkülMaßerweiterungZusammenhängender GraphArithmetischer AusdruckMultimengeSchlussregelRechter WinkelDesign by ContractAlgorithmusDatenstrukturFormale SpracheMathematische LogikKategorie <Mathematik>Ausdruck <Logik>Derivation <Algebra>Inverser LimesKalkülMaßerweiterungZusammenhängender GraphArithmetischer AusdruckComputeranimation
AlgorithmusFolge <Mathematik>Derivation <Algebra>EntscheidungstheorieKalkülParametersystemSchlussregelDesign by ContractDatenstrukturDerivation <Algebra>KalkülLemma <Logik>MaßerweiterungParametersystemDesign by ContractComputeranimation
SchlussregelDesign by ContractDatenstrukturAusdruck <Logik>Lemma <Logik>MaßerweiterungMultiplikationParametersystemComputeranimation
Folge <Mathematik>BeweistheorieInverser LimesPermutationCASE <Informatik>HypercubeLuenberger-BeobachterElement <Gruppentheorie>StandardabweichungDesign by ContractDatenstrukturLemma <Logik>MaßerweiterungPermutationParametersystemZusammenhängender GraphLuenberger-BeobachterElement <Gruppentheorie>Design by ContractComputeranimation
Folge <Mathematik>Ausdruck <Logik>Inverser LimesLokales MinimumPrimidealZusammenhängender GraphSchlussregelDesign by ContractAusdruck <Logik>Lemma <Logik>ParametersystemZusammenhängender GraphElement <Gruppentheorie>SchlussregelDesign by ContractComputeranimation
Folge <Mathematik>Ordnung <Mathematik>RelativitätstheorieÄquivalenzklasseEndlichkeitHypercubeElement <Gruppentheorie>SchlussregelDesign by ContractFolge <Mathematik>Ausdruck <Logik>ÄquivalenzklasseLemma <Logik>Kartesische KoordinatenComputeranimation
Folge <Mathematik>Ordnung <Mathematik>Ausdruck <Logik>ÄquivalenzklasseEndlichkeitHypercubeZusammenhängender GraphElektronische UnterschriftKlasse <Mathematik>SchnittmengeFolge <Mathematik>Ausdruck <Logik>FinitismusLemma <Logik>Elektronische UnterschriftSchnittmengeComputeranimation
Folge <Mathematik>Natürliche ZahlUnendlichkeitÄquivalenzklasseKette <Mathematik>PotenzmengeTeilmengeTheoremZusammenhängender GraphElektronische UnterschriftPunktKlasse <Mathematik>Abgeschlossene MengeTupelElement <Gruppentheorie>Folge <Mathematik>FinitismusUnendlichkeitKette <Mathematik>Lemma <Logik>TeilmengeTheoremRamsey-TheorieElektronische UnterschriftMultifunktionElement <Gruppentheorie>Computeranimation
DatenstrukturFolge <Mathematik>Ordnung <Mathematik>Kette <Mathematik>PotenzmengeResultanteNichtlinearer OperatorHypercubeElektronische UnterschriftBereichstheorieElement <Gruppentheorie>Kontextbezogenes SystemSchlussregelRechter WinkelDesign by ContractFolge <Mathematik>Ausdruck <Logik>Kette <Mathematik>Lemma <Logik>Elektronische UnterschriftKartesische KoordinatenBereichstheorieKontextbezogenes SystemComputeranimation
Folge <Mathematik>Mathematische LogikEntscheidungstheorieBeweistheorieMonoidParametersystemAusnahmebehandlungCASE <Informatik>HypercubeSchlussregelT-NormDesign by ContractFolge <Mathematik>Mathematische LogikFormale SemantikEntscheidungstheorieKomplex <Algebra>MaßerweiterungResultanteDesign by ContractComputeranimation
Folge <Mathematik>Mathematische LogikBildschirmmaskeFunktionalKomplex <Algebra>Radikal <Mathematik>Quasigeordnete MengeMatchingParametersystemCASE <Informatik>HypercubeGebundener ZustandSchnittmengeEntropie <Informationstheorie>SchlussregelGamecontrollerFolge <Mathematik>Mathematische LogikRekursive FunktionBeweistheorieFunktionalKalkülKomplex <Algebra>Radikal <Mathematik>Gebundener ZustandPrimitive <Informatik>GamecontrollerComputeranimation
AnalysisFolge <Mathematik>MathematikMathematische LogikModallogikAxiomFinitismusUniformer RaumEntscheidungstheorieAlgorithmische ProgrammierspracheAnalytische MengeFormale GrammatikIdeal <Mathematik>KalkülKette <Mathematik>Komplex <Algebra>Statistische HypotheseAbstraktionsebenePunktgitterSchnittmengeKonstruktor <Informatik>SchlussregelComputeranimation
Transkript: Englisch(automatisch erzeugt)
The main result of this work is the decidability of substructural logics, commutative substructural logics with contraction
that have a hyper-sequent calculus with the sub-formula property. I'll explain what all these terms mean, but to start off, when I say logic, what I mean here is a set of formulas, what's also called its theorems. For example, if you take classical propositional logic,
it contains formulas, theorems like P or not P, and also some of the other formulas you see on the screen. The logic can be defined in various ways, for example, as a set of formulas that is valid on a class of structures or via a proof calculus.
A proof calculus is a formal object that generates derivations, that's the formal word for formal proof, and through these theorems of the logic. One of the most important questions for a logic is whether it is decidable. That means if you give me a formula, can I efficiently decide
if the formula belongs to the logic or not? Can I decide this? And it's natural to use a proof calculus for this purpose and also, in fact, to compute upper bounds, complexity upper bounds. And in this talk, we will be talking about
using the proof calculus for decidability. Jensen introduced a type of proof calculus called a sequent calculus. And let me start, in case you've not encountered this before, let me start by explaining the sequent calculus for intuitionistic logic. The sequent calculus here is simply a set of functions,
what I call inference rules, whose inputs and output are sequents. A sequent, meanwhile, has the form x turn style a, as shown on the screen, where x multi-set union, x is a multi-set and x union a is a multi-set of formulas. Then a derivation is constructed starting from initial rules
by applying logical rules and the structural rules. The logical rules introduce a logical connective on the left-hand side, that's the antecedent, or on the right-hand side of the sequent at each step. For example, in the derivation that I've shown on the screen, you can see that it starts with this initial rule
over here, and then disjunction is introduced on the right-hand side. Here's implication left introduced here, and you proceed downwards, creating more and more complex sequence. The structural rules don't introduce logical connectives, but instead they play on the structure of the sequence.
So for example, here you have two copies of a in the multi-set on the left, and it becomes a single copy in the conclusion. To use the sequent calculus to say something about the logic, of course you need a relationship between the two, and that's what the soundness and completeness theorem says,
which says that you give me a formula a, if it is a theorem of intuitionistic logic, well, then the sequent containing that formula on the right is derivable, and vice versa. What makes the sequent calculus a powerful tool is when it has the set sub-formula property.
So as does the sequent calculus for intuitionistic logic, where every formula, if you give me a sequent and you consider a derivation of the sequent X turns style a, that's where X turns style a is at the bottom, every formula in this derivation is a sub-formula of X union a.
This is a significant restriction on the space of derivations, and you can contrast this perhaps with the Hilbert calculus, where arbitrary formulas can occur in the proof. And to see that this holds, it suffices to look at the form of the rules in the sequent calculus and observe that every formula in a premise would be a sub-formula of some formula in the conclusion.
Of course, this doesn't hold if you have a rule, like the famously the cut rule, which violates this property, but I'm considering post-cut elimination. So there's a cut elimination result in the background. It says that you can avoid rules that break this property.
Great. So once you have a sequent calculus for the sub-formula property, you can do backward proof search, which means you can search for derivation starting with the given sequent by applying the rules backwards. If it terminates, then you can see if inside this tree that you obtain, if you can find a derivation, then it is derivable,
else it is not. So that sounds great. The problem is that for most logics of interest, there is not a sequent calculus with the sub-formula property. And this is what has motivated extensions, more expressive types of proof, and in particular the hyper-sequent calculus,
which will be of importance in this talk. But I'll talk about the hyper-sequent calculus in a moment. I want to first go on and talk about substructural logics. Substructural logic is one that lacks some of the structural rules of intuitionist logic. For example, the weakening rule that we saw on the previous page or the contraction rule.
Also, I talked about a sequent as being a multi-set on the left and implicitly that builds in exchange and associativity. By using a different data structure, you can also remove these properties and then you get a substructural logic.
The sequent calculus for intuitionistic logic, therefore we can look as coming from the full lambda calculus by the addition of exchange, contraction, and weakening. And therefore we can talk about intuitionistic calculation. Calculus has been FLECW. If I delete just the weakening rule from the intuitionistic calculus,
I will get FLEC. I'll remind you once more of the structural rules. This is what I mean by the contraction rule and this is what I mean by the weakening rule. There are in fact lots of substructural logics because not only can you delete
some of the structural rules, say from FLECW, because you can then add further axioms and rules for properties like linearity, weak-excluded, middle-bound, and so on, and infinitely many other properties in fact. And consequently, the logical connectives of substructural logic can model a broad range of phenomena.
And you can contrast this perhaps with classical logic where the logical connectives model truth or in intuitionistic logic where they model constructivity. With substructural logics, many behaviors and specifications in computer science in particular can be described using these logics. For example, with respect to the full lambda calculus,
if you add restricted contraction and restricted commutativity, you can model syntactic types of natural language, context-free grammars, linguistic phenomena. If you keep commutativity but the restricted contraction, restricted weakening, then you're in the realm of linear logic and variance, computational, and resource awareness logics.
FLEC gives a refined account of implication because the weakening rule has been eliminated, removed, and this falls into the realm of relevance logics. In fact, every axiomatic extension of FLEC plus linearity is known to be a fuzzy logic
with applications in fuzzy systems modeling. In fact, new applications appear all the time that use the lambda calculus with extensions of axioms, maybe language extensions of modality. You could think of the bunch logics which combine the substructural logic, the APT intuitionistic logic leading in the direction of separation logics.
And this vast number of different logics, substructural logics, motivates the interest in general results. And it's in that context that we have this general decidability result for the commutative substructural logics with contraction that have high-precipient calculus
with the sub-formula property. Let's look at it via a diagram, the logics that we're talking about here. So here's some selected substructural logics. We can see these are ordered by subset containment. And so you have FLEC here,
and here are extensions of FLEC by various axioms. Here are the known decidability and complexity results in this region of logics. Of course, we have intuitionistic logic here, and we have FLEW.
FLEC was famously proved decidable by Kripke in 1959. And this work will show how his argument can be extended to new proof calculus to capture all of an infinitely many extensions of FLEC by various axioms and properties.
There are some scattered results on extensions of FLEC decidability, which, for example, with the Mingle axioms and Mingle-type axioms, which are shown over here. I should also mention that in the case of FLEC already, the complexity bounds are horrendous
in the sense of a quad showed roughly matching lower and upper bounds that are not primitive recursive. FLEC is not primitive recursive, but it is primitive recursive in the Ackermann function.
To make sense of the logics that we're studying, it's helpful to consider which ones have a sequent calculus with sub-formula property. And those are all the ones in black where the existing results were known. There is, for hyper-sequent calculus with the sub-formula property, there is the scattered result in the presence also of the Mingle.
And our result shows how to extend Kripke's argument broadly to the large class of hyper-sequent substructural logics. Here's the calculus, sequent calculus for FLEC. I won't look at the details, but feel free to pause and have a look if you want to have calculus rules in mind.
Let me sketch the Kripke's argument and then show how it extends to hyper-sequent calculate. So Kripke says something like this. You give me a formula F. If it has a derivation, first of all, then it has an everywhere minimal derivation. And everywhere minimal derivation means
that every sub-derivation has minimum. There's an algorithm for computing the everywhere minimal derivation from a derivation, but I won't go into that. The second point I want to make is that FLEC has high preserving admissibility of contraction.
That means that if you give me the contraction rule, which has been written here, then the conclusion can be obtained by proof transformation without increasing the height of the derivation. So if you combine items one and two, what it says is if you start with an everywhere minimal derivation
and you have some sequence S1 that is above S naught, then it cannot be that S1 is contractible to S naught, i.e. using contraction rules to obtain S naught because then Curry's lemma would imply a smaller derivation for S naught. And that would violate the everywhere minimal assumption.
So this relation of contractible, which I'm using this symbol to denote, you can check is a partial order. Well, step four, we start generating the proof search tree. As I said, it's a backward application of all possible rule instances, but we add a side condition.
We omit rule instances whose premise would be contractible to an earlier element. So if you look at this diagram here, you have, this is not a proof rule, right? Because we have applied all possible rule instances here. And this is coming from, these last two premises
are coming from the disjunction rule. But one of the premises is contractible to an earlier sequence, just this one over here. And therefore we omit this rule instance. It remains to prove termination of this algorithm. For then, as I've stated before,
we can decide if it has a derivation by looking at the final proof search tree and determining if it contains a derivation as a sub-tree. So let's get on to the creepy termination argument. If it does not terminate in the limit, we can say that the proof search tree has an infinite branch.
By the sub-formula property, we know that every formula in every sequence on this branch is a sub-formula of F. So let's extract the infinite sub-sequence on this branch whose succeedent is identical, some formula here. We recall that every sequence from a partially ordered set
has a sub-sequence that is either descending, ascending, constant, or an anti-chain in the sense of the definitions here. Anti-chain meaning that every pair of elements is incomparable, cannot be compared. United direction.
And we have seen from the construction, the proof search construction, and that the star site condition that ascending and constant sub-sequences have been ruled out. Therefore, this sub-sequence must contain
a descending or anti-chain sub-sequence. And Kripke's Lemma shows that no such descending anti-chain exists. Another way of seeing this result is by observing that since every formula in the proof is a sub-formula of F,
that means that for every multi-set xi in this sequence, it corresponds in a natural way to an n-tuple where n is the cardinality of the sub-formulas of F. And Dixon's Lemma says that over the set of n-tuples, there is no descending chain and no anti-chain.
Kripke uses sledgehammer. If you're not familiar with this phrase, it means to use significant force to carry out an action. And I say that because the argument ultimately depends very little on the actual rules of the calculus. After all, Kripke's Lemma, or Dixon's Lemma,
applies to all sequences of sequence or n-tuples, irrespective of how they were generated. So it's enticing to ask, can we then extend these arguments to other logics where the rules are different? Unfortunately, the big limiting factor is that most logics do not have a sequence calculus
with the sub-formula property. And that's where the hyper-sequence calculus introduced independently by Myths, Poitinger and Avron comes into this picture. So the reason for the limitations on the sub-formula property, sequence calculus, is because of the limited expressivity
of its structural language of the comma. It's simply the comma and the turnstile. Hyper-sequence, consider multi-sets of sequence. And therefore it has a more expressive structural language because it has the bar, which is a sequence multi-set comma, you could read it. In particular, Ciavattoni et al. have shown
that infinitely many axiomatic extensions of FLE, of FLEC, have a sounded complete for hyper-sequence calculus with the sub-formula property. In fact, these logics, these hyper-sequence logics, as I call them here, have syntactic and semantic characterizations,
which I won't go into. I do want to show you an example of hyper-sequence derivation, just to show you how it works. So here is a hyper-sequence with two components, and then the logical rule, the implication right rule, applies just to a single component. And then the same rule now is applying
to the other component. And when you have two components that are identical, as you have here, there is the external contraction rule, which can reduce the two to a single component. Here's the hyper-sequence calculus for FLEC. You can feel free to pause and have a look, if you wish.
Right, so let's see how we could extend the arguments of decidability to the hyper-sequence algorithm. First of all, carries them out. We want to show that external leaking, external contraction, and C, let's call this internal contraction, are all height-preserving admissible.
So one way of showing height-preserving admissibility is to show that the weakening rule is actually not a problem. So it's the contraction rules that we have to worry about would be to show that we can permit the contraction rules upwards and hence eliminate them from a derivation
by pushing them upwards and eliminating them at the top. And that's what you see here, how to permit internal contraction rule. And here is showing you how to permit an external contraction rule. In both cases, this works because the premises, the sequence at the top, already contains the duplicates. So in particular, it fails when the duplicates
have been created in the conclusion or when they come from different premises. So take this example here of the implication left rule. There are three copies of A implies B in the conclusion, but one has been created and each of the others comes from one of the premises. So we cannot permit the contraction rule here.
So the observation is that permutation may be blocked when there are too few elements in the conclusion. And the solution which generalizes the sequence proof of Paris Lemma is to internalize some limited contraction into the conclusion to handle this case. Specifically, if you take this hyper sequence rule,
take as an example the implication left rule, this is the standard conclusion here. And we replace that with a hyper sequence G which can be obtained from the standard conclusion by applying some limited amount of internal contraction followed by some limited amount of external contraction.
To be specific about what I mean by a limited amount of each, it means that there is a G prime, that G goes to G prime by applying contraction rules so that each formula in any component occurs up to k less and then G prime goes to H
where any component in G prime occurs up to L less in H. But neither the formula or the component can disappear because you're always applying contraction rules. You can determine what values of k and L, the minimum values of k and L that suffice. And by replacing all your rules
with the rules internalizing contraction in this way, we obtain the high preserving admissibility. It is hyper sequence carries them on. Next onto the extended cryptilemma where we want to say, given a sequence of hyper sequence using a finite set of formulas,
that there exists some element of the sequence such that it can be obtained from a later element by applying internal external contraction or external weakling. So at this point, it could be tempting to define the relation simply as being obtainable using these rules.
Unfortunately, this is not a partial order as it is not anti-symmetric. You can see this in this extract here where P, Q as well as this more complex hyper sequence can each be obtained from the other using these rules. To get the partial order, we want to treat such hyper sequence as equivalent.
This also leads onto the definition of the signature of a hyper sequence, which means that for each component in the hyper sequence, you look at the formulas that are on the left and you get a formula on the right, and you collect them across all the components and you obtain for every hyper sequence, you can extract its signature.
You define equivalence relation we were talking about before. For technical reasons, weakling is restricted to signature preserving weaklings, but I won't go into the technical details there. And then what do we have? We have, if you give me a set of, take the set of hyper sequence built from this finite set of formulas,
we can take the portion classes under this equivalence relation, and then we define the partial order as we planned to do before. Now, suppose I'm given a sequence of a hyper sequence, I can extract first of all the sub sequence, which has the same signature, instead of finitely many options.
And we consider the equivalence classes of that sequence. Suppose that there's a descending sequence, we use the infinite Ramsey theorem to extract another descending sub sequence, where each hyper sequence has the singleton signature.
And the point is that when we have a hyper sequence with a singleton signature, we can associate it with an element of the power set of omega size tuples of the natural numbers. We just forget the succeeded B because it's the same in each component. So as a consequence, descending chains in the equivalence classes
implies an ascending chain on upward closed subsets of these tuples. Similarly, an anti-chain implies an anti-chain on the upward closed subsets. However, at least since 2001, it is known that such ascending chains do not exist
and there is no anti-chain on the upward closed subsets. And therefore we conclude that this sequence has no descending chain, and therefore we can obtain the result that there must be an ascending non-descending chain and the result follows. As a side comment,
it turns out that the WQO on hyper sequence with singleton signature or equivalently the elements of the power set appears in the context of domain theory as the minoring of Smith ordering. And you can, if you look at the right hand side,
it's suggestive of the structure rule operations of contraction and weakening that we've been using. Future work. So this work focused on the hyper sequent substructure logics extending FLEC. In the case of FLEW, it is mostly on the status of their decidability.
The exception is MTL, monoidal T-norm logic, whose decidability was shown by Onom using algebraic semantic argument, but in the large case, decidability is open. And the argument of proof search that we used here
does not work because here we managed to prohibit ascending sequences of hyper sequence using admissibility of the contraction rules. But of course, in FLEW, we don't have internal contraction. So this seems a rather challenging problem.
The second work I want to, question I'm gonna draw attention to is complexity bounds. ERQAC obtained complexity upper and low bounds for FLEC roughly matching. In the case of the hyper sequent, we can, the size of increase of the hyper sequence size is controlled because of the rule form.
Termination we saw ultimately comes down to the minor quasi order. Balasubramaniam has given upper bounds for control bad sequences with respect disorder. And it's reasonable to imagine upper bound from this argument, following this argument. What would be very interesting is if we can obtain a lower bound for some logic,
if it exists within this set of logics that exceeds the primitive recursive bound in that common function of FLEC. Thank you very much for your attention.