Constructing Finite Least Kripke Models for Positive Logic Programs in Serial Regular Grammar Logics

A serial context-free grammar logic is a normal multimodal logicL characterized by the seriality axioms and a set of inclusionaxioms of the form _ts1..._sk. Such an inclusion axiom correspondsto the grammar rule t s₁... s_k. Thus the inclusion axioms ofL capture a context-free grammar . If for every modal index t, the set of words derivable fromt using is a regular language, then L is a serial regular grammar logic. In this paper, we present an algorithm that, given a positivemultimodal logic program P and a set of finite automata specifyinga serial regular grammar logic L, constructs a finite leastL-model of P. (A model M is less than or equal to model M' iffor every positive formula , if M then M' .) A least L-modelM of P has the property that for every positive formula , P iff M . The algorithm runs in exponential time and returnsa model with size 2^O(n³). We give examples of P and L, for bothof the case when L is fixed or P is fixed, such that every finiteleast L-model of P must have size 2⁽ⁿ⁾. We also prove that ifG is a context-free grammar and L is the serial grammar logiccorresponding to G then there exists a finite least L-modelof _s p iff the set of words derivable from s using G is a regularlanguage.     

The Weak Normalization of the Simply Typed {lambda}se-calculus

In this paper, we show the weak normalization (WN) of the simply-typeds_e-calculus with open terms where abstractions are decoratedwith types, and metavariables, de Bruijn indices and updatingoperators are decorated with environments. We show a proof ofWN using the _e-calculus, a calculus isomorphic to . This proof is strongly influenced by Goubault-Larrecq'sproof of WN for the -calculus but with subtle differences whichshow that the two styles require different attention. Furthermore,we give a new calculus '_e which works like s_e but which iscloser to than _e. For both _e and '_e we prove WN for typedsemi-open terms (i.e. those which allow term variables but nosubstitution variables), unlike the result of Goubault-Larrecqwhich covered all open terms.     

Congruences on Dynamic Algebras

The lattice Cong of all dynamic congruences on a given dynamic algebra is presented. Whenever is separable with zero we define dynamic ideal on , given rise to the lattice Ide. The notions of kernel of a dynamic congruence andthe congruence generated by a dynamic ideal are introduced todescribe a Galois connection between Cong and Ide. We study conditions under which a dynamic congruence is determined byits kernel.     

Dynamic Topological Completeness for

Dynamic topological logic (DTL) combines topological and temporalmodalities to express asymptotic properties of dynamic systemson topological spaces. A dynamic topological model is a tripleX ,f , V , where X is a topological space, f : X X a continuousfunction and V a truth valuation assigning subsets of X to propositionalvariables. Valid formulas are those that are true in every model,independently of X or f. A natural problem that arises is toidentify the logics obtained on familiar spaces, such as . It [9] it was shown that any satisfiable formulacould be satisfied in some for n large enough, but the question of how the logic varieswith n remained open. In this paper we prove that any fragment of DTL that is completefor locally finite Kripke frames is complete for . This includes DTL; it also includes some largerfragments, such as DTL₁, where "henceforth" may not appear inthe scope of a topological operator. We show that satisfiabilityof any formula of our language in a locally finite Kripke frameimplies satisfiability in by constructing continuous, open maps from the plane intoarbitrary locally finite Kripke frames, which give us a typeof bisimulation. We also show that the results cannot be extendedto arbitrary formulas of DTL by exhibiting a formula which isvalid in but not in arbitrarytopological spaces.     

First-Order Theories of Orthogonality Structures

We investigate certain aspects of the first-order theory oforthogonality structures - structures consisting of a domainof lines subject to a binary orthogonality relation. In particular,we establish definitions of various geometric and algebraicnotions in terms of orthogonality, describe the constructionof extremal subspaces using orthogonality, and show that thefirst-order theory of line orthogonality in the Euclidean n-spaceis not ₀-categorical for n 3.     

A Bizarre Property Equivalent to the -Fan Theorem

It is shown, with intuitionistic logic, that if every locallyconstant function from to has a property akinto constancy, then the fan theorem for -bars holds, and conversely.     

Satisfiability Decay along Conjunctions of Pseudo-Random Clauses

