Une démonstration du théorème de complétude de Godel
Un'estensione del teorema di Löb
Unimodular rows over Laurent polynomial rings
We prove that for any ring of Krull dimension not greater than 1 and , the group acts transitively on . In particular, we obtain that for any ring with Krull dimension not greater than 1, all finitely generated stably free modules over are free. All the obtained results are proved constructively.
Unsolvable systems of equations and proof complexity.
Veblen Hierarchy
The Veblen hierarchy is an extension of the construction of epsilon numbers (fixpoints of the exponential map: ωε = ε). It is a collection φα of the Veblen Functions where φ0(β) = ωβ and φ1(β) = εβ. The sequence of fixpoints of φ1 function form φ2, etc. For a limit non empty ordinal λ the function φλ is the sequence of common fixpoints of all functions φα where α < λ.The Mizar formalization of the concept cannot be done directly as the Veblen functions are classes (not (small) sets). It is done...
Vergleich zweier Bezeichnungssysteme für Ordinalzahlen.
Vollständigkeit und Schnittelimination in der intuitionistischen Typenlogik.
Why semisets?
Wie die Beweistheorie zu ihren Ordinalzahlen kam und kommt.
Zur Konstruktiven Deutung der semantischen Vollständigkeit klassischer Quantoren- und Modalkalküle.
Zur konstruktiven Differenzierbarkeit von monotonen berechenbaren Funktionen.
Zur Theorie der zusammengesetzten Gruppen.
-tautologies, uniform and non-uniform upper bounds in computation theory
Una -tautologia è una tautologia del tipo avente un solo interpolante di Craig , a meno di equivalenza logica. Utilizzando misure di complessità relative al problema di trovare tale , mostriamo come si possano ottenere limiti non uniformi di complessità mediante limiti uniformi, e viceversa.
-cofinalities of
ω-models of second order arithmetic and admissible sets
Алгоритмы, алгебры и интуиционистская логика
Аппроксимируемость операторов в конструктивных метрических пространствах
Базисы допустимых правил модальной системы Grz и интуиционистской логики
Базы допустимых правил логик S4 и Int
Бескванторные и однокванторные системы