Die Möglichkeit, Walter Benjamins Allegorie-Begriff in akademischen Untersuchungen mit der Prosa Jean Pauls in Verbindung zu bringen, wurde von Benjamin noch selbst abgewogen: in der Rezension einer frühen Abhandlung zu diesem Thema, die er für zu kurz gegriffen befand. Ein solches Vorhaben, das beste Chancen böte, dürfe sich nämlich nicht auf literaturwissenschaftliche und geistesgeschichtliche Perspektiven beschränken. Notwendig sei vielmehr, auch die Dimension der Alltagskultur einzubeziehen und Jean Pauls Hinabgreifen in Tiefen des Volkstums und der Tradition zu berücksichtigen. Diesem Hinweis Benjamins (...) folgt die vorliegende Untersuchung. Indem sie sich auf den Bereich der materiellen Kultur konzentriert, legt sie eine Geschichte der Theorie der Dingwelt offen. Jean Pauls ästhetische Überlegungen zur projektiven Belehnung der Dingwelt mit seelischen Regungen wurden von Aby Warburg aufgegriffen und für seine kulturwissenschaftliche Methode fruchtbar gemacht. Dabei erschliesst er unter anderem einen Traditionsstrang des Denkens von materieller Kultur im ästhetischen und kultur anthropologischen Kontext, der geprägt ist von aus der Antike herrührenden abergläubischen Vorstellungen über die Einflüsse der Planeten auf die menschliche Geistesverfassung wie etwa die Saturnfürchtigkeit. (shrink)

LK is much more difficult than NK, and to make matters worse, Gentzen's intention is still unclear when it comes to that system (LK). -/- This book, Vol.1 of the series titled What is LK?, tackles this issue, focusing on the sequent, the most enigmatic notion we find in LK. The dependence-relation we find in NK shall play a crucial role in that investigation. -/- The style is typically textbook-like, so readers can learn the system of LK, using this series (...) as a guidance, too. (shrink)

LK is much more difficult than NK, and to make matters worse, Gentzen's intention is still unclear when it comes to that system (LK). -/- The second and third volumes of the series titled What is LK? conduct the detailed survey of each inference-figure in a toe-to-toe way, as it were, which most mathematicians looked through. -/- The present volume, Vol.2, looks deeper into structural inference-figures, which is never an easy task.

LK is much more difficult than NK, and to make matters worse, Gentzen's intention is still unclear when it comes to that system (LK). -/- The second and third volumes of the series titled What is LK? conduct the detailed survey of each inference-figure in a toe-to-toe way, as it were, which most mathematicians looked through. -/- The present volume, Vol.3, looks deeper into those operational inference-figures which concerns propositional logic.

Gentzen’s sequent calculi LK and LJ are landmark proof systems. They identify the structural rules of weakening and contraction as notable inference rules, and they allow for an elegant statement and proof of both cut elimination and consistency for classical and intuitionistic logics. Among the undesirable features of those sequent calculi is that their inferences rules are low-level and frequently permute over each other. As a result, large-scale structures within sequent calculus proofs are hard to identify. In this paper, we (...) present a different approach to designing a sequent calculus for classical logic. Starting with Gentzen’s LK proof system, we examine the proof search meaning of his inference rules and classify those rules as involving either don’t care nondeterminism or don’t know nondeterminism. Based on that classification, we design the focused proof system LKF in which inference rules belong to one of two phases of proof construction depending on which flavor of nondeterminism they involve. We then prove that the cut rule and the general form of the initial rule are admissible in LKF. Finally, by showing that the inference rules for LK are all admissible in LKF, we can give a relative completeness proof for LKF provability with respect to LK provability. We shall also apply these properties of the LKF proof system to establish other meta-theoretic properties of classical logic, including Herbrand’s theorem. (shrink)

The interpretability of AI is just as important as its performance. In the LegalAI field, there have been efforts to enhance the interpretability of models, but a trade-off between interpretability and prediction accuracy remains inevitable. In this paper, we introduce a novel framework called LK-IB for compulsory measure prediction (CMP), one of the critical tasks in LegalAI. LK-IB leverages Legal Knowledge and combines an Interpretable model and a Black-box model to balance interpretability and prediction performance. Specifically, LK-IB involves three steps: (...) (1) inputting cases into the first module, where first-order logic (FOL) rules are used to make predictions and output them directly if possible; (2) sending cases to the second module if FOL rules are not applicable, where a case distributor categorizes them as either “simple” or “complex“; and (3) sending simple cases to an interpretable model with strong interpretability and complex cases to a black-box model with outstanding performance. Experimental results demonstrate that the LK-IB framework provides more interpretable and accurate predictions than other state-of-the-art models. Given that the majority of cases in LegalAI are simple, the idea of model combination has significant potential for practical applications. (shrink)