k-SAT is a fundamental constraint satisfaction problem. It involvesS(m), the satisfaction set of the conjunction of m clauses,each clause a disjunction of k literals. The problem has manytheoretical, algorithmic and practical aspects. When the clauses are chosen at random it is anticipated (butnot fully proven) that, as the density parameter m/n (n thenumber of variables) grows, the transition of S(m) to beingempty, is abrupt: It has a "sharp threshold", with probability1 – o(1). In this article we replace the random ensemble analysis by apseudo-random one: Derive the decay rule for individual sequencesof clauses, subject to combinatorial conditions, which in turnhold with probability 1 – o(1). This is carried out under the big relaxation that k is not constantbut k = log n , or even r log log n . Then the decay of S isslow, "near-perfect" (like a radioactive decay), which entailssharp thresholds for the transition-time of S below any givenlevel, down to S = .     

The Heavenly {alpha with psili}{nu}{alpha}{tau}o{lambda}eeacgr (Luke 1:78-9)

A consideration of the o figure in Luke 1:78–9 leads tothe suggestion that this is not merely a Davidic messiah, butalso a heavenly, pre-existent figure. After a review of themain lines of debate in the past century, the discussion iscentred on four points. First, the visitation () gives a strongimpression of a divine figure. Secondly, from the evidence ofthe LXX and elsewhere in Luke, the advent of the figure ‘fromon high’ ( &;o) points clearly to a heavenly origin forthe o. Thirdly, though less conclusively, the reference to Isaiah9 LXX strengthens the impression of an angelic ruler figure.Finally, the o itself is defined as both light-bringer and heavenlymessiah, especially in contrast to the o character in Zech.6:12, who comes not ‘from on high’ but ‘frombeneath’.     

Naming and Diagonalization, from Cantor to Godel to Kleene

We trace self-reference phenomena to the possibility of namingfunctions by names that belong to the domain over which thefunctions are defined. A naming system is a structure of theform (D, type( ),{ }), where D is a non-empty set; for everya D, which is a name of a k-ary function, {a}: D^k D is thefunction named by a, and type(a) is the type of a, which tellsus if a is a name and, if it is, the arity of the named function.Under quite general conditions we get a fixed point theorem,whose special cases include the fixed point theorem underlyingGödel's proof, Kleene's recursion theorem and many othertheorems of this nature, including the solution to simultaneousfixed point equations. Partial functions are accommodated byincluding "undefined" values; we investigate different systemsarising out of different ways of dealing with them. Many-sortednaming systems are suggested as a natural approach to generalcomputatability with many data types over arbitrary structures.The first part of the paper is a historical reconstruction ofthe way Gödel probably derived his proof from Cantor'sdiagonalization, through the semantic version of Richard. Theincompleteness proof–including the fixed point construction–resultfrom a natural line of thought, thereby dispelling the appearanceof a "magic trick". The analysis goes on to show how Kleene'srecursion theorem is obtained along the same lines.     

Domus Ecclesiae: Rethinking a Category of Ante-Pacem Christian Space

Historians of religion, art, and archaeology often invoke theterm domus ecclesiae (oo ) as a technical category to denotea house or building that had been materially adapted for Christianritual during the ante-pacem period. Most employ the term inthe belief that it is genuinely pre-Constantinian, and thatChristians in this period described their cult spaces as renovatedhouses. This essay demonstrates the inaccuracy of both assumptions,and shows that the first attested literary use of the term datesno earlier than 313 CE, when Eusebius of Caesarea (d. 339) usedit in his writings to designate a church building without anyindication of its architectural form or history. Following adiscussion of the term's modern history and an analysis of theancient literary evidence, the essay concludes with a brieflook at the material evidence for domus ecclesiae, which, withone exception (the complex at Dura-Europos), also dates to thepost-Constantinian period.     

Origen's Version of Genesis 1:2

Chalcidius attributes to Origen an interpretation of the phrase in Genesis 1:2 which personifies the earth: terra autem stupidaquadam erat admiratione. This can be explained by noting thatGenesis Rabba on Genesis 1:2 supports a similar interpretationof , probably on the basis of the Aramaic roots and , bothof which denote amazement or perplexity.     

Oh {delta}{iota}{alpha with oxia}! How is Romans 4:25 to be Understood?

How are we to understand the difficult expression ‘raisedfor our justification’ (Romans 4:25b)? The clue lies intaking seriously the two + accusatives in Romans 4:23. Therethey express a parallel between the promise of righteousness‘for him (Abraham)’ and the same kind of promise,still valid ‘for us’. This same emphasis shouldbe taken into 4:25, ‘for us ... for us.’ Such areading is not only backed up by the Isaiah 53 echo and thecontents of Romans 5, it also serves to explain the meaningof Romans 4:25b. Abraham was given an opportunity for ‘righteousness-producingfaith’ through a tension between ‘under-realizedreality’ and God's faithfulness (vv.18–22). Throughthe resurrection of Jesus Christ, the same opportunity is nowafforded to ‘us’.     

