Definability of arithmetical operations from binary quadratic forms
Definability within structures related to Pascal’s triangle modulo an integer
Let Sq denote the set of squares, and let be the squaring function restricted to powers of n; let ⊥ denote the coprimeness relation. Let . For every integer n ≥ 2 addition and multiplication are definable in the structures ⟨ℕ; Bn,⊥⟩ and ⟨ℕ; Bn,Sq⟩; thus their elementary theories are undecidable. On the other hand, for every prime p the elementary theory of ⟨ℕ; Bp,SQp⟩ is decidable.
...-definable functionals and ... Conversion.
...-definierbare Funktionen auf Peanoalgebren.
Definierbare Funktionen im ...-Kalkül mit Typen.
Definition and Properties of Direct Sum Decomposition of Groups1
In this article, direct sum decomposition of group is mainly discussed. In the second section, support of element of direct product group is defined and its properties are formalized. It is formalized here that an element of direct product group belongs to its direct sum if and only if support of the element is finite. In the third section, product map and sum map are prepared. In the fourth section, internal and external direct sum are defined. In the last section, an equivalent form of internal...
Definition of First Order Language with Arbitrary Alphabet. Syntax of Terms, Atomic Formulas and their Subterms
Second of a series of articles laying down the bases for classical first order model theory. A language is defined basically as a tuple made of an integer-valued function (adicity), a symbol of equality and a symbol for the NOR logical connective. The only requests for this tuple to be a language is that the value of the adicity in = is -2 and that its preimage (i.e. the variables set) in 0 is infinite. Existential quantification will be rendered (see [11]) by mere prefixing a formula with a letter....
Definition of Flat Poset and Existence Theorems for Recursive Call
This text includes the definition and basic notions of product of posets, chain-complete and flat posets, flattening operation, and the existence theorems of recursive call using the flattening operator. First part of the article, devoted to product and flat posets has a purely mathematical quality. Definition 3 allows to construct a flat poset from arbitrary non-empty set [12] in order to provide formal apparatus which eanbles to work with recursive calls within the Mizar langauge. To achieve this...
Definitions: the primitive concept of logics or The Leśniewski-Tarski legacy [Book]
Degradation in probability logic: When more information leads to less precise conclusions
Probability logic studies the properties resulting from the probabilistic interpretation of logical argument forms. Typical examples are probabilistic Modus Ponens and Modus Tollens. Argument forms with two premises usually lead from precise probabilities of the premises to imprecise or interval probabilities of the conclusion. In the contribution, we study generalized inference forms having three or more premises. Recently, Gilio has shown that these generalized forms “degrade” – more premises...
Degrees of interpretability
Demonic semantics: using monotypes and residuals.
Denotational aspects of untyped normalization by evaluation
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 forms,...
Denotational aspects of untyped normalization by evaluation
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...
Der Cohensche Eliminationssatz in positiver Charakteristik
Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie.
Der Verband der normalen verzweigten Modallogiken.
Deux propriétés décidables des suites récurrentes linéaires
Deux relations dénombrables, logiquement équivalentes pour le second ordre, sont isomorphes
Diagonal reasonings in mathematical logic
First we show a few well known mathematical diagonal reasonings. Then we concentrate on diagonal reasonings typical for mathematical logic.