In this paper, we study the relationship among classical logic, intuitionistic logic, and quantum logic . These logics are related in an interesting way and are not far apart from each other, as is widely believed. The results in this paper show how they are related with each other through a dual intuitionistic logic . Our study is completely syntactical.

Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...) inductions. We also give a new purely inductive proof of the cut theorem for the original single cut rule in Gentzen’s sequent calculus $ LK $ without any use of mix. (shrink)

The article is on the exegesis of the parable of the Good Samaritan (Lk 10:25–35) and its relevance to the challenges that are being posed by COVID-19. Through the historical-critical approach, the article has concluded that the parable is relevant in troubleshooting the challenges that are caused by COVID-19, such as discrimination, stigma, hate and stereotypes. The article sees COVID-19 as teaching humanity the important lesson that no one can live in isolation, however powerful or economically strong they are. Therefore, (...) there is a need to take the opportunity of being a neighbour. Neighbourhood is understood as offering services to those in need and COVID-19 has presented a chance to the entire world to help someone with needs. A need-based world requires neighbours and this makes the parable relevant. Contribution: This article is a reflection of the challenges that are currently faced by people in response to the COVID-19 pandemic. It is within the scope of this theological journal that issues of identity, relationships, and theological reflection should be addressed, hence the article fits well within this scope. (shrink)

Augustine’s interpretation of the parable of the rich man and Lazarus from Lk 16 shows how much the parables of Jesus are open to a variety of interpretations and applications depending upon which part of the parable is emphasised. In Augustine’s writings the second part of the parable only is commented upon (the exception being ep. 157) to illustrate points about the afterlife and the fate of the soul. However, in his homilies we find him engaging with both sections of (...) the parable (this life and the afterlife). We can note the dexterity with which Augustine handled diverse themes in the parable by selectively emphasising either the fate of the rich man in this life or the next or the fate of Lazarus in this life or the next. From these different perspectives Augustine could deal with questions of wealth and poverty either materially or spiritually. This research supports the notion that whatever Augustine had to say about almsgiving is to be understood within a soteriological context to urge his congregation to be rich in humility and poor in pride. (shrink)

Resolution and cut-free LK are the most popular propositional systems used for logical automated reasoning. The question whether or not resolution and cut-free LK have the same efficiency on the system of CNF formulas has been asked and studied since 1960 425–467). It was shown in Cook and Reckhow, J. Symbolic Logic 44 36–50 that tree resolution has super-polynomial speed-up over cut-free LK. Naturally, the current issue is whether or not resolution and cut-free LK expressed as directed acyclic graphs have (...) the same efficiency. In this paper, we introduce a new algorithm to eliminate atomic cuts and show that cut-free LK polynomially simulates resolution when the input formula is expressed as a k-CNF formula. As a corollary, we show that regular resolution does not polynomially simulate cut-free LK . We also show that cut-free LK polynomially simulates regular resolution. (shrink)

This article seeks to reconstruct the phrase τὸν ἄρτον ἡμῶν τὸν ἐπιούσιον in the light of an African predicament with the Ewe-Ghanaian context in focus. The article posits that the various interpretations of the phrase throughout the epochs of Christianity have arisen as a result of the ambiguity associated with ἐπιούσιος and the quest to make the Lord’s Prayer in general relevant to the life situation of the recipient communities. Although the Lord’s Prayer is still regarded as a prayer par (...) excellence in the Ewe-Ghanaian Christian community, its central theme in popular Ewe-Ghanaian spirituality has been demonological instead of eschatological. The demonological interpretation is premised on the primal Ewe belief that successful spiritual warfare against the evil forces believed to be militating against one’s destiny in life can restore one’s fortunes and lead to the blessing of material prosperity. Thus, the phrase τὸν ἄρτον ἡμῶν τὸν ἐπιούσιον in popular Ewe-Ghanaian Christian spirituality is a call on God to ‘grant us the blessing of material prosperity, good health and longevity’. The demonological approach towards material prosperity, however, is discontinuous with the evangelisation approach, which was introduced into Ewe-Ghanaian spirituality through missionary activities in the mid-19th century. The missionaries identified the cardinal Ewe-Ghanaian predicament – poverty of the mind and spirit – and addressed them holistically through the message of the Gospel and the establishment of schools, hospitals, and agriculture to guarantee food security. This holistic approach to alleviating the poverty of the spirit and mind laid the foundation for the socio-economic development of their Ewe-Ghanaian Christian converts and the communities in which they practise their faith.Contribution: This article forms part of the researcher’s contribution to the academic knowledge on the Lord’s Prayer and inspires the use of Mother Tongue Biblical hermeneutics in the development of theological materials for the Ewe-Ghanaian Christian communities in Ghana, Togo, and Benin. (shrink)

