We show that the standard normalization-by-evaluation construction for the simply-typed ${\lambda }_{\beta \eta }$-calculus has a natural counterpart for the untyped ${\lambda }_{\beta }$-calculus, with the central type-indexed logical relation replaced by a “recursively defined” invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal forms,...

We show that the standard normalization-by-evaluation construction for the simply-typed λβη-calculus has a natural counterpart for the untyped λβ-calculus, with the central type-indexed logical relation replaced by a “recursively defined” invariant relation, in the style of Pitts. In fact, the construction can be seen as generalizing a computational-adequacy argument for an untyped, call-by-name language to normalization instead of evaluation.In the untyped setting, not all terms have normal...

The structure of definable sets and maps in dense elementary pairs of o-minimal expansions of ordered abelian groups is described. It turns out that a certain notion of "small definable set" plays a special role in this description.

Some modifications of the definition of density of subsets in ordered (= partially ordered) sets are given and the corresponding concepts are compared.

G. Szász, J. Szendrei, K. Iseki and J. Nieminen have made an extensive study of derivations and translations on lattices. In this paper, the concepts of meet-translations and derivations have been studied in trellises (also called weakly associative lattices or WA-lattices) and several results in lattices are extended to trellises. The main theorem of this paper, namely, that every derivatrion of a trellis is a meet-translation, is proved without using associativity and it generalizes a well-known...

Using the general hypergraph technique developed in [7], we first give a much simpler proof of Shultz's theorem [10]: Each compact convex set is affinely homeomorphic to the state space of an orthomodular lattice. We also present partial solutions to open questions formulated in [10] - we show that not every compact convex set has to be a state space of a unital orthomodular lattice and that for unital orthomodular lattices the state space characterization can be obtained in the context of unital...

Here, we present determinants of some square matrices of field elements. First, the determinat of 2 * 2 matrix is shown. Secondly, the determinants of zero matrix and unit matrix are shown, which are equal to 0 in the field and 1 in the field respectively. Thirdly, the determinant of diagonal matrix is shown, which is a product of all diagonal elements of the matrix. At the end, we prove that the determinant of a matrix is the same as the determinant of its transpose.

Let $S=\{x_1,\cdots ,x_n\}$ be a finite subset of a partially ordered set $P$. Let $f$ be an incidence function of $P$. Let $\left[f(x_i\wedge x_j)\right]$ denote the $n\times n$ matrix having $f$ evaluated at the meet $x_i\wedge x_j$ of $x_i$ and $x_j$ as its $i,j$-entry and $\left[f(x_i\vee x_j)\right]$ denote the $n\times n$ matrix having $f$ evaluated at the join $x_i\vee x_j$ of $x_i$ and $x_j$ as its $i,j$-entry. The set $S$ is said to be meet-closed if $x_i\wedge x_j\in S$ for all $1\le i,j\le n$. In this paper we get explicit combinatorial formulas for the determinants of matrices $\left[f(x_i\wedge x_j)\right]$ and $\left[f(x_i\vee x_j)\right]$ on any meet-closed set $S$. We also obtain necessary and sufficient conditions for the matrices...

For a countable compact metric space and a seminormalized weakly null sequence (fₙ)ₙ in C() we provide some upper bounds for the norm of the vectors in the linear span of a subsequence of (fₙ)ₙ. These bounds depend on the complexity of and also on the sequence (fₙ)ₙ itself. Moreover, we introduce the class of c₀-hierarchies. We prove that for every α < ω₁, every normalized weakly null sequence (fₙ)ₙ in $C\left({\omega }^{{\omega }^{\alpha }}\right)$ and every c₀-hierarchy generated by (fₙ)ₙ, there exists β ≤ α such that a sequence of β-blocks...

For a class $K$ of structures and $A\in K$ let ${Con}^{*}\left(A\right)$ resp. ${Con}^K\left(A\right)$ denote the lattices of $*$-congruences resp. $K$-congruences of $A$, cf. Weaver [25]. Let ${Con}^{*}\left(K\right):=I\{{Con}^{*}\left(A\right):A\in K\}$ where $I$ is the operator of forming isomorphic copies, and ${Con}^r\left(K\right):=I\{{Con}^K\left(A\right):A\in K\}$. For an ordered algebra $A$ the lattice of order congruences of $A$ is denoted by ${Con}^{<}\left(A\right)$, and let ${Con}^{<}\left(K\right):=I\{{Con}^{<}\left(A\right):A\in K\}$ if $K$ is a class of ordered algebras. The operators of forming subdirect squares and direct products are denoted by $Q^s$ and $P$, respectively. Let $\lambda$ be a lattice identity and let $\Sigma$ be a set of lattice identities. Let $\Sigma {\vDash }_c\lambda (r;Q^s,P)$ denote...

This note deals with two logical topics and concerns Boolean Algebras from an elementary point of view. First we consider the class of operations on a Boolean Algebra that can be used for modelling If-then propositions. These operations, or Conditionals, are characterized under the hypothesis that they only obey to the Modus Ponens-Inequality, and it is shown that only six of them are boolean two-place functions. Is the Conditional Probability the Probability of a Conditional? This problem will...