Page 1 Next
Displaying 1 – 20 of 46
A one axiom set theory based on higher order predicate calculus.
M.W. Bunder (1983)
Archiv für mathematische Logik und Grundlagenforschung
A Theory Of Variable Types.
Solomon Feferman (1985)
Revista colombiana de matematicas
Ambiguity and stratification
Marcel Crabbé (1978)
Fundamenta Mathematicae
An intensional approach to questions
Pavel Materna (1979)
Kybernetika
Axiomatizability of second order arithmetic with ω-rule
Paweł Zbierski (1978)
Fundamenta Mathematicae
Choice functions and well-orderings over the infinite binary tree
Arnaud Carayol, Christof Löding, Damian Niwinski, Igor Walukiewicz (2010)
Open Mathematics
We give a new proof showing that it is not possible to define in monadic second-order logic (MSO) a choice function on the infinite binary tree. This result was first obtained by Gurevich and Shelah using set theoretical arguments. Our proof is much simpler and only uses basic tools from automata theory. We show how the result can be used to prove the inherent ambiguity of languages of infinite trees. In a second part we strengthen the result of the non-existence of an MSO-definable well-founded...
Completeness of cut-free type theories.
Mitsuru Yasuhara (1974)
Archiv für mathematische Logik und Grundlagenforschung
Completeness properties of classical theories of finite type and the normal form theorem [Book]
Peter Päppinghaus (1983)
...-definable functionals and ... Conversion.
R. Statman (1983)
Archiv für mathematische Logik und Grundlagenforschung
Definitions: the primitive concept of logics or The Leśniewski-Tarski legacy [Book]
E. G. K. López-Escobar, Francisco Miraglia (2002)
Deux relations dénombrables, logiquement équivalentes pour le second ordre, sont isomorphes
R. Fraisse (1977)
Publications du Département de mathématiques (Lyon)
Ein starker Normalisationssatz für die intuitionistische Typentheorie.
Wolfram Pohler (1973)
Manuscripta mathematica
Enumerated type semantics for the calculus of looping sequences
Livio Bioglio (2011)
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
The calculus of looping sequences is a formalism for describing the evolution of biological systems by means of term rewriting rules. In this paper we enrich this calculus with a type discipline which preserves some biological properties depending on the minimum and the maximum number of elements of some type requested by the present elements. The type system enforces these properties and typed reductions guarantee...
Enumerated type semantics for the calculus of looping sequences
Livio Bioglio (2011)
RAIRO - Theoretical Informatics and Applications
The calculus of looping sequences is a formalism for describing the evolution of biological systems by means of term rewriting rules. In this paper we enrich this calculus with a type discipline which preserves some biological properties depending on the minimum and the maximum number of elements of some type requested by the present elements. The type system enforces these properties and typed reductions guarantee that evolution preserves them. As an example, we model the hemoglobin structure...
First order topology [Book]
C.W. Henson, C.G. Jockusch, Jr., L.A. Rubel, G. Takeuti (1977)
Ganzgeschlossene und prädikatgeschlossene Logiken I.
Jörg Flum (1971)
Archiv für mathematische Logik und Grundlagenforschung
Ganzgeschlossene und prädikatgeschlossene Logiken II.
Jörg Flum (1971)
Archiv für mathematische Logik und Grundlagenforschung
General operators binding variables in the interpreted modal calculus
Aldo Bressan, Alberto Zanardo (1981)
Atti della Accademia Nazionale dei Lincei. Classe di Scienze Fisiche, Matematiche e Naturali. Rendiconti Lincei. Matematica e Applicazioni
Si considera il calcolo modale interpretato , che è basato su un sistema di tipi con infiniti livelli, contiene descrizioni, ed è dotato di una semantica di tipo generale - v. [2], o [3], o [4], o [5]. In modo semplice e naturale si introducono in operatori vincolanti variabili, di tipo generale. Per teorie basate sul calcolo logico risultante vale un teorema di completezza, che si dimostra in modo immediato sulla base dell'estensione del teorema parziale di completezza stabilito in [11], fatta...
Geometric and higher order logic in terms of abstract Stone duality.
Taylor, Paul (2000)
Theory and Applications of Categories [electronic only]
Currently displaying 1 – 20 of 46
Page 1 Next