This paper aims to develop the notion of ‘therapy of desire’ as a hermeneutic key for understanding Kierkegaard’s view of desire. First, I develop the notion of ‘therapy of desire’ as it has appeared in the secondary literature on Kierkegaard and Augustine, particularly in Lee C. Barrett. In my reading, I underscore how a ‘therapy of desire’ implies that the desire can be ‘healed’ and that the desirer has ‘agency’ over his/her desires. Second, I conduct a textual analysis of Kierkegaard’s (...) discourse on Lk 22:15, which deals with the desire for the Eucharist. In employing the notion of ‘therapy of desire’ as a hermeneutic key to interpret it, I characterize Kierkegaard’s view of desire as a lack of satisfaction and verify how the ideas of ‘agency’ and ‘healing’ appear in Kierkegaard’s text. Finally, I show how the characterization of desire as a constant lack of satisfaction that consists in a gift from God, that implies the possibility of undertaking a healing process and that underscores the agency of the desirer, differs from some Lutheran ideas, namely the relationship between grace and deeds and the understanding of original sin. (shrink)

Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...) inductions. We also give a new purely inductive proof of the cut theorem for the original single cut rule in Gentzen’s sequent calculus $ LK $ without any use of mix. (shrink)

Working within the sensing, intuition, feeling, thinking (SIFT) approach to biblical hermeneutics, the present study focuses attention on the distinctive voices of introverted intuition and extraverted intuition, by analysing the way in which two small groups, one comprising dominant introverted intuitive types and the other comprising dominant extraverted intuitive types, explored and reflected on the Lucan narrative of the Good Samaritan, a passage rich in material to stimulate the perceiving process. Two distinctive voices emerged from these two groups. CONTRIBUTION: Situated (...) within the reader perspective approach to biblical hermeneutics, the SIFT method is concerned with identifying the influence of the psychological type of the reader in shaping the interpretation of text. The foundations of the SIFT approach distinguish among the four functions of sensing, intuition, feeling, and thinking. The present study builds on this foundation by developing the nuance of the orientation in which the function is expressed, in this case focusing specifically on the comparison between introverted intuition and extraverted intuition. (shrink)

Nigeria is an example of developing countries characterised by mass poverty in the midst of plenty. Coincidentally, the Nigerian church is stupendously rich. Pastor Emmanuel, a former National Coordinator of the Redeemed Christian Church of God, Germany, notes that the annual revenue of the Nigeria church in 2014 is over ₦3 trillion while surprisingly, the national budget is ₦4.69tn for the year. Gigantic buildings, exotic cars and private jets are the hallmarks of the church’s wealth. Some pastors acquire jets ranging (...) from ₦2.3 to ₦6.4 billion with additional ₦8.4bn for maintenance and salaries annually. Surrounded by this ‘affluence’ are thousands of poor, unemployed and barely surviving church members. This calls for the need to examine what Lukan Jesus would have wanted the church to do with her wealth. This article examines Lukan parables on the rich and the poor using narratological method. Thus, the parables’ context, the characterisation and the plot is analysed, including lexical-syntactical relationships. Finally, the lessons derived is used via socio-scientific reading of the Nigerian situation to arrive at a theology of social action for the poor. Most parables are open-ended, a literary device that ensures the readers take a decision, therefore the message focuses on the church rather than individual Christians. Contribution: The article recommends that church-owned institutions should make education accessible to the poor, rise against socio-economic policies that will impoverish people while seeking economic independence of the poor. Finally, the church should also integrate the differently-abled into the church. (shrink)

Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional (...) inductions. We also give a new purely inductive proof of the cut theorem for the original single cut rule in Gentzen’s sequent calculus \documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$ LK $$\end{document} without any use of mix. (shrink)

We prove that every finitely axiomatizable extension of Heyting's intuitionistic logic has a corresponding cut-free Gentzen-type formulation. It is shown how one can use this result to find the corresponding normalizable natural deduction system and to give a criterion for separability of considered logic. Obviously, the question how to obtain an effective definition of a sequent calculus which corresponds to a concrete logic remains a separate problem for every logic.

