scholarly journals The number of proofs for a BCK-formula

1993 ◽  
Vol 58 (2) ◽  
pp. 626-628 ◽  
Author(s):  
Yuichi Komori ◽  
Sachio Hirokawa
Keyword(s):  
Normal Form ◽  
Modus Ponens ◽  
Basic Notion ◽  
Type Assignment ◽  
Natural Deduction System ◽  
Cartesian Closed Categories ◽  
Image Position ◽  
Coherence Theorem ◽  
Cartesian Closed ◽  
Necessary And Sufficient

In this note, we give a necessary and sufficient condition for a BCK-formula to have the unique normal form proof.We call implicational propositional formulas formulas for short. BCK-formulas are the formulas which are derivable from axioms B = (a → b) → (c → a) → c → b, C = (a→b→c)→b→a→c, and K = a→b→a by substitution and modus ponens. It is known that the property of being a BCK-formula is decidable (Jaskowski [11, Theorem 6.5], Ben-Yelles [3, Chapter 3, Theorem 3.22], Komori [12, Corollary 6]). The set of BCK-formulas is identical to the set of provable formulas in the natural deduction system with the following two inference rules.Here γ occurs at most once in (→I). By the formulae-as-types correspondence [10], this set is identical to the set of type-schemes of closed BCK-λ-terms. (See [5].) A BCK-λ-term is a λ-term in which no variable occurs twice. Basic notion concerning the type assignment system can be found [4]. Uniqueness of normal form proofs has been known for balanced formulas. (See [2,14].) It is related to the coherence theorem in cartesian closed categories. A formula is balanced when no variable occurs more than twice in it. It was shown in [8] that the proofs of balanced formulas are BCK-proofs. Relevantly balanced formulas were defined in [9], and it was proved that such formulas have unique normal form proofs. Balanced formulas are included in the set of relevantly balanced formulas.

A sequent calculus for type assignment

1977 ◽  
Vol 42 (1) ◽  
pp. 11-28 ◽  
Author(s):  
Jonathan P. Seldin
Keyword(s):  
Normal Form ◽  
Main Part ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
Cut Elimination ◽  
Type Assignment ◽  
Image Position ◽  
Atomic Type

The sequent calculus formulation (L-formulation) of the theory of functionality without the rules allowing for conversion of subjects of [3, §14E6] fails because the (cut) elimination theorem (ET) fails. This can be most easily seen by the fact that it is easy to prove in the systemandbut not (as is obvious if α is an atomic type [an F-simple])The error in the “proof” of ET in [14, §3E6], [3, §14E6], and [7, §9C] occurs in Stage 3, where it is implicitly assumed that if [x]X ≡ [x] Y then X ≡ Y. In the above counterexample, we have [x]x ≡ ∣ ≡ [x](∣x) but x ≢ ∣x. Since the formulation of [2, §9F] is not really satisfactory (for reasons stated in [3, §14E]), a new seguent calculus formulation is needed for the case in which the rules for subject conversions are not present. The main part of this paper is devoted to presenting such a formulation and proving it equivalent to the natural deduction formulation (T-formulation). The paper will conclude in §6 with some remarks on the result that every ob (term) with a type (functional character) has a normal form.The conventions and definitions of [3], especially of §12D and Chapter 14, will be used throughout the paper.

Note on a problem of L. Henkin

1956 ◽  
Vol 21 (1) ◽  
pp. 33-35 ◽  
Author(s):  
Abraham Robinson
Keyword(s):  
Normal Form ◽  
Predicate Calculus ◽  
Universal Quantifiers ◽  
Image Position ◽  
Necessary And Sufficient

A statement X in the lower predicate calculus is said to be persistent with respect to the set of statements K ([2], [3]), if whenever X holds in a model M of K then X holds also in all extensions of M which are models of K. If X is persistent with respect to the empty set, then it may be said to be absolutely persistent.A statement X is called existential, if it is in prenex normal form and does not contain any universal quantifiers. This includes the possibility that X does not contain any quantifiers at all.Let E be the class of all existential statements. Then it is not difficult to see that E is quasi-disjunctive. That is to say, given statements Y1, Y2 in E, there exists a statement Y in E such thatis provable.L. Henkin [1] has raised the question how to characterise the statements X which are persistent with respect to a given set K (e.g. a set of axioms for a field or a group) by a syntactical condition. He has shown that, in order that a statement X be absolutely persistent, it is necessary and sufficient that there exist a statement Y ϵ E such thatis provable.