'The Doers of the Law Will Be Justified': The Exegetical Origins of Martin Bucer's Triplex Iustificatio

This essay seeks to sketch the profile of Martin Bucer's viewson the doctrine of justification as developed in his 1536 commentaryon Romans, focusing in particular on his idiosyncratic languageof ‘threefold justification’ in his comments onRom. 2:13. This text is taken as a vantage point from whichto survey the history of interpretation of the Pauline conceptof justification within the Augustinian tradition, giving extendedconsideration to exegesis by Augustine and Thomas Aquinas. Bucer'sinitial discussion of the Pauline usage of o in the praefatato his commentary is examined next, and it is concluded thathis understanding of justification falls more or less withinthe trajectory charted by previous medieval interpreters. Turningthen to Bucer's comments on Rom. 2:13, it is argued that thenotion of ‘threefold justification’ arises as anattempt to integrate the early evangelical appropriation ofthe Scotist language of ‘divine acceptation’ withina traditional Augustinian account of justification as both eventand process. The resulting formula collapses predestinationinto justification, making the latter the unifying concept inBucer's soteriology. It is hoped that this essay will contributeto deepening our understanding of an oft-neglected reformerwhile at the same time broadening our understanding of earlyevangelical teaching on a central doctrinal locus.     

The Meaning of syriacalaphsyriaclamadhsyriacshin in Theodore of Mopsuestia's Sixteenth Catechetical Lecture and the Silent Recitation of the Eucharistic Prayer

Georg Kretschmar cited Theodore of Mopsuestia, Catechesis 16in support of his thesis that part of the eucharistic prayercould be recited silently by the end of the fourth century.This note points out that the use of the Syriac verb , to ‘desist’or to ‘be silent’, in this text does not supportKretschmar's interpretation.     

An Apocalyptic and Magical Interpretation of Paul's 'Beast Fight' in Ephesus (1 Corinthians 15:32)

This article argues that Paul's mention of a fight with ‘wildanimals’ during his time in Ephesus (1 Cor. 15:32) shouldbe understood as a reference to the evil spirits, or ‘beasts’,at work in the demon-possessed, sorcerers, and idolaters ofthe city. Two major arguments are given. First, in Jewish apocalypticcircles, o was commonly used in reference to evil spirits andsupernatural monsters. This connects with the magical tendencyof referring to daimones as wild animals, a practice that Paulmay well have encountered in Ephesus. Secondly, the book ofActs remembers Paul's time in Ephesus as characterized by exorcisms,magical rivalries, and conflict with idolatry—an accountthat fits with other historical information. The early receptionof the verse is also discussed, with particular attention beingpaid to the interpretation of Origen.     

Compatible Functions in Algebras Associated to Extensions of Positive Logic

In [4], Caicedo and Cignoli study compatible functions on Heytingalgebras and the corresponding logical properties of connectivesdefined on intuitionistic propositional calculus. In this paperwe study some aspects of compatible functions on the algebrasassociated to positive propositional calculus and successiveextensions of it: intuitionistic calculus itself, the modalsymmetric propositional calculus of Moisil and n-valued ukasiewiczpropositional calculus.     

Diodorean modality in Minkowski spacetime

The Diodorean interpretation of modality reads the operator as it is now and always will be the case that. In this paper time is modelled by the four-dimensional Minkowskian geometry that forms the basis of Einstein's special theory of relativity, with event y coming after event x just in case a signal can be sent from x to y at a speed at most that of the speed of light (so that y is in the causal future of x).It is shown that the modal sentences valid in this structure are precisely the theorems of the well-known logic S4.2, and that this system axiomatises the logics of two and three dimensional spacetimes as well.Requiring signals to travel slower than light makes no difference to what is valid under the Diodorean interpretation. However if the is now part is deleted, so that the temporal ordering becomes irreflexive, then there are sentences that distinguish two and three dimensions, and sentences that can be falsified by approaching the future at the speed of light, but not otherwise.     

Parts and differences

Part/whole is said in many ways: the leg is part of the table, the subset is part of the set, rectangularity is part of squareness, and so on. Do the various flavors of part/whole have anything in common? They may be partial orders, but so are lots of non-mereological relations. I propose an “upward difference transmission” principle: x is part of y if and only if x cannot change in specified respects while y stays the same in those respects.