We present a sequent calculus with the Henkin constants in the place of the free variables. By disposing of the eigenvariable condition, we obtained a proof system with a strong locality property—the validity of each inference step depends only on its active formulas, not its context. Our major outcomes are: the cut elimination via a non-Gentzen-style algorithm without resorting to regularization and the elimination of Skolem functions with linear increase in the proof length for a subclass of derivations with cuts.

The present report is a, somewhat lengthy, addendum to "A new deconstructive logic: linear logic," where the elimination of cuts from derivations in sequent calculus for classical logic was studied ‘from the point of view of linear logic’. To that purpose a formulation of classical logic was used, that - as in linear logic - distinguishes between multiplicative and additive versions of the binary connectives.The main novelty here is the observation that this type-distinction is not essential: we can allow classical (...) sequent derivations to use any combination of additive and multiplicative introduction rules for each of the connectives, and still have strong normalization and confluence of tq-reductions.We give a detailed description of the simulation of tq-reductions by means of reductions of the interpre- tation of any given classical proof as a proof net of PN2 (the system of second order proof nets for linear logic), in which moreover all connectives can be taken to be of one type, e.g., multiplicative.We finally observe that dynamically the different logical cuts, as determined by the four possible combinations of introduction rules, are independent: it is not possible to simulate them internally, i.e., by only one specific combination, and structural rules. (shrink)

This article offers a reading of the parable of the Dishonest Steward from the perspective of Greco-Roman status concern. It observes that the parable has a long and complicated history of interpretation. The different approaches in the reading of the parable reveal the unresolved quest in scholarship to establish a reading of the parable that takes into account both the steward’s act of generosity towards his master’s debtors and the praise that follows this action. This article proposes the Greco-Roman status (...) concern as a framework for understanding the meaning of the parable in its original context. Status concern was the spirit of tenacity in maintaining one’s status and honour against all odds characteristic of Greco-Roman honour and shame culture. The article argues that when the parable is read within its literary context, it reveals that at the heart of Jesus’ message in the parable is the theme of persistence as an attribute of authentic discipleship. This understanding of the parable resonates with the entrenched Greco-Roman spirit of status concern. The interpretation would also have been relevant to Luke’s Greco-Roman auditors living on the periphery of the Greco-Roman culture with the constant pressures to conform to the ethos of the larger social context. The steward’s resolve to maintain his status even in the most difficult circumstances provided a paradigm for those Christ-followers to remain steadfast in the faith against all odds. Contribution: The article presents an alternative interpretation of the parable of the Dishonest Steward. By proposing status concern as an interpretative framework, it offers both new insights into the socio-economic and socio-cultural realities of Luke’s world and the continuing evidence of the contribution of Greco-Roman world to the development of the New Testament texts. (shrink)

LK is a natural modification of Gentzen sequent calculus for propositional logic with connectives ¬ and $\bigwedge, \bigvee$. Then for every d ≥ 0 and n ≥ 2, there is a set Td n of depth d sequents of total size O which are refutable in LK by depth d + 1 proof of size exp) but such that every depth d refutation must have the size at least exp). The sets Td n express a weaker form of the pigeonhole (...) principle. (shrink)

This article investigates the proof theory of the Quantified Argument Calculus as developed and systematically studied by Hanoch Ben-Yami [3, 4]. Ben-Yami makes use of natural deduction, we, however, have chosen a sequent calculus presentation, which allows for the proofs of a multitude of significant meta-theoretic results with minor modifications to the Gentzen’s original framework, i.e., LK. As will be made clear in course of the article LK-Quarc will enjoy cut elimination and its corollaries.

Extending previous results from work on the complexity of cut elimination for the sequent calculus LK, we discuss the role of quantifier alternations and develop a measure to describe the complexity of cut elimination in terms of quantifier alternations in cut formulas and contractions on such formulas.

A many-valued modal logic, called linear abelian modal logic \(\rm {\mathbf{LK(A)}}\) is introduced as an extension of the abelian modal logic \(\rm \mathbf{K(A)}\). Abelian modal logic \(\rm \mathbf{K(A)}\) is the minimal modal extension of the logic of lattice-ordered abelian groups. The logic \(\rm \mathbf{LK(A)}\) is axiomatized by extending \(\rm \mathbf{K(A)}\) with the modal axiom schemas \(\Box(\varphi\vee\psi)\rightarrow(\Box\varphi\vee\Box\psi)\) and \((\Box\varphi\wedge\Box\psi)\rightarrow\Box(\varphi\wedge\psi)\). Completeness theorem with respect to algebraic semantics and a hypersequent calculus admitting cut-elimination are established. Finally, the correspondence between hypersequent calculi and axiomatization (...) is investigated. (shrink)