scholarly journals A Note on Decomposable and Reducible Integer Matrices

Symmetry ◽  
2021 ◽  
Vol 13 (7) ◽  
pp. 1125
Author(s):  
Carlos Marijuán ◽  
Ignacio Ojeda ◽  
Alberto Vigneron-Tenorio
Keyword(s):  
Normal Form ◽  
Linear Algebra ◽  
Sufficient Conditions ◽  
Necessary And Sufficient Conditions ◽  
Integer Matrix ◽  
Hermite Normal Form ◽  
Necessary And Sufficient

We propose necessary and sufficient conditions for an integer matrix to be decomposable in terms of its Hermite normal form. Specifically, to each integer matrix, we associate a symmetric integer matrix whose reducibility can be efficiently determined by elementary linear algebra techniques, and which completely determines the decomposability of the first one.

scholarly journals Dynamic game semantics

2020 ◽  
pp. 1-60
Author(s):  
Norihiro Yamada ◽  
Samson Abramsky
Keyword(s):  
Programming Languages ◽  
Functional Programming ◽  
Operational Semantics ◽  
Dynamic Game ◽  
Standard Interpretation ◽  
Functional Programming Languages ◽  
Game Semantics ◽  
Wide Range ◽  
Cartesian Closed Categories ◽  
Cartesian Closed

Abstract The present work achieves a mathematical, in particular syntax-independent, formulation of dynamics and intensionality of computation in terms of games and strategies. Specifically, we give game semantics of a higher-order programming language that distinguishes programmes with the same value yet different algorithms (or intensionality) and the hiding operation on strategies that precisely corresponds to the (small-step) operational semantics (or dynamics) of the language. Categorically, our games and strategies give rise to a cartesian closed bicategory, and our game semantics forms an instance of a bicategorical generalisation of the standard interpretation of functional programming languages in cartesian closed categories. This work is intended to be a step towards a mathematical foundation of intensional and dynamic aspects of logic and computation; it should be applicable to a wide range of logics and computations.

Post completeness in modal logic

1972 ◽  
Vol 37 (4) ◽  
pp. 711-715 ◽  
Author(s):  
Krister Segerberg
Keyword(s):  
Modal Logic ◽  
Upper Bound ◽  
Modus Ponens ◽  
Proper Subset ◽  
Proper Extension ◽  
Image Position

Let ⊥, →, and □ be primitive, and let us have a countable supply of propositional letters. By a (modal) logic we understand a proper subset of the set of all formulas containing every tautology and being closed under modus ponens and substitution. A logic is regular if it contains every instance of □A ∧ □B ↔ □(A ∧ B) and is closed under the ruleA regular logic is normal if it contains □⊤. The smallest regular logic we denote by C (the same as Lemmon's C2), the smallest normal one by K. If L and L' are logics and L ⊆ L′, then L is a sublogic of L', and L' is an extension of L; properly so if L ≠ L'. A logic is quasi-regular (respectively, quasi-normal) if it is an extension of C (respectively, K).A logic is Post complete if it has no proper extension. The Post number, denoted by p(L), is the number of Post complete extensions of L. Thanks to Lindenbaum, we know thatThere is an obvious upper bound, too:Furthermore,.

Delay stabilization of periodic orbits in coupled oscillator systems

2010 ◽  
Vol 368 (1911) ◽  
pp. 319-341 ◽  
Author(s):  
B. Fiedler ◽  
V. Flunkert ◽  
P. Hövel ◽  
E. Schöll
Keyword(s):  
Normal Form ◽  
Numerical Simulations ◽  
Periodic Orbits ◽  
Coupled Oscillators ◽  
Coupled Oscillator ◽  
Non Invasive ◽  
Coupling Parameters ◽  
Necessary And Sufficient ◽  
Time Delayed Feedback ◽  
Coupled Oscillator Systems

We study diffusively coupled oscillators in Hopf normal form. By introducing a non-invasive delay coupling, we are able to stabilize the inherently unstable anti-phase orbits. For the super- and subcritical cases, we state a condition on the oscillator’s nonlinearity that is necessary and sufficient to find coupling parameters for successful stabilization. We prove these conditions and review previous results on the stabilization of odd-number orbits by time-delayed feedback. Finally, we illustrate the results with numerical simulations.

scholarly journals Topological entropy in totally disconnected locally compact groups

2016 ◽  
Vol 37 (7) ◽  
pp. 2163-2186 ◽  
Author(s):  
ANNA GIORDANO BRUNO ◽  
SIMONE VIRILI
Keyword(s):  
Topological Entropy ◽  
Sufficient Conditions ◽  
Invariant Subgroup ◽  
Locally Compact Groups ◽  
Compact Groups ◽  
Locally Compact ◽  
Image Position ◽  
Necessary And Sufficient ◽  
Totally Disconnected ◽  
Dynamical Interpretation

Let $G$ be a topological group, let $\unicode[STIX]{x1D719}$ be a continuous endomorphism of $G$ and let $H$ be a closed $\unicode[STIX]{x1D719}$-invariant subgroup of $G$. We study whether the topological entropy is an additive invariant, that is, $$\begin{eqnarray}h_{\text{top}}(\unicode[STIX]{x1D719})=h_{\text{top}}(\unicode[STIX]{x1D719}\restriction _{H})+h_{\text{top}}(\bar{\unicode[STIX]{x1D719}}),\end{eqnarray}$$ where $\bar{\unicode[STIX]{x1D719}}:G/H\rightarrow G/H$ is the map induced by $\unicode[STIX]{x1D719}$. We concentrate on the case when $G$ is totally disconnected locally compact and $H$ is either compact or normal. Under these hypotheses, we show that the above additivity property holds true whenever $\unicode[STIX]{x1D719}H=H$ and $\ker (\unicode[STIX]{x1D719})\leq H$. As an application, we give a dynamical interpretation of the scale $s(\unicode[STIX]{x1D719})$ by showing that $\log s(\unicode[STIX]{x1D719})$ is the topological entropy of a suitable map induced by $\unicode[STIX]{x1D719}$. Finally, we give necessary and sufficient conditions for the equality $\log s(\unicode[STIX]{x1D719})=h_{\text{top}}(\unicode[STIX]{x1D719})$ to hold.

scholarly journals Existence of nonoscillatory solutions of first order nonlinear neutral equations

1990 ◽  
Vol 32 (2) ◽  
pp. 180-192 ◽  
Author(s):  
Lu Wudu
Keyword(s):  
Nonoscillatory Solution ◽  
Sufficient Condition ◽  
Neutral Equation ◽  
Necessary And Sufficient Condition ◽  
Nonoscillatory Solutions ◽  
Neutral Equations ◽  
First Order ◽  
Image Position ◽  
Necessary And Sufficient

AbstractConsider the nonlinear neutral equationwhere pi(t), hi(t), gj(t), Q(t) Є C[t0, ∞), limt→∞hi(t) = ∞, limt→∞gj(t) = ∞ i Є Im = {1, 2, …, m}, j Є In = {1, 2, …, n}. We obtain a necessary and sufficient condition (2) for this equation to have a nonoscillatory solution x(t) with limt→∞ inf|x(t)| > 0 (Theorems 5 and 6) or to have a bounded nonoscillatory solution x(t) with limt→∞ inf|x(t)| > 0 (Theorem 7).

scholarly journals All cartesian closed categories of quasicontinuous domains consist of domains

2015 ◽  
Vol 594 ◽  
pp. 143-150 ◽  
Author(s):  
Xiaodong Jia ◽  
Achim Jung ◽  
Hui Kou ◽  
Qingguo Li ◽  
Haoran Zhao
Keyword(s):  
Cartesian Closed Categories ◽  
Cartesian Closed
Sign in / Sign up

Export Citation Format

Share Document